Merge pull request #479 from diffblue/smv-property-pretty-name

tautschnig · web-flow · commit d20c7c864569 · 2024-05-03T11:07:22.000+02:00
SMV frontend: strip `main::` from property pretty names
diff --git a/regression/ebmc/BDD/AF1.desc b/regression/ebmc/BDD/AF1.desc
@@ -1,8 +1,8 @@
 CORE
 AF1.smv
 --bdd
-^\[main::spec1\] AF some_var = TRUE: REFUTED$
-^\[main::spec2\] AF some_var = FALSE: PROVED$
+^\[spec1\] AF some_var = TRUE: REFUTED$
+^\[spec2\] AF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AF2.desc b/regression/ebmc/BDD/AF2.desc
@@ -1,8 +1,8 @@
 CORE
 AF2.smv
 --bdd
-^\[main::spec1\] AF some_var = TRUE: REFUTED$
-^\[main::spec2\] AF some_var = FALSE: PROVED$
+^\[spec1\] AF some_var = TRUE: REFUTED$
+^\[spec2\] AF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AG1.desc b/regression/ebmc/BDD/AG1.desc
@@ -1,8 +1,8 @@
 CORE
 AG1.smv
 --bdd
-^\[main::spec1\] AG some_var = TRUE: REFUTED$
-^\[main::spec2\] AG some_var = FALSE: PROVED$
+^\[spec1\] AG some_var = TRUE: REFUTED$
+^\[spec2\] AG some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AG2.desc b/regression/ebmc/BDD/AG2.desc
@@ -1,8 +1,8 @@
 CORE
 AG2.smv
 --bdd
-^\[main::spec1\] AG some_var = TRUE: REFUTED$
-^\[main::spec2\] AG some_var = FALSE: REFUTED$
+^\[spec1\] AG some_var = TRUE: REFUTED$
+^\[spec2\] AG some_var = FALSE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/AX1.desc b/regression/ebmc/BDD/AX1.desc
@@ -1,8 +1,8 @@
 CORE
 AX1.smv
 --bdd
-^\[main::spec1\] AX some_var = TRUE: REFUTED$
-^\[main::spec2\] AX some_var = FALSE: PROVED$
+^\[spec1\] AX some_var = TRUE: REFUTED$
+^\[spec2\] AX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/BDD1.desc b/regression/ebmc/BDD/BDD1.desc
@@ -3,6 +3,6 @@ BDD1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!some_var = off\): PROVED$
+^\[spec1\] AG \(!some_var = off\): PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/BDD4.desc b/regression/ebmc/BDD/BDD4.desc
@@ -3,6 +3,6 @@ BDD4.smv
 --bdd
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG .*: REFUTED$
+^\[spec1\] AG .*: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/BDD5.desc b/regression/ebmc/BDD/BDD5.desc
@@ -3,6 +3,6 @@ BDD5.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG .*: PROVED$
+^\[spec1\] AG .*: PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/BDD/EF1.desc b/regression/ebmc/BDD/EF1.desc
@@ -1,8 +1,8 @@
 CORE
 EF1.smv
 --bdd
-^\[main::spec1\] EF some_var = TRUE: REFUTED$
-^\[main::spec2\] EF some_var = FALSE: PROVED$
+^\[spec1\] EF some_var = TRUE: REFUTED$
+^\[spec2\] EF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EF2.desc b/regression/ebmc/BDD/EF2.desc
@@ -1,8 +1,8 @@
 CORE
 EF2.smv
 --bdd
-^\[main::spec1\] EF some_var = TRUE: REFUTED$
-^\[main::spec2\] EF some_var = FALSE: PROVED$
+^\[spec1\] EF some_var = TRUE: REFUTED$
+^\[spec2\] EF some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EG1.desc b/regression/ebmc/BDD/EG1.desc
@@ -1,8 +1,8 @@
 CORE
 EG1.smv
 --bdd
-^\[main::spec1\] EG some_var = TRUE: REFUTED$
-^\[main::spec2\] EG some_var = FALSE: PROVED$
+^\[spec1\] EG some_var = TRUE: REFUTED$
+^\[spec2\] EG some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EG2.desc b/regression/ebmc/BDD/EG2.desc
@@ -1,8 +1,8 @@
 CORE
 EG2.smv
 --bdd
