add folding flag to the CI

nptav2maude/README.md

@@ -27,7 +27,7 @@ specification.
 
 ```
 λ> python3 app.py -h
-usage: app.py [-h] [--output OUTPUT] --input INPUT
+usage: app.py [-h] [--output OUTPUT] --input INPUT [--folding]
 
 From Imitator to Maude specifications
 
@@ -35,6 +35,7 @@ options:
   -h, --help       show this help message and exit
   --output OUTPUT  Maude output file (default: ./model.maude)
   --input INPUT    Imitator file (default: None)
+  --folding        Flag to use folding (default: False)
 ```
 
 Next, an example of use:

nptav2maude/app.py

@@ -3,7 +3,7 @@ import argparse
 from src.Parser import InterpreterParser
 
 
-def main(input_filename, output_filename):
+def main(input_filename, output_filename, folding):
     """
     Parse an Imitator file
 
@@ -13,12 +13,12 @@ def main(input_filename, output_filename):
         Imitator filename
     output_filename : str
         Path of the output file
-    version :str
-        Version of the maude encoding
+    folding : bool
+        Use folding technique
     """
     try:
         parser = InterpreterParser()
-        output = parser.parse_file(input_filename)
+        output = parser.parse_file(input_filename, folding)
 
         # write to file
         with open(output_filename, "w") as f:
@@ -40,5 +40,7 @@ if __name__ == "__main__":
 
     parser.add_argument("--input", type=str, required=True, help="Imitator file")
 
+    parser.add_argument("--folding", action="store_true", help="Flag to use folding")
+
     args = parser.parse_args()
-    main(args.input, args.output)
+    main(args.input, args.output, args.folding)

nptav2maude/src/Parser.py

@@ -328,13 +328,15 @@ class InterpreterParser:
         cmd = f"red search-folding {params} in 'MODEL : init => (<replace>) ."
         return cmd
 
-    def to_maude(self, model: Model) -> str:
+    def to_maude(self, model: Model, folding: bool = False) -> str:
         """Parse an Imitator model into Maude
 
         Parameters
         ----------
         model : Model
             Imitator model
+        folding : bool
+            Use folding technique in the search command
 
         Returns
         -------
@@ -359,9 +361,7 @@ class InterpreterParser:
         equations = "\n".join(
             [self._get_automaton(a, sync_actions) for a in model.automata]
         )
-
-        synthesis_cmd = self._get_synthesis_cmd(1)
-        search_cmd = self._get_search_cmd(1)
+        cmd = self._get_search_cmd(1) if folding else self._get_synthesis_cmd(1)
 
         model_str = f"""\
         {load}
@@ -374,8 +374,7 @@ class InterpreterParser:
             {init}
         endm
 
-        {synthesis_cmd}
-        {search_cmd}
+        {cmd}
 
         quit .
 
@@ -384,7 +383,7 @@ class InterpreterParser:
 
         return textwrap.dedent(model_str).strip()
 
-    def parse_file(self, filename: str) -> str:
+    def parse_file(self, filename: str, folding: bool) -> str:
         """
         Parse an Imitator file into a Maude model
 
@@ -392,9 +391,8 @@ class InterpreterParser:
         ----------
         filename : str
             Imitator file
-
-        sync_product : bool
-            Computes the synchronisation product of the automata
+        folding : bool
+            Use folding technique in the search command
 
         Returns
         -------
@@ -415,6 +413,6 @@ class InterpreterParser:
         model = visitor.visit(tree)
 
         # parse to Maude
-        output = self.to_maude(model)
+        output = self.to_maude(model, folding)
 
         return output

nptav2maude/tests/examples/coffee-intrpr.maude

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

nptav2maude/tests/examples/fischer-intrpr.maude

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

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

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