SMV: rewrite assignment grammar rules

This rewrites the SMV grammar for assignments and define to match the NuSMV
2.7 manual.

Author: kroening

src/smvlang/parser.y

@@ -648,36 +648,27 @@ assignments: assignment
            | assignments assignment
            ;
 
-assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
+assignment : init_Token '(' complex_identifier ')' BECOMES_Token simple_expr ';'
            {
-             if(stack_expr($1).id()==ID_smv_next)
-             {
-               PARSER.module->add_assign_next(
-                 unary_exprt{ID_smv_next, std::move(stack_expr($3))},
-                 std::move(stack_expr($6)));
-             }
-             else
-               PARSER.module->add_assign_init(std::move(stack_expr($3)), std::move(stack_expr($6)));
+             PARSER.module->add_assign_init(std::move(stack_expr($3)), std::move(stack_expr($6)));
            }
-           | assignment_var BECOMES_Token formula ';'
+           | next_Token '(' complex_identifier ')' BECOMES_Token next_expr ';'
+           {
+             PARSER.module->add_assign_next(
+               unary_exprt{ID_smv_next, std::move(stack_expr($3))},
+               std::move(stack_expr($6)));
+           }
+           | complex_identifier BECOMES_Token formula ';'
            {
              PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
 
-assignment_var: variable_identifier
-           ;
-
-assignment_head:
-             init_Token { init($$, ID_init); }
-           | next_Token { init($$, ID_smv_next); }
-           ;
-
 defines:     define
            | defines define
            ;
 
-define     : assignment_var BECOMES_Token formula ';'
+define     : complex_identifier BECOMES_Token formula ';'
            {
              PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
@@ -724,6 +715,12 @@ word_constant:
            }
            ;
 
+next_expr  : basic_expr
+           ;
+
+simple_expr: basic_expr
+           ;
+
 basic_expr : constant
            | identifier
            {
@@ -738,7 +735,7 @@ basic_expr : constant
              unary($$, ID_member, $1);
              stack_expr($$).set(ID_component_name, stack_expr($3).id());
            }
-           | basic_expr '(' basic_expr ')'
+           | basic_expr '(' simple_expr ')'
            {
              // Not in the NuSMV grammar.
              binary($$, $1, ID_index, $3);