-^\[main::spec1\] EG some_var = TRUE: REFUTED$
-^\[main::spec2\] EG some_var = FALSE: REFUTED$
+^\[spec1\] EG some_var = TRUE: REFUTED$
+^\[spec2\] EG some_var = FALSE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EX1.desc b/regression/ebmc/BDD/EX1.desc
@@ -1,8 +1,8 @@
 CORE
 EX1.smv
 --bdd
-^\[main::spec1\] EX some_var = TRUE: REFUTED$
-^\[main::spec2\] EX some_var = FALSE: PROVED$
+^\[spec1\] EX some_var = TRUE: REFUTED$
+^\[spec2\] EX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/EX2.desc b/regression/ebmc/BDD/EX2.desc
@@ -1,8 +1,8 @@
 CORE
 EX2.smv
 --bdd
-^\[main::spec1\] EX some_var = TRUE: REFUTED$
-^\[main::spec2\] EX some_var = FALSE: PROVED$
+^\[spec1\] EX some_var = TRUE: REFUTED$
+^\[spec2\] EX some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/GF1.desc b/regression/ebmc/BDD/GF1.desc
@@ -1,7 +1,7 @@
 CORE
 GF1.smv
 --bdd
-^\[main::spec1\] G F some_var: REFUTED$
+^\[spec1\] G F some_var: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/BDD/just_p.desc b/regression/ebmc/BDD/just_p.desc
@@ -1,8 +1,8 @@
 CORE
 just_p.smv
 --bdd
-^\[main::spec1\] some_var = TRUE: REFUTED$
-^\[main::spec2\] some_var = FALSE: PROVED$
+^\[spec1\] some_var = TRUE: REFUTED$
+^\[spec2\] some_var = FALSE: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/Properties1/test.desc b/regression/ebmc/Properties1/test.desc
@@ -1,9 +1,9 @@
 CORE broken-smt-backend
 main.smv
---bound 10 --property main::spec2
+--bound 10 --property spec2
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec2\] .* PROVED up to bound 10$
+^\[spec2\] .* PROVED up to bound 10$
 --
 ^warning: ignoring
-$\[main::spec1\] .*$
+$\[spec1\] .*$
diff --git a/regression/ebmc/elbtunnel/test.desc b/regression/ebmc/elbtunnel/test.desc
@@ -3,13 +3,13 @@ elbtunnel.aig.smv
 --bound 12
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
-^\[main::spec2\] .* PROVED up to bound 12$
-^\[main::spec3\] .* REFUTED$
-^\[main::spec4\] .* REFUTED$
-^\[main::spec5\] .* PROVED up to bound 12$
-^\[main::spec6\] .* PROVED up to bound 12$
-^\[main::spec7\] .* REFUTED$
-^\[main::spec8\] .* REFUTED$
+^\[spec1\] .* REFUTED$
+^\[spec2\] .* PROVED up to bound 12$
+^\[spec3\] .* REFUTED$
+^\[spec4\] .* REFUTED$
+^\[spec5\] .* PROVED up to bound 12$
+^\[spec6\] .* PROVED up to bound 12$
+^\[spec7\] .* REFUTED$
+^\[spec8\] .* REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type1.desc b/regression/ebmc/range_type/range_type1.desc
@@ -3,6 +3,6 @@ range_type1.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG x != 4: PROVED up to bound 10$
+^\[spec1\] AG x != 4: PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type2.desc b/regression/ebmc/range_type/range_type2.desc
@@ -3,7 +3,7 @@ range_type2.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG TRUE: PROVED up to bound 10$
-^\[main::spec2\] AG NET_tmp9: PROVED up to bound 10$
+^\[spec1\] AG TRUE: PROVED up to bound 10$
+^\[spec2\] AG NET_tmp9: PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type3.desc b/regression/ebmc/range_type/range_type3.desc
@@ -3,7 +3,7 @@ range_type3.smv
 --bound 10 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample:$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type4.desc b/regression/ebmc/range_type/range_type4.desc
@@ -3,6 +3,6 @@ range_type4.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 10$
+^\[spec1\] AG \(!x = 6\): PROVED up to bound 10$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/range_type/range_type5.desc b/regression/ebmc/range_type/range_type5.desc
@@ -3,6 +3,6 @@ range_type5.smv
 --bound 3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 3$
+^\[spec1\] AG \(!x = 6\): PROVED up to bound 3$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/small-test1/test.desc b/regression/ebmc/small-test1/test.desc
@@ -3,6 +3,6 @@ main.smv
 --bound 10 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG x = 1: REFUTED$
