Merge pull request #475 from diffblue/CTL-engine

BDD engine: support full CTL

regression/ebmc/BDD/AF1.desc

@@ -0,0 +1,10 @@
+CORE
+AF1.smv
+--bdd
+^\[main::spec1\] AF some_var = TRUE: REFUTED$
+^\[main::spec2\] AF some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AF1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC AF some_var = 1
+
+-- should pass
+SPEC AF some_var = 0

regression/ebmc/BDD/AF2.desc

@@ -0,0 +1,10 @@
+CORE
+AF2.smv
+--bdd
+^\[main::spec1\] AF some_var = TRUE: REFUTED$
+^\[main::spec2\] AF some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AF2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN next(some_var) := 0;
+
+-- should fail
+SPEC AF some_var = 1
+
+-- should pass
+SPEC AF some_var = 0

regression/ebmc/BDD/AG1.desc

@@ -0,0 +1,10 @@
+CORE
+AG1.smv
+--bdd
+^\[main::spec1\] AG some_var = TRUE: REFUTED$
+^\[main::spec2\] AG some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AG1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC AG some_var = 1
+
+-- should pass
+SPEC AG some_var = 0

regression/ebmc/BDD/AG2.desc

@@ -0,0 +1,10 @@
+CORE
+AG2.smv
+--bdd
+^\[main::spec1\] AG some_var = TRUE: REFUTED$
+^\[main::spec2\] AG some_var = FALSE: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AG2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN next(some_var) := 0;
+
+-- should fail
+SPEC AG some_var = 1
+
+-- should fail
+SPEC AG some_var = 0

regression/ebmc/BDD/AU1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+AU1.smv
+--bdd
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AU1.smv

@@ -0,0 +1,16 @@
+MODULE main
+
+VAR x : 0..10;
+
+-- 1, 2, 3, ..., 10
+ASSIGN init(x) := 1;
+ASSIGN next(x) := case
+    x = 10 : 10;
+    1      : x + 1;
+  esac;
+
+-- should fail, since x=0 is not reachable
+SPEC A x>=1 U x=0
+
+-- should pass
+SPEC A x>=1 U x=10

regression/ebmc/BDD/AX1.desc

@@ -0,0 +1,10 @@
+CORE
+AX1.smv
+--bdd
+^\[main::spec1\] AX some_var = TRUE: REFUTED$
+^\[main::spec2\] AX some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/AX1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC AX some_var = 1
+
+-- should pass
+SPEC AX some_var = 0

regression/ebmc/BDD/EF1.desc

@@ -0,0 +1,10 @@
+CORE
+EF1.smv
+--bdd
+^\[main::spec1\] EF some_var = TRUE: REFUTED$
+^\[main::spec2\] EF some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EF1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC EF some_var = 1
+
+-- should pass
+SPEC EF some_var = 0

regression/ebmc/BDD/EF2.desc

@@ -0,0 +1,10 @@
+CORE
+EF2.smv
+--bdd
+^\[main::spec1\] EF some_var = TRUE: REFUTED$
+^\[main::spec2\] EF some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EF2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN next(some_var) := 0;
+
+-- should fail
+SPEC EF some_var = 1
+
+-- should pass
+SPEC EF some_var = 0

regression/ebmc/BDD/EG1.desc

@@ -0,0 +1,10 @@
+CORE
+EG1.smv
+--bdd
+^\[main::spec1\] EG some_var = TRUE: REFUTED$
+^\[main::spec2\] EG some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EG1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC EG some_var = 1
+
+-- should pass
+SPEC EG some_var = 0

regression/ebmc/BDD/EG2.desc

@@ -0,0 +1,10 @@
+CORE
+EG2.smv
+--bdd
+^\[main::spec1\] EG some_var = TRUE: REFUTED$
+^\[main::spec2\] EG some_var = FALSE: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EG2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN next(some_var) := 0;
+
+-- should fail
+SPEC EG some_var = 1
+
+-- should fail
+SPEC EG some_var = 0

regression/ebmc/BDD/EX1.desc

@@ -0,0 +1,10 @@
+CORE
+EX1.smv
+--bdd
+^\[main::spec1\] EX some_var = TRUE: REFUTED$
+^\[main::spec2\] EX some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EX1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = 0
+
+-- should fail
+SPEC EX some_var = 1
+
+-- should pass
+SPEC EX some_var = 0

regression/ebmc/BDD/EX2.desc

@@ -0,0 +1,10 @@
+CORE
+EX2.smv
+--bdd
+^\[main::spec1\] EX some_var = TRUE: REFUTED$
+^\[main::spec2\] EX some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/EX2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN next(some_var) := 0;
+
+-- should fail
+SPEC EX some_var = 1
+
+-- should pass
+SPEC EX some_var = 0

regression/ebmc/BDD/GF1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 GF1.smv
 --bdd
 ^\[main::spec1\] G F some_var: REFUTED$

regression/ebmc/BDD/just_p.desc

@@ -0,0 +1,10 @@
+CORE
+just_p.smv
+--bdd
+^\[main::spec1\] some_var = TRUE: REFUTED$
+^\[main::spec2\] some_var = FALSE: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/BDD/just_p.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+ASSIGN init(some_var) := 0;
+
+-- should fail
+SPEC some_var = 1
+
+-- should pass
+SPEC some_var = 0

regression/ebmc/smv/smv_ltlspec2.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 smv_ltlspec2.smv
 --bdd
 ^EXIT=0$
 ^SIGNAL=0$
-^\[smv::main::spec1\] G F x = 3: PROVED$
+^\[main::spec1\] G F x = 3: PROVED$
 --
 ^warning: ignoring
 --
-The BDD engine returns REFUTED.