Merge branch 'release/1.2.0'

grayswandyr · Oct 3, 2024 · 38bed9d · 38bed9d
2 parents e48a8ff + 4ee682e
commit 38bed9d
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 12 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,6 @@
+### 1.2.0 (2024-10-03)
+- fix bug: several lassos in some SMV traces. The BMC algorithm now is now "sbmc_inc" and the complete algorithm is (for nuXmv) "ic3 -i".
+
 ### 1.1.1 (2024-09-27)
 - fix bug: some arithmetic auxiliaries were absent from the generated SMV file
 

diff --git a/res/nusmv-default-bmc-script.scr b/res/nusmv-default-bmc-script.scr
@@ -1,5 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
 go_bmc;
-check_ltlspec_bmc_inc;
-quit -x
+check_ltlspec_sbmc_inc;
+quit -x
diff --git a/res/nusmv-default-script.scr b/res/nusmv-default-script.scr
@@ -5,4 +5,4 @@ flatten_hierarchy;
 encode_variables;
 build_model;
 check_ltlspec;
-quit -x
+quit -x
diff --git a/res/nuxmv-default-bmc-script.scr b/res/nuxmv-default-bmc-script.scr
@@ -1,5 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
 go_bmc;
-check_ltlspec_bmc_inc;
-quit -x
+check_ltlspec_sbmc_inc;
+quit -x
diff --git a/res/nuxmv-default-script.scr b/res/nuxmv-default-script.scr
@@ -1,9 +1,5 @@
 set default_trace_plugin 1;
 set on_failure_script_quits 1;
-read_model;
-flatten_hierarchy;
-build_flat_model;
-encode_variables;
-build_boolean_model;
-check_ltlspec_ic3;
-quit -x
+go_msat;
+check_ltlspec_ic3 -i;
+quit -x