SMV: grammar for missing declarations

regression/smv/compute/compute1.desc

@@ -0,0 +1,8 @@
+CORE
+compute1.smv
+
+^file .* line 3: No support for COMPUTE specifications .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/compute/compute1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+COMPUTE MIN [TRUE, TRUE];

regression/smv/constants/constants1.desc

@@ -0,0 +1,8 @@
+CORE
+constants1.smv
+
+^file .* line 3: No support for CONSTANTS declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/constants/constants1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+CONSTANTS some_constant;

regression/smv/frozenvar/frozenvar1.desc

@@ -0,0 +1,8 @@
+CORE
+frozenvar1.smv
+
+^file .* line 3: No support for FROZENVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/frozenvar/frozenvar1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+FROZENVAR some_var : boolean;

regression/smv/isa/isa1.desc

@@ -0,0 +1,8 @@
+CORE
+isa1.smv
+
+^file .* line 3: No support for ISA declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/isa/isa1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+ISA some_isa

regression/smv/ivar/ivar1.desc

@@ -0,0 +1,8 @@
+CORE
+ivar1.smv
+
+^file .* line 3: No support for IVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--

regression/smv/ivar/ivar1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+IVAR some_input : boolean;

src/smvlang/parser.y

@@ -369,14 +369,20 @@ semi_opt   :    /* empty */
 
 module_element:
              var_declaration
+           | ivar_declaration
+           | frozenvar_declaration
            | define_declaration
+           | constants_declaration
            | assign_constraint
            | trans_constraint
            | init_constraint
            | invar_constraint
            | fairness_constraint
            | ctl_specification
            | ltl_specification
+           | compute_specification
+           | isa_declaration
+           /* not in the NuSMV manual */
            | EXTERN_Token extern_var semi_opt
            | EXTERN_Token
            ;
@@ -386,11 +392,78 @@ var_declaration:
            | VAR_Token
            ;
 
+ivar_declaration:
+             IVAR_Token simple_var_list
+           {
+             yyerror("No support for IVAR declarations");
+             YYERROR;
+           }
+           ;
+
+frozenvar_declaration:
+             FROZENVAR_Token simple_var_list
+           {
+             yyerror("No support for FROZENVAR declarations");
+             YYERROR;
+           }
+           ;
+
+simple_var_list:
+             identifier ':' simple_type_specifier ';'
+           | simple_var_list identifier ':' simple_type_specifier ';'
+
 define_declaration:
              DEFINE_Token defines
            | DEFINE_Token
            ;
 
+constants_declaration:
+             CONSTANTS_Token constants_body ';'
+           {
+             yyerror("No support for CONSTANTS declarations");
+             YYERROR;
+           }
+           ;
+
+constants_body:
+             complex_identifier
+           | constants_body ',' complex_identifier
+           ;
+
+compute_specification:
+             COMPUTE_Token compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           ;
+
+compute_expr:
+           ;
+
+isa_declaration:
+             ISA_Token identifier
+           {
+             yyerror("No support for ISA declarations");
+             YYERROR;
+           }
+           ;
+
 assign_constraint:
              ASSIGN_Token assignments
            | ASSIGN_Token