add discrete variables in preamble

pta2maude/src/Maude.py

@@ -84,6 +84,9 @@ class Maude:
         ------
         str
         """
+        if not len(identifiers):
+            return ""
+
         sorts_l = " ".join(identifiers)
         keyword = "sorts" if (len(identifiers) > 1) else "sort"
         sorts_str = f"{keyword} {sorts_l} ."
@@ -128,6 +131,9 @@ class Maude:
         ------
         str
         """
+        if not len(identifiers):
+            return ""
+
         keyword = "vars" if (len(identifiers) > 1) else "var"
         identifiers_l = " ".join(identifiers)
         variables_str = f"{keyword} {identifiers_l} : {sort} ."
@@ -185,6 +191,9 @@ class Maude:
         ------
         str
         """
+        if not len(identifiers):
+            return ""
+
         keyword = "ops" if (len(identifiers) > 1) else "op"
         identifiers_l = " ".join(identifiers)
         domain = " ".join(domain_sorts)

pta2maude/src/Parser.py

@@ -913,14 +913,21 @@ class InterpreterParser(Parser):
         parameters = sorted(model.parameters)
         parameters_str = self.maude.operators(parameters, [], "Parameter", ["ctor"])
 
+        # discrete variables
+        discrete_vars = sorted(model.discrete_vars)
+        discrete_str = self.maude.operators(discrete_vars, [], "DVariable", ["ctor"])
+
         preamble = f"""
             {locations_str}
             {actions_str}
             {names_str}
             {clocks_str}
+            {discrete_str}
             {parameters_str}"""
 
-        return preamble
+        # remove empty lines
+        preamble = "\n".join([s for s in preamble.split("\n") if s.strip()])
+        return preamble.strip()
 
     def _get_init_eq(self, model: Model) -> str:
         """Get the initial state of the Maude interpreter
@@ -1073,10 +1080,25 @@ class InterpreterParser(Parser):
         cmd = f"red synthesis {params} in 'MODEL : init => (<replace>) ."
         return cmd
 
-    def _get_search_cmd(self) -> str:
-        """Return the command for reachability analysis"""
+    def _get_search_cmd(self, nb_traces: int = None, nb_steps: int = None) -> str:
+        """Return the command for reachability analysis
+
+        Parameters
+        ----------
+        nb_traces : int
+            number of traces to be found in the synthesis analysis
+        nb_steps : int
+            number of steps of the synthesis analysis
+        """
+        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 = "red search-folding in 'MODEL : init => (<replace>) ."
+        cmd = f"red search-folding {params} in 'MODEL : init => (<replace>) ."
         return cmd
 
     def to_maude(self, model: Model) -> str:
@@ -1112,13 +1134,14 @@ class InterpreterParser(Parser):
         )
 
         synthesis_cmd = self._get_synthesis_cmd(1)
-        search_cmd = self._get_search_cmd()
+        search_cmd = self._get_search_cmd(1)
 
         model_str = f"""\
         {load}
 
         mod MODEL is
             {import_dynamics}
+
             {preamble}
             {equations}
             {init}

pta2maude/tests/examples/coffee-intrpr.maude

@@ -36,7 +36,7 @@ mod MODEL is
 endm
 
 red synthesis [ 1 ] in 'MODEL : init => (<replace>) .
-red search-folding in 'MODEL : init => (<replace>) .
+red search-folding [ 1 ] in 'MODEL : init => (<replace>) .
 
 quit .
 

pta2maude/tests/examples/fischer-intrpr.maude

---- Fisher Mutual Exclusion Problem
-load ../analysis .
+load analysis .
 
-mod FISCHER is
+mod MODEL is
   extending ANALYSIS .
 
- var N : Nat .
-
  ops obs-obs idle active check access-l cs  : Nat -> Location  [ctor] .
  ops obs-waiting obs-violation              :     -> Location  [ctor] .
  ops exit try update no-access access enter : Nat -> Action    [ctor] .
  op process                                 : Nat -> Agent     [ctor] .
  op observer                                :     -> Agent     [ctor] .
  op turn                                    :     -> DVariable [ctor] .
- ops x                                      : Nat -> Clock     [ctor] .
+ ops x1 x2                                      : Clock     [ctor] .
  ops delta gamma                            :     -> Parameter [ctor] .
 
  op proc : Nat -> Automaton .
- eq proc(N) = 
+ eq proc(N) =
    < process(N) | (
-                 (@ idle(N) inv true : 
+                 (@ idle(N) inv true :
                          (when (turn = -1) local try(N) do {x(N) := 0} goto active(N))),
-                 (@ active(N) inv (x(N) <= delta) : 
+                 (@ active(N) inv (x(N) <= delta) :
                          (when true local update(N) do {x(N) := 0 ; turn := N} goto check(N))),
                  (@ check(N) inv true :
-                         (when ( (turn != N) and (x(N) >= gamma)) local no-access(N) do { nothing } goto idle(N) , 
+                         (when ( (turn != N) and (x(N) >= gamma)) local no-access(N) do { nothing } goto idle(N) ,
                          when ( (turn = N)  and (x(N) >= gamma)) local access(N) do { nothing } goto access-l(N))) ,
-                 (@ access-l(N) inv true : 
+                 (@ access-l(N) inv true :
                          (when true sync enter(N) do { nothing } goto cs(N))),
-                 (@ cs(N) inv true : 
+                 (@ cs(N) inv true :
                          (when true sync exit(N) do { turn := -1 } goto idle(N)))) > .
 
  op observer : -> Automaton .
 
- eq observer = 
-   < observer  | 
+ eq observer =
+   < observer  |
         (@ obs-waiting inv true :
-          ( (when true sync enter(1) do {nothing} goto obs-obs(1)) , 
-            (when true sync enter(2) do {nothing} goto obs-obs(2)))) , 
+          ( (when true sync enter(1) do {nothing} goto obs-obs(1)) ,
+            (when true sync enter(2) do {nothing} goto obs-obs(2)))) ,
         (@ obs-obs(1) inv true :
              ( ( when true sync enter(2) do {nothing} goto obs-violation),
                ( when true sync exit(1) do {nothing} goto obs-waiting))),
@@ -52,26 +49,17 @@ mod FISCHER is
 
    op init : -> State .
    eq init = { observer,  proc(1), proc(2) }
-              < tick: tickOk 
+              < tick: tickOk
                 locs: (process(1) @ idle(1), process(2) @ idle(2), observer @ obs-waiting)
                 clocks: (x(1) : 0 , x(2) : 0)
                 parameters: (
                              gamma : rr(var(gamma)),
                              delta : rr(var(delta)))
                 dvariables: turn : -1
-                constraint: init-constraint --- and rr(var(gamma)) > rr(var(delta)) 
+                constraint: init-constraint --- and rr(var(gamma)) > rr(var(delta))
                 n: 1 > .
 
 endm
-eof 
---- set print attribute on .
---- EF(observer @ violation)
-red synthesis [1] in 'FISCHER :  init => (observer @ obs-violation) .
---- EF(observer @ violation) using folding 
+eof
+red synthesis [1] in 'MODEL :  init => (observer @ obs-violation) .
 red search-folding [1] in 'FISCHER : init => (observer @ obs-violation) .
---- Computing the whole PZG 
-red search-folding  in 'FISCHER :  init .
---- Synthesizing 
-red synthesis-folding  in 'FISCHER :  init => (observer @ obs-violation) .
---- If gamma > delta, the answer is no
-red search-folding  [1] in 'FISCHER :  init => (observer @ obs-violation) .