From a6c12a6185014fcfe46eca6203f694f4eb7c363e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 1 Nov 2025 13:52:13 -0700 Subject: [PATCH] SMV grammar: rename term -> basic_expr This renames the nonterminal "term" to "basic_expr" in the SMV grammar, to match the NuSMV manual. --- src/smvlang/parser.y | 173 +++++++++++++++++++++---------------------- 1 file changed, 86 insertions(+), 87 deletions(-) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index d09130e67..fa1265e31 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -810,7 +810,7 @@ define : assignment_var BECOMES_Token formula ';' } ; -formula : term +formula : basic_expr ; constant : NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); } @@ -818,92 +818,91 @@ constant : NUMBER_Token { init($$, ID_constant); stack_expr($$).se | FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); } ; -term : constant +basic_expr : constant | variable_identifier - | '(' formula ')' { $$=$2; } - | NOT_Token term { init($$, ID_not); mto($$, $2); } - | "abs" '(' term ')' { unary($$, ID_smv_abs, $3); } - | "max" '(' term ',' term ')' { binary($$, $3, ID_smv_max, $5); } - | "min" '(' term ',' term ')' { binary($$, $3, ID_smv_min, $5); } - | term AND_Token term { j_binary($$, $1, ID_and, $3); } - | term OR_Token term { j_binary($$, $1, ID_or, $3); } - | term xor_Token term { j_binary($$, $1, ID_xor, $3); } - | term xnor_Token term { binary($$, $1, ID_xnor, $3); } - | term IMPLIES_Token term { binary($$, $1, ID_implies, $3); } - | term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); } - | term EQUAL_Token term { binary($$, $1, ID_equal, $3); } - | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); } - | term LT_Token term { binary($$, $1, ID_lt, $3); } - | term LE_Token term { binary($$, $1, ID_le, $3); } - | term GT_Token term { binary($$, $1, ID_gt, $3); } - | term GE_Token term { binary($$, $1, ID_ge, $3); } - | MINUS_Token term %prec UMINUS - { init($$, ID_unary_minus); mto($$, $2); } - | term PLUS_Token term { binary($$, $1, ID_plus, $3); } - | term MINUS_Token term { binary($$, $1, ID_minus, $3); } - | term TIMES_Token term { binary($$, $1, ID_mult, $3); } - | term DIVIDE_Token term { binary($$, $1, ID_div, $3); } - | term mod_Token term { binary($$, $1, ID_mod, $3); } - | term GTGT_Token term { binary($$, $1, ID_shr, $3); } - | term LTLT_Token term { binary($$, $1, ID_shl, $3); } - | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); } - | "word1" '(' term ')' { unary($$, ID_smv_word1, $3); } - | "bool" '(' term ')' { unary($$, ID_smv_bool, $3); } - | "toint" '(' term ')' { unary($$, ID_smv_toint, $3); } - | "count" '(' term_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); } - | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); } - | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); } - | signed_Token '(' term ')' { unary($$, ID_smv_signed_cast, $3); } - | unsigned_Token '(' term ')' { unary($$, ID_smv_unsigned_cast, $3); } - | sizeof_Token '(' term ')' { unary($$, ID_smv_sizeof, $3); } - | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); } - | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); } - | term union_Token term { binary($$, $1, ID_smv_union, $3); } - | '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); } - | term in_Token term { binary($$, $1, ID_smv_setin, $3); } - | term IF_Token term ':' term %prec IF_Token - { init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); } - | case_Token cases esac_Token { $$=$2; } - | next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); } + | '(' formula ')' { $$=$2; } + | NOT_Token basic_expr { init($$, ID_not); mto($$, $2); } + | "abs" '(' basic_expr ')' { unary($$, ID_smv_abs, $3); } + | "max" '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_max, $5); } + | "min" '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_min, $5); } + | basic_expr AND_Token basic_expr { j_binary($$, $1, ID_and, $3); } + | basic_expr OR_Token basic_expr { j_binary($$, $1, ID_or, $3); } + | basic_expr xor_Token basic_expr { j_binary($$, $1, ID_xor, $3); } + | basic_expr xnor_Token basic_expr { binary($$, $1, ID_xnor, $3); } + | basic_expr IMPLIES_Token basic_expr { binary($$, $1, ID_implies, $3); } + | basic_expr EQUIV_Token basic_expr { binary($$, $1, ID_smv_iff, $3); } + | basic_expr EQUAL_Token basic_expr { binary($$, $1, ID_equal, $3); } + | basic_expr NOTEQUAL_Token basic_expr { binary($$, $1, ID_notequal, $3); } + | basic_expr LT_Token basic_expr { binary($$, $1, ID_lt, $3); } + | basic_expr LE_Token basic_expr { binary($$, $1, ID_le, $3); } + | basic_expr GT_Token basic_expr { binary($$, $1, ID_gt, $3); } + | basic_expr GE_Token basic_expr { binary($$, $1, ID_ge, $3); } + | MINUS_Token basic_expr %prec UMINUS { init($$, ID_unary_minus); mto($$, $2); } + | basic_expr PLUS_Token basic_expr { binary($$, $1, ID_plus, $3); } + | basic_expr MINUS_Token basic_expr { binary($$, $1, ID_minus, $3); } + | basic_expr TIMES_Token basic_expr { binary($$, $1, ID_mult, $3); } + | basic_expr DIVIDE_Token basic_expr { binary($$, $1, ID_div, $3); } + | basic_expr mod_Token basic_expr { binary($$, $1, ID_mod, $3); } + | basic_expr GTGT_Token basic_expr { binary($$, $1, ID_shr, $3); } + | basic_expr LTLT_Token basic_expr { binary($$, $1, ID_shl, $3); } + | basic_expr COLONCOLON_Token basic_expr { binary($$, $1, ID_concatenation, $3); } + | "word1" '(' basic_expr ')' { unary($$, ID_smv_word1, $3); } + | "bool" '(' basic_expr ')' { unary($$, ID_smv_bool, $3); } + | "toint" '(' basic_expr ')' { unary($$, ID_smv_toint, $3); } + | "count" '(' basic_expr_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); } + | swconst_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_swconst, $5); } + | uwconst_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_uwconst, $5); } + | signed_Token '(' basic_expr ')' { unary($$, ID_smv_signed_cast, $3); } + | unsigned_Token '(' basic_expr ')' { unary($$, ID_smv_unsigned_cast, $3); } + | sizeof_Token '(' basic_expr ')' { unary($$, ID_smv_sizeof, $3); } + | extend_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_extend, $5); } + | resize_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_resize, $5); } + | basic_expr union_Token basic_expr { binary($$, $1, ID_smv_union, $3); } + | '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); } + | basic_expr in_Token basic_expr { binary($$, $1, ID_smv_setin, $3); } + | basic_expr IF_Token basic_expr ':' basic_expr %prec IF_Token + { init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); } + | case_Token cases esac_Token { $$=$2; } + | next_Token '(' basic_expr ')' { init($$, ID_smv_next); mto($$, $3); } /* Not in NuSMV manual */ - | INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); } - | DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); } - | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); } - | SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); } + | INC_Token '(' basic_expr ')' { init($$, "inc"); mto($$, $3); } + | DEC_Token '(' basic_expr ')' { init($$, "dec"); mto($$, $3); } + | ADD_Token '(' basic_expr ',' basic_expr ')' { j_binary($$, $3, ID_plus, $5); } + | SUB_Token '(' basic_expr ',' basic_expr ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); } | switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); } /* CTL */ - | AX_Token term { init($$, ID_AX); mto($$, $2); } - | AF_Token term { init($$, ID_AF); mto($$, $2); } - | AG_Token term { init($$, ID_AG); mto($$, $2); } - | 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 U_Token term ']' { binary($$, $3, ID_AU, $5); } - | A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); } - | E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); } - | E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); } + | AX_Token basic_expr { init($$, ID_AX); mto($$, $2); } + | AF_Token basic_expr { init($$, ID_AF); mto($$, $2); } + | AG_Token basic_expr { init($$, ID_AG); mto($$, $2); } + | EX_Token basic_expr { init($$, ID_EX); mto($$, $2); } + | EF_Token basic_expr { init($$, ID_EF); mto($$, $2); } + | EG_Token basic_expr { init($$, ID_EG); mto($$, $2); } + | A_Token '[' basic_expr U_Token basic_expr ']' { binary($$, $3, ID_AU, $5); } + | A_Token '[' basic_expr R_Token basic_expr ']' { binary($$, $3, ID_AR, $5); } + | E_Token '[' basic_expr U_Token basic_expr ']' { binary($$, $3, ID_EU, $5); } + | E_Token '[' basic_expr R_Token basic_expr ']' { binary($$, $3, ID_ER, $5); } /* LTL */ - | 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); } - | term R_Token term { binary($$, $1, ID_R, $3); } - | term V_Token term { binary($$, $1, ID_R, $3); } + | F_Token basic_expr { init($$, ID_F); mto($$, $2); } + | G_Token basic_expr { init($$, ID_G); mto($$, $2); } + | X_Token basic_expr { init($$, ID_X); mto($$, $2); } + | basic_expr U_Token basic_expr { binary($$, $1, ID_U, $3); } + | basic_expr R_Token basic_expr { binary($$, $1, ID_R, $3); } + | basic_expr V_Token basic_expr { binary($$, $1, ID_R, $3); } /* LTL PAST */ - | Y_Token term { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); } - | Z_Token term { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); } - | H_Token term { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); } - | H_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); } - | O_Token term { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); } - | 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); } + | Y_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); } + | Z_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); } + | H_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); } + | H_Token bound basic_expr { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); } + | O_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); } + | O_Token bound basic_expr { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); } + | basic_expr S_Token basic_expr { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); } + | basic_expr T_Token basic_expr { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); } /* Real-time CTL */ - | EBF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } - | ABF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } - | EBG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } - | ABG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } - | A_Token '[' term BU_Token range term ']' + | EBF_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_EBF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } + | ABF_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_ABF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } + | EBG_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_EBG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } + | ABG_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_ABG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); } + | A_Token '[' basic_expr BU_Token range basic_expr ']' { $$ = $1; stack_expr($$).id(ID_smv_ABU); @@ -912,7 +911,7 @@ term : constant stack_expr($$).add_to_operands(stack_expr($5).operands()[1]); mto($$, $6); } - | E_Token '[' term BU_Token range term ']' + | E_Token '[' basic_expr BU_Token range basic_expr ']' { $$ = $1; stack_expr($$).id(ID_smv_EBU); @@ -936,9 +935,9 @@ set_body_expr: | set_body_expr ',' formula { $$=$1; mto($$, $3); } ; -term_list: - term { init($$); mto($$, $1); } - | term_list ',' term { $$=$1; mto($$, $3); } +basic_expr_list: + basic_expr { init($$); mto($$, $1); } + | basic_expr_list ',' basic_expr { $$=$1; mto($$, $3); } ; identifier : IDENTIFIER_Token @@ -985,11 +984,11 @@ complex_identifier: unary($$, ID_member, $1); stack_expr($$).set(ID_component_name, stack_expr($3).id()); } - | complex_identifier '[' term ']' + | complex_identifier '[' basic_expr ']' { binary($$, $1, ID_index, $3); } - | complex_identifier '(' term ')' + | complex_identifier '(' basic_expr ')' { // Not in the NuSMV grammar. binary($$, $1, ID_index, $3); @@ -1012,7 +1011,7 @@ switches : { $$=$1; mto($$, $2); } ; -switch : NUMBER_Token ':' term ';' +switch : NUMBER_Token ':' basic_expr ';' { init($$, ID_switch); mto($$, $1); mto($$, $3); } ;