replace names in the test example

pta2maude/src/Parser.py

@@ -885,11 +885,19 @@ class InterpreterParser(Parser):
         label = "init"
         init_op = self.maude.operators([label], [], "State", [])
 
+        # tick
         tick = "tickOk"
+
+        # clocks
         clocks = [clock for clock in model.clocks]
         clocks_str = f"({', '.join(clocks)})" if len(clocks) else "empty"
+
+        # params
         params = [param for param in model.parameters]
         params_str = f"({', '.join(params)})" if len(params) else "empty"
+
+        # variables
+        # TODO: add variables to the imitator parser (antlr)
         variables = []
         vars_str = f"({', '.join(variables)})" if len(variables) else "empty"
 

pta2maude/tests/examples/coffee-intrpr.maude

@@ -6,20 +6,21 @@ mod MODEL is
   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] .
+  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 { 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 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 <= c(10) :
+                    (when x = c(10) local sleep goto idle ;
+                     when True local press do { x := 0 ; y := 0 } goto sugar))
               > .
 
    op init : -> State .
@@ -40,4 +41,4 @@ mod MODEL is
 
 endm
 
-search [1] init =>* { < coffee @ done | SSTDEF >  } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > .
+search [1] init =>* { < machine @ cdone | SSTDEF >  } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > .