KNOWNBUG test for FGp

regression/smv/CTL/smv_ctlspec_AFAG1.bdd.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_AFAG1.smv
+--bdd
+^\[spec1\] AF AG !buechi_state: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BDD engine returns the wrong answer.

regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_AFAG1.smv
+--bound 3
+^\[spec1\] AF AG !buechi_state: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine returns the wrong answer.

regression/smv/CTL/smv_ctlspec_AFAG1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR flag : boolean;
+VAR buechi_state : boolean;
+
+TRANS next(flag) = !flag
+
+TRANS !buechi_state & !next(buechi_state)
+    | !buechi_state & !flag & next(buechi_state)
+    | buechi_state  & flag  & next(buechi_state)
+
+CTLSPEC AF AG !buechi_state

regression/smv/LTL/smv_ltlspec_FG1.bdd.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_FG1.smv
+--bdd
+^\[spec1\] F G x!=1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BDD engine returns the wrong answer.

regression/smv/LTL/smv_ltlspec_FG1.bmc.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_FG1.smv
+--bound 2
+^\[spec1\] F G x!=1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine returns the wrong answer.

regression/smv/LTL/smv_ltlspec_FG1.smv

@@ -0,0 +1,13 @@
+MODULE main
+
+VAR x : 0..2;
+
+ASSIGN init(x) := 0;
+
+TRANS x=0 -> (next(x)=0 | next(x)=1)
+
+TRANS x=1 -> next(x)=2
+
+TRANS x=2 -> next(x)=2
+
+LTLSPEC F G x!=1