Introduce support for randomness in the model

Signed-off-by: Marco Lampacrescia <[email protected]>

src/as2fm/as2fm_common/ecmascript_interpretation.py

@@ -45,7 +45,10 @@ def interpret_ecma_script_expr(
         msg_addition = ""
         if expr in ("True", "False"):
             msg_addition = "Did you mean to use 'true' or 'false' instead?"
-        raise RuntimeError(f"Failed to interpret JS expression: 'result = {expr}'. {msg_addition}")
+        raise RuntimeError(
+            f"Failed to interpret JS expression using variables {variables}: ",
+            f"'result = {expr}'. {msg_addition}",
+        )
     expr_result = context.result
     if isinstance(expr_result, BasicJsTypes):
         return expr_result

src/as2fm/jani_generator/jani_entries/__init__.py

@@ -1,7 +1,12 @@
 # isort: skip_file
 # Skipping file to avoid circular import problem
 from .jani_value import JaniValue  # noqa: F401
-from .jani_expression import JaniExpression, JaniExpressionType  # noqa: F401
+from .jani_expression import (  # noqa: F401
+    JaniExpression,
+    JaniExpressionType,
+    JaniDistribution,
+    generate_jani_expression,
+)  # noqa: F401
 from .jani_constant import JaniConstant  # noqa: F401
 from .jani_variable import JaniVariable  # noqa: F401
 from .jani_assignment import JaniAssignment  # noqa: F401

src/as2fm/jani_generator/jani_entries/jani_assignment.py

@@ -19,7 +19,7 @@
 
 from typing import Dict
 
-from as2fm.jani_generator.jani_entries import JaniConstant, JaniExpression
+from as2fm.jani_generator.jani_entries import JaniConstant, JaniExpression, generate_jani_expression
 from as2fm.jani_generator.jani_entries.jani_convince_expression_expansion import expand_expression
 
 
@@ -30,12 +30,23 @@ class JaniAssignment:
 
     def __init__(self, assignment_dict: dict):
         """Initialize the assignment from a dictionary"""
-        self._var_name = JaniExpression(assignment_dict["ref"])
-        self._value = JaniExpression(assignment_dict["value"])
+        self._var_name = generate_jani_expression(assignment_dict["ref"])
+        self._value: JaniExpression = generate_jani_expression(assignment_dict["value"])
         self._index = 0
         if "index" in assignment_dict:
             self._index = assignment_dict["index"]
 
+    def get_target(self):
+        """Return the variable storing the expression result."""
+        return self._var_name
+
+    def get_expression(self):
+        """Return the expression assigned to the target variable (or array entry)"""
+        return self._value
+
+    def get_index(self) -> int:
+        return self._index
+
     def as_dict(self, constants: Dict[str, JaniConstant]):
         """Transform the assignment to a dictionary"""
         expanded_value = expand_expression(self._value, constants)

src/as2fm/jani_generator/jani_entries/jani_automaton.py

@@ -78,6 +78,12 @@ def add_edge(self, edge: JaniEdge):
             self._edge_id += 1
         self._edges.append(edge)
 
+    def set_edges(self, new_edges: List[JaniEdge]) -> None:
+        """Replace the edges in the Automaton."""
+        self._edges = []
+        for edge in new_edges:
+            self.add_edge(edge)
+
     def get_edges(self) -> List[JaniEdge]:
         return self._edges
 

src/as2fm/jani_generator/jani_entries/jani_convince_expression_expansion.py

@@ -15,15 +15,22 @@
 
 """Expand expressions into jani."""
 
+from copy import deepcopy
 from math import pi
-from typing import Callable, Dict, Union
+from typing import Callable, Dict, List
 
-from as2fm.jani_generator.jani_entries import JaniConstant, JaniExpression, JaniValue
+from as2fm.jani_generator.jani_entries import (
+    JaniConstant,
+    JaniDistribution,
+    JaniExpression,
+    JaniExpressionType,
+)
 from as2fm.jani_generator.jani_entries.jani_expression_generator import (
     abs_operator,
     and_operator,
     ceil_operator,
     cos_operator,
+    distribution_expression,
     divide_operator,
     equal_operator,
     floor_operator,
@@ -83,6 +90,11 @@
 }
 
 
+def random_operator() -> JaniDistribution:
+    """Function to get a random number between 0 and 1 in the Jani Model."""
+    return distribution_expression("Uniform", [0.0, 1.0])
+
+
 # Custom operators (CONVINCE, specific to mobile 2D robot use case)
 def intersection_operator(left, right) -> JaniExpression:
     return JaniExpression(
@@ -453,7 +465,7 @@ def __substitute_expression_op(expression: JaniExpression) -> JaniExpression:
 
 
 def expand_expression(
-    expression: Union[JaniExpression, JaniValue], jani_constants: Dict[str, JaniConstant]
+    expression: JaniExpression, jani_constants: Dict[str, JaniConstant]
 ) -> JaniExpression:
     # Given a CONVINCE JaniExpression, expand it to a plain JaniExpression
     assert isinstance(
@@ -462,6 +474,9 @@ def expand_expression(
     assert (
         expression.is_valid()
     ), "The expression is not valid: it defines no value, nor variable, nor operation to be done."
+    if expression.get_expression_type() == JaniExpressionType.DISTRIBUTION:
+        # For now this is fine, since we expect only real values in the args
+        return expression
     if expression.op is None:
         # It is either a variable/constant identifier or a value
         return expression
@@ -492,6 +507,48 @@ def expand_expression(
     return __substitute_expression_op(expression)
 
 
+def expand_distribution_expressions(
+    expression: JaniExpression, *, n_options: int = 101
+) -> List[JaniExpression]:
+    """
+    Traverse the expression and substitute each distribution with n expressions.
+
+    This is a workaround, until we can support it in our model checker.
+
+    :param expression: The expression to expand.
+    :param n_options: How many options to generate for each encountered distribution.
+    :return: One expression, if no distribution is found, n_options^n_distributions expr. otherwise.
+    """
+    assert isinstance(
+        expression, JaniExpression
+    ), f"Unexpected expression type: {type(expression)} != (JaniExpression, JaniDistribution)."
+    assert expression.is_valid(), f"Invalid expression found: {expression}."
+    expr_type = expression.get_expression_type()
+    if expr_type == JaniExpressionType.OPERATOR:
+        # Generate all possible expressions, if expansion returns many expressions for an operand
+        expanded_expressions: List[JaniExpression] = [deepcopy(expression)]
+        for key, value in expression.operands.items():
+            expanded_operand = expand_distribution_expressions(value, n_options=n_options)
+            base_expressions = expanded_expressions
+            expanded_expressions = []
+            for expr in base_expressions:
+                for key_value in expanded_operand:
+                    expr.operands[key] = key_value
+                    expanded_expressions.append(deepcopy(expr))
+        return expanded_expressions
+    elif expr_type == JaniExpressionType.DISTRIBUTION:
+        # Here we need to substitute the distribution with a number of constants
+        assert isinstance(expression, JaniDistribution) and expression.is_valid()
+        lower_bound = expression.get_dist_args()[0]
+        dist_width = expression.get_dist_args()[1] - lower_bound
+        # Generate a (constant) JaniExpression for each possible outcome
+        return [
+            JaniExpression(lower_bound + (x * dist_width / (n_options - 1)))
+            for x in range(n_options)
+        ]
+    return [expression]
+
+
 # Map each function name to the corresponding Expression generator
 CALLABLE_OPERATORS_MAP: Dict[str, Callable] = {
     "abs": abs_operator,
@@ -503,4 +560,5 @@ def expand_expression(
     "pow": pow_operator,
     "min": min_operator,
     "max": max_operator,
+    "random": random_operator,
 }

src/as2fm/jani_generator/jani_entries/jani_edge.py

@@ -15,7 +15,7 @@
 
 """And edge defining the possible transition from one state to another in jani."""
 
-from typing import Dict, Optional
+from typing import Dict, List, Optional
 
 from as2fm.jani_generator.jani_entries import (
     JaniAssignment,
@@ -52,6 +52,7 @@ def __init__(self, edge_dict: dict):
                         jani_destination["assignments"].append(assignment)
                     else:
                         raise RuntimeError(f"Unexpected type {type(assignment)} in assignments")
+                _sort_assignments_by_index(jani_destination["assignments"])
             self.destinations.append(jani_destination)
 
     def get_action(self) -> Optional[str]:
@@ -93,3 +94,8 @@ def as_dict(self, constants: Dict[str, JaniConstant]):
                 single_destination.update({"assignments": expanded_assignments})
             edge_dict["destinations"].append(single_destination)
         return edge_dict
+
+
+def _sort_assignments_by_index(assignments: List[JaniAssignment]) -> None:
+    """Sorts a list of assignments by assignment index."""
+    assignments.sort(key=lambda assignment: assignment.get_index())