From 3cb61933692e4de5e2e68252abde3d25f30a0548 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 18 Feb 2025 10:26:33 +0000
Subject: [PATCH] SMV: rename production rules in grammar

This renames some production rules in the SMV grammar to match the NuSMV manual.
https://nusmv.fbk.eu/userman/v27/nusmv.pdf
---
 src/smvlang/parser.y | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index c6885d90..99b4aa64 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -380,7 +380,13 @@ module_argument_list_opt: /* empty */
            | module_argument_list
            ;
 
-type       : array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token type
+type_specifier:
+             simple_type_specifier
+           | module_type_specifier
+           ;
+
+simple_type_specifier:
+             array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token simple_type_specifier
            {
              init($$, ID_array);
              int start=atoi(stack_expr($2).id().c_str());
@@ -404,10 +410,10 @@ type       : array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token type
              stack_type($$).set(ID_from, stack_expr($1));
              stack_type($$).set(ID_to, stack_expr($3));
            }
-           | usertype
            ;
 
-usertype   : module_name
+module_type_specifier:
+             module_name
            {
              init($$, "submodule");
              stack_expr($$).set(ID_identifier,
@@ -441,7 +447,7 @@ enum_element: STRING_Token
            }
            ;
 
-vardecl    : variable_name ':' type ';'
+vardecl    : variable_name ':' type_specifier ';'
 {
   const irep_idt &identifier=stack_expr($1).get(ID_identifier);
   smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];