KNOWNBUG test for FGp

Both the BDD and BMC engines return the wrong answer for this test.

Author: kroening

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 !buechi_state: 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 3
+^\[spec1\] F G !buechi_state: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine returns the wrong answer.

regression/smv/LTL/smv_ltlspec_FG1.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)
+
+LTLSPEC F G !buechi_state