wip: smt_search

benchmarks/benchmarks.sh

@@ -25,12 +25,11 @@ function run_imitator {
   timeout $timeout_value $imitator "${model}" "${property}" -output-prefix "${property}"
 }
 
-
 # run parser pta2maude
 function parser_files {
   model=$1
   mode=$2
-  echo "parsing" $name "..."
+  echo "parsing" $name "with mode" "$mode" "..."
   python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.${mode}.maude" "--${mode}"
 }
 
@@ -46,7 +45,7 @@ function create_folder {
   path=$1
 
   if [ ! -d "$path" ]; then
-  mkdir -p "$path";
+    mkdir -p "$path";
   fi
 }
 

pta2maude/src/Parser.py

@@ -491,6 +491,16 @@ class NoCollapsingParser(Parser):
 
         return rule
 
+    def _get_search_cmd(
+        self, initial_location, clocks, parameters, nb_traces, nb_steps
+    ):
+        initial_state = self._get_state(initial_location, clocks, parameters, True)
+
+        fresh_clocks = [f"{c}:{self.var_type}" for c in clocks]
+        final_state = self._get_state("<replace>", fresh_clocks, parameters, True)
+        cmd = f"smt-search [{nb_traces}] {initial_state} =>{nb_steps} {final_state} ."
+        return cmd
+
     def to_maude(self, model: Model) -> str:
         """
         Parse an Imitator model into Maude
@@ -530,6 +540,9 @@ class NoCollapsingParser(Parser):
         load_smt = self.maude.loadFile("smt")
         import_real = self.maude.importModule("REAL", ImportType.PROTECTING)
         preamble = self._get_preamble(automaton, clocks, parameters)
+        search_cmd = self._get_search_cmd(
+            automaton.initial_location(), clocks, parameters, 1, "*"
+        )
 
         model_str = f"""\
         {load_smt}
@@ -541,6 +554,10 @@ class NoCollapsingParser(Parser):
             {rules}
         endm
 
+        {search_cmd}
+
+        quit .
+
         eof
         """