wip: add preamble

pta2maude/src/Parser.py

@@ -315,7 +315,7 @@ class NoCollapsingParser(Parser):
             variables.append(self.maude.variables(clocks, self.var_type))
         if parameters:
             variables.append(self.maude.variables(parameters, self.var_type))
-        ""
+
         variables_str = "\n            ".join(variables)
 
         # define location constructors
@@ -830,7 +830,39 @@ class InterpreterParser(Parser):
         super().__init__(var_type)
 
     def _get_preamble(self, model: Model) -> str:
-        return ""
+        clocks = model.clocks
+        parameters = model.parameters
+
+        # locations
+        locations = [
+            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_str = self.maude.operators(actions, [], "Action", ["ctor"])
+
+        # automata label
+        names = [automaton.name for automaton in model.automata]
+        names_str = self.maude.operators(names, [], "Agent", ["ctor"])
+
+        # clocks
+        clocks = [clock for clock in model.clocks]
+        clocks_str = self.maude.operators(clocks, [], "Clock", ["ctor"])
+
+        # parameters
+        parameters = [param for param in model.parameters]
+        parameters_str = self.maude.operators(parameters, [], "Parameter", ["ctor"])
+
+        preamble = f"""
+            {locations_str}
+            {actions_str}
+            {names_str}
+            {clocks_str}
+            {parameters_str}"""
+
+        return preamble
 
     def _get_search_cmd(self) -> str:
         return ""

pta2maude/tests/examples/coffee-intrpr.maude

 load Semantics .
 
-mod COFFEE is
+mod MODEL is
   extending  DYNAMICS .
 
-  ops idle addsugar preparing done   : -> Location [ctor] .
-  ops bstart bsugar cup coffee sleep : -> Action [ctor] .
-  ops coffee                         : -> Agent [ctor] .
-  ops x1 x2                          : -> Clock [ctor] .
+  ops idle sugar coffee cdone : -> Location [ctor] .
+  ops press cup sleep coffee : -> Action [ctor] .
+  ops machine : -> Agent [ctor] .
+  ops x y                          : -> Clock [ctor] .
   ops p1 p2 p3                       : -> Parameter [ctor] .
 
  op Coffee : -> Automaton .
  eq Coffee = < coffee @ idle | (@ idle inv True :
-                           (when True local bstart do { x1 := 0 ; x2 := 0 } goto addsugar)),
-                        (@ addsugar inv x2 <= p2 :
-                            (when p1 <= x1 local bsugar do { x1 := 0 } goto addsugar ;
-                             when x2 = p2 local cup goto preparing)),
-                        (@ preparing inv x2 <= p3 :
-                             (when x2 = p3 local coffee do { x1 := 0 } goto done)) ,
-                        (@ done inv x1 <= c(10) :
-                             (when x1 = c(10) local sleep goto idle ;
-                              when True local bstart do { x1 := 0 ; x2 := 0 } goto addsugar))
+                           (when True local bstart do { x := 0 ; y := 0 } goto addsugar)),
+                        (@ addsugar inv y <= p2 :
+                            (when p1 <= x local bsugar do { x := 0 } goto addsugar ;
+                             when y = p2 local cup goto preparing)),
+                        (@ preparing inv y <= p3 :
+                             (when y = p3 local coffee do { x := 0 } goto done)) ,
+                        (@ done inv x <= c(10) :
+                             (when x = c(10) local sleep goto idle ;
+                              when True local bstart do { x := 0 ; y := 0 } goto addsugar))
               > .
 
    op init : -> State .
    eq init = { Coffee }
               < tick: tickOk
-                clocks: (x1 : 0/1, x2 : 0/1)
+                clocks: (x : 0/1, y : 0/1)
                 parameters: (p1 : 1, p2 : 1, p3 : 1)
                 dvariables: empty >
                 .