diff --git a/README.md b/README.md
index a0e1436f39352282a7bb93fec0fe3ee8325b1fcd..1fbaff24614f7b399b07396a94621838263dc464 100644
--- a/README.md
+++ b/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
diff --git a/pitpn2maude/app.py b/pitpn2maude/app.py
index 930319a07856dc433f207bc461767147fe2ea0ce..5e11258425a38323c04bddf0b1dcb69d038cf0bc 100644
--- a/pitpn2maude/app.py
+++ b/pitpn2maude/app.py
@@ -1,6 +1,6 @@
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")
diff --git a/pitpn2maude/src/Parser.py b/pitpn2maude/src/Parser.py
index fb6eea21d164f7ca2bd44354c6a0688eeceffd2b..76e14fcafc3a5b3a5962cd3dcb34a49e922b37a1 100644
--- a/pitpn2maude/src/Parser.py
+++ b/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()