Prepare RosConn Deliberation workshop example

as2fm_common/pyproject.toml

@@ -17,7 +17,7 @@ classifiers = [
 ]
 keywords = []
 dependencies = [
-
+    "js2py"
 ]
 requires-python = ">=3.10"
 

as2fm_common/src/as2fm_common/common.py

@@ -1,4 +1,4 @@
 # Copyright (c) 2024 - for information on the respective copyright owner
 # see the NOTICE file
 
 # Licensed under the Apache License, Version 2.0 (the "License");
@@ -17,16 +17,16 @@
 Common functionalities used throughout the toolchain.
 """
 
-from typing import get_args, MutableSequence, Union, Type
+from typing import get_args, get_origin, MutableSequence, Union, Type
 from array import array
 
 """
 Set of basic types that are supported by the Jani language.
 
 Basic types (from Jani docs):
 Types
 We cover only the most basic types at the moment.
 In the remainder of the specification, all requirements like "y must be of type x" are to be
 interpreted as "type x must be assignable from y's type".
 var BasicType = schema([
 "bool", // assignable from bool
@@ -38,7 +38,7 @@
 
 Additionally, we support the array types from the array extension.
 """
 ValidTypes = Union[bool, int, float, MutableSequence[int], MutableSequence[float]]
 
 
 def remove_namespace(tag: str) -> str:
@@ -57,10 +57,10 @@
     return tag_wo_ns
 
 
 def get_default_expression_for_type(field_type: Type[ValidTypes]) -> ValidTypes:
     """Generate a default expression for a field type."""
     assert field_type in get_args(ValidTypes), f"Error: Unsupported data type {field_type}."
     if field_type is MutableSequence[int]:
         return array('i')
     elif field_type is MutableSequence[float]:
         return array('d')
@@ -71,12 +71,12 @@
 def value_to_type(value: ValidTypes) -> Type[ValidTypes]:
     """Convert a value to a type."""
     if isinstance(value, array):
         if value.typecode == 'i':
             return MutableSequence[int]
         elif value.typecode == 'd':
             return MutableSequence[float]
         else:
             raise ValueError(f"Type of array '{value.typecode}' not supported.")
     elif isinstance(value, (int, float, bool)):
         return type(value)
     else:
@@ -85,7 +85,7 @@
 
 def value_to_string(value: ValidTypes) -> str:
     """Convert a value to a string."""
     if isinstance(value, MutableSequence):
         # Expect value to be an array
         return f'[{",".join(str(v) for v in value)}]'
     elif isinstance(value, bool):
@@ -96,8 +96,36 @@
         raise ValueError(f"Unsupported value type {type(value)}.")
 
 
+def string_to_value(value_str: str, value_type: Type[ValidTypes]) -> ValidTypes:
+    """Convert a string to a value of the desired type."""
+    value_str = value_str.strip()
+    assert isinstance(value_str, str), \
+        f"Error: provided value is of type {type(value_str)}, expected a string."
+    assert len(value_str) > 0, "Error: provided value is an empty string, cannot convert."
+    is_array_value = value_str.startswith('[') and value_str.endswith(']')
+    if not is_array_value:
+        assert value_type in (bool, int, float), \
+            f"Error: the value {value_str} shall be converted to a base type."
+        return value_type(value_str)
+    else:
+        str_entries = value_str.strip('[]').split(',')
+        if str_entries == ['']:
+            str_entries = []
+        if value_type is MutableSequence[int]:
+            return array('i', [int(v) for v in str_entries])
+        elif value_type is MutableSequence[float]:
+            return array('d', [float(v) for v in str_entries])
+        else:
+            raise ValueError(f"Unsupported value type {value_type}.")
+
+
 def check_value_type_compatible(value: ValidTypes, field_type: Type[ValidTypes]) -> bool:
     """Check if the value is compatible with the field type."""
     if field_type is float:
         return isinstance(value, (int, float))
     return isinstance(value, field_type)
+
+
+def is_array_type(field_type: Type[ValidTypes]) -> bool:
+    """Check if the field type is an array type."""
+    return get_origin(field_type) == get_origin(MutableSequence)

as2fm_common/src/as2fm_common/ecmascript_interpretation.py

@@ -1,4 +1,4 @@
 # Copyright (c) 2024 - for information on the respective copyright owner
 # see the NOTICE file
 
 # Licensed under the Apache License, Version 2.0 (the "License");
@@ -17,7 +17,8 @@
 Module for interpreting ecmascript.
 """
 
-from typing import Dict, Optional, Union
+import re
+from typing import Dict, List, Optional, Union
 from array import array
 
 import js2py
@@ -25,8 +26,18 @@
 from as2fm_common.common import ValidTypes
 
 
 BASIC_JS_TYPES = Union[int, float, bool]
 
+# Functions that, if found in the expression, should be interpreted as math functions (Math.fun())
+MATH_FUNCTIONS: List[str] = ["abs", "floor", "ceil", "cos", "sin", "log", "pow", "min", "max"]
+
+
+def prepend_math_functions(expr: str) -> str:
+    """Append 'Math.' to the functions in the provided expression and return a copy."""
+    for fun in MATH_FUNCTIONS:
+        expr = re.sub(rf"(^|[^a-zA-Z0-9_]){fun}\(", rf"\g<1>Math.{fun}(", expr)
+    return expr
+
 
 def interpret_ecma_script_expr(
         expr: str, variables: Optional[Dict[str, ValidTypes]] = None) -> object:
@@ -36,6 +47,7 @@
     :param expr: The ECMA script expression
     :return: The interpreted object
     """
+    expr = prepend_math_functions(expr)
     if variables is None:
         variables = {}
     context = js2py.EvalJs(variables)
@@ -45,16 +57,20 @@
         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}")
     expr_result = context.result
     if isinstance(expr_result, BASIC_JS_TYPES):
         return expr_result
     elif isinstance(expr_result, js2py.base.JsObjectWrapper):
         if isinstance(expr_result._obj, js2py.base.PyJsArray):
-            return expr_result.to_list()
+            res_as_list = expr_result.to_list()
+            if all(isinstance(x, int) for x in res_as_list):
+                return array("i", res_as_list)
+            else:
+                return array('d', res_as_list)
         else:
             raise ValueError(f"Expected expr. {expr} to be of type {BASIC_JS_TYPES} or "
                              f"an array, got '{type(expr_result._obj)}'")
     elif isinstance(expr_result, array):
         return expr_result
     else:

as2fm_common/test/test_unittest_ecmascript_interpretation.py

@@ -17,6 +17,7 @@
 
 import unittest
 import pytest
+from array import array
 
 from as2fm_common.ecmascript_interpretation import interpret_ecma_script_expr
 
@@ -34,7 +35,7 @@ def test_ecmascript_types(self):
         self.assertEqual(interpret_ecma_script_expr("1.1"), 1.1)
         self.assertEqual(interpret_ecma_script_expr("true"), True)
         self.assertEqual(interpret_ecma_script_expr("false"), False)
-        self.assertEqual(interpret_ecma_script_expr("[1,2,3]"), [1, 2, 3])
+        self.assertEqual(interpret_ecma_script_expr("[1,2,3]"), array('i', [1, 2, 3]))
 
     def test_ecmascript_unsupported(self):
         """

jani_generator/src/jani_generator/jani_entries/jani_convince_expression_expansion.py

@@ -1,4 +1,4 @@
 # Copyright (c) 2024 - for information on the respective copyright owner
 # see the NOTICE file
 
 # Licensed under the Apache License, Version 2.0 (the "License");
@@ -63,6 +63,7 @@
     "=>": "⇒",
     "aa": "aa",
     "ac": "ac",
+    "av": "av",
 }
 
 
@@ -206,8 +207,8 @@
     e_y = f"robots.{robot_name}.goal.y"
     a_x = f"boundaries.{boundary_id}.x"
     a_y = f"boundaries.{boundary_id}.y"
     b_x = f"boundaries.{(boundary_id + 1) % n_vertices}.x"
     b_y = f"boundaries.{(boundary_id + 1) % n_vertices}.y"
     # Segments expressions
     ab_x = minus_operator(b_x, a_x)
     ab_y = minus_operator(b_y, a_y)

jani_generator/src/jani_generator/jani_entries/jani_expression.py

@@ -22,7 +22,7 @@
 
 from jani_generator.jani_entries import JaniValue
 
-SupportedExp = Union[str, int, float, bool, dict]
+SupportedExp = Union[str, int, float, bool, dict, list]
 
 
 class JaniExpressionType(Enum):
@@ -57,7 +57,7 @@
         elif isinstance(expression, JaniValue):
             self.value = expression
         else:
             assert isinstance(expression, SupportedExp), \
                 f"Unexpected expression type: {type(expression)} should be a dict or a base type."
             if isinstance(expression, str):
                 # If it is a reference to a constant or variable, we do not need to expand further
@@ -118,6 +118,9 @@
             return {
                 "exp": JaniExpression(expression_dict["exp"]),
                 "index": JaniExpression(expression_dict["index"])}
+        if (self.op == "av"):
+            return {
+                "elements": JaniExpression(expression_dict["elements"])}
         # Convince specific expressions
         if (self.op in ("norm2d")):
             return {
@@ -190,7 +193,7 @@
         if self.identifier is not None:
             return self.identifier
         if self.value is not None:
             return self.value.as_dict()
         op_dict: Dict[str, Any] = {
             "op": self.op,
         }

jani_generator/src/jani_generator/jani_entries/jani_expression_generator.py

@@ -143,3 +143,12 @@ def array_access_operator(exp, index) -> JaniExpression:
     :param index: The index to access on exp
     """
     return JaniExpression({"op": "aa", "exp": exp, "index": index})
+
+
+def array_value_operator(elements) -> JaniExpression:
+    """
+    Generate an array value expression
+
+    :param elements: The elements of the array
+    """
+    return JaniExpression({"op": "av", "elements": elements})

jani_generator/src/jani_generator/jani_entries/jani_utils.py

@@ -0,0 +1,90 @@
+# Copyright (c) 2024 - for information on the respective copyright owner
+# see the NOTICE file
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     http://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Collection of various utilities for Jani entries."""
+
+from typing import Any, Dict, Optional, MutableSequence, Tuple, Type, get_args
+from as2fm_common.common import get_default_expression_for_type, is_array_type
+from jani_generator.jani_entries import JaniAutomaton
+
+
+def get_variable_type(jani_automaton: JaniAutomaton, variable_name: Optional[str]) -> type:
+    """
+    Retrieve the variable type from the Jani automaton.
+
+    :param jani_automaton: The Jani automaton to check the variable in.
+    :param variable_name: The name of the variable to check.
+    :return: The retrieved type.
+    """
+    assert variable_name is not None, "Variable name must be provided."
+    variable = jani_automaton.get_variables().get(variable_name)
+    assert variable is not None, \
+        f"Variable {variable_name} not found in {jani_automaton.get_variables()}."
+    return variable.get_type()
+
+
+def is_variable_array(jani_automaton: JaniAutomaton, variable_name: Optional[str]) -> bool:
+    """Check if a variable is an array.
+
+    :param jani_automaton: The Jani automaton to check the variable in.
+    :param variable_name: The name of the variable to check.
+    :return: True if the variable is an array, False otherwise.
+    """
+    return is_array_type(get_variable_type(jani_automaton, variable_name))
+
+
+def get_array_type_and_size(jani_automaton: JaniAutomaton, var_name: str) -> Tuple[Type, int]:
+    """
+    Generate the ArrayInfo obj. related to the provided variable.
+
+    :param jani_automaton: The Jani automaton to get the variable from.
+    :param var_name: The name of the variable to generate the info from.
+    :return: The ArrayInfo obj. with array type and max size.
+    """
+    assert var_name is not None, "Variable name must be provided."
+    variable = jani_automaton.get_variables().get(var_name)
+    var_type = variable.get_type()
+    assert is_array_type(var_type), f"Variable {var_name} not an array, cannot extract array info."
+    array_type = get_args(var_type)[0]
+    assert array_type in (int, float), f"Array type {array_type} not supported."
+    init_operator = variable.get_init_expr().as_operator()
+    assert init_operator is not None, f"Expected init expr of {var_name} to be an operator expr."
+    if init_operator[0] == "av":
+        max_size = len(init_operator[1]['elements'].as_literal().value())
+    elif init_operator[0] == "ac":
+        max_size = init_operator[1]['length'].as_literal().value()
+    else:
+        raise ValueError(f"Unexpected operator {init_operator[0]} for {var_name} init expr.")
+    return (array_type, max_size)
+
+
+def get_all_variables_and_instantiations(jani_automaton: JaniAutomaton) -> Dict[str, Any]:
+    """
+    Retrieve all variables and their instantiations from the Jani automaton.
+
+    :param jani_automaton: The Jani automaton to retrieve the variables from.
+    :return: A dictionary mapping each variable to a dummy value
+    """
+    variables: Dict[str, Any] = {}
+    for n, v in jani_automaton.get_variables().items():
+        variables[n] = get_default_expression_for_type(v.get_type())
+        # Hack to solve issue for expressions with explicit access to array entries
+        if isinstance(variables[n], MutableSequence):
+            for _ in range(50):
+                variables[n].append(0)
+        # Another hack, since javascript interprets 0.0 as int...
+        if isinstance(variables[n], float):
+            variables[n] = 0.1
+    return variables

jani_generator/src/jani_generator/jani_entries/jani_value.py

@@ -32,7 +32,8 @@ def is_valid(self) -> bool:
                 assert self._value["constant"] in ("e", "π"), \
                     f"Unknown constant value {self._value['constant']}. Only 'e' and 'π' supported."
                 return True
-            return False
+        elif isinstance(self._value, list):
+            return all(JaniValue(v).is_valid() for v in self._value)
         return isinstance(self._value, (int, float, bool))
 
     def value(self) -> Union[int, float, bool]:
@@ -45,6 +46,6 @@ def value(self) -> Union[int, float, bool]:
                 return pi
         return self._value
 
-    def as_dict(self) -> Union[dict, int, float, bool]:
+    def as_dict(self) -> Union[dict, int, float, bool, list]:
         # Note: this might be a value or a dictionary
         return self._value

jani_generator/src/jani_generator/jani_entries/jani_variable.py

@@ -37,7 +37,7 @@
         if isinstance(initial_value, str):
             # Check if conversion from string to variable_type is possible
             try:
                 init_value_cast = variable_type(initial_value)
                 return JaniVariable(variable_name,
                                     variable_type,
                                     JaniExpression(init_value_cast),
@@ -84,10 +84,14 @@
         """Get name."""
         return self._name
 
-    def get_type(self):
+    def get_type(self) -> Type[ValidTypes]:
         """Get type."""
         return self._type
 
+    def get_init_expr(self) -> Optional[JaniExpression]:
+        """Get initial expression.  if available. None otherwise."""
+        return self._init_expr
+
     def as_dict(self):
         """Return the variable as a dictionary."""
         d = {