wip: computes sync actions

pta2maude/app.py

@@ -18,17 +18,19 @@ def main(input_filename, output_filename, version):
     """
     try:
         # parse Imitator file
-        parser = None
         if version == "collapsing":
             parser = CollapsingParser()
+            sync_product = True
         elif version == "no-collapsing":
             parser = NoCollapsingParser()
+            sync_product = True
         elif version == "interpreter":
             parser = InterpreterParser()
+            sync_product = False
         else:
             raise Exception(f"the version '{version}' is not supported")
 
-        output = parser.parse_file(input_filename)
+        output = parser.parse_file(input_filename, sync_product)
 
         # write to file
         with open(output_filename, "w") as f:

pta2maude/src/Parser.py

@@ -232,7 +232,7 @@ class Parser(ABC):
 
         return imitator_str
 
-    def parse_file(self, filename: str) -> str:
+    def parse_file(self, filename: str, sync_product: bool) -> str:
         """
         Parse an Imitator file into a Maude model
 
@@ -241,6 +241,9 @@ class Parser(ABC):
         filename : str
             Imitator file
 
+        sync_product : bool
+            Computes the synchronisation product of the automata
+
         Returns
         -------
         str
@@ -260,14 +263,15 @@ class Parser(ABC):
         model = visitor.visit(tree)
 
         # compute synchronized product if there are more than 1 automaton
-        if len(model.automata) > 1:
+        if sync_product and len(model.automata) > 1:
             model_name = os.path.splitext(os.path.basename(filename))[0]
             model = model.get_synchronized_product(model_name.replace("-", "_"))
             with open(f"{filename}.full", "w") as f:
                 f.write(self.to_imitator(model))
 
+            assert len(model.automata) == 1, "Only 1 automaton is supported."
+
         # parse to Maude
-        assert len(model.automata) == 1, "Only 1 automaton is supported."
         output = self.to_maude(model)
 
         return output
@@ -899,11 +903,13 @@ class InterpreterParser(Parser):
         tick = "tickOk"
 
         # clocks
-        clocks = [clock for clock in model.clocks]
+        # TODO: check this with Carlos
+        clocks = [f"{clock} : 0" for clock in model.clocks]
         clocks_str = f"({', '.join(clocks)})" if len(clocks) else "empty"
 
         # params
-        params = [param for param in model.parameters]
+        # TODO: check this with Carlos
+        params = [f"{param} : 1" for param in model.parameters]
         params_str = f"({', '.join(params)})" if len(params) else "empty"
 
         # variables
@@ -930,7 +936,7 @@ class InterpreterParser(Parser):
 
         return eq
 
-    def _get_transition(self, t: Transition) -> str:
+    def _get_transition(self, t: Transition, sync_actions: list[str]) -> str:
         # updates
         updates = " ; ".join(
             [re.sub(r"(\S+)\s*:=\s*(\S+)", r"\1 := \2", u) for u in t.update]
@@ -938,14 +944,15 @@ class InterpreterParser(Parser):
         updates_str = "" if (updates == "") else f" do {{ {updates} }}"
 
         # sync
-        sync = t.sync
+        actions = t.sync
+        sync_str = f"sync {actions}" if actions in sync_actions else f"local {actions}"
 
         # guard
         guard = self._normalize_constraints(t.guard)
 
-        return f"when {guard} sync {sync}{updates_str} goto {t.target}"
+        return f"when {guard} {sync_str}{updates_str} goto {t.target}"
 
-    def _get_automaton(self, automaton: Automaton) -> str:
+    def _get_automaton(self, automaton: Automaton, sync_actions: list[str]) -> str:
         name = automaton.name
         initial_state = f"{name} @ {automaton.initial_location.name}"
         tab = " " * 26
@@ -956,7 +963,8 @@ class InterpreterParser(Parser):
         locations = []
         for loc in automaton.locations:
             trans = [
-                self._get_transition(t) for t in automaton.transitions_from(loc.name)
+                self._get_transition(t, sync_actions)
+                for t in automaton.transitions_from(loc.name)
             ]
 
             trans_str = f" ;\n{tab}     ".join(trans)
@@ -986,7 +994,14 @@ class InterpreterParser(Parser):
 
         init = self._get_init_eq(model)
 
-        equations = "\n".join([self._get_automaton(a) for a in model.automata])
+        actions = [
+            action for a in model.automata for action in {t.sync for t in a.transitions}
+        ]
+        sync_actions = list(set([a for a in actions if actions.count(a) > 1]))
+
+        equations = "\n".join(
+            [self._get_automaton(a, sync_actions) for a in model.automata]
+        )
         search_cmd = self._get_search_cmd()
 
         model_str = f"""\

pta2maude/tests/examples/coffee-intrpr.maude

@@ -18,7 +18,7 @@ mod MODEL is
                        when y = p2 local cup goto coffee)),
                    (@ coffee inv y <= p3 :
                       (when y = p3 local coffee do { x := 0 } goto cdone)),
-                   (@ cdone inv x <= 10  :
+                   (@ cdone inv x <= 10 :
                       (when true local press do { x := 0 ; y := 0 } goto sugar ;
                        when x = 10 local sleep goto idle)) >
                   .

pta2maude/tests/test_parser.py

@@ -23,19 +23,21 @@ def remove_spaces(output_str):
 )
 def test_parser(examples_dir, imitator_file, maude_file, version):
     # select the correct parser
-    parser = None
     if version == "collapsing":
         parser = CollapsingParser()
+        sync_product = True
     elif version == "no-collapsing":
         parser = NoCollapsingParser()
+        sync_product = True
     elif version == "interpreter":
         parser = InterpreterParser()
+        sync_product = False
     else:
         raise Exception(f"the version '{version}' is not supported")
 
     # parse the imitator file
     input_file = os.path.join(examples_dir, imitator_file)
-    output = parser.parse_file(input_file)
+    output = parser.parse_file(input_file, sync_product)
 
     # read the file with the expected output
     expected_file = os.path.join(examples_dir, maude_file)