Merge pull request #702 from diffblue/smv-U-R

SMV: parse LTL U and R

Author: tautschnig

regression/ebmc/smv/smv_ltlspec_R1.desc

@@ -1,9 +1,14 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_ltlspec_R1.smv
 --bound 10
+^\[.*\] x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] FALSE R x != 4: FAILURE: property not supported by BMC engine$
+^\[.*\] x = 2 R x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: FAILURE: property not supported by BMC engine$
+^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Parsing for LTL R does not work.

regression/ebmc/smv/smv_ltlspec_U1.desc

@@ -1,9 +1,13 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_ltlspec_U1.smv
 --bound 10
+\[.*\] x = 1 U x = 2: FAILURE: property not supported by BMC engine$
+\[.*\] x != 0 U FALSE: FAILURE: property not supported by BMC engine$
+\[.*\] x = 1 U x = 3: FAILURE: property not supported by BMC engine$
+\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: FAILURE: property not supported by BMC engine$
+\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Parsing for LTL U does not work.

src/smvlang/parser.y

@@ -474,6 +474,8 @@ term       : variable_name
            | F_Token  term            { init($$, ID_F);  mto($$, $2); }
            | G_Token  term            { init($$, ID_G);  mto($$, $2); }
            | X_Token  term            { init($$, ID_X);  mto($$, $2); }
+           | term U_Token term        { binary($$, $1, ID_U, $3, bool_typet{}); }
+           | term R_Token term        { binary($$, $1, ID_R, $3, bool_typet{}); }
            | term EQUAL_Token    term { binary($$, $1, ID_equal,  $3, bool_typet{}); }
            | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3, bool_typet{}); }
            | term LT_Token       term { binary($$, $1, ID_lt,  $3, bool_typet{}); }

src/smvlang/scanner.l

@@ -92,6 +92,7 @@ void newlocation(YYSTYPE &x)
 "X"		return X_Token;
 "G"		return G_Token;
 "U"		return U_Token;
+"R"		return R_Token;
 "next"		return NEXT_Token;
 "init"		return init_Token;
 "case"		return CASE_Token;