diff --git a/src/storm/abstraction/prism/GameBddResult.cpp b/src/storm/abstraction/GameBddResult.cpp similarity index 100% rename from src/storm/abstraction/prism/GameBddResult.cpp rename to src/storm/abstraction/GameBddResult.cpp diff --git a/src/storm/abstraction/prism/GameBddResult.h b/src/storm/abstraction/GameBddResult.h similarity index 100% rename from src/storm/abstraction/prism/GameBddResult.h rename to src/storm/abstraction/GameBddResult.h diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index ad836a318..e8bc703bd 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -10,9 +10,15 @@ namespace storm { template class MenuGameAbstractor { public: + /// Retrieves the abstraction. virtual storm::abstraction::MenuGame abstract() = 0; + + /// Methods to refine the abstraction. virtual void refine(std::vector const& predicates) = 0; virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) = 0; + + /// Exports a representation of the current abstraction state in the dot format. + virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const = 0; }; } diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h index 2e7b65689..5a67d4a30 100644 --- a/src/storm/abstraction/prism/AbstractCommand.h +++ b/src/storm/abstraction/prism/AbstractCommand.h @@ -7,7 +7,7 @@ #include "storm/abstraction/LocalExpressionInformation.h" #include "storm/abstraction/StateSetAbstractor.h" -#include "storm/abstraction/prism/GameBddResult.h" +#include "storm/abstraction/GameBddResult.h" #include "storm/storage/expressions/ExpressionEvaluator.h" @@ -44,10 +44,10 @@ namespace storm { template class BottomStateResult; + template + struct GameBddResult; + namespace prism { - template - struct GameBddResult; - template class AbstractCommand { public: diff --git a/src/storm/abstraction/prism/AbstractModule.cpp b/src/storm/abstraction/prism/AbstractModule.cpp index 8630e28a3..24de6ba15 100644 --- a/src/storm/abstraction/prism/AbstractModule.cpp +++ b/src/storm/abstraction/prism/AbstractModule.cpp @@ -2,7 +2,7 @@ #include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/prism/GameBddResult.h" +#include "storm/abstraction/GameBddResult.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" diff --git a/src/storm/abstraction/prism/AbstractModule.h b/src/storm/abstraction/prism/AbstractModule.h index b507a39e5..b51be372e 100644 --- a/src/storm/abstraction/prism/AbstractModule.h +++ b/src/storm/abstraction/prism/AbstractModule.h @@ -20,11 +20,11 @@ namespace storm { template struct BottomStateResult; - + + template + struct GameBddResult; + namespace prism { - template - struct GameBddResult; - template class AbstractModule { public: diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp index e108945e5..29e627806 100644 --- a/src/storm/abstraction/prism/AbstractProgram.cpp +++ b/src/storm/abstraction/prism/AbstractProgram.cpp @@ -1,6 +1,7 @@ #include "storm/abstraction/prism/AbstractProgram.h" #include "storm/abstraction/BottomStateResult.h" +#include "storm/abstraction/GameBddResult.h" #include "storm/storage/BitVector.h" diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index a99c202ac..7214a380e 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -17,7 +17,7 @@ namespace storm { virtual void refine(std::vector const& predicates) override; virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) override; - void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const; + void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const override; private: /// The abstract program that performs the actual abstraction. diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 26c6f77ac..a6133da95 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -1,6 +1,8 @@ #ifndef STORM_ENTRYPOINTS_H_H #define STORM_ENTRYPOINTS_H_H +#include + #include "storm/utility/storm.h" #include "storm/storage/SymbolicModelDescription.h" @@ -9,6 +11,7 @@ #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/InvalidTypeException.h" namespace storm { namespace cli { @@ -113,13 +116,10 @@ namespace storm { template void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { - STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotImplementedException, "Abstraction-refinement is currently only available for PRISM programs."); - storm::prism::Program const& program = model.asPrismProgram(); - typedef double ValueType; for (auto const& property : properties) { std::cout << std::endl << "Model checking property: " << property << " ..."; - std::unique_ptr result(storm::verifyProgramWithAbstractionRefinementEngine(program, property.getFilter().getFormula(), onlyInitialStatesRelevant)); + std::unique_ptr result(storm::verifySymbolicModelWithAbstractionRefinementEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -309,6 +309,7 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + STORM_LOG_THROW((std::is_same::value), storm::exceptions::InvalidTypeException, "The value type is not supported by abstraction refinement."); auto ddlib = storm::settings::getModule().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { verifySymbolicModelWithAbstractionRefinementEngine(model, formulas, onlyInitialStatesRelevant); diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 2f817e3d1..435a25e45 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -160,7 +160,14 @@ namespace storm { storm::logic::Bound const& getBound() const { return bound.get(); } - + + /*! + * Retrieves the bound (if set). + */ + boost::optional> const& getOptionalBound() const { + return bound; + } + /*! * Retrieves whether the computation only needs to be performed qualitatively, because the values will only * be compared to 0/1. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 789a1c07c..520d2ac5e 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -32,31 +32,22 @@ namespace storm { namespace modelchecker { - namespace detail { - template - GameProb01Result::GameProb01Result(storm::utility::graph::GameProb01Result const& prob0Min, storm::utility::graph::GameProb01Result const& prob1Min, storm::utility::graph::GameProb01Result const& prob0Max, storm::utility::graph::GameProb01Result const& prob1Max) : min(std::make_pair(prob0Min, prob1Min)), max(std::make_pair(prob0Max, prob1Max)) { - // Intentionally left empty. - } - } template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : originalProgram(program), smtSolverFactory(smtSolverFactory) { - STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory) { + 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) { - preprocessedProgram = originalProgram.flattenModules(this->smtSolverFactory); + preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory); } else { - preprocessedProgram = originalProgram; + preprocessedModel = originalProgram; } } - template - GameBasedMdpModelChecker::~GameBasedMdpModelChecker() { - // Intentionally left empty. - } - template bool GameBasedMdpModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); @@ -67,32 +58,15 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - std::map labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping(); - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping)); + std::map labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); } template std::unique_ptr GameBasedMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); - std::map labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping(); - return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), originalProgram.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping)); - } - - template - bool getResultConsideringBound(ValueType const& value, storm::logic::Bound const& bound) { - if (storm::logic::isLowerBound(bound.comparisonType)) { - if (storm::logic::isStrict(bound.comparisonType)) { - return value > bound.threshold; - } else { - return value >= bound.threshold; - } - } else { - if (storm::logic::isStrict(bound.comparisonType)) { - return value < bound.threshold; - } else { - return value <= bound.threshold; - } - } + std::map labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping(); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping)); } template @@ -108,14 +82,15 @@ namespace storm { std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { std::unique_ptr result; - if (checkTask.isBoundSet()) { - if (player2Direction == storm::OptimizationDirection::Minimize && storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + boost::optional> const& bound = checkTask.getOptionalBound(); + if (bound) { + if (player2Direction == storm::OptimizationDirection::Minimize && storm::logic::isLowerBound(bound.get().comparisonType)) { if ((prob1 && initialStates) == initialStates) { result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); } else if (checkTask.isQualitativeSet()) { result = std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); } - } else if (player2Direction == storm::OptimizationDirection::Maximize && !storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + } else if (player2Direction == storm::OptimizationDirection::Maximize && !storm::logic::isLowerBound(bound.get().comparisonType)) { if ((prob0 && initialStates) == initialStates) { result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); } else if (checkTask.isQualitativeSet()) { @@ -126,6 +101,20 @@ namespace storm { return result; } + + template + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, detail::GameProb01ResultMinMax const& qualitativeResult) { + // Check whether we can already give the answer based on the current information. + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob0Max.getPlayer1States(), true); + if (result) { + return result; + } + result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult.prob1Min.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States(), false); + if (result) { + return result; + } + return result; + } template std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, ValueType const& value) { @@ -135,27 +124,35 @@ namespace storm { // return the value because the property will definitely hold. Vice versa, if the minimum value exceeds an // upper bound or the maximum value is below a lower bound, the property will definitely not hold and we can // return the value. - if (checkTask.isBoundSet() && storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + boost::optional> const& bound = checkTask.getOptionalBound(); + if (!bound) { + return result; + } + + storm::logic::ComparisonType comparisonType = bound.get().comparisonType; + ValueType threshold = bound.get().threshold; + + if (storm::logic::isLowerBound(comparisonType)) { if (player2Direction == storm::OptimizationDirection::Minimize) { - if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold()) - || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold())) { + if ((storm::logic::isStrict(comparisonType) && value > threshold) + || (!storm::logic::isStrict(comparisonType) && value >= threshold)) { result = std::make_unique>(storm::storage::sparse::state_type(0), value); } } else { - if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold()) - || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold())) { + if ((storm::logic::isStrict(comparisonType) && value <= threshold) + || (!storm::logic::isStrict(comparisonType) && value < threshold)) { result = std::make_unique>(storm::storage::sparse::state_type(0), value); } } - } else if (checkTask.isBoundSet() && !storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + } else if (!storm::logic::isLowerBound(comparisonType)) { if (player2Direction == storm::OptimizationDirection::Maximize) { - if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold()) || - (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold())) { + if ((storm::logic::isStrict(comparisonType) && value < threshold) || + (!storm::logic::isStrict(comparisonType) && value <= threshold)) { result = std::make_unique>(storm::storage::sparse::state_type(0), value); } } else { - if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold()) || - (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold())) { + if ((storm::logic::isStrict(comparisonType) && value >= threshold) || + (!storm::logic::isStrict(comparisonType) && value > threshold)) { result = std::make_unique>(storm::storage::sparse::state_type(0), value); } } @@ -207,17 +204,17 @@ namespace storm { } template - bool refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { + void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01ResultMinMax const& qualitativeResult, storm::dd::Bdd const& transitionMatrixBdd) { STORM_LOG_TRACE("Trying refinement after qualitative check."); // Get all relevant strategies. - storm::dd::Bdd minPlayer1Strategy = prob01.min.first.getPlayer1Strategy(); - storm::dd::Bdd minPlayer2Strategy = prob01.min.first.getPlayer2Strategy(); - storm::dd::Bdd maxPlayer1Strategy = prob01.max.second.getPlayer1Strategy(); - storm::dd::Bdd maxPlayer2Strategy = prob01.max.second.getPlayer2Strategy(); + storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); + storm::dd::Bdd minPlayer2Strategy = qualitativeResult.prob0Min.getPlayer2Strategy(); + storm::dd::Bdd maxPlayer1Strategy = qualitativeResult.prob1Max.getPlayer1Strategy(); + storm::dd::Bdd maxPlayer2Strategy = qualitativeResult.prob1Max.getPlayer2Strategy(); // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 // state that is also a prob 0 state. - minPlayer1Strategy = (maxPlayer1Strategy && prob01.min.first.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); + minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); // Build the fragment of transitions that is reachable by both the min and the max strategies. storm::dd::Bdd reachableTransitions = transitionMatrixBdd && (minPlayer1Strategy || minPlayer2Strategy) && maxPlayer1Strategy && maxPlayer2Strategy; @@ -245,7 +242,7 @@ namespace storm { // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state // is found. In this case, we abort the qualitative refinement here. if (pivotStates.isZero()) { - return false; + return; } STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); @@ -267,7 +264,7 @@ namespace storm { abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; + return; } else { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); @@ -280,16 +277,15 @@ namespace storm { abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); - return true; + return; } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); } } - return false; } template - void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Add const& minResult, storm::dd::Add const& maxResult, detail::GameProb01Result const& prob01, std::pair, storm::dd::Bdd> const& minStrategyPair, std::pair, storm::dd::Bdd> const& maxStrategyPair, storm::dd::Bdd const& transitionMatrixBdd) { + void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Add const& minResult, storm::dd::Add const& maxResult, detail::GameProb01ResultMinMax const& qualitativeResult, std::pair, storm::dd::Bdd> const& minStrategyPair, std::pair, storm::dd::Bdd> const& maxStrategyPair, storm::dd::Bdd const& transitionMatrixBdd) { STORM_LOG_TRACE("Refining after quantitative check."); // Get all relevant strategies. storm::dd::Bdd minPlayer1Strategy = minStrategyPair.first; @@ -410,105 +406,80 @@ namespace storm { // Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.) // Set up initial predicates. - std::vector initialPredicates; - initialPredicates.push_back(targetStateExpression); - if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) { - initialPredicates.push_back(constraintExpression); - } + std::vector initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression); // Derive the optimization direction for player 1 (assuming menu-game abstraction). - storm::OptimizationDirection player1Direction; - if (originalProgram.isDeterministicModel()) { - player1Direction = storm::OptimizationDirection::Maximize; - } else if (checkTask.isOptimizationDirectionSet()) { - player1Direction = checkTask.getOptimizationDirection(); - } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) { - player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize; - } else { - STORM_LOG_THROW(originalProgram.isDeterministicModel(), storm::exceptions::InvalidPropertyException, "Requiring either min or max annotation in property for nondeterministic models."); - player1Direction = storm::OptimizationDirection::Maximize; - } + storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask); + + // Create the abstractor. + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedModel.asPrismProgram(), initialPredicates, smtSolverFactory); + + // TODO: create refiner and move initial predicates there. - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); + // Enter the main-loop of abstraction refinement. for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); - // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + // (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. storm::abstraction::MenuGame game = abstractor.abstract(); STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state."); - // 1.5 build a BDD from the transition matrix for various later uses. + // (2) Prepare transition matrix BDD and target state BDD for later use. storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); - - // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). - detail::GameProb01Result prob01; + storm::dd::Bdd constraintStates = game.getStates(constraintExpression); storm::dd::Bdd targetStates = game.getStates(targetStateExpression); if (player1Direction == storm::OptimizationDirection::Minimize) { targetStates |= game.getBottomStates(); } - + // #ifdef LOCAL_DEBUG // abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); // #endif + // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); - if (result) { - return result; - } - - prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); - result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States()); + detail::GameProb01ResultMinMax qualitativeResult; + std::unique_ptr result = computeProb01States(checkTask, qualitativeResult, game, player1Direction, transitionMatrixBdd, game.getInitialStates(), constraintStates, targetStates); if (result) { return result; } - - // 3. compute the states for which we know the result/for which we know there is more work to be done. - storm::dd::Bdd maybeMin = !(prob01.min.first.getPlayer1States() || prob01.min.second.getPlayer1States()) && game.getReachableStates(); - storm::dd::Bdd maybeMax = !(prob01.max.first.getPlayer1States() || prob01.max.second.getPlayer1States()) && game.getReachableStates(); + auto qualitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); + + // (4) compute the states for which we have to determine quantitative information. + storm::dd::Bdd maybeMin = !(qualitativeResult.prob0Min.getPlayer1States() || qualitativeResult.prob1Min.getPlayer1States()) && game.getReachableStates(); + storm::dd::Bdd maybeMax = !(qualitativeResult.prob0Max.getPlayer1States() || qualitativeResult.prob1Max.getPlayer1States()) && game.getReachableStates(); - // 4. if the initial states are not maybe states, then we can refine at this point. + // (5) if the initial states are not maybe states, then we can refine at this point. storm::dd::Bdd initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax); - bool qualitativeRefinement = false; if (initialMaybeStates.isZero()) { // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); - // Check whether we can already give the answer based on the current information. - result = checkForResultAfterQualitativeCheck(checkTask, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.max.first.getPlayer1States(), true); + result = checkForResultAfterQualitativeCheck(checkTask, game.getInitialStates(), qualitativeResult); if (result) { return result; + } else { + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); + + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) + // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + refineAfterQualitativeCheck(abstractor, game, qualitativeResult, transitionMatrixBdd); } - result = checkForResultAfterQualitativeCheck(checkTask, game.getInitialStates(), prob01.min.second.getPlayer1States(), prob01.max.second.getPlayer1States(), false); - if (result) { - return result; - } - - STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states."); - - // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) - // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. - qualitativeRefinement = refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); - } - - auto qualitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Qualitative step completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); - - if (!qualitativeRefinement) { + } else { // At this point, we know that we cannot answer the query without further numeric computation. STORM_LOG_TRACE("Starting numerical solution step."); auto quantitativeStart = std::chrono::high_resolution_clock::now(); // Prepare some storage that we use on-demand during the quantitative solving step. - storm::dd::Add minResult = prob01.min.second.getPlayer1States().template toAdd(); - storm::dd::Add maxResult = prob01.max.second.getPlayer1States().template toAdd(); + storm::dd::Add minResult = qualitativeResult.prob1Min.getPlayer1States().template toAdd(); + storm::dd::Add maxResult = qualitativeResult.prob1Max.getPlayer1States().template toAdd(); storm::dd::Add initialStatesAdd = game.getInitialStates().template toAdd(); - storm::dd::Bdd combinedMinPlayer1QualitativeStrategies = (prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy()); - storm::dd::Bdd combinedMinPlayer2QualitativeStrategies = (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy()); + storm::dd::Bdd combinedMinPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy()); + storm::dd::Bdd combinedMinPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy()); // The minimal value after qualitative checking can only be zero. It it was 1, we could have given // the result right away. @@ -516,7 +487,7 @@ namespace storm { MaybeStateResult minMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); auto minStart = std::chrono::high_resolution_clock::now(); if (!maybeMin.isZero()) { - minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); + minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, qualitativeResult.prob1Min.getPlayer1States()); minMaybeStateResult.player1Strategy &= game.getReachableStates(); minMaybeStateResult.player2Strategy &= game.getReachableStates(); minResult += minMaybeStateResult.values; @@ -537,8 +508,8 @@ namespace storm { return result; } - storm::dd::Bdd combinedMaxPlayer1QualitativeStrategies = (prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy()); - storm::dd::Bdd combinedMaxPlayer2QualitativeStrategies = (prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy()); + storm::dd::Bdd combinedMaxPlayer1QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer1Strategy() || qualitativeResult.prob1Max.getPlayer1Strategy()); + storm::dd::Bdd combinedMaxPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy()); // Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have // given the result right awy. @@ -546,7 +517,7 @@ namespace storm { auto maxStart = std::chrono::high_resolution_clock::now(); MaybeStateResult maxMaybeStateResult(game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); if (!maybeMax.isZero()) { - maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.getPlayer1States(), boost::make_optional(minMaybeStateResult)); + maxMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, qualitativeResult.prob1Max.getPlayer1States(), boost::make_optional(minMaybeStateResult)); maxMaybeStateResult.player1Strategy &= game.getReachableStates(); maxMaybeStateResult.player2Strategy &= game.getReachableStates(); maxResult += maxMaybeStateResult.values; @@ -590,7 +561,7 @@ namespace storm { storm::dd::Bdd commonReach = storm::utility::dd::computeReachableStates(game.getInitialStates(), tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables()); STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide."); - refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); + refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, qualitativeResult, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } auto iterationEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); @@ -601,19 +572,61 @@ namespace storm { } template - std::pair, storm::utility::graph::GameProb01Result> GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - // Compute the states with probability 0/1. - storm::utility::graph::GameProb01Result prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); - storm::utility::graph::GameProb01Result prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + std::vector GameBasedMdpModelChecker::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { + std::vector initialPredicates; + initialPredicates.push_back(targetStateExpression); + if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) { + initialPredicates.push_back(constraintExpression); + } + return initialPredicates; + } + + template + storm::OptimizationDirection GameBasedMdpModelChecker::getPlayer1Direction(CheckTask const& checkTask) { + if (preprocessedModel.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { + return storm::OptimizationDirection::Maximize; + } else if (checkTask.isOptimizationDirectionSet()) { + return checkTask.getOptimizationDirection(); + } else if (checkTask.isBoundSet() && preprocessedModel.getModelType() != storm::storage::SymbolicModelDescription::ModelType::DTMC) { + return storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not derive player 1 optimization direction."); + return storm::OptimizationDirection::Maximize; + } + + template + std::unique_ptr GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, detail::GameProb01ResultMinMax& qualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + qualitativeResult.prob0Min = computeProb01States(true, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); + qualitativeResult.prob1Min = computeProb01States(false, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); + if (result) { + return result; + } - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer1Strategy() && (prob0.getPlayer1States().isZero() || !prob0.getPlayer1Strategy().isZero())), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || (prob0.hasPlayer2Strategy() && (prob0.getPlayer1States().isZero() || !prob0.getPlayer2Strategy().isZero())), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer1Strategy() && (prob1.getPlayer1States().isZero() || !prob1.getPlayer1Strategy().isZero())), "Unable to proceed without strategy."); - STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || (prob1.hasPlayer2Strategy() && (prob1.getPlayer1States().isZero() || !prob1.getPlayer2Strategy().isZero())), "Unable to proceed without strategy."); + qualitativeResult.prob0Max = computeProb01States(true, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates); + qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates); + result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); + if (result) { + return result; + } + return result; + } + + template + storm::utility::graph::GameProb01Result GameBasedMdpModelChecker::computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + storm::utility::graph::GameProb01Result result; + if (prob0) { + result = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + } else { + result = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + } + + STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); - STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.getPlayer1States().getNonZeroCount() << " 'no' states, " << prob1.getPlayer1States().getNonZeroCount() << " 'yes' states."); + STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states."); - return std::make_pair(prob0, prob1); + return result; } template @@ -621,11 +634,11 @@ namespace storm { STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); storm::expressions::Expression result; if (formula.isAtomicLabelFormula()) { - result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel()); + result = preprocessedModel.asPrismProgram().getLabelExpression(formula.asAtomicLabelFormula().getLabel()); } else if (formula.isAtomicExpressionFormula()) { result = formula.asAtomicExpressionFormula().getExpression(); } else { - result = formula.asBooleanLiteralFormula().isTrueFormula() ? originalProgram.getManager().boolean(true) : originalProgram.getManager().boolean(false); + result = formula.asBooleanLiteralFormula().isTrueFormula() ? preprocessedModel.getManager().boolean(true) : preprocessedModel.getManager().boolean(false); } return result; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 3323d55a4..68e949b50 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -7,6 +7,10 @@ #include "storm/storage/dd/DdType.h" +#include "storm/storage/SymbolicModelDescription.h" + +#include "storm/logic/Bound.h" + #include "storm/utility/solver.h" #include "storm/utility/graph.h" @@ -19,13 +23,14 @@ namespace storm { namespace modelchecker { namespace detail { template - struct GameProb01Result { + struct GameProb01ResultMinMax { public: - GameProb01Result() = default; - GameProb01Result(storm::utility::graph::GameProb01Result const& prob0Min, storm::utility::graph::GameProb01Result const& prob1Min, storm::utility::graph::GameProb01Result const& prob0Max, storm::utility::graph::GameProb01Result const& prob1Max); - - std::pair, storm::utility::graph::GameProb01Result> min; - std::pair, storm::utility::graph::GameProb01Result> max; + GameProb01ResultMinMax() = default; + + storm::utility::graph::GameProb01Result prob0Min; + storm::utility::graph::GameProb01Result prob1Min; + storm::utility::graph::GameProb01Result prob0Max; + storm::utility::graph::GameProb01Result prob1Max; }; } @@ -38,33 +43,49 @@ namespace storm { * Constructs a model checker whose underlying model is implicitly given by the provided program. All * verification calls will be answererd with respect to this model. * - * @param program The program that implicitly specifies the model to check. + * @param model The model description that (symbolically) specifies the model to check. * @param smtSolverFactory A factory used to create SMT solver when necessary. */ - explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); + explicit GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory = std::make_shared()); - virtual ~GameBasedMdpModelChecker() override; - + /// Overridden methods from super class. virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; private: + /*! + * Performs the core part of the abstraction-refinement loop. + */ std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - std::pair, storm::utility::graph::GameProb01Result> computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + /*! + * Retrieves the initial predicates for the abstraction. + */ + std::vector getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + + /*! + * Derives the optimization direction of player 1. + */ + storm::OptimizationDirection getPlayer1Direction(CheckTask const& checkTask); - storm::expressions::Expression getExpression(storm::logic::Formula const& formula); + /*! + * Performs a qualitative check on the the given game to compute the (player 1) states that have probability + * 0 or 1, respectively, to reach a target state and only visiting constraint states before. + */ + std::unique_ptr computeProb01States(CheckTask const& checkTask, detail::GameProb01ResultMinMax& qualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + storm::utility::graph::GameProb01Result computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - // The original program that was used to create this model checker. - storm::prism::Program originalProgram; + /* + * Retrieves the expression characterized by the formula. The formula needs to be propositional. + */ + storm::expressions::Expression getExpression(storm::logic::Formula const& formula); - // The preprocessed program that contains only one module and otherwhise corresponds to the semantics of the - // original program. - storm::prism::Program preprocessedProgram; + /// The preprocessed model that contains only one module/automaton and otherwhise corresponds to the semantics + /// of the original model description. + storm::storage::SymbolicModelDescription preprocessedModel; - // A factory that is used for creating SMT solvers when needed. + /// A factory that is used for creating SMT solvers when needed. std::shared_ptr smtSolverFactory; }; } diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index f944f38d6..c156dc176 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -5,6 +5,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/InvalidTypeException.h" namespace storm { namespace storage { @@ -39,6 +40,38 @@ namespace storm { return modelDescription.get().which() == 1; } + SymbolicModelDescription::ModelType SymbolicModelDescription::getModelType() const { + if (this->isJaniModel()) { + storm::jani::Model const& janiModel = this->asJaniModel(); + switch (janiModel.getModelType()) { + case storm::jani::ModelType::DTMC: return SymbolicModelDescription::ModelType::DTMC; + case storm::jani::ModelType::CTMC: return SymbolicModelDescription::ModelType::CTMC; + case storm::jani::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP; + case storm::jani::ModelType::MA: return SymbolicModelDescription::ModelType::MA; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other JANI model type."); + } + } else { + storm::prism::Program const& prismProgram = this->asPrismProgram(); + switch (prismProgram.getModelType()) { + case storm::prism::Program::ModelType::DTMC: return SymbolicModelDescription::ModelType::DTMC; + case storm::prism::Program::ModelType::CTMC: return SymbolicModelDescription::ModelType::CTMC; + case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP; + case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type."); + } + } + } + + storm::expressions::ExpressionManager& SymbolicModelDescription::getManager() const { + if (this->isPrismProgram()) { + return this->asPrismProgram().getManager(); + } else { + return this->asJaniModel().getManager(); + } + } + void SymbolicModelDescription::setModel(storm::jani::Model const& model) { modelDescription = model; } @@ -59,7 +92,7 @@ namespace storm { std::vector SymbolicModelDescription::getParameterNames() const { std::vector result; - if(isJaniModel()) { + if (isJaniModel()) { for(auto const& c : asJaniModel().getUndefinedConstants()) { result.push_back(c.get().getName()); } diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index a76ae084a..e576b8866 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -10,6 +10,10 @@ namespace storm { class SymbolicModelDescription { public: + enum class ModelType { + DTMC, CTMC, MDP, MA + }; + SymbolicModelDescription() = default; SymbolicModelDescription(storm::jani::Model const& model); SymbolicModelDescription(storm::prism::Program const& program); @@ -20,6 +24,9 @@ namespace storm { bool hasModel() const; bool isJaniModel() const; bool isPrismProgram() const; + + ModelType getModelType() const; + storm::expressions::ExpressionManager& getManager() const; void setModel(storm::jani::Model const& model); void setModel(storm::prism::Program const& program); diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 07307c917..abac269f6 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -577,15 +577,16 @@ namespace storm { } template - std::unique_ptr verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); + std::unique_ptr verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - if (program.isDeterministicModel()) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(program); + STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); + + if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); return modelchecker.check(task); } else { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(program); + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); return modelchecker.check(task); }