From 032d68b9b0adb458b4998ba24cb74e499fd477e8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 18 Sep 2018 22:40:53 +0200 Subject: [PATCH] switching to recursive synchronization resolution for JANI explicit model exploration --- .../generator/JaniNextStateGenerator.cpp | 84 ++++++++----------- src/storm/generator/JaniNextStateGenerator.h | 8 ++ src/storm/storage/jani/Automaton.cpp | 14 +++- src/storm/storage/jani/Automaton.h | 4 +- src/storm/storage/jani/Model.cpp | 10 ++- src/storm/storage/jani/Model.h | 5 +- 6 files changed, 67 insertions(+), 58 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f052133a9..7a5b211ae 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -173,7 +173,7 @@ namespace storm { std::vector JaniNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { std::vector initialStateIndices; - if (this->model.hasNonTrivialInitialStatesRestriction()) { + if (this->model.hasNonTrivialInitialStates()) { // Prepare an SMT solver to enumerate all initial states. storm::utility::solver::SmtSolverFactory factory; std::unique_ptr solver = factory.create(model.getExpressionManager()); @@ -473,6 +473,33 @@ namespace storm { return choice; } + template + void JaniNextStateGenerator::generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback) { + + if (storm::utility::isZero(probability)) { + return; + } + + if (position >= iteratorList.size()) { + StateType id = stateToIdCallback(state); + distribution.add(id, probability); + } else { + auto const& indexAndEdge = *iteratorList[position]; + auto const& edge = *indexAndEdge.second; + + for (auto const& destination : edge.getDestinations()) { + generateSynchronizedDistribution(applyUpdate(state, destination, this->variableInformation.locationVariables[edgeCombination[position].first]), probability * this->evaluator->asRational(destination.getProbability()), position + 1, edgeCombination, iteratorList, distribution, stateActionRewards, edgeIndices, stateToIdCallback); + } + + if (this->getOptions().isBuildChoiceOriginsSet()) { + edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[position].first, indexAndEdge.first)); + } + + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + } + } + template std::vector> JaniNextStateGenerator::expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector> result; @@ -489,57 +516,17 @@ namespace storm { iteratorList[i] = edgeCombination[i].second.cbegin(); } - storm::builder::jit::Distribution currentDistribution; - storm::builder::jit::Distribution nextDistribution; + storm::builder::jit::Distribution distribution; // As long as there is one feasible combination of commands, keep on expanding it. bool done = false; while (!done) { - currentDistribution.clear(); - nextDistribution.clear(); - - std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); - - currentDistribution.add(state, storm::utility::one()); + distribution.clear(); EdgeIndexSet edgeIndices; - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - auto const& indexAndEdge = *iteratorList[i]; - - if (this->getOptions().isBuildChoiceOriginsSet()) { - edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, indexAndEdge.first)); - } - - storm::jani::Edge const& edge = *indexAndEdge.second; - - for (auto const& destination : edge.getDestinations()) { - for (auto const& stateProbability : currentDistribution) { - // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first]); - - // If the new state was already found as a successor state, update the probability - // and otherwise insert it. - ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability()); - if (edge.hasRate()) { - probability *= this->evaluator->asRational(edge.getRate()); - } - if (probability != storm::utility::zero()) { - nextDistribution.add(newTargetState, probability); - } - } - } - - // Create the state-action reward for the newly created choice. - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); - - nextDistribution.compress(); - - // If there is one more command to come, shift the target states one time step back. - if (i < iteratorList.size() - 1) { - currentDistribution = std::move(nextDistribution); - } - } + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); + generateSynchronizedDistribution(state, storm::utility::one(), 0, edgeCombination, iteratorList, distribution, stateActionRewards, edgeIndices, stateToIdCallback); + distribution.compress(); // At this point, we applied all commands of the current command combination and newTargetStates // contains all target states and their respective probabilities. That means we are now ready to @@ -559,9 +546,8 @@ namespace storm { // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero(); - for (auto const& stateProbability : nextDistribution) { - StateType actualIndex = stateToIdCallback(stateProbability.getState()); - choice.addProbability(actualIndex, stateProbability.getValue()); + for (auto const& stateProbability : distribution) { + choice.addProbability(stateProbability.getState(), stateProbability.getValue()); if (this->options.isExplorationChecksSet()) { probabilitySum += stateProbability.getValue(); diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index bd6b0c922..61091be7d 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -8,6 +8,13 @@ #include "storm/storage/jani/OrderedAssignments.h" namespace storm { + namespace builder { + namespace jit { + template + class Distribution; + } + } + namespace jani { class Edge; class EdgeDestination; @@ -93,6 +100,7 @@ namespace storm { typedef std::vector AutomataEdgeSets; std::vector> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback); + void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector const& iteratorList, storm::builder::jit::Distribution& distribution, std::vector& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback); /*! * Checks the list of enabled edges for multiple synchronized writes to the same global variable. diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 5e97ebed3..8ee3c506f 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -323,8 +323,18 @@ namespace storm { return initialStatesRestriction.isInitialized(); } - bool Automaton::hasNonTrivialInitialStatesRestriction() const { - return this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue(); + bool Automaton::hasNonTrivialInitialStates() const { + if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) { + return true; + } + + for (auto const& variable : this->getVariables()) { + if (variable.hasInitExpression() && !variable.isTransient()) { + return true; + } + } + + return false; } storm::expressions::Expression const& Automaton::getInitialStatesRestriction() const { diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 2b5a833a6..1eadab14f 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -242,9 +242,9 @@ namespace storm { bool hasInitialStatesRestriction() const; /*! - * Retrieves whether there is a non-trivial initial states restriction. + * Retrieves whether this automaton has non-trivial initial states. */ - bool hasNonTrivialInitialStatesRestriction() const; + bool hasNonTrivialInitialStates() const; /*! * Gets the expression restricting the legal initial values of the automaton's variables. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 32af102ec..eba24f1da 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -939,12 +939,18 @@ namespace storm { return initialStatesRestriction; } - bool Model::hasNonTrivialInitialStatesRestriction() const { + bool Model::hasNonTrivialInitialStates() const { if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) { return true; } else { + for (auto const& variable : this->getGlobalVariables()) { + if (variable.hasInitExpression() && !variable.isTransient()) { + return true; + } + } + for (auto const& automaton : this->automata) { - if (automaton.hasInitialStatesRestriction() && !automaton.getInitialStatesRestriction().isTrue()) { + if (automaton.hasNonTrivialInitialStates()) { return true; } } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 70f6d9637..c1bcc1c45 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -358,10 +358,9 @@ namespace storm { bool hasInitialStatesRestriction() const; /*! - * Retrieves whether there is a non-trivial initial states restriction in the model or any of the contained - * automata. + * Retrieves whether there are non-trivial initial states in the model or any of the contained automata. */ - bool hasNonTrivialInitialStatesRestriction() const; + bool hasNonTrivialInitialStates() const; /*! * Sets the expression restricting the legal initial values of the global variables.