+^\[spec1\] AG x = 1: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/small-test2/test.desc b/regression/ebmc/small-test2/test.desc
@@ -3,6 +3,6 @@ main.smv
 --bound 2
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] AG z: REFUTED$
+^\[spec1\] AG z: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bdd_unsupported_property.desc b/regression/ebmc/smv/bdd_unsupported_property.desc
@@ -3,7 +3,7 @@ bdd_unsupported_property.smv
 --bdd
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property1.desc b/regression/ebmc/smv/bmc_unsupported_property1.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property1.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property2.desc b/regression/ebmc/smv/bmc_unsupported_property2.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property2.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
-^\[main::spec2\] G x = TRUE: PROVED up to bound 1$
+^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$
+^\[spec2\] G x = TRUE: PROVED up to bound 1$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property3.desc b/regression/ebmc/smv/bmc_unsupported_property3.desc
@@ -3,7 +3,7 @@ bmc_unsupported_property3.smv
 --aig
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$
-^\[main::spec2\] G x = FALSE: REFUTED$
+^\[spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$
+^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/initial1.desc b/regression/ebmc/smv/initial1.desc
@@ -1,8 +1,8 @@
 CORE
 initial1.smv
 --bound 0
-^\[main::spec1\] tmp1 = TRUE: PROVED up to bound 0$
-^\[main::spec2\] tmp2 = TRUE: REFUTED$
+^\[spec1\] tmp1 = TRUE: PROVED up to bound 0$
+^\[spec2\] tmp2 = TRUE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/smv/smv1.desc b/regression/ebmc/smv/smv1.desc
@@ -3,6 +3,6 @@ smv1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv2.desc b/regression/ebmc/smv/smv2.desc
@@ -3,6 +3,6 @@ smv2.smv
 --module main --bound 2 --k-induction
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv3.desc b/regression/ebmc/smv/smv3.desc
@@ -3,6 +3,6 @@ smv3.smv
 --module main --bound 2 --k-induction
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] .* PROVED$
+^\[spec1\] .* PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv_ltlspec1.desc b/regression/ebmc/smv/smv_ltlspec1.desc
@@ -3,6 +3,6 @@ smv_ltlspec1.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] G x != 0: PROVED$
+^\[spec1\] G x != 0: PROVED$
 --
 ^warning: ignoring
diff --git a/regression/ebmc/smv/smv_ltlspec2.desc b/regression/ebmc/smv/smv_ltlspec2.desc
@@ -3,7 +3,7 @@ smv_ltlspec2.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main::spec1\] G F x = 3: PROVED$
+^\[spec1\] G F x = 3: PROVED$
 --
 ^warning: ignoring
 --
diff --git a/regression/ebmc/smv/smv_ltlspec3.desc b/regression/ebmc/smv/smv_ltlspec3.desc
@@ -3,7 +3,7 @@ smv_ltlspec3.smv
 --bound 10 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] X X x = TRUE: REFUTED$
+^\[spec1\] X X x = TRUE: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = FALSE$
 ^x@1 = FALSE$
diff --git a/regression/ebmc/smv/smv_ltlspec4.desc b/regression/ebmc/smv/smv_ltlspec4.desc
@@ -3,12 +3,12 @@ smv_ltlspec4.smv
 --bound 10 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] F x = 0: REFUTED$
+^\[spec1\] F x = 0: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$
 ^x@2 = 2$
-^\[main::spec2\] F x = 2: PROVED up to bound 10$
+^\[spec2\] F x = 2: PROVED up to bound 10$
 --
 ^warning: ignoring
 --
diff --git a/regression/ebmc/traces/numbered1.desc b/regression/ebmc/traces/numbered1.desc
@@ -3,7 +3,7 @@ waveform1.smv
 --bound 20 --numbered-trace
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample with 21 states:$
 ^y@0 = 0$
 ^y@10 = 100$
diff --git a/regression/ebmc/traces/waveform1.desc b/regression/ebmc/traces/waveform1.desc
@@ -3,7 +3,7 @@ waveform1.smv
 --bound 20 --waveform
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] .* REFUTED$
+^\[spec1\] .* REFUTED$
 ^Counterexample:$
 ^   0  1  2  3  4  5  6  7  8  9  10  11  12  13  14  15  16  17  18  19  20$
 ^x  0  1  2  3  4  5  6  7  8  9  10  11  12  13  14  15  16  17  18  19  20$
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
