From db629a19fe394bc3a48fe059199098677ab68207 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 10 Dec 2025 08:11:40 -0800 Subject: [PATCH] SMV: prefix -> context The NuSMV 2.7 manual uses the term "context" for the prefix that is added to identifiers when instantiating a module. --- src/smvlang/smv_typecheck.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index d8137836d..5bb2166ff 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -269,7 +269,10 @@ void smv_typecheckt::instantiate( parameter_map.emplace(parameters[i], arguments[i]); } - const std::string prefix = id2string(instance) + '.'; + // We add a prefix to all identifiers in the instantiated + // module -- this prefix is called "context" in Sec. 2.3.16 in + // the NuSMV 2.7 manual. + const std::string context = id2string(instance) + '.'; // copy the parse tree elements for(auto &src_element : instantiated_module.elements) @@ -277,9 +280,9 @@ void smv_typecheckt::instantiate( auto copy = src_element; // replace the parameter identifiers, - // and add the prefix to non-parameter, non-enum identifiers + // and add the context prefix to non-parameter, non-enum identifiers copy.expr.visit_post( - [¶meter_map, &prefix, this](exprt &expr) + [¶meter_map, &context, this](exprt &expr) { if(expr.id() == ID_smv_identifier) { @@ -298,9 +301,9 @@ void smv_typecheckt::instantiate( } else { - // add the prefix + // add the context prefix to_smv_identifier_expr(expr).identifier( - prefix + id2string(identifier)); + context + id2string(identifier)); } } });