From e6387bf364369f8d43dd5eb6e28cacd6d3b2c2c8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 11 Jul 2025 10:28:53 -0700
Subject: [PATCH] SMV: grammar for module parameters

1.  The production rule for module parameters is renamed from
module_argument_list to module_parameters, to match the NuSMV manual.

2.  A module parameter now needs to be an identifier, as opposed to a
complex identifier, to match what NuSMV does.
---
 src/smvlang/parser.y | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 471303b12..c73f2d164 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -321,7 +321,7 @@ module_name: IDENTIFIER_Token
            ;
 
 module_head: MODULE_Token module_name { new_module($2); }
-           | MODULE_Token module_name { new_module($2); } '(' module_argument_list_opt ')'
+           | MODULE_Token module_name { new_module($2); } '(' module_parameters_opt ')'
            ;
 
 module_body: /* optional */
@@ -446,7 +446,7 @@ vardecls   : vardecl
            | vardecls vardecl
            ;
 
-module_argument: variable_identifier
+module_parameter: identifier
            {
              const irep_idt &identifier=stack_expr($1).get(ID_identifier);
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
@@ -455,12 +455,13 @@ module_argument: variable_identifier
            }
            ;
 
-module_argument_list: module_argument
-           | module_argument_list ',' module_argument
+module_parameters:
+             module_parameter
+           | module_parameters ',' module_parameter
            ;
 
-module_argument_list_opt: /* empty */
-           | module_argument_list
+module_parameters_opt: /* empty */
+           | module_parameters
            ;
 
 type_specifier: