Merge pull request #1003 from diffblue/SMV-V

SMV: the LTL release operator is "V"

Author: tautschnig

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
+--

regression/smv/LTL/smv_ltlspec_V3.smv

@@ -0,0 +1,16 @@
+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
+-- hence no trace with k=1
+LTLSPEC FALSE V x != 3

regression/smv/LTL/smv_ltlspec_V4.desc

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

regression/smv/LTL/smv_ltlspec_V4.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;
+
+-- should pass
+LTLSPEC FALSE V x != 0

src/smvlang/expr2smv.cpp

@@ -566,7 +566,7 @@ bool expr2smvt::convert(
 
   else if(
     src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
-    src.id() == ID_ER || src.id() == ID_U || src.id() == ID_R)
+    src.id() == ID_ER || src.id() == ID_U)
   {
     return convert_binary(
       to_binary_expr(src),
@@ -575,6 +575,13 @@ bool expr2smvt::convert(
       precedence = precedencet::TEMPORAL);
   }
 
+  else if(src.id() == ID_R)
+  {
+    // LTL release is "V" in NuSMV
+    return convert_binary(
+      to_binary_expr(src), dest, "V", precedence = precedencet::TEMPORAL);
+  }
+
   else if(src.id() == ID_if)
     return convert_if(to_if_expr(src), dest, precedencet::IF);
 

src/smvlang/parser.y

@@ -284,7 +284,7 @@ static void new_module(YYSTYPE &module)
 %left  OR_Token
 %left  AND_Token
 %left  NOT_Token
-%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token F_Token G_Token X_Token
+%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token X_Token
 %left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
 %left  union_Token
 %left  IN_Token NOTIN_Token
@@ -694,6 +694,7 @@ term       : variable_name
            | X_Token  term            { init($$, ID_X);  mto($$, $2); }
            | term U_Token term        { binary($$, $1, ID_U, $3); }
            | term R_Token term        { binary($$, $1, ID_R, $3); }
+           | term V_Token term        { binary($$, $1, ID_R, $3); }
            | term EQUAL_Token    term { binary($$, $1, ID_equal, $3); }
            | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
            | term LT_Token       term { binary($$, $1, ID_lt, $3); }