diff --git a/src/storm/abstraction/GameBddResult.cpp b/src/storm/abstraction/GameBddResult.cpp index 9c6111acc..87aaeaee8 100644 --- a/src/storm/abstraction/GameBddResult.cpp +++ b/src/storm/abstraction/GameBddResult.cpp @@ -2,20 +2,19 @@ namespace storm { namespace abstraction { - namespace prism { - - template - GameBddResult::GameBddResult() : bdd(), numberOfPlayer2Variables(0) { - // Intentionally left empty. - } - - template - GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) { - // Intentionally left empty. - } - - template class GameBddResult; - template class GameBddResult; + + template + GameBddResult::GameBddResult() : bdd(), numberOfPlayer2Variables(0) { + // Intentionally left empty. } + + template + GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) { + // Intentionally left empty. + } + + template class GameBddResult; + template class GameBddResult; + } } diff --git a/src/storm/abstraction/GameBddResult.h b/src/storm/abstraction/GameBddResult.h index 386549e46..84ecbcd80 100644 --- a/src/storm/abstraction/GameBddResult.h +++ b/src/storm/abstraction/GameBddResult.h @@ -4,17 +4,15 @@ namespace storm { namespace abstraction { - namespace prism { + + template + struct GameBddResult { + GameBddResult(); + GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables); - template - struct GameBddResult { - GameBddResult(); - GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables); - - storm::dd::Bdd bdd; - uint_fast64_t numberOfPlayer2Variables; - }; - - } + storm::dd::Bdd bdd; + uint_fast64_t numberOfPlayer2Variables; + }; + } } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp new file mode 100644 index 000000000..77684b842 --- /dev/null +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -0,0 +1,127 @@ +#include "storm/abstraction/jani/AutomatonAbstractor.h" + +#include "storm/abstraction/AbstractionInformation.h" +#include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/GameBddResult.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" + +#include "storm/storage/jani/Automaton.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm-config.h" +#include "storm/adapters/CarlAdapter.h" + +#include "storm/utility/macros.h" + +namespace storm { + namespace abstraction { + namespace jani { + + using storm::settings::modules::AbstractionSettings; + + template + AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { + + bool allowInvalidSuccessorsInCommands = false; + if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { + allowInvalidSuccessorsInCommands = true; + } + + // For each concrete command, we create an abstract counterpart. + uint64_t edgeId = 0; + for (auto const& edge : automaton.getEdges()) { + edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands); + ++edgeId; + } + } + + template + void AutomatonAbstractor::refine(std::vector const& predicates) { + for (uint_fast64_t index = 0; index < edges.size(); ++index) { + STORM_LOG_TRACE("Refining edge with index " << index << "."); + edges[index].refine(predicates); + } + } + + template + storm::expressions::Expression const& AutomatonAbstractor::getGuard(uint64_t player1Choice) const { + return edges[player1Choice].getGuard(); + } + + template + std::map AutomatonAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + return edges[player1Choice].getVariableUpdates(auxiliaryChoice); + } + + template + GameBddResult AutomatonAbstractor::abstract() { + // First, we retrieve the abstractions of all commands. + std::vector> edgeDdsAndUsedOptionVariableCounts; + uint_fast64_t maximalNumberOfUsedOptionVariables = 0; + for (auto& edge : edges) { + edgeDdsAndUsedOptionVariableCounts.push_back(edge.abstract()); + maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, edgeDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables); + } + + // Then, we build the module BDD by adding the single command DDs. We need to make sure that all command + // DDs use the same amount DD variable encoding the choices of player 2. + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + for (auto const& edgeDd : edgeDdsAndUsedOptionVariableCounts) { + result |= edgeDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); + } + return GameBddResult(result, maximalNumberOfUsedOptionVariables); + } + + template + BottomStateResult AutomatonAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); + + for (auto& edge : edges) { + BottomStateResult commandBottomStateResult = edge.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + result.states |= commandBottomStateResult.states; + result.transitions |= commandBottomStateResult.transitions; + } + + return result; + } + + template + storm::dd::Add AutomatonAbstractor::getEdgeUpdateProbabilitiesAdd() const { + storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); + for (auto const& edge : edges) { + result += edge.getEdgeUpdateProbabilitiesAdd(); + } + return result; + } + + template + std::vector> const& AutomatonAbstractor::getEdges() const { + return edges; + } + + template + std::vector>& AutomatonAbstractor::getEdges() { + return edges; + } + + template + std::size_t AutomatonAbstractor::getNumberOfEdges() const { + return edges.size(); + } + + template + AbstractionInformation const& AutomatonAbstractor::getAbstractionInformation() const { + return abstractionInformation.get(); + } + + template class AutomatonAbstractor; + template class AutomatonAbstractor; +#ifdef STORM_HAVE_CARL + template class AutomatonAbstractor; +#endif + } + } +} diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h new file mode 100644 index 000000000..bc7cce6e4 --- /dev/null +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -0,0 +1,131 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/jani/EdgeAbstractor.h" + +#include "storm/settings/modules/AbstractionSettings.h" + +#include "storm/storage/expressions/Expression.h" + +#include "storm/utility/solver.h" + +namespace storm { + namespace jani { + // Forward-declare concrete automaton class. + class Automaton; + } + + namespace abstraction { + template + class AbstractionInformation; + + template + struct BottomStateResult; + + namespace jani { + template + class AutomatonAbstractor { + public: + /*! + * Constructs an abstract module from the given automaton. + * + * @param automaton The concrete automaton for which to build the abstraction. + * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. + * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + */ + AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy); + + AutomatonAbstractor(AutomatonAbstractor const&) = default; + AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; + AutomatonAbstractor(AutomatonAbstractor&&) = default; + AutomatonAbstractor& operator=(AutomatonAbstractor&&) = default; + + /*! + * Refines the abstract automaton with the given predicates. + * + * @param predicates The new predicate indices. + */ + void refine(std::vector const& predicates); + + /*! + * Retrieves the guard of the given player 1 choice. + * + * @param player1Choice The choice of player 1. + * @return The guard of the player 1 choice. + */ + storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player + * 1 choice and auxiliary choice. + */ + std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const; + + /*! + * Computes the abstraction of the module wrt. to the current set of predicates. + * + * @return The abstraction of the module in the form of a BDD together with how many option variables were used. + */ + GameBddResult abstract(); + + /*! + * Retrieves the transitions to bottom states of this automaton. + * + * @param reachableStates A BDD representing the reachable states. + * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2. + * @return The bottom states and the necessary transitions. + */ + BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + + /*! + * Retrieves an ADD that maps the encodings of edges and their updates to their probabilities. + * + * @return The edge-update probability ADD. + */ + storm::dd::Add getEdgeUpdateProbabilitiesAdd() const; + + /*! + * Retrieves the abstract edges of this abstract automton. + * + * @return The abstract edges. + */ + std::vector> const& getEdges() const; + + /*! + * Retrieves the abstract edges of this abstract automaton. + * + * @return The abstract edges. + */ + std::vector>& getEdges(); + + /*! + * Retrieves the number of abstract edges of this abstract automaton. + * + * @param The number of edges. + */ + std::size_t getNumberOfEdges() const; + + private: + /*! + * Retrieves the abstraction information. + * + * @return The abstraction information. + */ + AbstractionInformation const& getAbstractionInformation() const; + + // A factory that can be used to create new SMT solvers. + std::shared_ptr smtSolverFactory; + + // The DD-related information. + std::reference_wrapper const> abstractionInformation; + + // The abstract edge of the abstract automaton. + std::vector> edges; + + // The concrete module this abstract automaton refers to. + std::reference_wrapper automaton; + }; + } + } +} diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp new file mode 100644 index 000000000..fadaef4a2 --- /dev/null +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -0,0 +1,415 @@ +#include "storm/abstraction/jani/EdgeAbstractor.h" + +#include + +#include + +#include "storm/abstraction/AbstractionInformation.h" +#include "storm/abstraction/BottomStateResult.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" + +#include "storm/utility/solver.h" +#include "storm/utility/macros.h" + +#include "storm-config.h" +#include "storm/adapters/CarlAdapter.h" + +namespace storm { + namespace abstraction { + namespace jani { + template + EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { + + // Make the second component of relevant predicates have the right size. + relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations()); + + // Assert all constraints to enforce legal variable values. + for (auto const& constraint : abstractionInformation.getConstraints()) { + smtSolver->add(constraint); + bottomStateAbstractor.constrain(constraint); + } + + // Assert the guard of the command. + smtSolver->add(edge.getGuard()); + } + + template + void EdgeAbstractor::refine(std::vector const& predicates) { + // Add all predicates to the variable partition. + for (auto predicateIndex : predicates) { + localExpressionInformation.addExpression(predicateIndex); + } + + // Next, we check whether there is work to be done by recomputing the relevant predicates and checking + // whether they changed. + std::pair, std::vector>> newRelevantPredicates = this->computeRelevantPredicates(); + + // Check whether we need to recompute the abstraction. + bool relevantPredicatesChanged = this->relevantPredicatesChanged(newRelevantPredicates); + if (relevantPredicatesChanged) { + addMissingPredicates(newRelevantPredicates); + } + forceRecomputation |= relevantPredicatesChanged; + + // Refine bottom state abstractor. Note that this does not trigger a recomputation yet. + bottomStateAbstractor.refine(predicates); + } + + template + storm::expressions::Expression const& EdgeAbstractor::getGuard() const { + return edge.get().getGuard(); + } + + template + std::map EdgeAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { + return edge.get().getDestination(auxiliaryChoice).getAsVariableToExpressionMap(); + } + + template + void EdgeAbstractor::recomputeCachedBdd() { + STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard()); + auto start = std::chrono::high_resolution_clock::now(); + + // Create a mapping from source state DDs to their distributions. + std::unordered_map, std::vector>> sourceToDistributionsMap; + uint64_t numberOfSolutions = 0; + smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) { + sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); + ++numberOfSolutions; + return true; + }); + + // Now we search for the maximal number of choices of player 2 to determine how many DD variables we + // need to encode the nondeterminism. + uint_fast64_t maximalNumberOfChoices = 0; + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast(sourceDistributionsPair.second.size())); + } + + // We now compute how many variables we need to encode the choices. We add one to the maximal number of + // choices to account for a possible transition to a bottom state. + uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + 1))); + + // Finally, build overall result. + storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); + if (!skipBottomStates) { + abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); + } + uint_fast64_t sourceStateIndex = 0; + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + if (!skipBottomStates) { + abstractGuard |= sourceDistributionsPair.first; + } + + STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); + STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); + // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice. + uint_fast64_t distributionIndex = 1; + storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); + for (auto const& distribution : sourceDistributionsPair.second) { + allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded); + ++distributionIndex; + STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); + } + resultBdd |= sourceDistributionsPair.first && allDistributions; + ++sourceStateIndex; + STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); + } + + resultBdd &= computeMissingIdentities(); + resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()); + STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); + + // Cache the result. + cachedDd = GameBddResult(resultBdd, numberOfVariablesNeeded); + auto end = std::chrono::high_resolution_clock::now(); + + STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); + forceRecomputation = false; + } + + template + std::pair, std::set> EdgeAbstractor::computeRelevantPredicates(storm::jani::OrderedAssignments const& assignments) const { + std::pair, std::set> result; + + std::set assignedVariables; + for (auto const& assignment : assignments.getAllAssignments()) { + // Also, variables appearing on the right-hand side of an assignment are relevant for source state. + auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getAssignedExpression().getVariables()); + result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end()); + + // Variables that are being assigned are relevant for the successor state. + storm::expressions::Variable const& assignedVariable = assignment.getExpressionVariable(); + auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable); + result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); + + // Keep track of all assigned variables, so we can find the related predicates later. + assignedVariables.insert(assignedVariable); + } + + if (!allowInvalidSuccessors) { + auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables); + result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); + } + + return result; + } + + template + std::pair, std::vector>> EdgeAbstractor::computeRelevantPredicates() const { + std::pair, std::vector>> result; + + // To start with, all predicates related to the guard are relevant source predicates. + result.first = localExpressionInformation.getExpressionsUsingVariables(edge.get().getGuard().getVariables()); + + // Then, we add the predicates that become relevant, because of some update. + for (auto const& destination : edge.get().getDestinations()) { + std::pair, std::set> relevantUpdatePredicates = computeRelevantPredicates(destination.getOrderedAssignments()); + result.first.insert(relevantUpdatePredicates.first.begin(), relevantUpdatePredicates.first.end()); + result.second.push_back(relevantUpdatePredicates.second); + } + + return result; + } + + template + bool EdgeAbstractor::relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const { + if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) { + return true; + } + + for (uint_fast64_t index = 0; index < edge.get().getNumberOfDestinations(); ++index) { + if (newRelevantPredicates.second[index].size() > relevantPredicatesAndVariables.second[index].size()) { + return true; + } + } + + return false; + } + + template + void EdgeAbstractor::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { + // Determine and add new relevant source predicates. + std::vector> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); + for (auto const& element : newSourceVariables) { + allRelevantPredicates.insert(element.second); + smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second))); + decisionVariables.push_back(element.first); + } + + // Insert the new variables into the record of relevant source variables. + relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end()); + std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair const& first, std::pair const& second) { return first.second < second.second; } ); + + // Do the same for every update. + for (uint_fast64_t index = 0; index < edge.get().getNumberOfDestinations(); ++index) { + std::vector> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + for (auto const& element : newSuccessorVariables) { + allRelevantPredicates.insert(element.second); + smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(edge.get().getDestination(index).getAsVariableToExpressionMap()))); + decisionVariables.push_back(element.first); + } + + relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newSuccessorVariables.begin(), newSuccessorVariables.end()); + std::sort(relevantPredicatesAndVariables.second[index].begin(), relevantPredicatesAndVariables.second[index].end(), [] (std::pair const& first, std::pair const& second) { return first.second < second.second; } ); + } + } + + template + storm::dd::Bdd EdgeAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); + for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { + if (model.getBooleanValue(variableIndexPair.first)) { + result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); + } else { + result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); + } + } + + STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty."); + return result; + } + + template + storm::dd::Bdd EdgeAbstractor::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + + for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) { + storm::dd::Bdd updateBdd = this->getAbstractionInformation().getDdManager().getBddOne(); + + // Translate block variables for this update into a successor block. + for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) { + if (model.getBooleanValue(variableIndexPair.first)) { + updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); + } else { + updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); + } + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + } + + result |= updateBdd; + } + + STORM_LOG_ASSERT(!result.isZero(), "Distribution must not be empty."); + return result; + } + + template + storm::dd::Bdd EdgeAbstractor::computeMissingIdentities() const { + storm::dd::Bdd identities = computeMissingGlobalIdentities(); + identities &= computeMissingUpdateIdentities(); + return identities; + } + + template + storm::dd::Bdd EdgeAbstractor::computeMissingUpdateIdentities() const { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + + for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) { + // Compute the identities that are missing for this update. + auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin(); + auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end(); + + storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); + if (allowInvalidSuccessors) { + for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { + if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) { + updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); + } else { + ++updateRelevantIt; + } + } + } else { + auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin(); + auto sourceRelevantIte = relevantPredicatesAndVariables.first.end(); + + // Go through all relevant source predicates. This is guaranteed to be a superset of the set of + // relevant successor predicates for any update. + for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) { + // If the predicates do not match, there is a predicate missing, so we need to add its identity. + if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) { + updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second); + } else { + ++updateRelevantIt; + } + } + } + + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + } + return result; + } + + template + storm::dd::Bdd EdgeAbstractor::computeMissingGlobalIdentities() const { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); + + if (allowInvalidSuccessors) { + auto allRelevantIt = allRelevantPredicates.cbegin(); + auto allRelevantIte = allRelevantPredicates.cend(); + + for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { + if (allRelevantIt == allRelevantIte || *allRelevantIt != predicateIndex) { + result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); + } else { + ++allRelevantIt; + } + } + } else { + auto relevantIt = relevantPredicatesAndVariables.first.begin(); + auto relevantIte = relevantPredicatesAndVariables.first.end(); + + for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { + if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { + result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); + } else { + ++relevantIt; + } + } + } + + return result; + } + + template + GameBddResult EdgeAbstractor::abstract() { + if (forceRecomputation) { + this->recomputeCachedBdd(); + } else { + cachedDd.bdd &= computeMissingGlobalIdentities(); + } + + return cachedDd; + } + + template + BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard()); + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); + + // If the guard of this edge is a predicate, there are not bottom states/transitions. + if (skipBottomStates) { + STORM_LOG_TRACE("Skipping bottom state computation for this edge."); + return result; + } + + // Use the state abstractor to compute the set of abstract states that has this edge enabled but still + // has a transition to a bottom state. + bottomStateAbstractor.constrain(reachableStates && abstractGuard); + result.states = bottomStateAbstractor.getAbstractStates(); + + // If the result is empty one time, we can skip the bottom state computation from now on. + if (result.states.isZero()) { + skipBottomStates = true; + } + + // Now equip all these states with an actual transition to a bottom state. + result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); + + // Mark the states as bottom states. + result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); + + // Add the edge encoding and the next free player 2 encoding. + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + + return result; + } + + template + storm::dd::Add EdgeAbstractor::getEdgeUpdateProbabilitiesAdd() const { + storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); + for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) { + result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(updateIndex).getProbability())); + } + result *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); + return result; + } + + template + storm::jani::Edge const& EdgeAbstractor::getConcreteEdge() const { + return edge.get(); + } + + template + AbstractionInformation const& EdgeAbstractor::getAbstractionInformation() const { + return abstractionInformation.get(); + } + + template + AbstractionInformation& EdgeAbstractor::getAbstractionInformation() { + return abstractionInformation.get(); + } + + template class EdgeAbstractor; + template class EdgeAbstractor; +#ifdef STORM_HAVE_CARL + template class EdgeAbstractor; +#endif + } + } +} diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h new file mode 100644 index 000000000..01be8bab7 --- /dev/null +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -0,0 +1,256 @@ +#pragma once + +#include +#include +#include +#include + +#include "storm/abstraction/LocalExpressionInformation.h" +#include "storm/abstraction/StateSetAbstractor.h" +#include "storm/abstraction/GameBddResult.h" + +#include "storm/storage/expressions/ExpressionEvaluator.h" + +#include "storm/storage/dd/DdType.h" +#include "storm/storage/expressions/Expression.h" + +#include "storm/solver/SmtSolver.h" + +namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace dd { + template + class Bdd; + + template + class Add; + } + + namespace jani { + // Forward-declare concrete edge and assignment classes. + class Edge; + class Assignment; + class OrderedAssignments; + } + + namespace abstraction { + template + class AbstractionInformation; + + template + class BottomStateResult; + + namespace jani { + template + class EdgeAbstractor { + public: + /*! + * Constructs an abstract edge from the given command and the initial predicates. + * + * @param edgeId The ID to assign to the edge. + * @param edge The concrete edge for which to build the abstraction. + * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. + * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors. + */ + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors); + + /*! + * Refines the abstract edge with the given predicates. + * + * @param predicates The new predicates. + */ + void refine(std::vector const& predicates); + + /*! + * Retrieves the guard of this edge. + */ + storm::expressions::Expression const& getGuard() const; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given + * auxiliary choice. + */ + std::map getVariableUpdates(uint64_t auxiliaryChoice) const; + + /*! + * Computes the abstraction of the edge wrt. to the current set of predicates. + * + * @return The abstraction of the edge in the form of a BDD together with the number of DD variables + * used to encode the choices of player 2. + */ + GameBddResult abstract(); + + /*! + * Retrieves the transitions to bottom states of this edge. + * + * @param reachableStates A BDD representing the reachable states. + * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2. + * @return The bottom state transitions in the form of a BDD. + */ + BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + + /*! + * Retrieves an ADD that maps the encoding of the edge and its updates to their probabilities. + * + * @return The edge-update probability ADD. + */ + storm::dd::Add getEdgeUpdateProbabilitiesAdd() const; + + /*! + * Retrieves the concrete edge that is abstracted by this abstract edge. + * + * @return The concrete edge. + */ + storm::jani::Edge const& getConcreteEdge() const; + + private: + /*! + * Determines the relevant predicates for source as well as successor states wrt. to the given assignments + * (that, for example, form an update). + * + * @param assignments The assignments that are to be considered. + * @return A pair whose first component represents the relevant source predicates and whose second + * component represents the relevant successor state predicates. + */ + std::pair, std::set> computeRelevantPredicates(storm::jani::OrderedAssignments const& assignments) const; + + /*! + * Determines the relevant predicates for source as well as successor states. + * + * @return A pair whose first component represents the relevant source predicates and whose second + * component represents the relevant successor state predicates. + */ + std::pair, std::vector>> computeRelevantPredicates() const; + + /*! + * Checks whether the relevant predicates changed. + * + * @param newRelevantPredicates The new relevant predicates. + */ + bool relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const; + + /*! + * Takes the new relevant predicates and creates the appropriate variables and assertions for the ones + * that are currently missing. + * + * @param newRelevantPredicates The new relevant predicates. + */ + void addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates); + + /*! + * Translates the given model to a source state DD. + * + * @param model The model to translate. + * @return The source state encoded as a DD. + */ + storm::dd::Bdd getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; + + /*! + * Translates the given model to a distribution over successor states. + * + * @param model The model to translate. + * @return The source state encoded as a DD. + */ + storm::dd::Bdd getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const; + + /*! + * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. + */ + void recomputeCachedBdd(); + + /*! + * Computes the missing state identities. + * + * @return A BDD that represents the all missing state identities. + */ + storm::dd::Bdd computeMissingIdentities() const; + + /*! + * Computes the missing state identities for the updates. + * + * @return A BDD that represents the state identities for predicates that are irrelevant for the + * successor states. + */ + storm::dd::Bdd computeMissingUpdateIdentities() const; + + /*! + * Retrieves the abstraction information object. + * + * @return The abstraction information object. + */ + AbstractionInformation const& getAbstractionInformation() const; + + /*! + * Retrieves the abstraction information object. + * + * @return The abstraction information object. + */ + AbstractionInformation& getAbstractionInformation(); + + /*! + * Computes the globally missing state identities. + * + * @return A BDD that represents the global state identities for predicates that are irrelevant for the + * source and successor states. + */ + storm::dd::Bdd computeMissingGlobalIdentities() const; + + // An SMT responsible for this abstract command. + std::unique_ptr smtSolver; + + // The abstraction-related information. + std::reference_wrapper> abstractionInformation; + + // The ID of the edge. + uint64_t edgeId; + + // The concrete edge this abstract command refers to. + std::reference_wrapper edge; + + // The local expression-related information. + LocalExpressionInformation localExpressionInformation; + + // The evaluator used to translate the probability expressions. + storm::expressions::ExpressionEvaluator evaluator; + + // The currently relevant source/successor predicates and the corresponding variables. + std::pair>, std::vector>>> relevantPredicatesAndVariables; + + // The set of all relevant predicates. + std::set allRelevantPredicates; + + // The most recent result of a call to computeDd. If nothing has changed regarding the relevant + // predicates, this result may be reused. + GameBddResult cachedDd; + + // All relevant decision variables over which to perform AllSat. + std::vector decisionVariables; + + // A flag indicating whether it is allowed to enumerate invalid successors. Invalid successors may be + // enumerated if the predicates that are (indirectly) related to an assignment variable are not + // considered as source predicates. + bool allowInvalidSuccessors; + + // A flag indicating whether the computation of bottom states can be skipped (for example, if the bottom + // states become empty at some point). + bool skipBottomStates; + + // A flag remembering whether we need to force recomputation of the BDD. + bool forceRecomputation; + + // The abstract guard of the edge. This is only used if the guard is not a predicate, because it can + // then be used to constrain the bottom state abstractor. + storm::dd::Bdd abstractGuard; + + // A state-set abstractor used to determine the bottom states if not all guards were added. + StateSetAbstractor bottomStateAbstractor; + }; + } + } +} diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp new file mode 100644 index 000000000..47f644159 --- /dev/null +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -0,0 +1,349 @@ +#include "storm/abstraction/jani/JaniMenuGameAbstractor.h" + +#include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/GameBddResult.h" + +#include "storm/storage/BitVector.h" + +#include "storm/storage/jani/Model.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" + +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm/utility/dd.h" +#include "storm/utility/macros.h" +#include "storm/utility/solver.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" + +#include "storm-config.h" +#include "storm/adapters/CarlAdapter.h" + +namespace storm { + namespace abstraction { + namespace jani { + + using storm::settings::modules::AbstractionSettings; + + template + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false), invalidBlockDetectionStrategy(storm::settings::getModule().getInvalidBlockDetectionStrategy()) { + + // For now, we assume that there is a single module. If the program has more than one module, it needs + // to be flattened before the procedure. + STORM_LOG_THROW(model.getNumberOfAutomata() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract model from program containing more than one automaton."); + + // Add all variables range expressions to the information object. + for (auto const& range : this->model.get().getAllRangeExpressions()) { + abstractionInformation.addConstraint(range); + initialStateAbstractor.constrain(range); + } + + uint_fast64_t totalNumberOfCommands = 0; + uint_fast64_t maximalUpdateCount = 0; + std::vector allGuards; + for (auto const& automaton : model.getAutomata()) { + for (auto const& edge : automaton.getEdges()) { + maximalUpdateCount = std::max(maximalUpdateCount, static_cast(edge.getNumberOfDestinations())); + } + + totalNumberOfCommands += automaton.getNumberOfEdges(); + } + + // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible + // choices. If for some reason this should not be enough, we could grow this vector dynamically, but + // odds are that it's impossible to treat such models in any event. + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + + // For each module of the concrete program, we create an abstract counterpart. + for (auto const& automaton : model.getAutomata()) { + automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy); + } + + // Retrieve the edge-update probability ADD, so we can multiply it with the abstraction BDD later. + edgeUpdateProbabilitiesAdd = automata.front().getEdgeUpdateProbabilitiesAdd(); + } + + template + void JaniMenuGameAbstractor::refine(RefinementCommand const& command) { + // Add the predicates to the global list of predicates and gather their indices. + std::vector predicateIndices; + for (auto const& predicate : command.getPredicates()) { + STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); + predicateIndices.push_back(abstractionInformation.getOrAddPredicate(predicate)); + } + + // Refine all abstract automata. + for (auto& automaton : automata) { + automaton.refine(predicateIndices); + } + + // Refine initial state abstractor. + initialStateAbstractor.refine(predicateIndices); + + // Refine the valid blocks. + validBlockAbstractor.refine(predicateIndices); + + refinementPerformed |= !command.getPredicates().empty(); + } + + template + MenuGame JaniMenuGameAbstractor::abstract() { + if (refinementPerformed) { + currentGame = buildGame(); + refinementPerformed = true; + } + return *currentGame; + } + + template + AbstractionInformation const& JaniMenuGameAbstractor::getAbstractionInformation() const { + return abstractionInformation; + } + + template + storm::expressions::Expression const& JaniMenuGameAbstractor::getGuard(uint64_t player1Choice) const { + return automata.front().getGuard(player1Choice); + } + + template + std::map JaniMenuGameAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { + return automata.front().getVariableUpdates(player1Choice, auxiliaryChoice); + } + + template + std::pair JaniMenuGameAbstractor::getPlayer1ChoiceRange() const { + return std::make_pair(0, automata.front().getNumberOfEdges()); + } + + template + storm::expressions::Expression JaniMenuGameAbstractor::getInitialExpression() const { + return model.get().getInitialStatesExpression(); + } + + template + storm::dd::Bdd JaniMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) { + STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); + return abstractionInformation.getPredicateSourceVariable(predicate); + } + + template + std::unique_ptr> JaniMenuGameAbstractor::buildGame() { + // As long as there is only one module, we only build its game representation. + GameBddResult game = automata.front().abstract(); + + if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { + auto validBlockStart = std::chrono::high_resolution_clock::now(); + storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + // Cut away all invalid successor blocks. + game.bdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + auto validBlockEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Global invalid block detection completed in " << std::chrono::duration_cast(validBlockEnd - validBlockStart).count() << "ms."); + } + + // Construct a set of all unnecessary variables, so we can abstract from it. + std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); + variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); + auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); + variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + + // Do a reachability analysis on the raw transition relation. + storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); + storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, + // as the bottom states are not contained in the reachable states. + storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); + deadlockStates = reachableStates && !deadlockStates; + + // If there are deadlock states, we fix them now. + storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); + if (!deadlockStates.isZero()) { + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + } + + // Compute bottom states and the appropriate transitions if necessary. + BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + bottomStateResult = automata.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + bool hasBottomStates = !bottomStateResult.states.isZero(); + + // Construct the transition matrix by cutting away the transitions of unreachable states. + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd(); + transitionMatrix *= edgeUpdateProbabilitiesAdd; + transitionMatrix += deadlockTransitions; + + // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions. + transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); + reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + initialStates &= abstractionInformation.getBottomStateBdd(true, true); + + // If there are bottom transitions, exnted the transition matrix and reachable states now. + if (hasBottomStates) { + transitionMatrix += bottomStateResult.transitions.template toAdd(); + reachableStates |= bottomStateResult.states; + } + + std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); + + std::set allNondeterminismVariables = usedPlayer2Variables; + allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); + + std::set allSourceVariables(abstractionInformation.getSourceVariables()); + allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); + std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); + allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); + + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + } + + template + void JaniMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { + std::ofstream out(filename); + + storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); + storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); + storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); + filteredTransitions *= filteredReachableStates.template toAdd(); + + // Determine all initial states so we can color them blue. + std::unordered_set initialStates; + storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); + for (auto stateValue : initialStatesAsAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + initialStates.insert(stateName.str()); + } + + // Determine all highlight states so we can color them red. + std::unordered_set highlightStates; + storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); + for (auto stateValue : highlightStatesAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + highlightStates.insert(stateName.str()); + } + + out << "digraph game {" << std::endl; + + // Create the player 1 nodes. + storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); + for (auto stateValue : statesAsAdd) { + out << "\tpl1_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + std::string stateNameAsString = stateName.str(); + out << stateNameAsString; + out << " [ label=\""; + if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { + out << "*\", margin=0, width=0, height=0, shape=\"none\""; + } else { + out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; + } + bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); + bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); + if (isInitial && isHighlight) { + out << ", style=\"filled\", fillcolor=\"yellow\""; + } else if (isInitial) { + out << ", style=\"filled\", fillcolor=\"blue\""; + } else if (isHighlight) { + out << ", style=\"filled\", fillcolor=\"red\""; + } + out << " ];" << std::endl; + } + + // Create the nodes of the second player. + storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); + for (auto stateValue : player2States) { + out << "\tpl2_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + out << stateName.str() << "_" << index; + out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; + out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + // Create the nodes of the probabilistic player. + storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); + for (auto stateValue : playerPStates) { + out << "\tplp_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + stateName << "_" << index; + index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); + out << stateName.str() << "_" << index; + out << " [ shape=\"point\", label=\"\" ];" << std::endl; + out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + for (auto stateValue : filteredTransitions) { + std::stringstream sourceStateName; + std::stringstream successorStateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + sourceStateName << "1"; + } else { + sourceStateName << "0"; + } + } + for (auto const& var : currentGame->getColumnVariables()) { + if (stateValue.first.getBooleanValue(var)) { + successorStateName << "1"; + } else { + successorStateName << "0"; + } + } + uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); + out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; + } + + out << "}" << std::endl; + } + + // Explicitly instantiate the class. + template class JaniMenuGameAbstractor; + template class JaniMenuGameAbstractor; +#ifdef STORM_HAVE_CARL + template class JaniMenuGameAbstractor; +#endif + } + } +} diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h new file mode 100644 index 000000000..d14ad0d06 --- /dev/null +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -0,0 +1,167 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/MenuGameAbstractor.h" +#include "storm/abstraction/AbstractionInformation.h" +#include "storm/abstraction/MenuGame.h" +#include "storm/abstraction/RefinementCommand.h" +#include "storm/abstraction/ValidBlockAbstractor.h" +#include "storm/abstraction/jani/AutomatonAbstractor.h" + +#include "storm/storage/dd/Add.h" + +#include "storm/storage/expressions/Expression.h" + +#include "storm/settings/modules/AbstractionSettings.h" + +namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace models { + namespace symbolic { + template + class StochasticTwoPlayerGame; + } + } + + namespace jani { + // Forward-declare concrete Model class. + class Model; + } + + namespace abstraction { + namespace jani { + + template + class JaniMenuGameAbstractor : public MenuGameAbstractor { + public: + /*! + * Constructs an abstractor for the given model. + * + * @param model The concrete model for which to build the abstraction. + * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + */ + JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory); + + JaniMenuGameAbstractor(JaniMenuGameAbstractor const&) = default; + JaniMenuGameAbstractor& operator=(JaniMenuGameAbstractor const&) = default; + JaniMenuGameAbstractor(JaniMenuGameAbstractor&&) = default; + JaniMenuGameAbstractor& operator=(JaniMenuGameAbstractor&&) = default; + + /*! + * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. + * + * @return The abstract stochastic two player game. + */ + MenuGame abstract() override; + + /*! + * Retrieves information about the abstraction. + * + * @return The abstraction information object. + */ + AbstractionInformation const& getAbstractionInformation() const override; + + /*! + * Retrieves the guard predicate of the given player 1 choice. + * + * @param player1Choice The choice for which to retrieve the guard. + * @return The guard of the player 1 choice. + */ + storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override; + + /*! + * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player + * 1 choice and auxiliary choice. + */ + std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override; + + /*! + * Retrieves the range of player 1 choices. + */ + std::pair getPlayer1ChoiceRange() const override; + + /*! + * Retrieves the expression that characterizes the initial states. + */ + storm::expressions::Expression getInitialExpression() const override; + + /*! + * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it + * was either given as an initial predicate or used as a refining predicate later. + * + * @param predicate The predicate for which to retrieve the states. + * @return The BDD representing the set of states. + */ + storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); + + /*! + * Performs the given refinement command. + * + * @param command The command to perform. + */ + virtual void refine(RefinementCommand const& command) override; + + /*! + * Exports the current state of the abstraction in the dot format to the given file. + * + * @param filename The name of the file to which to write the dot output. + * @param highlightStates A BDD characterizing states that will be highlighted. + * @param filter A filter that is applied to select which part of the game to export. + */ + void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; + + private: + /*! + * Builds the stochastic game representing the abstraction of the program. + * + * @return The stochastic game. + */ + std::unique_ptr> buildGame(); + + /*! + * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices + * to bit vectors representing the successors under these updates. + * + * @param choice The choice to decode. + */ + std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + + // The concrete model this abstractor refers to. + std::reference_wrapper model; + + // A factory that can be used to create new SMT solvers. + std::shared_ptr smtSolverFactory; + + // An object containing all information about the abstraction like predicates and the corresponding DDs. + AbstractionInformation abstractionInformation; + + // The abstract modules of the abstract program. + std::vector> automata; + + // A state-set abstractor used to determine the initial states of the abstraction. + StateSetAbstractor initialStateAbstractor; + + // An object that is used to compute the valid blocks. + ValidBlockAbstractor validBlockAbstractor; + + // An ADD characterizing the probabilities of edges and their updates. + storm::dd::Add edgeUpdateProbabilitiesAdd; + + // The current game-based abstraction. + std::unique_ptr> currentGame; + + // A flag storing whether a refinement was performed. + bool refinementPerformed; + + // The strategy to use for detecting invalid blocks. + storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy; + }; + } + } +} diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index ecf985bae..2b5d35845 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -44,9 +44,6 @@ namespace storm { template class BottomStateResult; - template - struct GameBddResult; - namespace prism { template class CommandAbstractor { diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 4ba63a56d..357d9682d 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -31,13 +31,13 @@ namespace storm { class ModuleAbstractor { public: /*! - * Constructs an abstract module from the given module and the initial predicates. + * Constructs an abstract module from the given module. * * @param module The concrete module for which to build the abstraction. * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy = storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy::Command); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy); ModuleAbstractor(ModuleAbstractor const&) = default; ModuleAbstractor& operator=(ModuleAbstractor const&) = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 6bfa3a30b..8eab6d22d 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -27,9 +27,7 @@ namespace storm { namespace abstraction { namespace prism { - -#undef LOCAL_DEBUG - + using storm::settings::modules::AbstractionSettings; template @@ -51,7 +49,6 @@ namespace storm { uint_fast64_t maximalUpdateCount = 0; std::vector allGuards; for (auto const& module : program.getModules()) { - // If we were requested to add all guards to the set of predicates, we do so now. for (auto const& command : module.getCommands()) { maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); } diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index a85c326f6..f0928a3be 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -41,13 +41,12 @@ namespace storm { class PrismMenuGameAbstractor : public MenuGameAbstractor { public: /*! - * Constructs an abstract program from the given program and the initial predicates. + * Constructs an abstractor for the given program. * - * @param expressionManager The manager responsible for the expressions of the program. * @param program The concrete program for which to build the abstraction. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); + PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory); PrismMenuGameAbstractor(PrismMenuGameAbstractor const&) = default; PrismMenuGameAbstractor& operator=(PrismMenuGameAbstractor const&) = default; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index ef3767c89..869b17c2e 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -12,6 +12,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" +#include "storm/abstraction/jani/JaniMenuGameAbstractor.h" #include "storm/abstraction/MenuGameRefiner.h" #include "storm/logic/FragmentSpecification.h" @@ -32,8 +33,6 @@ #include "storm/modelchecker/results/CheckResult.h" -//#define LOCAL_DEBUG - namespace storm { namespace modelchecker { @@ -42,16 +41,22 @@ namespace storm { template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) { - STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Currently only PRISM models are supported by the game-based model checker."); - storm::prism::Program const& originalProgram = model.asPrismProgram(); - STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); - storm::utility::prism::requireNoUndefinedConstants(originalProgram); - - // Start by preparing the program. That is, we flatten the modules if there is more than one. - if (originalProgram.getNumberOfModules() > 1) { - preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory); + model.requireNoUndefinedConstants(); + if (model.isPrismProgram()) { + storm::prism::Program const& originalProgram = model.asPrismProgram(); + STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); + + // Flatten the modules if there is more than one. + if (originalProgram.getNumberOfModules() > 1) { + preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory); + } else { + preprocessedModel = originalProgram; + } } else { - preprocessedModel = originalProgram; + storm::jani::Model const& originalModel = model.asJaniModel(); + STORM_LOG_THROW(originalModel.getModelType() == storm::jani::ModelType::DTMC || originalModel.getModelType() == storm::jani::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); + + preprocessedModel = model; } bool reuseAll = storm::settings::getModule().isReuseAllResultsSet(); @@ -76,7 +81,10 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); - std::map labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + std::map labelToExpressionMapping; + if (preprocessedModel.isPrismProgram()) { + labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + } return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); } @@ -286,10 +294,15 @@ namespace storm { storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask); // Create the abstractor. - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory); + std::shared_ptr> abstractor; + if (preprocessedModel.isPrismProgram()) { + abstractor = std::make_shared>(preprocessedModel.asPrismProgram(), smtSolverFactory); + } else { + abstractor = std::make_shared>(preprocessedModel.asJaniModel(), smtSolverFactory); + } // Create a refiner that can be used to refine the abstraction when needed. - storm::abstraction::MenuGameRefiner refiner(abstractor, smtSolverFactory->create(preprocessedModel.getManager())); + storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); refiner.refine(initialPredicates); // Enter the main-loop of abstraction refinement. @@ -301,7 +314,7 @@ namespace storm { // (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. auto abstractionStart = std::chrono::high_resolution_clock::now(); - storm::abstraction::MenuGame game = abstractor.abstract(); + storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state."); @@ -324,7 +337,7 @@ namespace storm { QualitativeResultMinMax qualitativeResult; std::unique_ptr result = computeProb01States(checkTask, qualitativeResult, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates, refiner.addedAllGuards()); if (result) { - printStatistics(abstractor, game); + printStatistics(*abstractor, game); return result; } previousQualitativeResult = qualitativeResult; @@ -344,7 +357,7 @@ namespace storm { result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { - printStatistics(abstractor, game); + printStatistics(*abstractor, game); return result; } else { STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); @@ -374,7 +387,7 @@ namespace storm { previousMinQuantitativeResult = quantitativeResult.min; result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue); if (result) { - printStatistics(abstractor, game); + printStatistics(*abstractor, game); return result; } @@ -382,7 +395,7 @@ namespace storm { quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStateValue); if (result) { - printStatistics(abstractor, game); + printStatistics(*abstractor, game); return result; } @@ -392,7 +405,7 @@ namespace storm { // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue, comparator); if (result) { - printStatistics(abstractor, game); + printStatistics(*abstractor, game); return result; } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 6cac964a2..939b9b7c4 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -37,9 +37,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(pivotHeuristic)).setDefaultValueString("nearest-max-dev").build()).build()); - std::vector invalidBlockStrategies = {"none", "command", "global"}; + std::vector invalidBlockStrategies = {"none", "local", "global"}; this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'command' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build()); @@ -90,8 +90,8 @@ namespace storm { std::string strategyName = this->getOption(invalidBlockStrategyOptionName).getArgumentByName("name").getValueAsString(); if (strategyName == "none") { return AbstractionSettings::InvalidBlockDetectionStrategy::None; - } else if (strategyName == "command") { - return AbstractionSettings::InvalidBlockDetectionStrategy::Command; + } else if (strategyName == "local") { + return AbstractionSettings::InvalidBlockDetectionStrategy::Local; } else if (strategyName == "global") { return AbstractionSettings::InvalidBlockDetectionStrategy::Global; } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 3852e744c..d00faa692 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -16,7 +16,7 @@ namespace storm { }; enum class InvalidBlockDetectionStrategy { - None, Command, Global + None, Local, Global }; /*! diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index c156dc176..a9e4488b3 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -127,5 +127,12 @@ namespace storm { return *this; } + void SymbolicModelDescription::requireNoUndefinedConstants() const { + if (this->isJaniModel()) { + storm::utility::jani::requireNoUndefinedConstants(this->asJaniModel()); + } else { + storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram()); + } + } } } diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index e576b8866..44e80d9f0 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -40,6 +40,8 @@ namespace storm { SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; + void requireNoUndefinedConstants() const; + private: boost::optional> modelDescription; }; diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index d9de26792..e2fd73153 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -97,6 +97,14 @@ namespace storm { return variables; } + std::set Automaton::getAllExpressionVariables() const { + std::set result; + for (auto const& variable : this->getVariables()) { + result.insert(variable.getExpressionVariable()); + } + return result; + } + bool Automaton::hasTransientVariable() const { return variables.hasTransientVariable(); } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 77ee820e7..c06a4b232 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -135,6 +135,13 @@ namespace storm { */ VariableSet const& getVariables() const; + /*! + * Retrieves all expression variables used by this automaton. + * + * @return The set of expression variables used by this automaton. + */ + std::set getAllExpressionVariables() const; + /*! * Retrieves whether this automaton has a transient variable. */ diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 515eb198e..5f68a2570 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -44,6 +44,10 @@ namespace storm { this->guard = guard; } + EdgeDestination const& Edge::getDestination(uint64_t index) const { + return destinations[index]; + } + std::vector const& Edge::getDestinations() const { return destinations; } @@ -52,6 +56,10 @@ namespace storm { return destinations; } + std::size_t Edge::getNumberOfDestinations() const { + return destinations.size(); + } + void Edge::addDestination(EdgeDestination const& destination) { destinations.push_back(destination); } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index 212e7656f..99cad452b 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -61,6 +61,11 @@ namespace storm { * Sets a new guard for this edge. */ void setGuard(storm::expressions::Expression const& guard); + + /*! + * Retrieves the destination with the given index. + */ + EdgeDestination const& getDestination(uint64_t index) const; /*! * Retrieves the destinations of this edge. @@ -72,6 +77,11 @@ namespace storm { */ std::vector& getDestinations(); + /*! + * Retrieves the number of destinations of this edge. + */ + std::size_t getNumberOfDestinations() const; + /*! * Adds the given destination to the destinations of this edge. */ diff --git a/src/storm/storage/jani/EdgeDestination.cpp b/src/storm/storage/jani/EdgeDestination.cpp index 27a07fe3f..77e2e7a78 100644 --- a/src/storm/storage/jani/EdgeDestination.cpp +++ b/src/storm/storage/jani/EdgeDestination.cpp @@ -34,6 +34,16 @@ namespace storm { this->probability = probability; } + std::map EdgeDestination::getAsVariableToExpressionMap() const { + std::map result; + + for (auto const& assignment : this->getOrderedAssignments()) { + result[assignment.getExpressionVariable()] = assignment.getAssignedExpression(); + } + + return result; + } + OrderedAssignments const& EdgeDestination::getOrderedAssignments() const { return assignments; } diff --git a/src/storm/storage/jani/EdgeDestination.h b/src/storm/storage/jani/EdgeDestination.h index a3bc0b49c..8fba514c2 100644 --- a/src/storm/storage/jani/EdgeDestination.h +++ b/src/storm/storage/jani/EdgeDestination.h @@ -39,6 +39,12 @@ namespace storm { */ void setProbability(storm::expressions::Expression const& probability); + /*! + * Retrieves the mapping from variables to their assigned expressions that corresponds to the assignments + * of this destination. + */ + std::map getAsVariableToExpressionMap() const; + /*! * Retrieves the assignments to make when choosing this destination. */ diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 281f8d1de..8b46c06c8 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -154,6 +154,23 @@ namespace storm { return globalVariables; } + std::set Model::getAllExpressionVariables() const { + std::set result; + + for (auto const& constant : constants) { + result.insert(constant.getExpressionVariable()); + } + for (auto const& variable : this->getGlobalVariables()) { + result.insert(variable.getExpressionVariable()); + } + for (auto const& automaton : automata) { + auto const& automatonVariables = automaton.getAllExpressionVariables(); + result.insert(automatonVariables.begin(), automatonVariables.end()); + } + + return result; + } + bool Model::hasGlobalVariable(std::string const& name) const { return globalVariables.hasVariable(name); } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 9150bc335..2fbe8e8b8 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -156,6 +156,13 @@ namespace storm { * Retrieves the variables of this automaton. */ VariableSet const& getGlobalVariables() const; + + /*! + * Retrieves all expression variables used by this model. + * + * @return The set of expression variables used by this model. + */ + std::set getAllExpressionVariables() const; /*! * Retrieves whether this model has a global variable with the given name. diff --git a/src/storm/utility/jani.cpp b/src/storm/utility/jani.cpp index ece6630fc..eedca0e37 100644 --- a/src/storm/utility/jani.cpp +++ b/src/storm/utility/jani.cpp @@ -66,7 +66,24 @@ namespace storm { return constantDefinitions; } - + + void requireNoUndefinedConstants(storm::jani::Model const& model) { + if (model.hasUndefinedConstants()) { + std::vector> undefinedConstants = model.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str()); + } + } } } } diff --git a/src/storm/utility/jani.h b/src/storm/utility/jani.h index 08bc75b91..303ef7397 100644 --- a/src/storm/utility/jani.h +++ b/src/storm/utility/jani.h @@ -17,6 +17,7 @@ namespace storm { std::map parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString); + void requireNoUndefinedConstants(storm::jani::Model const& model); } } }