fix tests

pta2maude/src/Parser.py

@@ -844,7 +844,7 @@ class InterpreterParser(Parser):
         params = model.parameters
         params_constraints = []
         for c in model.initial_constraints:
-            v1, op, v2 = self._normalize_constraints(c, False).split(" ")
+            v1, op, v2 = self._normalize_constraints(c, False, True).split(" ")
             new_v1 = f"rr(var({v1}))" if v1 in params else v1
             new_v2 = f"rr(var({v2}))" if v2 in params else v2
 
@@ -874,7 +874,9 @@ class InterpreterParser(Parser):
 
         return var_constraints
 
-    def _normalize_constraints(self, constraint: str, parens: bool = True) -> str:
+    def _normalize_constraints(
+        self, constraint: str, parens: bool = True, expand_equal: bool = False
+    ) -> str:
         """
         Normalize the string represention of a constraint. For instance, adding
         spaces around binary operators.
@@ -885,6 +887,8 @@ class InterpreterParser(Parser):
             string representation of the constraint
         parens : bool
             Flag to surround constraint with parenthesis
+        expand_equal : bool
+            Flag to use the maude symbol for equal
 
         Returns
         -------
@@ -902,6 +906,9 @@ class InterpreterParser(Parser):
         # replace binary & by and
         result = no_spaces.replace(" | ", " or ").replace(" & ", " and ")
 
+        if expand_equal:
+            result = result.replace(" = ", " === ")
+
         if parens and result != "true":
             c_list = [f"({g})" for g in result.split(" and ")]
             result_str = " and ".join(c_list)

pta2maude/tests/examples/train-intruder-intrpr.maude

@@ -80,13 +80,13 @@ mod MODEL is
                 clocks: (xtrain : 0, xintruder : 0, xgate : 0)
                 parameters: (pfar : rr(var(pfar)), papproaching : rr(var(papproaching)), pverynear : rr(var(pverynear)), pwalkingsensor : rr(var(pwalkingsensor)), pwalkinghouse : rr(var(pwalkinghouse)), pwaiting : rr(var(pwaiting)), plowering : rr(var(plowering)), pemergencywaiting : rr(var(pemergencywaiting)), pemergencylowering : rr(var(pemergencylowering)))
                 dvariables: (choice : 0, gatedown : 0, sensoractive : 1, start : 0)
-                constraint: rr(var(pwalkingsensor)) >= 0 and rr(var(pwalkinghouse)) >= 0 and rr(var(choice)) >= 0 and rr(var(choice)) <= 1 and rr(var(pfar)) === 3 and rr(var(papproaching)) === 2 and rr(var(pverynear)) === 1 and rr(var(pwaiting)) === 1 and rr(var(pemergencywaiting)) === 1 and rr(var(plowering)) === 2 and rr(var(pemergencylowering)) === 1
+                constraint: rr(var(pwalkingsensor)) >= 0 and rr(var(pwalkinghouse)) >= 0 and rr(var(pfar)) === 3 and rr(var(papproaching)) === 2 and rr(var(pverynear)) === 1 and rr(var(pwaiting)) === 1 and rr(var(pemergencywaiting)) === 1 and rr(var(plowering)) === 2 and rr(var(pemergencylowering)) === 1
                 n: 1 >
               .
 endm
 
-red synthesis [ 1 ] in 'MODEL : init => (train @ crash) .
-red search-folding [ 1 ] in 'MODEL : init => (train @ crash) .
+red synthesis [ 1 ] in 'MODEL : init => (<replace>) .
+red search-folding [ 1 ] in 'MODEL : init => (<replace>) .
 
 quit .