Skip to content

Commit 097a07a

Browse files
kroeningkroening
committed
SMV: tests for LTL properties
1 parent 35e5313 commit 097a07a

12 files changed

+199
-0
lines changed

‎regression/ebmc/smv/smv_ltlspec_F1.desc‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE broken-smt-backend
2+
smv_ltlspec_F1.smv
3+
--bound 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[.*\] F x = 0: REFUTED$
7+
^\[.*\] F x = 1: PROVED up to bound 10$
8+
^\[.*\] F x = 2: PROVED up to bound 10$
9+
^\[.*\] F x = 1 & F x = 2: PROVED up to bound 10$
10+
^\[.*\] F x = 0 & F x = 1: REFUTED$
11+
^\[.*\] F x = 0 \| F x = 1: FAILURE: property not supported by BMC engine$
12+
^\[.*\] F x = 0 -> FALSE: FAILURE: property not supported by BMC engine$
13+
^\[.*\] F x = 1 -> F x = 0: FAILURE: property not supported by BMC engine$
14+
--
15+
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec_F1.smv‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MODULE main
2+
3+
VAR x : 0..3;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC F x = 0 -- should fail
15+
LTLSPEC F x = 1 -- should pass
16+
LTLSPEC F x = 2 -- should pass
17+
LTLSPEC F x = 1 & F x = 2 -- should pass
18+
LTLSPEC F x = 0 & F x = 1 -- should fail
19+
LTLSPEC F x = 0 | F x = 1 -- should pass
20+
LTLSPEC F x = 0 -> FALSE -- should pass
21+
LTLSPEC F x = 1 -> F x = 0 -- should fail

‎regression/ebmc/smv/smv_ltlspec_F2.desc‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE broken-smt-backend
2+
smv_ltlspec_F2.smv
3+
--bound 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[.*\] !F x = 0: PROVED up to bound 10$
7+
^\[.*\] !F x = 1: REFUTED$
8+
^\[.*\] !F x = 2: REFUTED$
9+
^\[.*\] !\(F x = 1 & F x = 2\): FAILURE: property not supported by BMC engine$
10+
^\[.*\] !\(F x = 0 & F x = 1\): FAILURE: property not supported by BMC engine$
11+
^\[.*\] !\(F x = 0 \| F x = 1\): REFUTED$
12+
^\[.*\] !\(F x = 0 -> FALSE\): FAILURE: property not supported by BMC engine$
13+
^\[.*\] !\(F x = 1 -> F x = 0\): FAILURE: property not supported by BMC engine$
14+
--
15+
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec_F2.smv‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MODULE main
2+
3+
VAR x : 0..3;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC ! F x = 0 -- should pass
15+
LTLSPEC ! F x = 1 -- should fail
16+
LTLSPEC ! F x = 2 -- should fail
17+
LTLSPEC ! (F x = 1 & F x = 2) -- should fail
18+
LTLSPEC ! (F x = 0 & F x = 1) -- should pass
19+
LTLSPEC ! (F x = 0 | F x = 1) -- should fail
20+
LTLSPEC ! (F x = 0 -> FALSE) -- should fail
21+
LTLSPEC ! (F x = 1 -> F x = 0) -- should pass

‎regression/ebmc/smv/smv_ltlspec_G1.desc‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE broken-smt-backend
2+
smv_ltlspec_G1.smv
3+
--bound 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[.*\] G x != 5: PROVED up to bound 10$
7+
^\[.*\] G x != 6: PROVED up to bound 10$
8+
^\[.*\] G x != 2: REFUTED$
9+
^\[.*\] G x != 5 & G x != 6: PROVED up to bound 10$
10+
^\[.*\] G x != 2 & G x != 5: REFUTED$
11+
^\[.*\] G x != 5 \| G x != 2: FAILURE: property not supported by BMC engine$
12+
^\[.*\] G x != 2 -> FALSE: FAILURE: property not supported by BMC engine$
13+
^\[.*\] G x != 5 -> G x != 2: FAILURE: property not supported by BMC engine$
14+
--
15+
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec_G1.smv‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MODULE main
2+
3+
VAR x : 0..10;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x>=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC G x != 5 -- should pass
15+
LTLSPEC G x != 6 -- should pass
16+
LTLSPEC G x != 2 -- should fail
17+
LTLSPEC G x != 5 & G x != 6 -- should pass
18+
LTLSPEC G x != 2 & G x != 5 -- should fail
19+
LTLSPEC G x != 5 | G x != 2 -- should pass
20+
LTLSPEC G x != 2 -> FALSE -- should pass
21+
LTLSPEC G x != 5 -> G x != 2 -- should fail

‎regression/ebmc/smv/smv_ltlspec_G2.desc‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE broken-smt-backend
2+
smv_ltlspec_G2.smv
3+
--bound 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[.*\] !G x != 5: REFUTED$
7+
^\[.*\] !G x != 6: REFUTED$
8+
^\[.*\] !G x != 2: PROVED up to bound 10$
9+
^\[.*\] !\(G x != 5 & G x != 6\): FAILURE: property not supported by BMC engine$
10+
^\[.*\] !\(G x != 2 & G x != 5\): FAILURE: property not supported by BMC engine$
11+
^\[.*\] !\(G x != 5 \| G x != 2\): REFUTED$
12+
^\[.*\] !\(G x != 2 -> FALSE\): FAILURE: property not supported by BMC engine$
13+
^\[.*\] !\(G x != 5 -> G x != 2\): FAILURE: property not supported by BMC engine$
14+
--
15+
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec_G2.smv‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MODULE main
2+
3+
VAR x : 0..10;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x>=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC ! G x != 5 -- should pass
15+
LTLSPEC ! G x != 6 -- should pass
16+
LTLSPEC ! G x != 2 -- should fail
17+
LTLSPEC ! (G x != 5 & G x != 6) -- should pass
18+
LTLSPEC ! (G x != 2 & G x != 5) -- should fail
19+
LTLSPEC ! (G x != 5 | G x != 2) -- should pass
20+
LTLSPEC ! (G x != 2 -> FALSE) -- should pass
21+
LTLSPEC ! (G x != 5 -> G x != 2) -- should fail

‎regression/ebmc/smv/smv_ltlspec_R1.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG broken-smt-backend
2+
smv_ltlspec_R1.smv
3+
--bound 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Parsing for LTL R does not work.

‎regression/ebmc/smv/smv_ltlspec_R1.smv‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
MODULE main
2+
3+
VAR x : 0..10;
4+
5+
ASSIGN
6+
init(x) := 1;
7+
8+
next(x) :=
9+
case
10+
x>=3 : 3;
11+
TRUE: x+1;
12+
esac;
13+
14+
LTLSPEC x >= 1 R x = 1 -- should pass
15+
LTLSPEC FALSE R x != 4 -- should pass
16+
LTLSPEC x = 2 R x = 1 -- should fail
17+
LTLSPEC (x >= 1 R x = 1) & (FALSE R x != 4) -- should pass
18+
LTLSPEC (x = 2 R x = 1) & (x >= 1 R x = 1) -- should fail
19+
LTLSPEC (x = 2 R x = 1) | (x >= 1 R x = 1) -- should pass

0 commit comments

Comments
 (0)