Merge pull request #986 from diffblue/smv-enum-tests

SMV: add tests for enums

Author: tautschnig

regression/smv/enums/enum1.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+enum1.smv
+
+^\[.*\] AG some_var != off: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/enums/enum1.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR some_var: { red, green, yellow, off };
+
+ASSIGN next(some_var) :=
+  case
+    some_var=red: green;
+    some_var=green: yellow;
+    some_var=yellow: red;
+    TRUE: off;
+  esac;
+
+INIT some_var != off
+
+SPEC AG some_var != off

regression/smv/enums/enum2.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+enum2.smv
+
+^\[.*\] AG x != y: PROVED up to bound \d+$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/enums/enum2.smv

@@ -0,0 +1,18 @@
+MODULE main
+
+VAR x: { red, green, yellow };
+VAR y: { red, green, yellow };
+
+ASSIGN init(y) := green;
+ASSIGN next(y) := x;
+
+ASSIGN next(x) :=
+  case
+    x=red: green;
+    x=green: yellow;
+    x=yellow: red;
+  esac;
+
+ASSIGN init(x) := red;
+
+SPEC AG x != y;

regression/smv/enums/enum3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+enum3.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This should be a type error.

regression/smv/enums/enum3.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x: { a, b, c };
+VAR y: { a, b };
+
+ASSIGN init(x) := c; -- ok
+ASSIGN init(y) := c; -- error

regression/smv/enums/enum4.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+enum4.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails in the decision procedure.

regression/smv/enums/enum4.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x: { a, b, c };
+VAR y: { a, b };
+
+-- ok; it's a subset
+ASSIGN x := y; 
+
+SPEC AG x = y

regression/smv/enums/enum5.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+enum5.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails in the decision procedure.

regression/smv/enums/enum5.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x: { a, b };
+VAR y: { b, a };
+
+-- ok; the ordering does not matter
+ASSIGN x := y; 
+
+SPEC AG x = y