Merge pull request #608 from diffblue/CTL-AU-AR-EU-ER

SMV: parsing and type checking for CTL AR, ER, AU, EU

Author: tautschnig

regression/ebmc/BDD/AU1.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 AU1.smv
 --bdd
+^\[spec1\] x >= 1 AU x = 0: REFUTED$
+^\[spec2\] x >= 1 AU x = 10: PROVED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/BDD/AU1.smv

@@ -10,7 +10,7 @@ ASSIGN next(x) := case
   esac;
 
 -- should fail, since x=0 is not reachable
-SPEC A x>=1 U x=0
+SPEC A [x>=1 U x=0]
 
 -- should pass
-SPEC A x>=1 U x=10
+SPEC A [x>=1 U x=10]

src/smvlang/expr2smv.cpp

@@ -476,6 +476,14 @@ bool expr2smvt::convert(
     return convert_unary(
       to_unary_expr(src), dest, src.id_string() + " ", precedence = 7);
 
+  else if(
+    src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
+    src.id() == ID_ER || src.id() == ID_U || src.id() == ID_R)
+  {
+    return convert_binary(
+      to_binary_expr(src), dest, src.id_string(), precedence = 7);
+  }
+
   else if(src.id()==ID_symbol)
     return convert_symbol(to_symbol_expr(src), dest, precedence);
 

src/smvlang/parser.y

@@ -467,13 +467,13 @@ term       : variable_name
            | EX_Token  term           { init($$, ID_EX);  mto($$, $2); }
            | EF_Token  term           { init($$, ID_EF);  mto($$, $2); }
            | EG_Token  term           { init($$, ID_EG);  mto($$, $2); }
-           | A_Token  term            { init($$, ID_A);  mto($$, $2); }
-           | E_Token  term            { init($$, ID_E);  mto($$, $2); }
+           | A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5, bool_typet{}); }
+           | A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5, bool_typet{}); }
+           | E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5, bool_typet{}); }
+           | E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5, bool_typet{}); }
            | 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, stack_expr($1).type()); }
-           | term R_Token term        { binary($$, $1, ID_U, $3, stack_expr($1).type()); }
            | 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/smv_typecheck.cpp

@@ -933,11 +933,11 @@ void smv_typecheckt::typecheck(
         condition=!condition;
       }
     }
-  } 
-  else if(expr.id()==ID_AG || expr.id()==ID_AX || expr.id()==ID_AF || 
-          expr.id()==ID_EG || expr.id()==ID_EX || expr.id()==ID_EF ||
-          expr.id()==ID_A || expr.id()==ID_E || expr.id()==ID_X ||
-          expr.id()==ID_F || expr.id()==ID_G)
+  }
+  else if(
+    expr.id() == ID_AG || expr.id() == ID_AX || expr.id() == ID_AF ||
+    expr.id() == ID_EG || expr.id() == ID_EX || expr.id() == ID_EF ||
+    expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G)
   {
     if(expr.operands().size()!=1)
     {
@@ -951,7 +951,9 @@ void smv_typecheckt::typecheck(
 
     typecheck(to_unary_expr(expr).op(), expr.type(), mode);
   }
-  else if(expr.id() == ID_U || expr.id() == ID_R)
+  else if(
+    expr.id() == ID_EU || expr.id() == ID_ER || expr.id() == ID_AU ||
+    expr.id() == ID_AR || expr.id() == ID_U || expr.id() == ID_R)
   {
     auto &binary_expr = to_binary_expr(expr);
     expr.type() = bool_typet();