sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

started on optimizing bisimulation-based abstraction-refinement

tempestpy_adaptions
dehnert 7 years ago
parent
669940ccd3
commit
4fad33b5e8
17 changed files with 325 additions and 159 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm/abstraction/MenuGameRefiner.cpp
  2. 8
      src/storm/abstraction/MenuGameRefiner.h
  3. 2
      src/storm/abstraction/QualitativeGameResult.h
  4. 4
      src/storm/abstraction/QualitativeGameResultMinMax.h
  5. 13
      src/storm/abstraction/QualitativeMdpResult.h
  6. 21
      src/storm/abstraction/QualitativeMdpResultMinMax.h
  7. 6
      src/storm/abstraction/QuantitativeGameResult.h
  8. 21
      src/storm/abstraction/QuantitativeGameResultMinMax.h
  9. 21
      src/storm/abstraction/QuantitativeResultMinMax.h
  10. 30
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  11. 8
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
  12. 190
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
  13. 32
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
  14. 11
      src/storm/modelchecker/hints/ModelCheckerHint.h
  15. 2
      src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
  16. 15
      src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  17. 4
      src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h

6
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -120,7 +120,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
PivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<QualitativeResultMinMax<Type>> const& qualitativeResult, boost::optional<QuantitativeResultMinMax<Type, ValueType>> const& quantitativeResult) {
PivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<QualitativeGameResultMinMax<Type>> const& qualitativeResult, boost::optional<QuantitativeGameResultMinMax<Type, ValueType>> const& quantitativeResult) {
// Get easy access to strategies. // Get easy access to strategies.
storm::dd::Bdd<Type> minPlayer1Strategy; storm::dd::Bdd<Type> minPlayer1Strategy;
@ -571,7 +571,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) const {
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeGameResultMinMax<Type> const& qualitativeResult) const {
STORM_LOG_TRACE("Trying refinement after qualitative check."); STORM_LOG_TRACE("Trying refinement after qualitative check.");
// Get all relevant strategies. // Get all relevant strategies.
storm::dd::Bdd<Type> minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); storm::dd::Bdd<Type> minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy();
@ -616,7 +616,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const {
bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const {
STORM_LOG_TRACE("Refining after quantitative check."); STORM_LOG_TRACE("Refining after quantitative check.");
// Get all relevant strategies. // Get all relevant strategies.
storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy; storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy;

8
src/storm/abstraction/MenuGameRefiner.h
View File

@ -7,8 +7,8 @@
#include <boost/optional.hpp> #include <boost/optional.hpp>
#include "storm/abstraction/RefinementCommand.h" #include "storm/abstraction/RefinementCommand.h"
#include "storm/abstraction/QualitativeResultMinMax.h"
#include "storm/abstraction/QuantitativeResultMinMax.h"
#include "storm/abstraction/QualitativeGameResultMinMax.h"
#include "storm/abstraction/QuantitativeGameResultMinMax.h"
#include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/FullPredicateSplitter.h" #include "storm/storage/expressions/FullPredicateSplitter.h"
@ -85,14 +85,14 @@ namespace storm {
* *
* @param True if predicates for refinement could be derived, false otherwise. * @param True if predicates for refinement could be derived, false otherwise.
*/ */
bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) const;
bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeGameResultMinMax<Type> const& qualitativeResult) const;
/*! /*!
* Refines the abstractor based on the quantitative result by trying to derive suitable predicates. * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
* *
* @param True if predicates for refinement could be derived, false otherwise. * @param True if predicates for refinement could be derived, false otherwise.
*/ */
bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const;
bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const;
/*! /*!
* Retrieves whether all guards were added. * Retrieves whether all guards were added.

2
src/storm/abstraction/QualitativeResult.h → src/storm/abstraction/QualitativeGameResult.h
View File

@ -6,7 +6,7 @@ namespace storm {
namespace abstraction { namespace abstraction {
template <storm::dd::DdType Type> template <storm::dd::DdType Type>
using QualitativeResult = storm::utility::graph::GameProb01Result<Type>;
using QualitativeGameResult = storm::utility::graph::GameProb01Result<Type>;
} }
} }

4
src/storm/abstraction/QualitativeResultMinMax.h → src/storm/abstraction/QualitativeGameResultMinMax.h
View File

@ -8,9 +8,9 @@ namespace storm {
namespace abstraction { namespace abstraction {
template<storm::dd::DdType Type> template<storm::dd::DdType Type>
struct QualitativeResultMinMax {
struct QualitativeGameResultMinMax {
public: public:
QualitativeResultMinMax() = default;
QualitativeGameResultMinMax() = default;
storm::utility::graph::GameProb01Result<Type> prob0Min; storm::utility::graph::GameProb01Result<Type> prob0Min;
storm::utility::graph::GameProb01Result<Type> prob1Min; storm::utility::graph::GameProb01Result<Type> prob1Min;

13
src/storm/abstraction/QualitativeMdpResult.h
View File

@ -0,0 +1,13 @@
#pragma once
#include "storm/utility/graph.h"
namespace storm {
namespace abstraction {
template <storm::dd::DdType Type>
using QualitativeMdpResult = std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>>;
}
}

21
src/storm/abstraction/QualitativeMdpResultMinMax.h
View File

@ -0,0 +1,21 @@
#pragma once
#include "storm/storage/dd/DdType.h"
#include "storm/abstraction/QualitativeMdpResult.h"
namespace storm {
namespace abstraction {
template<storm::dd::DdType Type>
struct QualitativeMdpResultMinMax {
public:
QualitativeMdpResultMinMax() = default;
QualitativeMdpResult<Type> min;
QualitativeMdpResult<Type> max;
};
}
}

6
src/storm/abstraction/QuantitativeResult.h → src/storm/abstraction/QuantitativeGameResult.h
View File

@ -8,10 +8,10 @@ namespace storm {
namespace abstraction { namespace abstraction {
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
struct QuantitativeResult {
QuantitativeResult() = default;
struct QuantitativeGameResult {
QuantitativeGameResult() = default;
QuantitativeResult(std::pair<ValueType, ValueType> initialStatesRange, storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
QuantitativeGameResult(std::pair<ValueType, ValueType> initialStatesRange, storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
// Intentionally left empty. // Intentionally left empty.
} }

21
src/storm/abstraction/QuantitativeGameResultMinMax.h
View File

@ -0,0 +1,21 @@
#pragma once
#include "storm/abstraction/QuantitativeGameResult.h"
namespace storm {
namespace abstraction {
template<storm::dd::DdType Type, typename ValueType>
struct QuantitativeGameResultMinMax {
QuantitativeGameResultMinMax() = default;
QuantitativeGameResultMinMax(QuantitativeGameResult<Type, ValueType> const& min, QuantitativeGameResult<Type, ValueType> const& max) : min(min), max(max) {
// Intentionally left empty.
}
QuantitativeGameResult<Type, ValueType> min;
QuantitativeGameResult<Type, ValueType> max;
};
}
}

21
src/storm/abstraction/QuantitativeResultMinMax.h
View File

@ -1,21 +0,0 @@
#pragma once
#include "storm/abstraction/QuantitativeResult.h"
namespace storm {
namespace abstraction {
template<storm::dd::DdType Type, typename ValueType>
struct QuantitativeResultMinMax {
QuantitativeResultMinMax() = default;
QuantitativeResultMinMax(QuantitativeResult<Type, ValueType> const& min, QuantitativeResult<Type, ValueType> const& max) : min(min), max(max) {
// Intentionally left empty.
}
QuantitativeResult<Type, ValueType> min;
QuantitativeResult<Type, ValueType> max;
};
}
}

30
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -47,8 +47,8 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
using storm::abstraction::QuantitativeResult;
using storm::abstraction::QuantitativeResultMinMax;
using storm::abstraction::QuantitativeGameResult;
using storm::abstraction::QuantitativeGameResultMinMax;
template<storm::dd::DdType Type, typename ModelType> template<storm::dd::DdType Type, typename ModelType>
GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) { GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) {
@ -161,7 +161,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<Type> const& initialStates, QualitativeResultMinMax<Type> const& qualitativeResult) {
std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<Type> const& initialStates, QualitativeGameResultMinMax<Type> const& qualitativeResult) {
// Check whether we can already give the answer based on the current information. // Check whether we can already give the answer based on the current information.
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States());
if (result) { if (result) {
@ -234,7 +234,7 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
QuantitativeResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<QuantitativeResult<Type, ValueType>> const& startInfo = boost::none) {
QuantitativeGameResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<QuantitativeGameResult<Type, ValueType>> const& startInfo = boost::none) {
STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
@ -261,14 +261,14 @@ namespace storm {
std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
solver->setGeneratePlayersStrategies(true); solver->setGeneratePlayersStrategies(true);
auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none);
return QuantitativeResult<Type, ValueType>(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
return QuantitativeGameResult<Type, ValueType>(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
QuantitativeResult<Type, ValueType> computeQuantitativeResult(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, QualitativeResultMinMax<Type> const& qualitativeResult, storm::dd::Add<Type, ValueType> const& initialStatesAdd, storm::dd::Bdd<Type> const& maybeStates, boost::optional<QuantitativeResult<Type, ValueType>> const& startInfo = boost::none) {
QuantitativeGameResult<Type, ValueType> computeQuantitativeResult(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, QualitativeGameResultMinMax<Type> const& qualitativeResult, storm::dd::Add<Type, ValueType> const& initialStatesAdd, storm::dd::Bdd<Type> const& maybeStates, boost::optional<QuantitativeGameResult<Type, ValueType>> const& startInfo = boost::none) {
bool min = player2Direction == storm::OptimizationDirection::Minimize; bool min = player2Direction == storm::OptimizationDirection::Minimize;
QuantitativeResult<Type, ValueType> result;
QuantitativeGameResult<Type, ValueType> result;
// We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative // We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative
// preprocessing if possible. // preprocessing if possible.
@ -352,8 +352,8 @@ namespace storm {
storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression); storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
// Enter the main-loop of abstraction refinement. // Enter the main-loop of abstraction refinement.
boost::optional<QualitativeResultMinMax<Type>> previousQualitativeResult = boost::none;
boost::optional<QuantitativeResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
boost::optional<QualitativeGameResultMinMax<Type>> previousQualitativeResult = boost::none;
boost::optional<QuantitativeGameResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
auto iterationStart = std::chrono::high_resolution_clock::now(); auto iterationStart = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Starting iteration " << iterations << "."); STORM_LOG_TRACE("Starting iteration " << iterations << ".");
@ -382,7 +382,7 @@ namespace storm {
// (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). // (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(); auto qualitativeStart = std::chrono::high_resolution_clock::now();
QualitativeResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
QualitativeGameResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult); std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
if (result) { if (result) {
printStatistics(*abstractor, game); printStatistics(*abstractor, game);
@ -426,7 +426,7 @@ namespace storm {
STORM_LOG_TRACE("Starting numerical solution step."); STORM_LOG_TRACE("Starting numerical solution step.");
auto quantitativeStart = std::chrono::high_resolution_clock::now(); auto quantitativeStart = std::chrono::high_resolution_clock::now();
QuantitativeResultMinMax<Type, ValueType> quantitativeResult;
QuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
// (7) Solve the min values and check whether we can give the answer already. // (7) Solve the min values and check whether we can give the answer already.
quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
@ -513,7 +513,7 @@ namespace storm {
} }
template<storm::dd::DdType Type> template<storm::dd::DdType Type>
bool checkQualitativeStrategies(bool prob0, QualitativeResult<Type> const& result, storm::dd::Bdd<Type> const& targetStates) {
bool checkQualitativeStrategies(bool prob0, QualitativeGameResult<Type> const& result, storm::dd::Bdd<Type> const& targetStates) {
if (prob0) { if (prob0) {
STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
} else { } else {
@ -526,7 +526,7 @@ namespace storm {
} }
template<storm::dd::DdType Type> template<storm::dd::DdType Type>
bool checkQualitativeStrategies(QualitativeResultMinMax<Type> const& qualitativeResult, storm::dd::Bdd<Type> const& targetStates) {
bool checkQualitativeStrategies(QualitativeGameResultMinMax<Type> const& qualitativeResult, storm::dd::Bdd<Type> const& targetStates) {
bool result = true; bool result = true;
result &= checkQualitativeStrategies(true, qualitativeResult.prob0Min, targetStates); result &= checkQualitativeStrategies(true, qualitativeResult.prob0Min, targetStates);
result &= checkQualitativeStrategies(false, qualitativeResult.prob1Min, targetStates); result &= checkQualitativeStrategies(false, qualitativeResult.prob1Min, targetStates);
@ -536,9 +536,9 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ModelType> template<storm::dd::DdType Type, typename ModelType>
QualitativeResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
QualitativeGameResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<QualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
QualitativeResultMinMax<Type> result;
QualitativeGameResultMinMax<Type> result;
if (reuseQualitativeResults) { if (reuseQualitativeResults) {
// Depending on the player 1 direction, we choose a different order of operations. // Depending on the player 1 direction, we choose a different order of operations.

8
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
View File

@ -10,7 +10,7 @@
#include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/SymbolicModelDescription.h"
#include "storm/abstraction/QualitativeResult.h" #include "storm/abstraction/QualitativeResult.h"
#include "storm/abstraction/QualitativeResultMinMax.h"
#include "storm/abstraction/QualitativeGameResultMinMax.h"
#include "storm/logic/Bound.h" #include "storm/logic/Bound.h"
@ -29,8 +29,8 @@ namespace storm {
namespace modelchecker { namespace modelchecker {
using storm::abstraction::QualitativeResult;
using storm::abstraction::QualitativeResultMinMax;
using storm::abstraction::QualitativeGameResult;
using storm::abstraction::QualitativeGameResultMinMax;
template<storm::dd::DdType Type, typename ModelType> template<storm::dd::DdType Type, typename ModelType>
class GameBasedMdpModelChecker : public AbstractModelChecker<ModelType> { class GameBasedMdpModelChecker : public AbstractModelChecker<ModelType> {
@ -71,7 +71,7 @@ namespace storm {
* Performs a qualitative check on the the given game to compute the (player 1) states that have probability * 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. * 0 or 1, respectively, to reach a target state and only visiting constraint states before.
*/ */
QualitativeResultMinMax<Type> computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
QualitativeGameResultMinMax<Type> computeProb01States(boost::optional<QualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const; void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;

190
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
View File

@ -6,6 +6,7 @@
#include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
@ -15,6 +16,8 @@
#include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/BisimulationDecomposition.h" #include "storm/storage/dd/BisimulationDecomposition.h"
#include "storm/abstraction/QualitativeMdpResultMinMax.h"
#include "storm/settings/SettingsManager.h" #include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/AbstractionSettings.h"
@ -41,28 +44,28 @@ namespace storm {
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) { std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
return computeValuesAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) { std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
return computeValuesAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) { std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations."); STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations.");
return computeValuesAbstractionRefinement(true, checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
return computeValuesAbstractionRefinement(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeValuesAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask) {
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
// Create the appropriate preservation information. // Create the appropriate preservation information.
storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, {checkTask.getFormula().asSharedPointer()}); storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, {checkTask.getFormula().asSharedPointer()});
if (rewards) {
if (checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward) {
if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) { if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) {
preservationInformation.addRewardModel(model.getUniqueRewardModelName()); preservationInformation.addRewardModel(model.getUniqueRewardModelName());
} else if (checkTask.isRewardModelSet()) { } else if (checkTask.isRewardModelSet()) {
@ -85,10 +88,21 @@ namespace storm {
if (fullQuotient) { if (fullQuotient) {
STORM_LOG_TRACE("Reached final quotient."); STORM_LOG_TRACE("Reached final quotient.");
quotient->printModelInformationToStream(std::cout); quotient->printModelInformationToStream(std::cout);
result = computeResultFullQuotient(*quotient, rewards, checkTask);
result = computeResultFullQuotient(*quotient, checkTask);
} else { } else {
// Obtain lower and upper bounds from the partial quotient. // Obtain lower and upper bounds from the partial quotient.
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> bounds = computeBoundsPartialQuotient(*quotient, rewards, checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> bounds = computeBoundsPartialQuotient(*quotient, checkTask);
// If either of the two bounds does not exist, the answer can be derived from the existing bounds.
if (bounds.first == nullptr || bounds.second == nullptr) {
STORM_LOG_ASSERT(bounds.first || bounds.second, "Expected at least one bound.");
quotient->printModelInformationToStream(std::cout);
if (bounds.first) {
return std::move(bounds.first);
} else {
return std::move(bounds.second);
}
}
// Check whether the bounds are sufficiently close. // Check whether the bounds are sufficiently close.
bool converged = checkBoundsSufficientlyClose(bounds); bool converged = checkBoundsSufficientlyClose(bounds);
@ -153,46 +167,150 @@ namespace storm {
return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber<ValueType>(std::string("2.0")))); return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber<ValueType>(std::string("2.0"))));
} }
static int i = 0;
template<typename ModelType>
typename PartialBisimulationMdpModelChecker<ModelType>::ValueType PartialBisimulationMdpModelChecker<ModelType>::getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult<ValueType> const& result) {
if (dir == storm::OptimizationDirection::Minimize) {
return result.getMin();
} else {
return result.getMax();
}
}
template<typename ModelType> template<typename ModelType>
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
bool PartialBisimulationMdpModelChecker<ModelType>::boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold) {
if (lowerBounds) {
if (storm::logic::isLowerBound(comparisonType)) {
ValueType minimalLowerBound = getExtremalBound(storm::OptimizationDirection::Minimize, result);
return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold);
} else {
ValueType maximalLowerBound = getExtremalBound(storm::OptimizationDirection::Maximize, result);
return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold);
}
} else {
if (storm::logic::isLowerBound(comparisonType)) {
ValueType minimalUpperBound = getExtremalBound(storm::OptimizationDirection::Minimize, result);
return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold);
} else {
ValueType maximalUpperBound = getExtremalBound(storm::OptimizationDirection::Maximize, result);
return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold);
}
}
}
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>>& checker, storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::OptimizationDirection const& dir, CheckTask<storm::logic::Formula>& checkTask) {
CheckTask<storm::logic::Formula> newCheckTask(checkTask);
SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Minimize);
std::unique_ptr<CheckResult> result;
checkTask.setOptimizationDirection(dir);
if (rewards) { if (rewards) {
result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation,newCheckTask);
result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask);
} else { } else {
result.first = checker.computeProbabilities(newCheckTask);
result = checker.computeProbabilities(checkTask);
}
STORM_LOG_ASSERT(result, "Expected result.");
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
return result;
} }
STORM_LOG_ASSERT(result.first, "Expected result.");
result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot");
result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize);
if (rewards) {
result.second = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask);
template<typename ModelType>
std::pair<storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>, storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>> PartialBisimulationMdpModelChecker<ModelType>::getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> result;
SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
if (checkTask.getFormula().isUntilFormula()) {
std::unique_ptr<CheckResult> subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula());
result.first = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
subresult = checker.check(checkTask.getFormula().asUntilFormula().getRightSubformula());
result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
} else if (checkTask.getFormula().isEventuallyFormula()) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula().asEventuallyFormula();
result.first = quotient.getReachableStates();
std::unique_ptr<CheckResult> subresult = checker.check(eventuallyFormula.getSubformula());
result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula is not supported by this model checker.");
}
return result;
}
template<typename ModelType>
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
// We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part.
// Preparation: determine the constraint states and the target states of the reachability objective.
bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask);
// Phase (1): solve qualitatively.
storm::abstraction::QualitativeMdpResultMinMax<DdType> qualitativeResults;
storm::dd::Bdd<DdType> transitionMatrixBdd = quotient.getTransitionMatrix().notZero();
if (isRewardFormula) {
qualitativeResults.min.second = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second));
qualitativeResults.max.second = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, constraintTargetStates.first, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second));
} else { } else {
result.second = checker.computeProbabilities(newCheckTask);
qualitativeResults.min = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second);
qualitativeResults.max = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second);
} }
STORM_LOG_ASSERT(result.second, "Expected result.");
result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot");
result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
// CheckTask<storm::logic::Formula> newCheckTask(checkTask);
//
// if (!checkTask.isBoundSet() || storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
// // Check whether we can answer the query (lower bound above bound).
// result.first = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Minimize, newCheckTask);
// if (checkTask.isBoundSet()) {
// bool sufficient = boundsSufficient(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
// if (sufficient) {
// return result;
// }
// }
//
// // Check whether we can answer the query (upper bound below bound).
// result.second = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Maximize, newCheckTask);
// if (checkTask.isBoundSet()) {
// bool sufficient = boundsSufficient(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
// if (sufficient) {
// result.first = nullptr;
// return result;
// }
// }
// } else {
// // Check whether we can answer the query (upper bound below bound).
// result.second = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Maximize, newCheckTask);
// if (checkTask.isBoundSet()) {
// bool sufficient = boundsSufficient(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
// if (sufficient) {
// return result;
// }
// }
//
// // Check whether we can answer the query (lower bound above bound).
// result.first = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Minimize, newCheckTask);
// if (checkTask.isBoundSet()) {
// bool sufficient = boundsSufficient(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
// if (sufficient) {
// result.second = nullptr;
// return result;
// }
// }
// }
return result; return result;
} }
template<typename ModelType> template<typename ModelType>
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented.");
} }
template<typename ModelType> template<typename ModelType>
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
// Sanity checks. // Sanity checks.
STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
@ -200,14 +318,16 @@ namespace storm {
STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients."); STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients.");
if (modelType == storm::models::ModelType::Mdp) { if (modelType == storm::models::ModelType::Mdp) {
return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
return computeBoundsPartialQuotient(static_cast<storm::models::symbolic::Mdp<DdType, ValueType> const&>(quotient), checkTask);
} else { } else {
return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(), rewards, checkTask);
return computeBoundsPartialQuotient(static_cast<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const&>(quotient), checkTask);
} }
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> checker(quotient); SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> checker(quotient);
std::unique_ptr<CheckResult> result; std::unique_ptr<CheckResult> result;
if (rewards) { if (rewards) {
@ -220,7 +340,9 @@ namespace storm {
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient); SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
std::unique_ptr<CheckResult> result; std::unique_ptr<CheckResult> result;
if (rewards) { if (rewards) {
@ -233,7 +355,7 @@ namespace storm {
} }
template<typename ModelType> template<typename ModelType>
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
// Sanity checks. // Sanity checks.
STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient."); STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
@ -241,9 +363,9 @@ namespace storm {
STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients."); STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients.");
if (modelType == storm::models::ModelType::Dtmc) { if (modelType == storm::models::ModelType::Dtmc) {
return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), rewards, checkTask);
return computeResultFullQuotient(static_cast<storm::models::symbolic::Dtmc<DdType, ValueType> const&>(quotient), checkTask);
} else { } else {
return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
return computeResultFullQuotient(static_cast<storm::models::symbolic::Mdp<DdType, ValueType> const&>(quotient), checkTask);
} }
} }

