File tree Expand file tree Collapse file tree 1 file changed +8
-5
lines changed
Expand file tree Collapse file tree 1 file changed +8
-5
lines changed Original file line number Diff line number Diff line change @@ -269,17 +269,20 @@ void smv_typecheckt::instantiate(
269269 parameter_map.emplace (parameters[i], arguments[i]);
270270 }
271271
272- const std::string prefix = id2string (instance) + ' .' ;
272+ // We add a prefix to all identifiers in the instantiated
273+ // module -- this prefix is called "context" in Sec. 2.3.16 in
274+ // the NuSMV 2.7 manual.
275+ const std::string context = id2string (instance) + ' .' ;
273276
274277 // copy the parse tree elements
275278 for (auto &src_element : instantiated_module.elements )
276279 {
277280 auto copy = src_element;
278281
279282 // replace the parameter identifiers,
280- // and add the prefix to non-parameter, non-enum identifiers
283+ // and add the context prefix to non-parameter, non-enum identifiers
281284 copy.expr .visit_post (
282- [¶meter_map, &prefix , this ](exprt &expr)
285+ [¶meter_map, &context , this ](exprt &expr)
283286 {
284287 if (expr.id () == ID_smv_identifier)
285288 {
@@ -298,9 +301,9 @@ void smv_typecheckt::instantiate(
298301 }
299302 else
300303 {
301- // add the prefix
304+ // add the context prefix
302305 to_smv_identifier_expr (expr).identifier (
303- prefix + id2string (identifier));
306+ context + id2string (identifier));
304307 }
305308 }
306309 });
You can’t perform that action at this time.
0 commit comments