docs: add documentation of the code

pta2maude/src/Parser.py

@@ -17,23 +17,12 @@ class Parser(ABC):
 
     Attributes
     ----------
-    var_type : str
-        type of the variables
     maude : Maude
         Object containing methods to generate Maude statements
     """
 
-    def __init__(self, var_type="Real") -> None:
-        """
-        Constructor of the class
-
-        Parameters
-        ----------
-        var_type : str
-            type of the variables
-        """
-        self.var_type = var_type
-        self._time_var = "T"
+    def __init__(self) -> None:
+        """Constructor of the class"""
         self.maude = Maude()
 
     @abstractmethod
@@ -41,96 +30,6 @@ class Parser(ABC):
         """Parse Imitator model to Maude model"""
         pass
 
-    def _get_model_variables(self, model: Model) -> list[str]:
-        """
-        Get the variables of the model (clocks and parameters)
-
-        Parameters
-        ----------
-        model : Model
-            Imitator model
-
-        Returns
-        -------
-            list[str]
-        """
-        return model.clocks + model.parameters
-
-    def _normalize_float(self, number: str) -> str:
-        """Transforms float into rational"""
-        new_number = number.replace(".", "")
-        nb_decimals = len(new_number) - number.index(".")
-        new_number += f"/1{'0'*nb_decimals}"
-
-        return new_number.lstrip("0")
-
-    def _normalize_numbers(self, constraint: str) -> str:
-        """Add x/1 to the numbers in a constraint"""
-        number = re.sub(r"((?<!\.|\/)\b[0-9]+\b(?!\.|\/))", r"\1/1", constraint)
-        float = re.sub(
-            r"(\d+\.\d+)", lambda g: self._normalize_float(g.group(1)), number
-        )
-
-        return float
-
-    def _normalize_constraints(self, constraint: str) -> str:
-        """
-        Normalize the string represention of a constraint. For instance, adding
-        spaces around binary operators.
-
-        Parameters
-        ----------
-        constraint : str
-            string representation of the constraint
-
-        Returns
-        -------
-        str
-        """
-        # add space around binary operators
-        c_with_spaces = re.sub(r"((?!\.|\/)\W+)", r" \1 ", constraint)
-
-        # remove more than one space
-        result = re.sub(" +", " ", c_with_spaces)
-
-        # add x/1 to all the number
-        fix_numbers = self._normalize_numbers(result)
-
-        # replace binary & by and
-        good_operators = (
-            fix_numbers.replace(" | ", " or ")
-            .replace(" & ", " and ")
-            .replace(" = ", " === ")
-        )
-
-        return good_operators
-
-    def _get_updated_variables(
-        self, variables: list[str], updates: list[str]
-    ) -> list[str]:
-        """
-        Return the list of variables with the updated value
-
-        Parameters
-        ----------
-        variables : list[str]
-            list of variables to be updated
-        updates : list[str]
-            list of updates
-
-        Returns
-        -------
-        list[str]
-        """
-        new_vars = list(variables)
-        for u in updates:
-            matches = re.findall(r"(?P<var>\w+)\s*:=\s*(?P<val>\d+)", u)
-
-            # applying updates
-            for (var, value) in matches:
-                new_vars[new_vars.index(var)] = value
-        return new_vars
-
     def to_imitator(self, model: Model) -> str:
         """
         Parse an Imitator model with Imitator syntax
@@ -278,7 +177,7 @@ class Parser(ABC):
 
 
 class NoCollapsingParser(Parser):
-    """A class to represent the parser of Imitator using smt"""
+    """A class to represent the parser of Imitator to Maude using smt"""
 
     def __init__(self, var_type="Real") -> None:
         """
@@ -289,7 +188,99 @@ class NoCollapsingParser(Parser):
         var_type : str
             type of the variables
         """
