first draft of parser

pta2maude/src/Parser.py

@@ -1052,20 +1052,31 @@ class InterpreterParser(Parser):
 
         return result
 
-    def _get_search_cmd(self, nb_traces: int = None, nb_steps: int = None) -> str:
-        """Return the search command for reachability verification
+    def _get_synthesis_cmd(self, nb_traces: int = None, nb_steps: int = None) -> str:
+        """Return the command for parameter synthesis
 
         Parameters
         ----------
         nb_traces : int
-            number of traces to be found in the reachability analysis
+            number of traces to be found in the synthesis analysis
         nb_steps : int
-            number of steps of the reachability analysis
+            number of steps of the synthesis analysis
         """
-        nb_traces_str = "" if (nb_traces is None) else f" [{nb_traces}]"
-        nb_steps_str = "*" if (nb_steps is None) else f"{nb_steps}"
+        params = []
+        if nb_traces is not None:
+            params.append(str(nb_traces))
+        if nb_steps is not None:
+            params.append(str(nb_steps))
+
+        params = f"[ {' ; '.join(params)} ]"
 
-        cmd = f"search{nb_traces_str} init =>{nb_steps_str} {{ <replace> }} < tick: tickNotOk clocks: CLOCKS parameters: PARAMS dvariables: DVARS > ."
+        cmd = f"red synthesis {params} in 'MODEL : init => (<replace>) ."
+        return cmd
+
+    def _get_search_cmd(self) -> str:
+        """Return the command for reachability analysis"""
+
+        cmd = "red search-folding in 'MODEL : init => (<replace>) ."
         return cmd
 
     def to_maude(self, model: Model) -> str:
@@ -1100,7 +1111,9 @@ class InterpreterParser(Parser):
         equations = "\n".join(
             [self._get_automaton(a, sync_actions) for a in model.automata]
         )
-        search_cmd = self._get_search_cmd(1)
+
+        synthesis_cmd = self._get_synthesis_cmd(1)
+        search_cmd = self._get_search_cmd()
 
         model_str = f"""\
         {load}
@@ -1112,6 +1125,7 @@ class InterpreterParser(Parser):
             {init}
         endm
 
+        {synthesis_cmd}
         {search_cmd}
 
         quit .

pta2maude/tests/examples/coffee-intrpr.maude

@@ -34,14 +34,10 @@ mod MODEL is
                 n: 1 >
                 .
 endm
-eof
 
---- Solving EF(loc = cdone) --- one solution
-red synthesis [ 1 ] in 'COFFEE : init => (coffee @ cdone)  .
-red synthesis [ 1 ] in 'COFFEE : init => (coffee @ cdone)  such that ( y - x > 0 ) .
---- Solving EF(loc=cdone) with folding
---- This property does not hold
---- This loops
-red synthesis [ 1 ; 10 ] in 'COFFEE : init => empty  such that ( x - y > 0 ) .
---- This finishes (with answer no)
-red search-folding in 'COFFEE : init => empty  such that ( x - y > 0 ) .
+red synthesis [ 1 ] in 'MODEL : init => (<replace>) .
+red search-folding in 'MODEL : init => (<replace>) .
+
+quit .
+
+eof
\ No newline at end of file