32
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
View File

@ -4,6 +4,8 @@
#include "storm/storage/dd/DdType.h" #include "storm/storage/dd/DdType.h"
#include "storm/solver/OptimizationDirection.h"
namespace storm { namespace storm {
namespace dd { namespace dd {
template <storm::dd::DdType DdType> template <storm::dd::DdType DdType>
@ -27,6 +29,11 @@ namespace storm {
} }
namespace modelchecker { namespace modelchecker {
template <typename ModelType>
class SymbolicMdpPrctlModelChecker;
template <typename ValueType>
class QuantitativeCheckResult;
template<typename ModelType> template<typename ModelType>
class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> { class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> {
@ -46,22 +53,33 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override; virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
private: private:
std::unique_ptr<CheckResult> computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeValuesAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask);
// Methods to check for convergence and postprocessing the result. // Methods to check for convergence and postprocessing the result.
bool checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds); bool checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
std::unique_ptr<CheckResult> getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds); std::unique_ptr<CheckResult> getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
void printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds); void printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
// Retrieves the constraint and target states of the quotient wrt. to the formula in the check task.
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
// Retrieves the extremal bound (wrt. to the optimization direction) of the quantitative check result.
ValueType getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult<ValueType> const& result);
// Retrieves whether the quantitative bounds are sufficient to answer the the query given by the bound (comparison
// type and threshold).
bool boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold);
// Methods to compute bounds on the partial quotient. // Methods to compute bounds on the partial quotient.
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>>& checker, storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::OptimizationDirection const& dir, CheckTask<storm::logic::Formula>& checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
// Methods to solve the query on the full quotient. // Methods to solve the query on the full quotient.
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
// The non-abstracted model. // The non-abstracted model.
ModelType const& model; ModelType const& model;

11
src/storm/modelchecker/hints/ModelCheckerHint.h
View File

@ -1,5 +1,6 @@
#ifndef STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
#define STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
#pragma once
#include "storm/storage/dd/DdType.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
@ -15,10 +16,10 @@ namespace storm {
public: public:
ModelCheckerHint() = default; ModelCheckerHint() = default;
// Returns true iff this hint does not contain any information
// Returns true iff this hint does not contain any information.
virtual bool isEmpty() const; virtual bool isEmpty() const;
// Returns true iff this is an explicit model checker hint
// Returns true iff this is an explicit model checker hint.
virtual bool isExplicitModelCheckerHint() const; virtual bool isExplicitModelCheckerHint() const;
template<typename ValueType> template<typename ValueType>
@ -26,10 +27,8 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
ExplicitModelCheckerHint<ValueType> const& asExplicitModelCheckerHint() const; ExplicitModelCheckerHint<ValueType> const& asExplicitModelCheckerHint() const;
}; };
} }
} }
#endif /* STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H */

