feature: add smt_search command

pta2maude/src/Parser.py

@@ -492,13 +492,53 @@ class NoCollapsingParser(Parser):
         return rule
 
     def _get_search_cmd(
-        self, initial_location, clocks, parameters, nb_traces, nb_steps
-    ):
+        self,
+        initial_location: str,
+        clocks: list[str],
+        parameters: list[str],
+        nb_traces: int = None,
+        nb_steps: int = None,
+    ) -> str:
+        """
+        Return a the search command for reachability verification
+
+        Parameters
+        ----------
+        initial_location: str
+            Initial location of the model
+        clocks : list[str]
+            clocks of the model
+        parameters : list[str]
+            parameters of the model
+        nb_traces : int
+            number of traces to be found in the reachability analysis
+        nb_steps : int
+            number of steps of the reachability analysis
+
+        Returns
+        -------
+        str
+        """
+        # initial state
         initial_state = self._get_state(initial_location, clocks, parameters, True)
 
-        fresh_clocks = [f"{c}:{self.var_type}" for c in clocks]
+        # final state
+        fresh_clocks = [f"{c}':{self.var_type}" for c in clocks]
         final_state = self._get_state("<replace>", fresh_clocks, parameters, True)
-        cmd = f"smt-search [{nb_traces}] {initial_state} =>{nb_steps} {final_state} ."
+
+        # initial conditions
+        condition_1 = []
+        if len(clocks) > 1:
+            condition_1 = [f"{clocks[0]} === {c}" for c in clocks[1:]]
+
+        condition_2 = [f"{v} >= 0/1" for v in clocks + parameters]
+        condition = " and ".join(condition_1 + condition_2)
+        condition = f" such that ( {condition} ) = true" if condition != "" else ""
+
+        nb_traces_str = "" if (nb_traces is None) else f" [{nb_traces}]"
+        nb_steps_str = "*" if (nb_steps is None) else f"{nb_steps}"
+
+        cmd = f"smt-search{nb_traces_str} {initial_state} =>{nb_steps_str} {final_state}{condition} ."
         return cmd
 
     def to_maude(self, model: Model) -> str:
@@ -518,6 +558,11 @@ class NoCollapsingParser(Parser):
         clocks = model.clocks
         parameters = model.parameters
 
+        initial_constraints = model.initial_constraints
+        if len(initial_constraints):
+            print("Please check the initial constraints in the search command:")
+            print(f"    {initial_constraints}")
+
         rules = []
         for source in automaton.locations:
             for t in automaton.transitions_from(source.name):
@@ -541,7 +586,7 @@ class NoCollapsingParser(Parser):
         import_real = self.maude.importModule("REAL", ImportType.PROTECTING)
         preamble = self._get_preamble(automaton, clocks, parameters)
         search_cmd = self._get_search_cmd(
-            automaton.initial_location.name, clocks, parameters, 1, "*"
+            automaton.initial_location.name, clocks, parameters, 1
         )
 
         model_str = f"""\

pta2maude/tests/examples/coffee-nc.maude

@@ -30,4 +30,8 @@ mod MODEL is
 
 endm
 
+smt-search [1] < idle ; x ; y > < p1 ; p2 ; p3 > =>* < <replace> ; x':Real ; y':Real > < p1 ; p2 ; p3 > such that ( x === y and x >= 0/1 and y >= 0/1 and p1 >= 0/1 and p2 >= 0/1 and p3 >= 0/1 ) = true .
+
+quit .
+
 eof
\ No newline at end of file

pta2maude/tests/examples/ex1x-nc.maude

@@ -24,4 +24,8 @@ mod MODEL is
 
 endm
 
+smt-search [1] < l0 ; x > <> =>* < <replace> ; x':Real > <> such that ( x >= 0/1 ) = true .
+
+quit .
+
 eof
\ No newline at end of file

pta2maude/tests/examples/ex1xy-nc.maude

@@ -24,4 +24,8 @@ mod MODEL is
 
 endm
 
+smt-search [1] < l0 ; x ; y > <> =>* < <replace> ; x':Real ; y':Real > <> such that ( x === y and x >= 0/1 and y >= 0/1 ) = true .
+
+quit .
+
 eof
\ No newline at end of file