Skip to content

Commit a106857

Browse files
kroeningtautschnig
kroening
authored and
tautschnig
committed
SMV grammar: reorder rules to match NuSMV manual
This reorders the rules for SMV terms to match the ordering in the NuSMV 2.7 manual.
1 parent bb8deda commit a106857

File tree

1 file changed

+39
-35
lines changed

1 file changed

+39
-35
lines changed

‎src/smvlang/parser.y‎

Lines changed: 39 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -675,53 +675,57 @@ define : assignment_var BECOMES_Token formula ';'
675675
formula : term
676676
;
677677

678-
term : variable_identifier
679-
| next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); }
680-
| '(' formula ')' { $$=$2; }
681-
| '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
682-
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
683-
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
684-
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
685-
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
686-
| NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
678+
constant : NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
687679
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
688680
| FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
689-
| case_Token cases esac_Token { $$=$2; }
690-
| term IF_Token term ':' term %prec IF_Token
691-
{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
692-
| switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
693-
| MINUS_Token term %prec UMINUS
694-
{ init($$, ID_unary_minus); mto($$, $2); }
695-
| term mod_Token term { binary($$, $1, ID_mod, $3); }
696-
| term GTGT_Token term { binary($$, $1, ID_shr, $3); }
697-
| term LTLT_Token term { binary($$, $1, ID_shl, $3); }
698-
| term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
699-
| term TIMES_Token term { binary($$, $1, ID_mult, $3); }
700-
| term DIVIDE_Token term { binary($$, $1, ID_div, $3); }
701-
| term PLUS_Token term { binary($$, $1, ID_plus, $3); }
702-
| term MINUS_Token term { binary($$, $1, ID_minus, $3); }
703-
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); }
704-
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
681+
;
682+
683+
term : constant
684+
| variable_identifier
685+
| '(' formula ')' { $$=$2; }
686+
| NOT_Token term { init($$, ID_not); mto($$, $2); }
687+
| term AND_Token term { j_binary($$, $1, ID_and, $3); }
688+
| term OR_Token term { j_binary($$, $1, ID_or, $3); }
705689
| term xor_Token term { j_binary($$, $1, ID_xor, $3); }
706690
| term xnor_Token term { binary($$, $1, ID_xnor, $3); }
707-
| term OR_Token term { j_binary($$, $1, ID_or, $3); }
708-
| term AND_Token term { j_binary($$, $1, ID_and, $3); }
709-
| NOT_Token term { init($$, ID_not); mto($$, $2); }
691+
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
692+
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); }
710693
| term EQUAL_Token term { binary($$, $1, ID_equal, $3); }
711694
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
712695
| term LT_Token term { binary($$, $1, ID_lt, $3); }
713696
| term LE_Token term { binary($$, $1, ID_le, $3); }
714697
| term GT_Token term { binary($$, $1, ID_gt, $3); }
715698
| term GE_Token term { binary($$, $1, ID_ge, $3); }
716-
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
717-
| term in_Token term { binary($$, $1, ID_smv_setin, $3); }
718-
| extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
719-
| resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
720-
| signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
721-
| sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
699+
| MINUS_Token term %prec UMINUS
700+
{ init($$, ID_unary_minus); mto($$, $2); }
701+
| term PLUS_Token term { binary($$, $1, ID_plus, $3); }
702+
| term MINUS_Token term { binary($$, $1, ID_minus, $3); }
703+
| term TIMES_Token term { binary($$, $1, ID_mult, $3); }
704+
| term DIVIDE_Token term { binary($$, $1, ID_div, $3); }
705+
| term mod_Token term { binary($$, $1, ID_mod, $3); }
706+
| term GTGT_Token term { binary($$, $1, ID_shr, $3); }
707+
| term LTLT_Token term { binary($$, $1, ID_shl, $3); }
708+
| term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
722709
| swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
723-
| unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
724710
| uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
711+
| signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
712+
| unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
713+
| sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
714+
| extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
715+
| resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
716+
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
717+
| '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
718+
| term in_Token term { binary($$, $1, ID_smv_setin, $3); }
719+
| term IF_Token term ':' term %prec IF_Token
720+
{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
721+
| case_Token cases esac_Token { $$=$2; }
722+
| next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); }
723+
/* Not in NuSMV manual */
724+
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
725+
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
726+
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
727+
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
728+
| switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
725729
/* CTL */
726730
| AX_Token term { init($$, ID_AX); mto($$, $2); }
727731
| AF_Token term { init($$, ID_AF); mto($$, $2); }

0 commit comments

Comments
 (0)