2
src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
View File

@ -101,7 +101,7 @@ namespace storm {
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula()); std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory);
} }
template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>; template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;

15
src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -37,7 +37,7 @@ namespace storm {
} }
template<storm::dd::DdType DdType, typename ValueType> template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues) {
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
// probability 0 and 1 of satisfying the until-formula. // probability 0 and 1 of satisfying the until-formula.
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01; std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
@ -96,7 +96,7 @@ namespace storm {
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()); solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->setRequirementsChecked(); solver->setRequirementsChecked();
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, model.getManager().template getAddZero<ValueType>(), subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero<ValueType>()) : model.getManager().template getAddZero<ValueType>(), subvector);
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + result)); return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + result));
} else { } else {
@ -189,7 +189,7 @@ namespace storm {
} }
template<storm::dd::DdType DdType, typename ValueType> template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues) {
// Only compute the result if there is at least one reward model. // Only compute the result if there is at least one reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
@ -208,12 +208,6 @@ namespace storm {
STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining)."); STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
// Check whether we need to compute exact rewards for some states.
if (qualitative) {
// Set the values for all maybe-states to 1 to indicate that their reward values
// are neither 0 nor infinity.
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
} else {
// If there are maybe states, we need to solve an equation system. // If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) { if (!maybeStates.isZero()) {
// Create the matrix and the vector for the equation system. // Create the matrix and the vector for the equation system.
@ -255,14 +249,13 @@ namespace storm {
solver->setLowerBound(storm::utility::zero<ValueType>()); solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setRequirementsChecked(); solver->setRequirementsChecked();
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, model.getManager().template getAddZero<ValueType>(), subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero<ValueType>()) : model.getManager().template getAddZero<ValueType>(), subvector);
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result))); return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result)));
} else { } else {
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()))); return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
} }
} }
}
template class SymbolicMdpPrctlHelper<storm::dd::DdType::CUDD, double>; template class SymbolicMdpPrctlHelper<storm::dd::DdType::CUDD, double>;
template class SymbolicMdpPrctlHelper<storm::dd::DdType::Sylvan, double>; template class SymbolicMdpPrctlHelper<storm::dd::DdType::Sylvan, double>;

4
src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
View File

@ -25,7 +25,7 @@ namespace storm {
static std::unique_ptr<CheckResult> computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates); static std::unique_ptr<CheckResult> computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates);
static std::unique_ptr<CheckResult> computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues = boost::none);
static std::unique_ptr<CheckResult> computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); static std::unique_ptr<CheckResult> computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
@ -33,7 +33,7 @@ namespace storm {
static std::unique_ptr<CheckResult> computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); static std::unique_ptr<CheckResult> computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues = boost::none);
}; };
} }

Write Preview
Loading…
Cancel
Save