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

regression/smv/enums/enum6.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+enum6.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This crashes when generating the trace.

regression/smv/enums/enum6.smv

@@ -0,0 +1,13 @@
+MODULE main
+
+VAR x: { a, b, c };
+
+ASSIGN init(x) := a;
+ASSIGN next(x) := case
+                    x=a: b;
+                    x=b: c;
+                    TRUE: c;
+                  esac;
+
+-- fails
+SPEC AG x != c

regression/smv/enums/enum7.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+enum7.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The literal is converted incorrectly.

regression/smv/enums/enum7.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x: { a, b, c };
+
+DEFINE x_value := a;
+
+ASSIGN x := x_value;
+
+SPEC AG x = a

regression/smv/modules/module_with_enum1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+module_with_enum1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The enum literal is not found.

regression/smv/modules/module_with_enum1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR sub : my-module;
+
+-- the enum is visible here as well
+SPEC AG sub.some_enum = a
+
+MODULE my-module
+
+VAR some_enum : { a, b };
+
+ASSIGN some_enum := a;