-        super().__init__(var_type)
+        super().__init__()
+        self.var_type = var_type
+        self._time_var = "T"
+
+    def _get_model_variables(self, model: Model) -> list[str]:
+        """
+        Get the variables of the model (clocks and parameters)
+
+        Parameters
+        ----------
+        model : Model
+            Imitator model
+
+        Returns
+        -------
+            list[str]
+        """
+        return model.clocks + model.parameters
+
+    def _normalize_float(self, number: str) -> str:
+        """Transforms float into rational"""
+        new_number = number.replace(".", "")
+        nb_decimals = len(new_number) - number.index(".")
+        new_number += f"/1{'0'*nb_decimals}"
+
+        return new_number.lstrip("0")
+
+    def _normalize_numbers(self, constraint: str) -> str:
+        """Add x/1 to the numbers in a constraint"""
+        number = re.sub(r"((?<!\.|\/)\b[0-9]+\b(?!\.|\/))", r"\1/1", constraint)
+        float = re.sub(
+            r"(\d+\.\d+)", lambda g: self._normalize_float(g.group(1)), number
+        )
+
+        return float
+
+    def _normalize_constraints(self, constraint: str) -> str:
+        """
+        Normalize the string represention of a constraint. For instance, adding
+        spaces around binary operators.
+
+        Parameters
+        ----------
+        constraint : str
+            string representation of the constraint
+
+        Returns
+        -------
+        str
+        """
+        # add space around binary operators
+        c_with_spaces = re.sub(r"((?!\.|\/)\W+)", r" \1 ", constraint)
+
+        # remove more than one space
+        result = re.sub(" +", " ", c_with_spaces)
+
+        # add x/1 to all the number
+        fix_numbers = self._normalize_numbers(result)
+
+        # replace binary & by and
+        good_operators = (
+            fix_numbers.replace(" | ", " or ")
+            .replace(" & ", " and ")
+            .replace(" = ", " === ")
+        )
+
+        return good_operators
+
+    def _get_updated_variables(
+        self, variables: list[str], updates: list[str]
+    ) -> list[str]:
+        """
+        Return the list of variables with the updated value
+
+        Parameters
+        ----------
+        variables : list[str]
+            list of variables to be updated
+        updates : list[str]
+            list of updates
+
+        Returns
+        -------
+        list[str]
+        """
+        new_vars = list(variables)
+        for u in updates:
+            matches = re.findall(r"(?P<var>\w+)\s*:=\s*(?P<val>\d+)", u)
+
+            # applying updates
+            for (var, value) in matches:
+                new_vars[new_vars.index(var)] = value
+        return new_vars
 
     def _get_preamble(
         self, automaton: Automaton, clocks: list[str], parameters: list[str]
@@ -503,7 +494,7 @@ class NoCollapsingParser(Parser):
         nb_steps: int = None,
     ) -> str:
         """
-        Return a the search command for reachability verification
+        Return the search command for reachability verification
 
         Parameters
         ----------
@@ -613,7 +604,17 @@ class NoCollapsingParser(Parser):
 
 
 class CollapsingParser(NoCollapsingParser):
+    """A class to represent the parser of Imitator to Maude that does not collapse states"""
+
     def __init__(self, var_type="Real") -> None:
+        """
+        Constructor of the class
+
+        Parameters
+        ----------
+        var_type : str
+            type of the variables
+        """
         super().__init__(var_type)
 
     def _get_preamble(
@@ -822,18 +823,26 @@ class CollapsingParser(NoCollapsingParser):
 
 
 class InterpreterParser(Parser):
-    def __init__(self, var_type="Real") -> None:
+    """A class to represent the parser of Imitator to Maude using the interpreter version"""
+
+    def __init__(self) -> None:
+        """Constructor of the class"""
+        super().__init__()
+
+    def _normalize_constraints(self, constraint: str) -> str:
         """
-        Constructor of the class
+        Normalize the string represention of a constraint. For instance, adding
+        spaces around binary operators.
 
         Parameters
         ----------
-        var_type : str
-            type of the variables
-        """
-        super().__init__(var_type)
+        constraint : str
+            string representation of the constraint
 
-    def _normalize_constraints(self, constraint: str) -> str:
+        Returns
+        -------
+        str
+        """
         # replace True by true
         new_constr = "true" if constraint == "True" else constraint
 
@@ -846,7 +855,18 @@ class InterpreterParser(Parser):
         return result
 
     def _get_preamble(self, model: Model) -> str:
