Merge pull request #1189 from diffblue/smv-next

SMV: tests for `next(...)`

Author: tautschnig

regression/smv/next/next1.desc

@@ -0,0 +1,8 @@
+CORE
+next1.smv
+--bdd
+^\[.*\] !x: PROVED$
+^\[.*\] AX x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/smv/next/next1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : boolean;
+
+INIT !x
+TRANS next(x)
+
+CTLSPEC !x
+CTLSPEC AX x

regression/smv/next/next2.desc

@@ -0,0 +1,7 @@
+CORE
+next2.smv
+--bdd
+^\[.*\] AX x <-> !x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/smv/next/next2.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x : boolean;
+
+TRANS next(x)=!x
+
+CTLSPEC (AX x) <-> !x

regression/smv/next/next3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+next3.smv
+--bdd
+^\[.*\] AX x <-> !x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The BDD engine gives the wrong answer.

regression/smv/next/next3.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x : boolean;
+
+TRANS next(!x)=x
+
+CTLSPEC (AX x) <-> !x