SMV: the LTL release operator is "V"

NuSMV's LTL release operator is "V", not "R".

Author: kroening

CHANGELOG

@@ -2,6 +2,7 @@
 
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
+* SMV: LTL V operator
 
 # EBMC 5.5
 

regression/smv/LTL/smv_ltlspec_R1.desc

@@ -1,12 +1,12 @@
 CORE
 smv_ltlspec_R1.smv
 --bound 10
-^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
-^\[.*\] FALSE R x != 4: PROVED up to bound 10$
-^\[.*\] x = 2 R x = 1: REFUTED$
-^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: PROVED up to bound 10$
-^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$
-^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$
+^\[.*\] x >= 1 V x = 1: PROVED up to bound 10$
+^\[.*\] FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1: REFUTED$
+^\[.*\] x >= 1 V x = 1 & FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1 & x >= 1 V x = 1: REFUTED$
+^\[.*\] x = 2 V x = 1 \| x >= 1 V x = 1: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/smv/LTL/smv_ltlspec_R2.desc

@@ -1,7 +1,7 @@
 KNOWNBUG broken-smt-backend
 smv_ltlspec_R2.smv
 --bound 10
-^\[.*\] FALSE R x != 3: REFUTED$
+^\[.*\] FALSE V x != 3: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$

regression/smv/LTL/smv_ltlspec_R3.desc

@@ -1,7 +1,7 @@
 CORE
 smv_ltlspec_R3.smv
 --bound 1
-^\[.*\] FALSE R x != 3: PROVED up to bound 1$
+^\[.*\] FALSE V x != 3: PROVED up to bound 1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/LTL/smv_ltlspec_R4.desc

@@ -1,7 +1,7 @@
 CORE
 smv_ltlspec_R4.smv
 --bound 10
-^\[.*\] FALSE R x != 0: PROVED up to bound 10$
+^\[.*\] FALSE V x != 0: PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/LTL/smv_ltlspec_V1.desc

@@ -0,0 +1,14 @@
+CORE
+smv_ltlspec_V1.smv
+--bound 10
+^\[.*\] x >= 1 V x = 1: PROVED up to bound 10$
+^\[.*\] FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1: REFUTED$
+^\[.*\] x >= 1 V x = 1 & FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1 & x >= 1 V x = 1: REFUTED$
+^\[.*\] x = 2 V x = 1 \| x >= 1 V x = 1: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/LTL/smv_ltlspec_V1.smv

@@ -0,0 +1,19 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC x >= 1 V x = 1 -- should pass
+LTLSPEC FALSE V x != 4 -- should pass
+LTLSPEC x = 2 V x = 1 -- should fail
+LTLSPEC (x >= 1 V x = 1) & (FALSE V x != 4) -- should pass
+LTLSPEC (x = 2 V x = 1) & (x >= 1 V x = 1) -- should fail
+LTLSPEC (x = 2 V x = 1) | (x >= 1 V x = 1) -- should pass

regression/smv/LTL/smv_ltlspec_V2.desc

@@ -0,0 +1,14 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_V2.smv
+--bound 10
+^\[.*\] FALSE V x != 3: REFUTED$
+^Counterexample with 3 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The trace has too many states.

regression/smv/LTL/smv_ltlspec_V2.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+LTLSPEC FALSE V x != 3

regression/smv/LTL/smv_ltlspec_V3.desc

@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_V3.smv
+--bound 1
+^\[.*\] FALSE V x != 3: PROVED up to bound 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--