add Dockerfile

nptav2maude/Dockerfile

+FROM --platform=linux/x86_64 ubuntu:22.04
+
+LABEL maintainer="Jaime Arias <arias@lipn.univ-paris13.fr>"
+
+# update install basic packages
+RUN apt update && \
+  apt install -y git wget
+
+# install maude-se-yices
+RUN wget -c https://tinyurl.com/3zttax25 -O - | tar -xz && \
+  ln -s /maude-se-yices2/maude-se-yices2 /usr/local/bin/maude-se-yices2 && \
+  echo "export MAUDE_LIB=/maude-se-yices2" >> ${HOME}/.bashrc
+
+# change working directory
+WORKDIR /app
\ No newline at end of file

nptav2maude/src/Parser.py

@@ -61,6 +61,23 @@ class InterpreterParser:
 
         return var_constraints
 
+    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, parens: bool = True, expand_equal: bool = False
     ) -> str:
@@ -90,8 +107,11 @@ class InterpreterParser:
         # remove more than one space
         no_spaces = re.sub(" +", " ", c_with_spaces)
 
+        # add x/1 to all the number
+        fix_numbers = self._normalize_numbers(no_spaces)
+
         # replace binary & by and
-        result = no_spaces.replace(" | ", " or ").replace(" & ", " and ")
+        result = fix_numbers.replace(" | ", " or ").replace(" & ", " and ")
 
         if expand_equal:
             result = result.replace(" = ", " === ")

nptav2maude/tests/examples/coffee-intrpr.maude

@@ -20,7 +20,7 @@ mod MODEL is
                      (when (y = p3) local coffee do { x := 0 } goto cdone)),
                   (@ cdone inv (x <= 10) :
                      (when true local press do { x := 0 ; y := 0 } goto sugar ,
-                      when (x = 10) local sleep do { nothing } goto idle)) >
+                      when (x = 10/1) local sleep do { nothing } goto idle)) >
                   .
 
    op init : -> State .

nptav2maude/tests/examples/coffee.imi

@@ -46,7 +46,7 @@ loc preparing: invariant y <= p3
 
 accepting loc cdone: invariant x <= 10
 	when True sync press do {x := 0, y := 0} goto sugar;
-	when x = 10 sync sleep goto idle;
+	when x = 10.0 sync sleep goto idle;
 
 end (* machine *)