From 2a90b5d73737fabdc9feac8d1bea4b11b0b030ce Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 2 Nov 2016 17:01:50 +0100 Subject: [PATCH] more transient assignments Former-commit-id: a18c4030ebf3146081f6405876b0dcc241399069 [formerly 2f39009d01c87240f7bd7714dd17e16c6870b98d] Former-commit-id: e38777fd539aa7e4a53f7a404ff010171b402491 --- src/adapters/DereferenceIteratorAdapter.h | 8 + src/builder/DdJaniModelBuilder.cpp | 8 +- .../jit/ExplicitJitJaniModelBuilder.cpp | 176 ++++++++++++++---- src/builder/jit/ExplicitJitJaniModelBuilder.h | 3 + src/solver/MinMaxLinearEquationSolver.cpp | 2 +- .../StandardMinMaxLinearEquationSolver.cpp | 13 +- src/storage/jani/Location.h | 4 +- src/storage/jani/VariableSet.cpp | 22 ++- src/storage/jani/VariableSet.h | 7 +- 9 files changed, 186 insertions(+), 57 deletions(-) diff --git a/src/adapters/DereferenceIteratorAdapter.h b/src/adapters/DereferenceIteratorAdapter.h index 9a6e2b4fc..70f5ea3c1 100644 --- a/src/adapters/DereferenceIteratorAdapter.h +++ b/src/adapters/DereferenceIteratorAdapter.h @@ -41,6 +41,14 @@ namespace storm { return it == ite; } + decltype((*std::declval())) front() const { + return *it; + } + + decltype((*std::declval())) back() const { + return *(ite - 1); + } + std::size_t size() const { return std::distance(it, ite); } diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 5a7ecae4e..3fb013ad1 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1745,7 +1745,7 @@ namespace storm { // If no reward model was yet added, but there was one that was given in the options, we try to build the // standard reward model. if (result.empty() && !options.getRewardModelNames().empty()) { - result.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable()); + result.push_back(globalVariables.getTransientVariables().front().getExpressionVariable()); } } @@ -1782,9 +1782,9 @@ namespace storm { std::map result; 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); + if (variable.isBooleanVariable()) { + if (options.buildAllLabels || options.labelNames.find(variable.getName()) != options.labelNames.end()) { + result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), variables.automatonToLocationVariableMap); } } } diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index 2623ee831..ea7f7cd27 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -39,7 +39,7 @@ namespace storm { template ExplicitJitJaniModelBuilder::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model), modelComponentsBuilder(model.getModelType()) { for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) { - transientVariables.insert(variable->getExpressionVariable()); + transientVariables.insert(variable.getExpressionVariable()); } for (auto& automaton : this->model.getAutomata()) { @@ -235,17 +235,23 @@ namespace storm { return {$discrete_time_model}; } + // Non-synchronizing edges. {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { if ({$edge.guard}) { return true; } return false; } + + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } {% for destination in edge.destinations %} static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} } {% endfor %} @@ -259,9 +265,9 @@ namespace storm { static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} - {% for assignment in level.transientAssignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; {% endfor %} } {% endfor %} @@ -272,9 +278,9 @@ namespace storm { destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); {% endfor %} } - {% endfor %} - {% endfor %} + {% endfor %}{% endfor %} + // Synchronizing edges. {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { if ({$edge.guard}) { return true; @@ -282,10 +288,15 @@ namespace storm { return false; } + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% for destination in edge.destinations %} static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} } {% endfor %} @@ -299,9 +310,9 @@ namespace storm { static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} - {% for assignment in level.transientAssignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; {% endfor %} } {% endfor %} @@ -312,9 +323,7 @@ namespace storm { destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); {% endfor %} } - {% endfor %} - {% endfor %} - + {% endfor %}{% endfor %} typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariables const&, TransientVariables&); typedef void (*DestinationFunctionPtr)(StateType const&, StateType&, TransientVariables const&, TransientVariables&); @@ -370,6 +379,7 @@ namespace storm { }; typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); + typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out); class Edge { public: @@ -379,7 +389,7 @@ namespace storm { // Intentionally left empty. } - Edge(EdgeEnabledFunctionPtr edgeEnabledFunction) : edgeEnabledFunction(edgeEnabledFunction) { + Edge(EdgeEnabledFunctionPtr edgeEnabledFunction, EdgeTransientFunctionPtr edgeTransientFunction = nullptr) : edgeEnabledFunction(edgeEnabledFunction), edgeTransientFunction(edgeTransientFunction) { // Intentionally left empty. } @@ -407,10 +417,22 @@ namespace storm { return destinations.end(); } + void perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) const { + edgeTransientFunction(in, transientIn, transientOut); + } + private: EdgeEnabledFunctionPtr edgeEnabledFunction; + EdgeTransientFunctionPtr edgeTransientFunction; ContainerType destinations; }; + + void locations_perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& out) { + {% for location in locations %}if ({$location.guard}) { + {% for assignment in location.assignments %}transientOut.{$assignment.variable} = {$assignment.value};{% endfor %} + } + {% endfor %} + } class JitBuilder : public JitModelBuilderInterface { public: @@ -422,13 +444,13 @@ namespace storm { initialStates.push_back(state); }{% endfor %} {% for edge in nonsynch_edges %}{ - edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}{% if edge.transient_assignments %}, edge_perform_{$edge.name}{% endif %}); {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); {% endfor %} } {% endfor %} {% for edge in synch_edges %}{ - edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}{% if edge.transient_assignments %}, edge_perform_{$edge.name}{% endif %}); {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); {% endfor %} } @@ -496,7 +518,16 @@ namespace storm { #endif behaviour.setExpanded(); + + // Perform transient location assignments. + TransientVariables transientIn; + TransientVariables transientOut; + locations_perform(currentState, transientIn, transientOut); + + // Explore all edges that do not take part in synchronization vectors. exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); + + // Explore all edges that participate in synchronization vectors. exploreSynchronizingEdges(currentState, behaviour, statesToExplore); } @@ -516,14 +547,15 @@ namespace storm { void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for edge in nonsynch_edges %}{ if ({$edge.guard}) { - {% if edge.referenced_transient_variables %} TransientVariables transientIn; TransientVariables transientOut; + {% if edge.transient_assignments %} + edge_perform_{$edge.name}(in, transientIn, transientOut); {% endif %} Choice& choice = behaviour.addChoice(); {% for destination in edge.destinations %}{ StateType out(in); - destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %}); + destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.transient_variables_in_destinations %}, transientIn, transientOut{% endif %}); IndexType outStateIndex = getOrAddIndex(out, statesToExplore); choice.add(outStateIndex, {$destination.value}); } @@ -601,6 +633,8 @@ namespace storm { cpptempl::data_list initialStates = generateInitialStates(); modelData["initialStates"] = cpptempl::make_data(initialStates); generateEdges(modelData); + generateLocations(modelData); + generateRewards(modelData); cpptempl::data_list labels = generateLabels(); modelData["labels"] = cpptempl::make_data(labels); cpptempl::data_list terminalExpressions = generateTerminalExpressions(); @@ -879,6 +913,65 @@ namespace storm { modelData["transient_variables"] = transientVariables; } + template + void ExplicitJitJaniModelBuilder::generateLocations(cpptempl::data_map& modelData) { + cpptempl::data_list locations; + + for (auto const& automaton : this->model.getAutomata()) { + cpptempl::data_map locationData; + uint64_t locationIndex = 0; + for (auto const& location : automaton.getLocations()) { + cpptempl::data_list assignments; + for (auto const& assignment : location.getAssignments()) { + assignments.push_back(generateAssignment(assignment)); + } + locationData["assignments"] = cpptempl::make_data(assignments); + locationData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(getLocationVariable(automaton) == this->model.getManager().integer(locationIndex)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + ++locationIndex; + } + if (!locationData["assignments"]->empty()) { + locations.push_back(locationData); + } + } + + modelData["locations"] = cpptempl::make_data(locations); + } + + template + void ExplicitJitJaniModelBuilder::generateRewards(cpptempl::data_map& modelData) { + cpptempl::data_list rewards; + + // Extract the reward models from the program based on the names we were given. + std::vector> rewardVariables; + auto const& globalVariables = model.getGlobalVariables(); + for (auto const& rewardModelName : this->options.getRewardModelNames()) { + if (globalVariables.hasVariable(rewardModelName)) { + rewardVariables.push_back(globalVariables.getVariable(rewardModelName)); + } else { + STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'."); + STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); + } + } + + // If no reward model was yet added, but there was one that was given in the options, we try to build the + // standard reward model. + if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) { + bool foundTransientVariable = false; + for (auto const& transientVariable : globalVariables.getTransientVariables()) { + if (transientVariable.isUnboundedIntegerVariable() || transientVariable.isRealVariable()) { + rewardVariables.push_back(transientVariable); + foundTransientVariable = true; + break; + } + } + STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable."); + } + + + + modelData["rewards"] = cpptempl::make_data(rewards); + } + template cpptempl::data_list ExplicitJitJaniModelBuilder::generateLabels() { cpptempl::data_list labels; @@ -886,11 +979,11 @@ namespace storm { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { - if (variable->isBooleanVariable()) { - if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) { + if (variable.isBooleanVariable()) { + 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["name"] = variable.getName(); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); labels.push_back(label); } } @@ -1236,20 +1329,33 @@ namespace storm { cpptempl::data_map ExplicitJitJaniModelBuilder::generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge) { cpptempl::data_map edgeData; + std::set transientVariablesInEdge; + cpptempl::data_list edgeAssignments; + for (auto const& assignment : edge.getAssignments()) { + transientVariablesInEdge.insert(assignment.getExpressionVariable()); + std::set usedVariables = assignment.getAssignedExpression().getVariables(); + for (auto const& variable : usedVariables) { + if (transientVariables.find(variable) != transientVariables.end()) { + transientVariablesInEdge.insert(variable); + } + } + edgeAssignments.push_back(generateAssignment(assignment)); + } + cpptempl::data_list destinations; uint64_t destinationIndex = 0; - std::set referencedTransientVariables; + std::set transientVariablesInDestinations; for (auto const& destination : edge.getDestinations()) { destinations.push_back(generateDestination(destinationIndex, destination)); for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { if (assignment.isTransient()) { - referencedTransientVariables.insert(assignment.getExpressionVariable()); + transientVariablesInDestinations.insert(assignment.getExpressionVariable()); } std::set usedVariables = assignment.getAssignedExpression().getVariables(); for (auto const& variable : usedVariables) { if (transientVariables.find(variable) != transientVariables.end()) { - referencedTransientVariables.insert(variable); + transientVariablesInDestinations.insert(variable); } } } @@ -1260,12 +1366,18 @@ namespace storm { edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); edgeData["destinations"] = cpptempl::make_data(destinations); edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); + edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments); - cpptempl::data_list referencedTransientVariableData; - for (auto const& variable : referencedTransientVariables) { - referencedTransientVariableData.push_back(getVariableName(variable)); + cpptempl::data_list transientVariablesInDestinationsData; + for (auto const& variable : transientVariablesInDestinations) { + transientVariablesInDestinationsData.push_back(getVariableName(variable)); + } + edgeData["transient_variables_in_destinations"] = cpptempl::make_data(transientVariablesInDestinationsData); + cpptempl::data_list transientVariablesInEdgeData; + for (auto const& variable : transientVariablesInEdge) { + transientVariablesInEdgeData.push_back(getVariableName(variable)); } - edgeData["referenced_transient_variables"] = cpptempl::make_data(referencedTransientVariableData); + edgeData["transient_variables_in_edge"] = cpptempl::make_data(transientVariablesInEdgeData); return edgeData; } @@ -1301,8 +1413,8 @@ namespace storm { for (auto const& assignment : assignments) { if (assignment.getLevel() != currentLevel) { cpptempl::data_map level; - level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData); - level["transientAssignments"] = cpptempl::make_data(transientAssignmentData); + level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); + level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); level["index"] = asString(currentLevel); levels.push_back(level); @@ -1320,8 +1432,8 @@ namespace storm { // Close the last (open) level. cpptempl::data_map level; - level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData); - level["transientAssignments"] = cpptempl::make_data(transientAssignmentData); + level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); + level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); level["index"] = asString(currentLevel); levels.push_back(level); } diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index 552c1154f..357029873 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -59,6 +59,9 @@ namespace storm { cpptempl::data_map generateRealVariable(storm::jani::RealVariable const& variable); cpptempl::data_map generateLocationVariable(storm::jani::Automaton const& automaton); void generateVariables(cpptempl::data_map& modelData); + + void generateLocations(cpptempl::data_map& modelData); + void generateRewards(cpptempl::data_map& modelData); cpptempl::data_list generateLabels(); cpptempl::data_list generateTerminalExpressions(); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 9b7d65ff9..b718efbea 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -34,7 +34,7 @@ namespace storm { } template - void MinMaxLinearEquationSolver::repeatedMultiply( std::vector& x, std::vector* b, uint_fast64_t n) const { + void MinMaxLinearEquationSolver::repeatedMultiply(std::vector& x, std::vector* b, uint_fast64_t n) const { STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set."); return repeatedMultiply(convert(this->direction), x, b, n); } diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index 6e0313cf9..fe8a6615c 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -198,8 +198,6 @@ namespace storm { return this->getSettings().getRelativeTerminationCriterion(); } - - template bool StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { std::unique_ptr> solver = linearEquationSolverFactory->create(A); @@ -235,7 +233,6 @@ namespace storm { reportStatus(status, iterations); - // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. if (currentX == auxiliarySolvingVectorMemory.get()) { @@ -244,21 +241,21 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b + // Due to a custom termination condition, it may be the case that no iterations are performed. In this + // case we need to compute x'= A*x+b once. + if (iterations==0) { solver->multiply(x, &b, *auxiliarySolvingMultiplyMemory); } std::vector choices(this->A.getRowGroupCount()); - // Reduce the multiplyResult and keep track of the choices made + // Reduce the multiplyResult and keep track of the choices made. storm::utility::vector::reduceVectorMinOrMax(dir, *auxiliarySolvingMultiplyMemory, x, this->A.getRowGroupIndices(), &choices); this->scheduler = std::make_unique(std::move(choices)); } + // If we allocated auxiliary memory, we need to dispose of it now. if (allocatedAuxMemory) { this->deallocateAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations); } - - - if(status == Status::Converged || status == Status::TerminatedEarly) { return true; diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h index a2328cb22..2a84044cd 100644 --- a/src/storage/jani/Location.h +++ b/src/storage/jani/Location.h @@ -10,7 +10,7 @@ namespace storm { /** * Jani Location: * - * Whereas Jani Locations also support invariants, we do not have support for them (as we do not support any of the allowed model types) + * Whereas Jani Locations also support invariants, we do not have support for them (as we do not support any of the allowed model types). */ class Location { public: @@ -53,4 +53,4 @@ namespace storm { }; } -} \ No newline at end of file +} diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index 582fee73b..189c01578 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -48,6 +48,9 @@ namespace storm { std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); booleanVariables.push_back(newVariable); + if (variable.isTransient()) { + transientVariables.push_back(newVariable); + } nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); variableToVariable.emplace(variable.getExpressionVariable(), newVariable); return *newVariable; @@ -58,6 +61,9 @@ namespace storm { std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); boundedIntegerVariables.push_back(newVariable); + if (variable.isTransient()) { + transientVariables.push_back(newVariable); + } nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); variableToVariable.emplace(variable.getExpressionVariable(), newVariable); return *newVariable; @@ -68,6 +74,9 @@ namespace storm { std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); unboundedIntegerVariables.push_back(newVariable); + if (variable.isTransient()) { + transientVariables.push_back(newVariable); + } nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); variableToVariable.emplace(variable.getExpressionVariable(), newVariable); return *newVariable; @@ -78,6 +87,9 @@ namespace storm { std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); realVariables.push_back(newVariable); + if (variable.isTransient()) { + transientVariables.push_back(newVariable); + } nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); variableToVariable.emplace(variable.getExpressionVariable(), newVariable); return *newVariable; @@ -196,14 +208,8 @@ namespace storm { return result; } - std::vector> VariableSet::getTransientVariables() const { - std::vector> result; - for (auto const& variable : variables) { - if (variable->isTransient()) { - result.push_back(variable); - } - } - return result; + typename detail::ConstVariables VariableSet::getTransientVariables() const { + return detail::ConstVariables(transientVariables.begin(), transientVariables.end()); } bool VariableSet::containsVariablesInBoundExpressionsOrInitialValues(std::set const& variables) const { diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 031d56652..ffcc3f0f3 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -184,9 +184,9 @@ namespace storm { uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const; /*! - * Retrieves a vector of transient variables in this variable set. + * Retrieves the transient variables in this variable set. */ - std::vector> getTransientVariables() const; + typename detail::ConstVariables getTransientVariables() const; /*! * Checks whether any of the provided variables appears in bound expressions or initial values of the @@ -210,6 +210,9 @@ namespace storm { /// The real variables in this set. std::vector> realVariables; + /// The transient variables in this set. + std::vector> transientVariables; + /// A set of all variable names currently in use. std::map nameToVariable;