Skip to content

SMV grammar: rename term -> basic_expr #1378

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 2, 2025
+86 −87
Merged

SMV grammar: rename term -> basic_expr #1378

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
173 changes: 86 additions & 87 deletions src/smvlang/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -810,100 +810,99 @@ 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(); }
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
| 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);
Expand All @@ -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);
Expand All @@ -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
Expand Down Expand Up @@ -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);
Expand All @@ -1012,7 +1011,7 @@ switches :
{ $$=$1; mto($$, $2); }
;

switch : NUMBER_Token ':' term ';'
switch : NUMBER_Token ':' basic_expr ';'
{ init($$, ID_switch); mto($$, $1); mto($$, $3); }
;

Expand Down
Loading