Skip to content

Commit 9dd3385

Browse files
committed
SMV: split up and rename formula_list
This splits up and renames the formula_list production rule, to match the NuSMV manual.
1 parent 81c1bbb commit 9dd3385

File tree

1 file changed

+9
-4
lines changed

1 file changed

+9
-4
lines changed

src/smvlang/parser.y

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -510,7 +510,7 @@ module_type_specifier:
510510
stack_expr($$).set(ID_identifier,
511511
smv_module_symbol(stack_expr($1).id_string()));
512512
}
513-
| module_name '(' formula_list ')'
513+
| module_name '(' parameter_list ')'
514514
{
515515
init($$, "submodule");
516516
stack_expr($$).set(ID_identifier,
@@ -519,6 +519,11 @@ module_type_specifier:
519519
}
520520
;
521521

522+
parameter_list:
523+
formula { init($$); mto($$, $1); }
524+
| parameter_list ',' formula { $$=$1; mto($$, $3); }
525+
;
526+
522527
enum_list : enum_element
523528
{
524529
init($$, ID_enumeration);
@@ -672,7 +677,7 @@ formula : term
672677
term : variable_identifier
673678
| next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); }
674679
| '(' formula ')' { $$=$2; }
675-
| '{' formula_list '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
680+
| '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
676681
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
677682
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
678683
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
@@ -776,9 +781,9 @@ range : NUMBER_Token DOTDOT_Token NUMBER_Token
776781
{ init($$); mto($$, $1); mto($$, $3); }
777782
;
778783

779-
formula_list:
784+
set_body_expr:
780785
formula { init($$); mto($$, $1); }
781-
| formula_list ',' formula { $$=$1; mto($$, $3); }
786+
| set_body_expr ',' formula { $$=$1; mto($$, $3); }
782787
;
783788

784789
identifier : IDENTIFIER_Token

0 commit comments

Comments
 (0)