tests: update tests

pta2maude/src/Parser.py

@@ -669,7 +669,21 @@ class CollapsingParser(NoCollapsingParser):
 
         return preamble
 
-    def _get_equations(self, clocks, parameters) -> str:
+    def _get_equations(self, clocks: list[str], parameters: list[str]) -> str:
+        """
+        Get the equations for interpreting states
+
+        Parameters
+        ----------
+        clocks : list[str]
+            clocks of the model
+        parameters : list[str]
+            parameters of the model
+
+        Returns
+        -------
+        str
+        """
         variable = self.maude.variables(["l"], "Location")
 
         left_term = " ; ".join(["l"] + clocks)
@@ -699,6 +713,22 @@ class CollapsingParser(NoCollapsingParser):
         clocks: list[str],
         parameters: list[str],
     ) -> str:
+        """
+        Get reachability command for verification
+
+        Parameters
+        ----------
+        initial_location : str
+            identifier of the initial location of the automaton
+        clocks : list[str]
+            clocks of the model
+        parameters : list[str]
+            parameters of the model
+
+        Returns
+        -------
+        str
+        """
         fresh_clocks = [f"{c}:{self.var_type}" for c in clocks]
         fresh_params = [f"{p}:{self.var_type}" for p in parameters]
 

pta2maude/tests/examples/ex1x.maude

@@ -30,4 +30,8 @@ endm
 
 load meta-pta .
 
+red reachability (<replace>, ( < l0 ; x:Real > <> | ( x:Real >= 0/1 ) )) .
+
+quit .
+
 eof
\ No newline at end of file

pta2maude/tests/examples/ex1xy.maude

@@ -30,4 +30,8 @@ endm
 
 load meta-pta .
 
+red reachability (<replace>, ( < l0 ; x:Real ; y:Real > <> | ( x:Real === y:Real and x:Real >= 0/1 and y:Real >= 0/1 ) )) .
+
+quit .
+
 eof
\ No newline at end of file