SMV: grammar for asynchronous processes

regression/smv/process/process1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 process1.smv
 
-^EXIT=0$
+^file .* line 8: no support for asynchronous processes$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This does not parse.

src/hw_cbmc_irep_ids.h

@@ -39,6 +39,7 @@ IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
 IREP_ID_ONE(smv_sizeof)
 IREP_ID_ONE(smv_module_instance)
+IREP_ID_ONE(smv_process_module_instance)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)

src/smvlang/expr2smv.cpp

@@ -1060,7 +1060,7 @@ std::string type2smv(const typet &type, const namespacet &ns)
   }
   else if(type.id() == ID_smv_module_instance)
   {
-    auto code = id2string(to_smv_module_instance_type(type).identifier());
+    auto code = id2string(to_smv_module_instance_type(type).base_name());
     const exprt &e=(exprt &)type;
     if(e.has_operands())
     {

src/smvlang/parser.y

@@ -145,11 +145,11 @@ Function: new_module
 static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_name)
 {
   auto base_name = stack_expr(module_name).id_string();
-  const std::string identifier=smv_module_symbol(base_name);
+  const auto identifier=smv_module_symbol(base_name);
   PARSER.parse_tree.module_list.push_back(smv_parse_treet::modulet{});
   auto &module=PARSER.parse_tree.module_list.back();
-  PARSER.parse_tree.module_map[identifier] = --PARSER.parse_tree.module_list.end();
-  module.name = identifier;
+  PARSER.parse_tree.module_map[base_name] = --PARSER.parse_tree.module_list.end();
+  module.identifier = identifier;
   module.base_name = base_name;
   module.source_location = stack_expr(location).source_location();
   PARSER.module = &module;
@@ -598,18 +598,26 @@ simple_type_specifier:
            ;
 
 module_type_specifier:
-             module_name
+             module_name parameter_list_paren_opt
            {
              init($$, ID_smv_module_instance);
-             to_smv_module_instance_type(stack_type($$)).identifier(
-                           smv_module_symbol(stack_expr($1).id_string()));
+             to_smv_module_instance_type(stack_type($$)).base_name(stack_expr($1).id());
+             stack_expr($$).operands().swap(stack_expr($2).operands());
            }
-           | module_name '(' parameter_list ')'
+           | process_Token module_name parameter_list_paren_opt
            {
-             init($$, ID_smv_module_instance);
-             to_smv_module_instance_type(stack_type($$)).identifier(
-                           smv_module_symbol(stack_expr($1).id_string()));
-             stack_expr($$).operands().swap(stack_expr($3).operands());
+             init($$, ID_smv_process_module_instance);
+           }
+           ;
+
+parameter_list_paren_opt:
+             /* optional */
+           {
+             init($$);
+           }
+           | '(' parameter_list ')'
+           {
+             $$ = $2;
            }
            ;
 

src/smvlang/smv_ebmc_language.cpp

@@ -80,7 +80,7 @@ std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
 
     for(const auto &module : parse_tree.module_list)
       show_modules.modules.emplace_back(
-        module.name, module.base_name, "SMV", module.source_location);
+        module.identifier, module.base_name, "SMV", module.source_location);
 
     auto filename = cmdline.value_opt("outfile").value_or("-");
     output_filet output_file{filename};

src/smvlang/smv_language.cpp

@@ -62,7 +62,7 @@ void smv_languaget::dependencies(
   const std::string &module, 
   std::set<std::string> &module_set)
 {
-  auto m_it = smv_parse_tree.module_map.find(module);
+  auto m_it = smv_parse_tree.module_map.find(smv_module_base_name(module));
 
   if(m_it == smv_parse_tree.module_map.end())
     return;
@@ -71,8 +71,11 @@ void smv_languaget::dependencies(
 
   for(auto &element : smv_module.elements)
     if(element.is_var() && element.expr.type().id() == ID_smv_module_instance)
-      module_set.insert(id2string(
-        to_smv_module_instance_type(element.expr.type()).identifier()));
+    {
+      auto base_name =
+        to_smv_module_instance_type(element.expr.type()).base_name();
+      module_set.insert(id2string(smv_module_symbol(base_name)));
+    }
 }
 
 /*******************************************************************\
@@ -90,7 +93,7 @@ Function: smv_languaget::modules_provided
 void smv_languaget::modules_provided(std::set<std::string> &module_set)
 {
   for(const auto &module : smv_parse_tree.module_list)
-    module_set.insert(id2string(module.name));
+    module_set.insert(id2string(module.identifier));
 }
 
 /*******************************************************************\

src/smvlang/smv_parse_tree.h

@@ -30,7 +30,7 @@ class smv_parse_treet
   struct modulet
   {
     source_locationt source_location;
-    irep_idt name, base_name;
+    irep_idt identifier, base_name;
     std::vector<irep_idt> parameters;
 
     struct elementt
@@ -315,6 +315,7 @@ class smv_parse_treet
   using module_listt = std::list<modulet>;
   module_listt module_list;
 
+  // map from module base names into the module list
   using module_mapt =
     std::unordered_map<irep_idt, module_listt::iterator, irep_id_hash>;
   module_mapt module_map;