wip: fix order in the display of clocks, params, etc.

pta2maude/src/Parser.py

@@ -842,29 +842,27 @@ class InterpreterParser(Parser):
         return result
 
     def _get_preamble(self, model: Model) -> str:
-        clocks = model.clocks
-        parameters = model.parameters
 
         # locations
-        locations = [
-            loc.name for automaton in model.automata for loc in automaton.locations
-        ]
+        locations = sorted(
+            [loc.name for automaton in model.automata for loc in automaton.locations]
+        )
         locations_str = self.maude.operators(locations, [], "Location", ["ctor"])
 
         # actions
-        actions = [a for a in model.actions]
+        actions = sorted(model.actions)
         actions_str = self.maude.operators(actions, [], "Action", ["ctor"])
 
         # automata label
-        names = [automaton.name for automaton in model.automata]
+        names = sorted([automaton.name for automaton in model.automata])
         names_str = self.maude.operators(names, [], "Agent", ["ctor"])
 
         # clocks
-        clocks = [clock for clock in model.clocks]
+        clocks = sorted(model.clocks)
         clocks_str = self.maude.operators(clocks, [], "Clock", ["ctor"])
 
         # parameters
-        parameters = [param for param in model.parameters]
+        parameters = sorted(model.parameters)
         parameters_str = self.maude.operators(parameters, [], "Parameter", ["ctor"])
 
         preamble = f"""
@@ -968,7 +966,7 @@ class InterpreterParser(Parser):
         locations_str = f",\n{tab} ".join(locations)
 
         eq_str = (
-            f"eq {name.title()} = < {initial_state} |\n{tab} {locations_str}\n{tab}> ."
+            f"eq {name.title()} = < {initial_state} |\n{tab} {locations_str} >\n{tab}."
         )
 
         result = f"""
@@ -997,10 +995,8 @@ class InterpreterParser(Parser):
         mod MODEL is
             {import_dynamics}
             {preamble}
-
             {equations}
             {init}
-
             {variables}
         endm
 

pta2maude/tests/examples/coffee-intrpr.maude

 load Semantics .
 
 mod MODEL is
-  extending  DYNAMICS .
-
-  ops idle sugar coffee cdone   : -> Location [ctor] .
-  ops cup coffee press sleep : -> Action [ctor] .
-  ops machine                         : -> Agent [ctor] .
-  ops x y                          : -> Clock [ctor] .
-  ops p1 p2 p3                       : -> Parameter [ctor] .
-
- op Machine : -> Automaton .
- eq Machine = < machine @ idle |
-                        (@ idle inv true :
-                           (when true local press do { x := 0 ; y := 0 } goto sugar)),
-                        (@ sugar inv y <= p2 :
-                            (when p1 <= x local press do { x := 0 } goto sugar ;
-                             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  :
-                             (when true local press do { x := 0 ; y := 0 } goto sugar ;
-                              when x = 10 local sleep goto idle))
-              > .
-
-   op init : -> State .
-   eq init = { Machine }
+    extending DYNAMICS .
+
+    ops cdone coffee idle sugar : -> Location [ctor] .
+    ops coffee cup press sleep : -> Action [ctor] .
+    op machine : -> Agent [ctor] .
+    ops x y : -> Clock [ctor] .
+    ops p1 p2 p3 : -> Parameter [ctor] .
+
+    op Machine : -> Automaton .
+    eq Machine = < machine @ idle |
+                   (@ idle inv true :
+                      (when true local press do { x := 0 ; y := 0 } goto sugar)),
+                   (@ sugar inv y <= p2 :
+                      (when x >= p1 local press do { x := 0 } goto sugar ;
+                       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  :
+                      (when true local press do { x := 0 ; y := 0 } goto sugar ;
+                       when x = 10 local sleep goto idle)) >
+                  .
+
+    op init : -> State .
+    eq init = { Machine }
               < tick: tickOk
                 clocks: (x : 0, y : 0)
                 parameters: (p1 : 1, p2 : 1, p3 : 1)
                 dvariables: empty >
-                .
+              .
 
- --- -------------------------
- var NET    : Network .
- var CLOCKS : SetAssignment .
- var PARAMS : SetAssignment .
- var DVARS  : SetAssignment .
- var SSTDEF : SStateDef .
- --- -------------------------
+    --- -------------------------
+    var NET : Network .
+    var CLOCKS : SetAssignment .
+    var PARAMS : SetAssignment .
+    var DVARS : SetAssignment .
+    var SSTDEF : SStateDef .
+    --- -------------------------
 
 endm
 
-search [1] init =>* { < machine @ cdone | SSTDEF >  } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > .
+search [1] init =>* { < machine @ cdone | SSTDEF >  } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > .
\ No newline at end of file
+
+quit .
+
+eof
\ No newline at end of file

pta2maude/tests/test_parser.py

@@ -29,7 +29,7 @@ def test_parser(examples_dir, imitator_file, maude_file, version):
     elif version == "no-collapsing":
         parser = NoCollapsingParser()
     elif version == "interpreter":
-        parser = InterpreterParser
+        parser = InterpreterParser()
     else:
         raise Exception(f"the version '{version}' is not supported")