wip: add init equations

pta2maude/src/Parser.py

@@ -881,6 +881,37 @@ class InterpreterParser(Parser):
             --- -------------------------
         """
 
+    def _get_init_eq(self, model: Model) -> str:
+        label = "init"
+        init_op = self.maude.operators([label], [], "State", [])
+
+        tick = "tickOk"
+        clocks = [clock for clock in model.clocks]
+        clocks_str = f"({', '.join(clocks)})" if len(clocks) else "empty"
+        params = [param for param in model.parameters]
+        params_str = f"({', '.join(params)})" if len(params) else "empty"
+        variables = []
+        vars_str = f"({', '.join(variables)})" if len(variables) else "empty"
+
+        tab = " " * 22
+        config = f"\n{tab}".join(
+            [
+                f"tick: {tick}",
+                f"  clocks: {clocks_str}",
+                f"  parameters: {params_str}",
+                f"  dvariables: {vars_str}",
+            ]
+        )
+
+        agents = " ".join([automaton.name for automaton in model.automata])
+        init_eq_str = f"eq {label} = {{ {agents} }}\n{tab}< {config} >\n{tab}."
+
+        eq = f"""
+            {init_op}
+            {init_eq_str}"""
+
+        return eq
+
     def _get_search_cmd(self) -> str:
         return ""
 
@@ -890,6 +921,8 @@ class InterpreterParser(Parser):
         preamble = self._get_preamble(model)
         variables = self._get_variables()
 
+        init = self._get_init_eq(model)
+
         rules = ""
         search_cmd = self._get_search_cmd()
 
@@ -901,6 +934,8 @@ class InterpreterParser(Parser):
             {preamble}
 
             {rules}
+            {init}
+
             {variables}
         endm
 

pta2maude/tests/examples/coffee-intrpr.maude

@@ -23,7 +23,7 @@ mod MODEL is
               > .
 
    op init : -> State .
-   eq init = { Coffee }
+   eq init = { machine }
               < tick: tickOk
                 clocks: (x : 0/1, y : 0/1)
                 parameters: (p1 : 1, p2 : 1, p3 : 1)
@@ -37,6 +37,7 @@ mod MODEL is
  var DVARS  : SetAssignment .
  var SSTDEF : SStateDef .
  --- -------------------------
+
 endm
 
 search [1] init =>* { < coffee @ done | SSTDEF >  } < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > .