SMV: parsing for real-time CTL

Author: kroening

src/smvlang/parser.y

@@ -713,6 +713,13 @@ term       : variable_name
            | O_Token bound term       { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
            | term S_Token term        { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
            | term T_Token term        { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
+           /* Real-time CTL */
+           | EBF_Token range term     { binary($$, $2, ID_smv_EBF, $3); }
+           | ABF_Token range term     { binary($$, $2, ID_smv_ABF, $3); }
+           | EBG_Token range term     { binary($$, $2, ID_smv_EBG, $3); }
+           | ABG_Token range term     { binary($$, $2, ID_smv_ABG, $3); }
+           | A_Token '[' term BU_Token range term ']' { init($$, ID_smv_ABU); mto($$, $3); mto($$, $5); mto($$, $6); }
+           | E_Token '[' term BU_Token range term ']' { init($$, ID_smv_ABU); mto($$, $3); mto($$, $5); mto($$, $6); }
            ;
 
 bound:     '[' NUMBER_Token ',' NUMBER_Token ']'