Skip to content

Commit

Permalink
Cleanup hackathon code (#9)
Browse files Browse the repository at this point in the history
Signed-off-by: Marco Lampacrescia <[email protected]>
  • Loading branch information
MarcoLm993 authored Jul 11, 2024
1 parent 632f0f3 commit e8866b8
Show file tree
Hide file tree
Showing 24 changed files with 587 additions and 713 deletions.
Binary file modified docs/source/graphics/scxml_if_handling.drawio.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file modified docs/source/graphics/scxml_to_jani.drawio.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,8 @@ def __init__(self, composition_dict: Optional[Dict[str, Any]] = None):

def add_element(self, element: str):
"""Append a new automaton name in the composition."""
assert element not in self._elements, f"Element {element} already exists in the composition"
assert element not in self._elements, \
f"Element {element} already exists in the composition"
self._elements.append(element)
self._element_to_id[element] = len(self._elements) - 1

Expand All @@ -49,7 +50,8 @@ def add_sync(self, sync_name: str, syncs: Dict[str, str]):
}
# Generate the synchronize list
for automata, action in syncs.items():
assert automata in self._element_to_id, f"Automaton {automata} does not exist in the composition"
assert automata in self._element_to_id, \
f"Automaton {automata} does not exist in the composition"
new_sync["synchronise"][self._element_to_id[automata]] = action
self._syncs.append(new_sync)

Expand Down Expand Up @@ -92,6 +94,8 @@ def _generate_syncs(self, syncs_list):
return generated_syncs

def as_dict(self):
# Sort the syncs before return
self._syncs = sorted(self._syncs, key=lambda x: x["result"])
return {
"elements": [{"automaton": element} for element in self._elements],
"syncs": self._syncs
Expand Down
21 changes: 15 additions & 6 deletions jani_generator/src/jani_generator/jani_entries/jani_variable.py
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,22 @@
"""

from typing import Optional, Union, get_args
from jani_generator.jani_entries import JaniExpression
from jani_generator.jani_entries import JaniExpression, JaniValue

from mc_toolchain_jani_common.common import ValidTypes


class JaniVariable:
def __init__(self, v_name: str, v_type: ValidTypes, v_init_value: Optional[JaniExpression] = None, v_transient: bool = False):
assert v_init_value is None or isinstance(v_init_value, JaniExpression), "Init value should be a JaniExpression"
def __init__(self, v_name: str, v_type: ValidTypes,
v_init_value: Optional[Union[JaniExpression, JaniValue]] = None,
v_transient: bool = False):
assert v_init_value is None or isinstance(v_init_value, (JaniExpression, JaniValue)), \
"Init value should be a JaniExpression or a JaniValue"
if v_init_value is not None:
if isinstance(v_init_value, JaniExpression):
self._init_value = v_init_value
else: # In this case it can only be a JaniValue
self._init_value = JaniExpression(v_init_value)
assert v_type in get_args(ValidTypes), f"Type {v_type} not supported by Jani"
self._name = v_name
self._init_value = v_init_value
Expand All @@ -40,7 +48,8 @@ def __init__(self, v_name: str, v_type: ValidTypes, v_init_value: Optional[JaniE
elif self._type == float:
self._init_value = JaniExpression(0.0)
if not self._transient and self._type == float:
print(f"Warning: Variable {self._name} is not transient and has type float. This is not supported by STORM yet.")
print(f"Warning: Variable {self._name} is not transient and has type float."
"This is not supported by STORM yet.")

def name(self):
return self._name
Expand Down Expand Up @@ -77,8 +86,8 @@ def jani_type_to_string(v_type: ValidTypes) -> str:
// 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".
// 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
"int", // numeric; assignable from int and bounded int
Expand Down
2 changes: 1 addition & 1 deletion jani_generator/src/jani_generator/main.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@

from jani_generator.jani_entries import JaniModel
from jani_generator.convince_jani_helpers import convince_jani_parser
from jani_generator.scxml_helpers.scxml_to_jani import interpret_top_level_xml
from jani_generator.scxml_helpers.top_level_interpreter import interpret_top_level_xml


def main_convince_to_plain_jani(_args: Optional[Sequence[str]] = None) -> None:
Expand Down
Loading

0 comments on commit e8866b8

Please sign in to comment.