+        """
+        Get the preamble of the Maude file
+
+        Parameters
+        ----------
+        model : Model
+            Imitator model
 
+        Returns
+        -------
+        str
+        """
         # locations
         locations = sorted(
             [loc.name for automaton in model.automata for loc in automaton.locations]
@@ -879,6 +899,13 @@ class InterpreterParser(Parser):
         return preamble
 
     def _get_variables(self) -> str:
+        """
+        Get the definitions of the variables used in the Maude file
+
+        Returns
+        -------
+        str
+        """
         net = self.maude.variables(["NET"], "Network")
         clocks = self.maude.variables(["CLOCKS"], "SetAssignment")
         params = self.maude.variables(["PARAMS"], "SetAssignment")
@@ -892,16 +919,23 @@ class InterpreterParser(Parser):
             {params}
             {vars}
             {definition}
-            --- -------------------------
-        """
+            --- -------------------------"""
 
     def _get_init_eq(self, model: Model) -> str:
+        """Get the initial state of the Maude interpreter
+
+        Parameters
+        ----------
+        model : Model
+            Imitator model
+
+        Returns
+        -------
+        str
+        """
         label = "init"
         init_op = self.maude.operators([label], [], "State", [])
 
-        # tick
-        tick = "tickOk"
-
         # clocks
         # TODO: check this with Carlos
         clocks = [f"{clock} : 0" for clock in model.clocks]
@@ -920,7 +954,7 @@ class InterpreterParser(Parser):
         tab = " " * 22
         config = f"\n{tab}".join(
             [
-                f"tick: {tick}",
+                "tick: tickOk",
                 f"  clocks: {clocks_str}",
                 f"  parameters: {params_str}",
                 f"  dvariables: {vars_str}",
@@ -937,6 +971,19 @@ class InterpreterParser(Parser):
         return eq
 
     def _get_transition(self, t: Transition, sync_actions: list[str]) -> str:
+        """Get the enconding of the transition of an automaton
+
+        Parameters
+        ----------
+        t : Transition
+            automaton transition
+        sync_actions : list[str]
+            list of actions that synchronise in the automata
+
+        Returns
+        -------
+        str
+        """
         # updates
         updates = " ; ".join(
             [re.sub(r"(\S+)\s*:=\s*(\S+)", r"\1 := \2", u) for u in t.update]
@@ -953,6 +1000,19 @@ class InterpreterParser(Parser):
         return f"when {guard} {sync_str}{updates_str} goto {t.target}"
 
     def _get_automaton(self, automaton: Automaton, sync_actions: list[str]) -> str:
+        """Get the encoding of an automaton in the Maude interpreter
+
+        Parameters
+        ----------
+        automaton : Automaton
+            Imitator model
+        sync_actions : list[str]
+            list of actions that synchronise in the automata
+
+        Returns
+        -------
+        str
+        """
         name = automaton.name
         initial_state = f"{name} @ {automaton.initial_location.name}"
         tab = " " * 26
@@ -983,9 +1043,16 @@ class InterpreterParser(Parser):
 
         return result
 
-    def _get_search_cmd(
-        self, model: Model, nb_traces: int = None, nb_steps: int = None
-    ) -> str:
+    def _get_search_cmd(self, nb_traces: int = None, nb_steps: int = None) -> str:
+        """Return the search command for reachability verification
+
+        Parameters
+        ----------
+        nb_traces : int
+            number of traces to be found in the reachability analysis
+        nb_steps : int
+            number of steps of the reachability analysis
+        """
         nb_traces_str = "" if (nb_traces is None) else f" [{nb_traces}]"
         nb_steps_str = "*" if (nb_steps is None) else f"{nb_steps}"
 
@@ -993,6 +1060,17 @@ class InterpreterParser(Parser):
         return cmd
 
     def to_maude(self, model: Model) -> str:
+        """Parse an Imitator model into Maude
+
+        Parameters
+        ----------
+        model : Model
+            Imitator model
+
+        Returns
+        -------
+        str
+        """
         load = self.maude.loadFile("Semantics")
         import_dynamics = self.maude.importModule("DYNAMICS", ImportType.EXTENDING)
         preamble = self._get_preamble(model)
@@ -1008,7 +1086,7 @@ class InterpreterParser(Parser):
         equations = "\n".join(
             [self._get_automaton(a, sync_actions) for a in model.automata]
         )
-        search_cmd = self._get_search_cmd(model, 1)
+        search_cmd = self._get_search_cmd(1)
 
         model_str = f"""\
         {load}