fix: update theories

README.md

@@ -6,9 +6,9 @@ Details about the translation can be found in [this technical report](./paper.pd
 
 ## Getting started
 
-The project was tested in [Maude 3.2](http://maude.cs.illinois.edu/) and [Maude
+The project was tested in [Maude 3.3.1](http://maude.cs.illinois.edu/) and [Maude
 SE](https://maude-se.github.io/). A script written in [Python
-3.10](https://www.python.org/) is used to parse Imitator input files into Maude
+3.10](https://www.python.org/) is used to parse Roméo input files into Maude
 files.
 
 ### Maude files

pitpn2maude/app.py

 import argparse
 
-from src.Parser import SymbolicFoldingTheory, SymbolicTheory
+from src.Parser import SymbolicTheory
 
 
 def main(input_file: str, output_file: str, theory: str):
@@ -8,10 +8,14 @@ def main(input_file: str, output_file: str, theory: str):
         # parse Romeo file into Maude
         parser = None
 
-        if theory == "symbolic-theory" or theory == "symbolic-theory2":
+        if theory in [
+            "search-sym",
+            "search-sym2",
+            "search-folding",
+            "folding",
+            "AG-synthesis",
+        ]:
             parser = SymbolicTheory(theory)
-        elif theory == "symbolic-folding-tree":
-            parser = SymbolicFoldingTheory(theory)
         else:
             raise RuntimeError(f"Theory {theory} is not supported")
 

pitpn2maude/src/Parser.py

@@ -281,16 +281,10 @@ class SymbolicTheory(Parser):
         return eq
 
     def _get_search_cmd(self) -> str:
-        nb_traces = 1
-        nb_steps_str = "*"
+        nb_traces = "" if self.theory == "AG-synthesis" else "[ 1 ] "
+
+        cmd = f"""red {self.theory} {nb_traces}in 'MODEL : ( net, marking, constraint ) s.t. <replace_m> . """
 
-        state = "{ n:Nat , TS:TickState : <replace_p> ; REST:Marking : FT:FiringTimes : NET:Net , C:BooleanExpr }"
-        condition = (
-            "{SS:SatAssignmentSet} := smtCheck(C:BooleanExpr and <replace_m>, true)"
-        )
-        cmd = f"""search [{nb_traces}] init =>{nb_steps_str}
-                {state}
-                  such that {condition} ."""
         return cmd
 
     def to_maude(self, model: Net) -> str:
@@ -309,10 +303,10 @@ class SymbolicTheory(Parser):
         str
         """
         # load rewriting theory
-        load_theory = self.maude.loadFile(f"./{self.theory}")
+        load_theory = self.maude.loadFile("./analysis")
 
         # include petri net dynamics
-        import_pn = self.maude.importModule("PETRI-NET-DYNAMICS", ImportType.INCLUDING)
+        import_pn = self.maude.importModule("ANALYSIS", ImportType.INCLUDING)
 
         # maude preamble
         preamble = self._get_preamble(model)
@@ -343,116 +337,3 @@ class SymbolicTheory(Parser):
         eof"""
 
         return textwrap.dedent(model_str).strip()
-
-
-class SymbolicFoldingTheory(Parser):
-    def __init__(self, theory: str) -> None:
-        super().__init__(theory)
-
-    def _get_init_equation(self, model) -> str:
-        """Returns the initial state of the Petri net in Maude
-
-        Returns
-        -------
-        str
-        """
-        eq_name = "init"
-        eq_mark_name = "init-mark"
-        eq_const_name = "init-cons"
-
-        op_str = self.maude.operators([eq_name], [], "State", [])
-        op_mark_str = self.maude.operators([eq_mark_name], [], "Marking", [])
-        op_const_str = self.maude.operators([eq_const_name], [], "BooleanExpr", [])
-
-        # initial equation
-        init_eq_params = ", ".join([self.eq_name, eq_mark_name, eq_const_name])
-        init_eq_str = self.maude.equation(
-            eq_name, f"{eq_name}({init_eq_params})", [], []
-        )
-
-        # initial marking
-        places = [
-            self._get_place_sort(model, f'"{p.label}"', p.initial) for p in model.places
-        ]
-        places_str = " ; ".join(places)
-        init_mark_str = self.maude.equation(eq_mark_name, places_str, [], [])
-
-        # constraints on parameters
-        t_intervals = [(t.lower, t.upper) for t in model.transitions]
-        parameters = filter(self._is_parameter, set(sum(t_intervals, ())))
-        parameters_init = [f"{self._get_parameter_str(p)} >= 0/1" for p in parameters]
-        parameters_init += [
-            f"{self._get_parameter_str(lower)} <= {self._get_parameter_str(upper)}"
-            for (lower, upper) in t_intervals
-            if self._is_parameter(lower)
-            and self._is_parameter(upper)
-            and lower != upper
-        ]
-        parameters_init += [
-            f"{self._get_parameter_str(c.left)} {c.op} {self._get_parameter_str(c.right)}"
-            for c in model.constraints
-        ]
-        parameters_str = (
-            " and ".join(parameters_init) if len(parameters_init) else "true"
-        )
-        const_mark_str = self.maude.equation(eq_const_name, parameters_str, [], [])
-
-        eq = f"""
-            {op_str}
-            {init_eq_str}
-
-            {op_mark_str}
-            {init_mark_str}
-
-            {op_const_str}
-            {const_mark_str}"""
-
-        return eq
-
-    def to_maude(self, model: Net) -> str:
-        """
-        Parse a Petri net model into Maude
-
-        Parameters
-        ----------
-        model : Net
-            Petri net model
-        theory_file : str
-            rewriting theory to be loaded
-
-        Returns
-        -------
-        str
-        """
-        # load rewriting theory
-        load_theory = self.maude.loadFile(f"./{self.theory}")
-
-        # include petri net dynamics
-        import_pn = self.maude.importModule("SYMBOLIC-FOLDING", ImportType.PROTECTING)
-
-        # petri net equations
-        net_eq = self._get_net_equation(model)
-
-        # initial marking equations
-        init_eq = self._get_init_equation(model)
-
-        # search command
-        search_cmd = ""
-        # search_cmd = self._get_search_cmd(model)
-
-        model_str = f"""\
-        {load_theory}
-
-        mod MODEL is
-            {import_pn}
-            {net_eq}
-            {init_eq}
-        endm
-
-        {search_cmd}
-
-        quit .
-
-        eof"""
-
-        return textwrap.dedent(model_str).strip()