diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 219e5a521..07a44dd3b 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -324,7 +324,7 @@ namespace storm { out << "manager {" << std::endl; for (auto const& variableTypePair : manager) { - out << "\t" << variableTypePair.second << " " << variableTypePair.first.getName() << " [offset " << variableTypePair.first.getOffset() << "]" << std::endl; + out << "\t" << variableTypePair.second << " " << variableTypePair.first.getName() << " [offset " << variableTypePair.first.getOffset() << ", " << variableTypePair.first.getIndex() <<" ]" << std::endl; } out << "}" << std::endl; diff --git a/src/storm/storage/jani/JaniScopeChanger.cpp b/src/storm/storage/jani/JaniScopeChanger.cpp index 752dc033e..58e0bbbb1 100644 --- a/src/storm/storage/jani/JaniScopeChanger.cpp +++ b/src/storm/storage/jani/JaniScopeChanger.cpp @@ -24,6 +24,9 @@ namespace storm { bool* result = boost::any_cast(data); if (*result) { return; } *result = expression.containsVariable(varSet); + if (*result) { + STORM_LOG_TRACE("The expression " << expression << " 'contains' a variable in the variable set."); + } } private: @@ -34,6 +37,7 @@ namespace storm { std::set res; for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) { if (model.getAutomaton(i).getVariables().hasVariable(variable)) { + STORM_LOG_TRACE("The automaton " << model.getAutomaton(i).getName() << " 'has' the variable " << variable.getName() << "."); res.insert(i); } else { VariableAccessedTraverser vat({variable}); @@ -41,6 +45,8 @@ namespace storm { vat.traverse(model.getAutomaton(i), &varAccessed); if (varAccessed) { res.insert(i); + STORM_LOG_TRACE("The automaton " << model.getAutomaton(i).getName() << " 'accesses' the variable " << variable.getName() << "."); + } } } @@ -72,6 +78,8 @@ namespace storm { } bool JaniScopeChanger::canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const { + STORM_LOG_TRACE("Can the variable " << variable.getName() << " be made global?"); + if (model.hasGlobalVariable(variable.getName())) { return false; } @@ -87,8 +95,12 @@ namespace storm { } return foundVar; } - + + + std::pair JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector const& properties, boost::optional automatonIndex) const { + STORM_LOG_TRACE("Can the variable " << variable.getName() << " be made local?"); + uint64_t index = model.getNumberOfAutomata(); if (!model.getGlobalVariables().hasVariable(variable)) { @@ -97,26 +109,32 @@ namespace storm { auto accessingAutomata = detail::getAutomataAccessingVariable(variable, model); if (accessingAutomata.size() > 1 || (automatonIndex.is_initialized() && accessingAutomata.count(automatonIndex.get()) == 0)) { + STORM_LOG_TRACE(".. no!, multiple automata access the variable, e.g. automata " << model.getAutomaton(*accessingAutomata.begin()).getName() << " and " << model.getAutomaton(*accessingAutomata.rbegin()).getName()); return {false, index}; } if (model.getInitialStatesRestriction().containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, initial states restriction contains variable"); return {false, index}; } for (auto const& rewExp : model.getNonTrivialRewardExpressions()) { if (rewExp.second.containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, non trivial reward expression "); return {false, index}; } } for (auto const& funDef : model.getGlobalFunctionDefinitions()) { if (funDef.second.getFunctionBody().containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, function definition: "); return {false, index}; } } for (auto const& p : properties) { if (p.getUsedVariablesAndConstants().count(variable) > 0) { + STORM_LOG_TRACE(".. no!, used variables definition: "); return {false, index}; } if (p.getUsedLabels().count(variable.getName()) > 0) { + STORM_LOG_TRACE(".. no!, used labels definition: "); return {false, index}; } } @@ -127,6 +145,7 @@ namespace storm { index = *accessingAutomata.begin(); assert(!automatonIndex.is_initialized() || index == automatonIndex.get()); } + STORM_LOG_TRACE(".. Yes, made local in automaton with index " << index ); return {true, index}; }