SMV: tests for LTL properties

regression/ebmc/smv/smv_ltlspec_F1.desc

@@ -0,0 +1,15 @@
+CORE broken-smt-backend
+smv_ltlspec_F1.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] F x = 0: REFUTED$
+^\[.*\] F x = 1: PROVED up to bound 10$
+^\[.*\] F x = 2: PROVED up to bound 10$
+^\[.*\] F x = 1 & F x = 2: PROVED up to bound 10$
+^\[.*\] F x = 0 & F x = 1: REFUTED$
+^\[.*\] F x = 0 \| F x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] F x = 0 -> FALSE: FAILURE: property not supported by BMC engine$
+^\[.*\] F x = 1 -> F x = 0: FAILURE: property not supported by BMC engine$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_F1.smv

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

regression/ebmc/smv/smv_ltlspec_F2.desc

@@ -0,0 +1,15 @@
+CORE broken-smt-backend
+smv_ltlspec_F2.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] !F x = 0: PROVED up to bound 10$
+^\[.*\] !F x = 1: REFUTED$
+^\[.*\] !F x = 2: REFUTED$
+^\[.*\] !\(F x = 1 & F x = 2\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 0 & F x = 1\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 0 \| F x = 1\): REFUTED$
+^\[.*\] !\(F x = 0 -> FALSE\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 1 -> F x = 0\): FAILURE: property not supported by BMC engine$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_F2.smv

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

regression/ebmc/smv/smv_ltlspec_G1.desc

@@ -0,0 +1,15 @@
+CORE broken-smt-backend
+smv_ltlspec_G1.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] G x != 5: PROVED up to bound 10$
+^\[.*\] G x != 6: PROVED up to bound 10$
+^\[.*\] G x != 2: REFUTED$
+^\[.*\] G x != 5 & G x != 6: PROVED up to bound 10$
+^\[.*\] G x != 2 & G x != 5: REFUTED$
+^\[.*\] G x != 5 \| G x != 2: FAILURE: property not supported by BMC engine$
+^\[.*\] G x != 2 -> FALSE: FAILURE: property not supported by BMC engine$
+^\[.*\] G x != 5 -> G x != 2: FAILURE: property not supported by BMC engine$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G1.smv

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

regression/ebmc/smv/smv_ltlspec_G2.desc

@@ -0,0 +1,15 @@
+CORE broken-smt-backend
+smv_ltlspec_G2.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] !G x != 5: REFUTED$
+^\[.*\] !G x != 6: REFUTED$
+^\[.*\] !G x != 2: PROVED up to bound 10$
+^\[.*\] !\(G x != 5 & G x != 6\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 2 & G x != 5\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 5 \| G x != 2\): REFUTED$
+^\[.*\] !\(G x != 2 -> FALSE\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 5 -> G x != 2\): FAILURE: property not supported by BMC engine$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G2.smv

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

regression/ebmc/smv/smv_ltlspec_R1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_R1.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Parsing for LTL R does not work.

regression/ebmc/smv/smv_ltlspec_R1.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 R x = 1 -- should pass
+LTLSPEC FALSE R x != 4 -- should pass
+LTLSPEC x = 2 R x = 1 -- should fail
+LTLSPEC (x >= 1 R x = 1) & (FALSE R x != 4) -- should pass
+LTLSPEC (x = 2 R x = 1) & (x >= 1 R x = 1) -- should fail
+LTLSPEC (x = 2 R x = 1) | (x >= 1 R x = 1) -- should pass

regression/ebmc/smv/smv_ltlspec_U1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_U1.smv
+--bound 10
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Parsing for LTL U does not work.

regression/ebmc/smv/smv_ltlspec_U1.smv

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