From 04d3a649bc87a812234e32f24000dc62c1a1be4a Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 19 Dec 2016 13:43:22 +0100 Subject: [PATCH] finalized location variable for JANI automata --- src/storm/builder/DdJaniModelBuilder.cpp | 16 +++++++++++----- .../builder/jit/ExplicitJitJaniModelBuilder.cpp | 11 +++-------- .../builder/jit/ExplicitJitJaniModelBuilder.h | 1 - src/storm/generator/JaniNextStateGenerator.cpp | 16 ++++++---------- src/storm/storage/jani/Model.cpp | 11 ++++++----- src/storm/storage/jani/Model.h | 2 +- 6 files changed, 27 insertions(+), 30 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 82b1fe639..a6006a009 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -159,7 +159,6 @@ namespace storm { std::vector> rowColumnMetaVariablePairs; // A mapping from automata to the meta variables encoding their location. - std::map automatonToLocationVariableMap; std::map> automatonToLocationDdVariableMap; // A mapping from action indices to the meta variables used to encode these actions. @@ -264,10 +263,11 @@ namespace storm { result.allNondeterminismVariables.insert(result.markovNondeterminismVariable); } - for (auto const& automaton : this->model.getAutomata()) { + for (auto const& automatonName : this->automata) { + storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); + // Start by creating a meta variable for the location of the automaton. - storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc"); - result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable; + storm::expressions::Variable locationExpressionVariable = automaton.getLocationExpressionVariable(); std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair; result.rowColumnMetaVariablePairs.push_back(variablePair); @@ -1785,10 +1785,16 @@ namespace storm { std::map buildLabelExpressions(storm::jani::Model const& model, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { std::map result; + // Create a list of composed automata to restrict the labels to locations of these automata. + std::vector> composedAutomata; + for (auto const& entry : variables.automatonToIdentityMap) { + composedAutomata.emplace_back(model.getAutomaton(entry.first)); + } + for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { if (variable.isBooleanVariable()) { if (options.buildAllLabels || options.labelNames.find(variable.getName()) != options.labelNames.end()) { - result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), variables.automatonToLocationVariableMap); + result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata); } } } diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index bd0f1c89c..bf96e1e23 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -97,11 +97,6 @@ namespace storm { } } - // Create location variables for all the automata that we put in parallel. - for (auto const& automaton : parallelAutomata) { - automatonToLocationVariable.emplace(automaton.get().getName(), this->model.getManager().declareFreshIntegerVariable(false, automaton.get().getName() + "_")); - } - // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. #ifdef STORM_HAVE_CARL if (!std::is_same::value && this->model.hasUndefinedConstants()) { @@ -1514,7 +1509,7 @@ namespace storm { if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { cpptempl::data_map label; label["name"] = variable.getName(); - label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); labels.push_back(label); } } @@ -1542,7 +1537,7 @@ namespace storm { auto const& variable = variables.getVariable(labelOrExpression.getLabel()); STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << "."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << "."); - auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable); + auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata); if (terminalEntry.second) { labelExpression = !labelExpression; } @@ -1590,7 +1585,7 @@ namespace storm { template storm::expressions::Variable const& ExplicitJitJaniModelBuilder::getLocationVariable(storm::jani::Automaton const& automaton) const { - return automatonToLocationVariable.at(automaton.getName()); + return automaton.getLocationExpressionVariable(); } template diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index e3c4c0b94..062865459 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -161,7 +161,6 @@ namespace storm { // Members that store information about the model. They are used in the process of assembling the model // data that is used in the skeleton. std::unordered_map variableToName; - std::map automatonToLocationVariable; storm::expressions::ToCppVisitor expressionTranslator; std::map lowerBoundShiftSubstitution; std::map lowerBounds; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 51b96b122..a2c64c235 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -80,11 +80,9 @@ namespace storm { // If there are terminal states we need to handle, we now need to translate all labels to expressions. if (this->options.hasTerminalStates()) { - std::map locationVariables; - auto locationVariableIt = this->variableInformation.locationVariables.begin(); + std::vector> composedAutomata; for (auto const& automaton : this->model.getAutomata()) { - locationVariables[automaton.getName()] = locationVariableIt->variable; - ++locationVariableIt; + composedAutomata.emplace_back(automaton); } for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { @@ -100,7 +98,7 @@ namespace storm { STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); - this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second)); + this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), composedAutomata), expressionOrLabelAndBool.second)); } } } @@ -618,11 +616,9 @@ namespace storm { storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // Prepare a mapping from automata names to the location variables. - std::map locationVariables; - auto locationVariableIt = this->variableInformation.locationVariables.begin(); + std::vector> composedAutomata; for (auto const& automaton : model.getAutomata()) { - locationVariables[automaton.getName()] = locationVariableIt->variable; - ++locationVariableIt; + composedAutomata.emplace_back(automaton); } // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to @@ -631,7 +627,7 @@ namespace storm { for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { if (variable.isBooleanVariable()) { if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { - transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), locationVariables); + transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata); } } } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index abc49644d..1539c3329 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -969,18 +969,19 @@ namespace storm { STORM_LOG_ASSERT(composition != nullptr, "Composition is not set"); } - storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map const& automatonToLocationVariableMap) const { + storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::vector> const& automata) const { STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable."); storm::expressions::Expression result; bool negate = transientVariable.getInitExpression().isTrue(); - for (auto const& automaton : this->getAutomata()) { - storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName()); - for (auto const& location : automaton.getLocations()) { + for (auto const& automaton : automata) { + storm::expressions::Variable const& locationVariable = automaton.get().getLocationExpressionVariable(); + + for (auto const& location : automaton.get().getLocations()) { for (auto const& assignment : location.getAssignments().getTransientAssignments()) { if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) { - auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); + auto newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); if (result.isInitialized()) { result = result || newExpression; } else { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 5d56e8e1e..237ee827a 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -379,7 +379,7 @@ namespace storm { * Creates the expression that characterizes all states in which the provided transient boolean variable is * true. The provided location variables are used to encode the location of the automata. */ - storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map const& automatonToLocationVariableMap) const; + storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::vector> const& automata) const; /*! * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.