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

added option of splitting to predicate synthesis, added equivalence checker, fixed bug that caused some commands not to be abstracted

main
dehnert 8 years ago
parent
6fe633b2c7
commit
633f4293e3
15 changed files with 308 additions and 118 deletions
Split View
  1. 17
      src/storm/abstraction/prism/AbstractCommand.cpp
  2. 3
      src/storm/abstraction/prism/AbstractCommand.h
  3. 79
      src/storm/abstraction/prism/AbstractProgram.cpp
  4. 16
      src/storm/abstraction/prism/AbstractProgram.h
  5. 8
      src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
  6. 95
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  7. 6
      src/storm/settings/modules/AbstractionSettings.cpp
  8. 8
      src/storm/settings/modules/AbstractionSettings.h
  9. 23
      src/storm/storage/expressions/EquivalenceChecker.cpp
  10. 28
      src/storm/storage/expressions/EquivalenceChecker.h
  11. 14
      src/storm/storage/expressions/Expression.h
  12. 80
      src/storm/storage/expressions/PredicateSplitter.cpp
  13. 31
      src/storm/storage/expressions/PredicateSplitter.h
  14. 6
      src/storm/utility/graph.cpp
  15. 12
      src/test/abstraction/PrismMenuGameTest.cpp

17
src/storm/abstraction/prism/AbstractCommand.cpp
View File

@ -1,5 +1,7 @@
#include "storm/abstraction/prism/AbstractCommand.h"
#include <chrono>
#include <boost/iterator/transform_iterator.hpp>
#include "storm/abstraction/AbstractionInformation.h"
@ -40,11 +42,11 @@ namespace storm {
for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
allPredicateIndices[index] = index;
}
this->refine(allPredicateIndices);
this->refine(allPredicateIndices, true);
}
template <storm::dd::DdType DdType, typename ValueType>
void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation) {
// Add all predicates to the variable partition.
for (auto predicateIndex : predicates) {
localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
@ -57,7 +59,7 @@ namespace storm {
std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
// If the DD does not need recomputation, we can return the cached result.
bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
bool recomputeDd = forceRecomputation || this->relevantPredicatesChanged(newRelevantPredicates);
if (!recomputeDd) {
// If the new predicates are unrelated to the BDD of this command, we need to multiply their identities.
cachedDd.bdd &= computeMissingGlobalIdentities();
@ -76,11 +78,14 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
auto start = std::chrono::high_resolution_clock::now();
// Create a mapping from source state DDs to their distributions.
std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) {
uint64_t numberOfSolutions = 0;
smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) {
sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model));
++numberOfSolutions;
return true;
});
@ -127,6 +132,9 @@ namespace storm {
// Cache the result.
cachedDd = GameBddResult<DdType>(resultBdd, numberOfVariablesNeeded);
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
}
template <storm::dd::DdType DdType, typename ValueType>
@ -309,6 +317,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
BottomStateResult<DdType> AbstractCommand<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get());
BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
// If the guard of this command is a predicate, there are not bottom states/transitions.

3
src/storm/abstraction/prism/AbstractCommand.h
View File

@ -65,8 +65,9 @@ namespace storm {
* Refines the abstract command with the given predicates.
*
* @param predicates The new predicates.
* @param forceRecomputation If set, the BDD is recomputed even if the relevant predicates have not changed.
*/
void refine(std::vector<uint_fast64_t> const& predicates);
void refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation = false);
/*!
* Computes the abstraction of the command wrt. to the current set of predicates.

79
src/storm/abstraction/prism/AbstractProgram.cpp
View File

@ -20,8 +20,6 @@
#include "storm-config.h"
#include "storm/adapters/CarlAdapter.h"
//#define LOCAL_DEBUG
namespace storm {
namespace abstraction {
namespace prism {
@ -30,8 +28,8 @@ namespace storm {
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
std::vector<storm::expressions::Expression> const& initialPredicates,
std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
bool addAllGuards)
: program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr) {
bool addAllGuards, bool splitPredicates)
: program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) {
// For now, we assume that there is a single module. If the program has more than one module, it needs
// to be flattened before the procedure.
@ -66,42 +64,62 @@ namespace storm {
// odds are that it's impossible to treat such models in any event.
abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
// Now that we have created all other DD variables, we create the DD variables for the predicates.
std::vector<uint_fast64_t> allPredicateIndices;
if (addAllGuards) {
for (auto const& guard : allGuards) {
allPredicateIndices.push_back(abstractionInformation.addPredicate(guard));
}
}
for (auto const& predicate : initialPredicates) {
allPredicateIndices.push_back(abstractionInformation.addPredicate(predicate));
}
// For each module of the concrete program, we create an abstract counterpart.
for (auto const& module : program.getModules()) {
this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, addAllGuards);
}
// Refine the initial state abstractors using the initial predicates.
initialStateAbstractor.refine(allPredicateIndices);
// Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
// Finally, we build the game the first time.
currentGame = buildGame();
// Now that we have created all other DD variables, we create the DD variables for the predicates.
std::vector<std::pair<storm::expressions::Expression, bool>> allPredicates;
for (auto const& predicate : initialPredicates) {
allPredicates.push_back(std::make_pair(predicate, false));
}
if (addAllGuards) {
for (auto const& guard : allGuards) {
allPredicates.push_back(std::make_pair(guard, true));
}
}
// Finally, refine using the all predicates and build game as a by-product.
this->refine(allPredicates);
}
template <storm::dd::DdType DdType, typename ValueType>
void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
void AbstractProgram<DdType, ValueType>::refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates) {
STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
// Add the predicates to the global list of predicates.
std::vector<uint_fast64_t> newPredicateIndices;
for (auto const& predicate : predicates) {
for (auto const& predicateAllowSplitPair : predicates) {
storm::expressions::Expression const& predicate = predicateAllowSplitPair.first;
bool allowSplit = predicateAllowSplitPair.second;
STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate);
newPredicateIndices.push_back(newPredicateIndex);
if (allowSplit && splitPredicates) {
// Split the predicates.
std::vector<storm::expressions::Expression> atoms = splitter.split(predicate);
// Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have.
for (auto const& atom : atoms) {
bool addAtom = true;
for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
if (equivalenceChecker.areEquivalent(atom, oldPredicate)) {
addAtom = false;
break;
}
}
if (addAtom) {
uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(atom);
newPredicateIndices.push_back(newPredicateIndex);
}
}
} else {
uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate);
newPredicateIndices.push_back(newPredicateIndex);
}
}
// Refine all abstract modules.
@ -183,8 +201,8 @@ namespace storm {
STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate.");
abstractCommand.notifyGuardIsPredicate();
storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression();
STORM_LOG_TRACE("Derived new predicate: " << newPredicate);
this->refine({newPredicate});
STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
this->refine({std::make_pair(newPredicate, true)});
} else {
STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
@ -231,6 +249,7 @@ namespace storm {
for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
// Now we know the point of the deviation (command, update, predicate).
std::cout << "pred: " << abstractionInformation.getPredicateByIndex(predicateIndex) << " and update " << concreteCommand.getUpdate(updateIndex) << std::endl;
newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
break;
}
@ -239,9 +258,9 @@ namespace storm {
}
STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
STORM_LOG_TRACE("Derived new predicate: " << newPredicate);
STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
this->refine({newPredicate});
this->refine({std::make_pair(newPredicate, true)});
}
STORM_LOG_TRACE("Current set of predicates:");
@ -299,7 +318,9 @@ namespace storm {
}
// Construct the transition matrix by cutting away the transitions of unreachable states.
storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;
storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();
transitionMatrix *= commandUpdateProbabilitiesAdd;
transitionMatrix += deadlockTransitions;
// Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions.
transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd<ValueType>();

16
src/storm/abstraction/prism/AbstractProgram.h
View File

@ -9,6 +9,8 @@
#include "storm/storage/dd/Add.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/PredicateSplitter.h"
#include "storm/storage/expressions/EquivalenceChecker.h"
namespace storm {
namespace utility {
@ -43,8 +45,9 @@ namespace storm {
* @param initialPredicates The initial set of predicates.
* @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
* @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
* @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added.
*/
AbstractProgram(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false);
AbstractProgram(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
AbstractProgram(AbstractProgram const&) = default;
AbstractProgram& operator=(AbstractProgram const&) = default;
@ -72,7 +75,7 @@ namespace storm {
*
* @param predicates The new predicates.
*/
void refine(std::vector<storm::expressions::Expression> const& predicates);
void refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates);
/*!
* Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that
@ -125,6 +128,15 @@ namespace storm {
// A state-set abstractor used to determine the initial states of the abstraction.
StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
// A flag indicating whether predicates are to be split into atoms or not.
bool splitPredicates;
// An object that can be used for splitting predicates.
storm::expressions::PredicateSplitter splitter;
// An object that can be used to determine whether predicates are equivalent.
storm::expressions::EquivalenceChecker equivalenceChecker;
// A flag that stores whether all guards were added (which is relevant for determining the bottom states).
bool addedAllGuards;

8
src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
View File

@ -10,7 +10,7 @@ namespace storm {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()) {
// Intentionally left empty.
}
@ -21,7 +21,11 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
abstractProgram.refine(predicates);
std::vector<std::pair<storm::expressions::Expression, bool>> predicatesWithFlags;
for (auto const& predicate : predicates) {
predicatesWithFlags.emplace_back(predicate, true);
}
abstractProgram.refine(predicatesWithFlags);
}
template <storm::dd::DdType DdType, typename ValueType>

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

@ -263,7 +263,10 @@ namespace storm {
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Refining based on lower choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
return true;
} else {
storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
@ -273,7 +276,10 @@ namespace storm {
bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
if (upperChoicesDifferent) {
STORM_LOG_TRACE("Refining based on upper choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
return true;
} else {
STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
@ -309,11 +315,6 @@ namespace storm {
// Start with constructing the player 2 states that have a (min) and a (max) strategy.
// TODO: necessary?
storm::dd::Bdd<Type> constraint = minStrategyPair.second.existsAbstract(game.getPlayer2Variables()) && maxStrategyPair.second.existsAbstract(game.getPlayer2Variables());
// (minStrategyPair.first && pivotStates).template toAdd<ValueType>().exportToDot("piv_min_pl1.dot");
// (maxStrategyPair.first && pivotStates).template toAdd<ValueType>().exportToDot("piv_max_pl1.dot");
// (minStrategyPair.second && pivotStates).template toAdd<ValueType>().exportToDot("piv_min_pl2.dot");
// (maxStrategyPair.second && pivotStates).template toAdd<ValueType>().exportToDot("piv_max_pl2.dot");
// Now construct all player 2 choices that actually exist and differ in the min and max case.
constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy);
@ -326,55 +327,20 @@ namespace storm {
// Now that we have the pivot state candidates, we need to pick one.
storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
// storm::dd::Add<Type, ValueType> pivotStateLower = pivotState.template toAdd<ValueType>() * minResult;
// storm::dd::Add<Type, ValueType> pivotStateUpper = pivotState.template toAdd<ValueType>() * maxResult;
// storm::dd::Bdd<Type> pivotStateIsMinProb0 = pivotState && prob01.min.first.getPlayer1States();
// storm::dd::Bdd<Type> pivotStateIsMaxProb0 = pivotState && prob01.max.first.getPlayer1States();
// storm::dd::Bdd<Type> pivotStateLowerStrategies = pivotState && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy();
// storm::dd::Bdd<Type> pivotStateUpperStrategies = pivotState && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy();
// storm::dd::Bdd<Type> pivotStateLowerPl1Strategy = pivotState && prob01.min.first.getPlayer1Strategy();
// storm::dd::Bdd<Type> pivotStateUpperPl1Strategy = pivotState && prob01.max.first.getPlayer1Strategy();
// storm::dd::Bdd<Type> pivotStateLowerPl2Strategy = pivotState && prob01.min.first.getPlayer2Strategy();
// storm::dd::Bdd<Type> pivotStateUpperPl2Strategy = pivotState && prob01.max.first.getPlayer2Strategy();
//
// minResult.exportToDot("minresult.dot");
// maxResult.exportToDot("maxresult.dot");
// pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
// pivotStateLower.exportToDot("pivot_lower.dot");
// pivotStateUpper.exportToDot("pivot_upper.dot");
// pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot");
// pivotStateIsMaxProb0.template toAdd<ValueType>().exportToDot("pivot_is_maxprob0.dot");
// pivotStateLowerStrategies.template toAdd<ValueType>().exportToDot("pivot_lower_strats.dot");
// pivotStateUpperStrategies.template toAdd<ValueType>().exportToDot("pivot_upper_strats.dot");
// pivotStateLowerPl1Strategy.template toAdd<ValueType>().exportToDot("pivot_lower_pl1_strat.dot");
// pivotStateUpperPl1Strategy.template toAdd<ValueType>().exportToDot("pivot_upper_pl1_strat.dot");
// pivotStateLowerPl2Strategy.template toAdd<ValueType>().exportToDot("pivot_lower_pl2_strat.dot");
// pivotStateUpperPl2Strategy.template toAdd<ValueType>().exportToDot("pivot_upper_pl2_strat.dot");
// Compute the lower and the upper choice for the pivot state.
std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
// (pivotState && minStrategyPair.first).template toAdd<ValueType>().exportToDot("pl1_choice_in_pivot.dot");
// (pivotState && minStrategyPair.first && maxStrategyPair.second).template toAdd<ValueType>().exportToDot("pl1and2_choice_in_pivot.dot");
// (pivotState && maxStrategyPair.second).template toAdd<ValueType>().exportToDot("pl2_choice_in_pivot.dot");
storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
// lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
// maxStrategyPair.second.template toAdd<ValueType>().exportToDot("max_strat.dot");
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
// lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot");
// lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract);
#ifdef LOCAL_DEBUG
lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot");
lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot");
lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot");
#endif
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Refining based on lower choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
} else {
storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
@ -383,7 +349,10 @@ namespace storm {
bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
if (upperChoicesDifferent) {
STORM_LOG_TRACE("Refining based on upper choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
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<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
} else {
STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
}
@ -462,6 +431,7 @@ namespace storm {
storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
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.
@ -479,10 +449,11 @@ namespace storm {
targetStates |= game.getBottomStates();
}
#ifdef LOCAL_DEBUG
abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
#endif
// #ifdef LOCAL_DEBUG
// abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
// #endif
auto qualitativeStart = std::chrono::high_resolution_clock::now();
prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates);
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States());
if (result) {
@ -517,15 +488,19 @@ namespace storm {
}
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<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
if (!qualitativeRefinement) {
// 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<Type, ValueType> minResult = prob01.min.second.getPlayer1States().template toAdd<ValueType>();
@ -539,6 +514,7 @@ namespace storm {
// the result right away.
ValueType minValue = storm::utility::zero<ValueType>();
MaybeStateResult<Type, ValueType> minMaybeStateResult(game.getManager().template getAddZero<ValueType>(), 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.player1Strategy &= game.getReachableStates();
@ -549,7 +525,8 @@ namespace storm {
STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << ".");
minValue = initialStateMin.getMax();
}
STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << ".");
auto minEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(minEnd - minStart).count() << "ms.");
minMaybeStateResult.player1Strategy = combinedMinPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMinPlayer1QualitativeStrategies, minMaybeStateResult.player1Strategy);
minMaybeStateResult.player2Strategy = combinedMinPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMinPlayer2QualitativeStrategies, minMaybeStateResult.player2Strategy);
@ -566,6 +543,7 @@ namespace storm {
// Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have
// given the result right awy.
ValueType maxValue = storm::utility::one<ValueType>();
auto maxStart = std::chrono::high_resolution_clock::now();
MaybeStateResult<Type, ValueType> maxMaybeStateResult(game.getManager().template getAddZero<ValueType>(), 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));
@ -578,7 +556,8 @@ namespace storm {
STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states. Expected 1, but got " << initialStateMax.getNonZeroCount() << ".");
maxValue = initialStateMax.getMax();
}
STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << ".");
auto maxEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Obtained quantitative upper bound " << maxValue << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(maxEnd - maxStart).count() << "ms.");
maxMaybeStateResult.player1Strategy = combinedMaxPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedMaxPlayer1QualitativeStrategies, maxMaybeStateResult.player1Strategy);
maxMaybeStateResult.player2Strategy = combinedMaxPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedMaxPlayer2QualitativeStrategies, maxMaybeStateResult.player2Strategy);
@ -589,7 +568,8 @@ namespace storm {
return result;
}
STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states.");
auto quantitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, minValue, maxValue);
if (result) {
@ -608,19 +588,12 @@ namespace storm {
// Check whether the strategies coincide over the reachable parts.
storm::dd::Bdd<Type> tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy);
storm::dd::Bdd<Type> commonReach = storm::utility::dd::computeReachableStates(game.getInitialStates(), tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
//std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy)) << std::endl;
//std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl;
STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide.");
#ifdef LOCAL_DEBUG
abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy);
abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy);
abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy);
abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy));
#endif
refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, 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<std::chrono::milliseconds>(iterationEnd - iterationStart).count() << "ms.");
}
STORM_LOG_ASSERT(false, "This point must not be reached.");
@ -630,8 +603,6 @@ namespace storm {
template<storm::dd::DdType Type, typename ModelType>
std::pair<storm::utility::graph::GameProb01Result<Type>, storm::utility::graph::GameProb01Result<Type>> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
// Compute the states with probability 0/1.
// storm::utility::graph::GameProb01Result<Type> prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Minimize, player2Direction == storm::OptimizationDirection::Minimize);
// storm::utility::graph::GameProb01Result<Type> prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, player2Direction == storm::OptimizationDirection::Maximize, player2Direction == storm::OptimizationDirection::Maximize);
storm::utility::graph::GameProb01Result<Type> prob0 = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true);
storm::utility::graph::GameProb01Result<Type> prob1 = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true);

6
src/storm/settings/modules/AbstractionSettings.cpp
View File

@ -9,14 +9,20 @@ namespace storm {
const std::string AbstractionSettings::moduleName = "abstraction";
const std::string AbstractionSettings::addAllGuardsOptionName = "allguards";
const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds";
AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, splitPredicatesOptionName, true, "Sets whether the predicates are split into atoms before they are added.").build());
}
bool AbstractionSettings::isAddAllGuardsSet() const {
return this->getOption(addAllGuardsOptionName).getHasOptionBeenSet();
}
bool AbstractionSettings::isSplitPredicatesSet() const {
return this->getOption(splitPredicatesOptionName).getHasOptionBeenSet();
}
}
}

8
src/storm/settings/modules/AbstractionSettings.h
View File

@ -22,11 +22,19 @@ namespace storm {
* @return True iff the option was set.
*/
bool isAddAllGuardsSet() const;
/*!
* Retrieves whether the option to split predicates to atoms was set.
*
* @return True iff the option was set.
*/
bool isSplitPredicatesSet() const;
const static std::string moduleName;
private:
const static std::string addAllGuardsOptionName;
const static std::string splitPredicatesOptionName;
};
}

23
src/storm/storage/expressions/EquivalenceChecker.cpp
View File

@ -0,0 +1,23 @@
#include "storm/storage/expressions/EquivalenceChecker.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/expressions/Expression.h"
namespace storm {
namespace expressions {
EquivalenceChecker::EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, storm::expressions::Expression const& constraint) : smtSolver(std::move(smtSolver)) {
this->smtSolver->add(constraint);
}
bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {
this->smtSolver->push();
this->smtSolver->add((first && !second) || (!first && second));
bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat;
this->smtSolver->pop();
return equivalent;
}
}
}

28
src/storm/storage/expressions/EquivalenceChecker.h
View File

@ -0,0 +1,28 @@
#pragma once
#include <memory>
#include "storm/solver/SmtSolver.h"
namespace storm {
namespace expressions {
class Expression;
class EquivalenceChecker {
public:
/*!
* Creates an equivalence checker with the given solver and constraint.
*
* @param smtSolver The solver to use.
* @param constraint An additional constraint. Must be satisfiable.
*/
EquivalenceChecker(std::unique_ptr<storm::solver::SmtSolver>&& smtSolver, storm::expressions::Expression const& constraint);
bool areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second);
private:
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
};
}
}

14
src/storm/storage/expressions/Expression.h
View File

@ -66,6 +66,13 @@ namespace storm {
*/
Expression(Variable const& variable);
/*!
* Creates an expression with the given underlying base expression.
*
* @param expressionPtr A pointer to the underlying base expression.
*/
Expression(std::shared_ptr<BaseExpression const> const& expressionPtr);
// Instantiate constructors and assignments with their default implementations.
Expression(Expression const& other) = default;
Expression& operator=(Expression const& other) = default;
@ -332,13 +339,6 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Expression const& expression);
private:
/*!
* Creates an expression with the given underlying base expression.
*
* @param expressionPtr A pointer to the underlying base expression.
*/
Expression(std::shared_ptr<BaseExpression const> const& expressionPtr);
// A pointer to the underlying base expression.
std::shared_ptr<BaseExpression const> expressionPtr;
};

80
src/storm/storage/expressions/PredicateSplitter.cpp
View File

@ -0,0 +1,80 @@
#include "storm/storage/expressions/PredicateSplitter.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace expressions {
std::vector<storm::expressions::Expression> PredicateSplitter::split(storm::expressions::Expression const& expression) {
STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type.");
// Gather all atoms.
atomicExpressions.clear();
expression.accept(*this, boost::none);
// Remove all boolean literals from the atoms.
std::vector<storm::expressions::Expression> atomsToKeep;
for (auto const& atom : atomicExpressions) {
if (!atom.isTrue() && !atom.isFalse()) {
atomsToKeep.push_back(atom);
}
}
atomicExpressions = std::move(atomsToKeep);
return atomicExpressions;
}
boost::any PredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) {
atomicExpressions.push_back(expression.shared_from_this());
return boost::any();
}
boost::any PredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
expression.getFirstOperand()->accept(*this, data);
expression.getSecondOperand()->accept(*this, data);
return boost::any();
}
boost::any PredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
return boost::any();
}
boost::any PredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) {
atomicExpressions.push_back(expression.shared_from_this());
return boost::any();
}
boost::any PredicateSplitter::visit(VariableExpression const& expression, boost::any const&) {
if (expression.hasBooleanType()) {
atomicExpressions.push_back(expression.shared_from_this());
}
return boost::any();
}
boost::any PredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
expression.getOperand()->accept(*this, data);
return boost::any();
}
boost::any PredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
return boost::any();
}
boost::any PredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) {
return boost::any();
}
boost::any PredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) {
return boost::any();
}
boost::any PredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) {
return boost::any();
}
}
}

31
src/storm/storage/expressions/PredicateSplitter.h
View File

@ -0,0 +1,31 @@
#pragma once
#include <vector>
#include "storm/storage/expressions/ExpressionVisitor.h"
namespace storm {
namespace expressions {
class Expression;
class PredicateSplitter : public ExpressionVisitor {
public:
std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression);
virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
private:
std::vector<storm::expressions::Expression> atomicExpressions;
};
}
}

6
src/storm/utility/graph.cpp
View File

@ -929,7 +929,7 @@ namespace storm {
// The solution sets.
storm::dd::Bdd<Type> player1States = psiStates;
storm::dd::Bdd<Type> player2States = model.getManager().getBddZero();
bool done = false;
uint_fast64_t iterations = 0;
while (!done) {
@ -960,18 +960,14 @@ namespace storm {
}
// Since we have determined the complements of the desired sets, we need to complement it now.
player1States.template toAdd<ValueType>().exportToDot("not_pl1_prob0.dot");
(!player1States).template toAdd<ValueType>().exportToDot("pl1_negated_prob0.dot");
player1States = !player1States && model.getReachableStates();
player2States = !player2States && model.getReachableStates();
// Determine all transitions between prob0 states.
storm::dd::Bdd<Type> transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs()));
player1States.template toAdd<ValueType>().exportToDot("pl1_prob0.dot");
// Determine the distributions that have only successors that are prob0 states.
storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables());
onlyProb0Successors.template toAdd<ValueType>().exportToDot("only_prob0.dot");
boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
if (producePlayer2Strategy) {

12
src/test/abstraction/PrismMenuGameTest.cpp
View File

@ -434,7 +434,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
}
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -456,7 +456,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
}
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm");
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
program = program.substituteConstants();
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
@ -595,7 +595,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
EXPECT_EQ(1335, game.getNumberOfTransitions());
EXPECT_EQ(1379, game.getNumberOfTransitions());
EXPECT_EQ(12, game.getNumberOfStates());
EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
}
@ -616,7 +616,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
EXPECT_EQ(1335, game.getNumberOfTransitions());
EXPECT_EQ(1379, game.getNumberOfTransitions());
EXPECT_EQ(12, game.getNumberOfStates());
EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
}
@ -639,7 +639,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
EXPECT_EQ(2656, game.getNumberOfTransitions());
EXPECT_EQ(2744, game.getNumberOfTransitions());
EXPECT_EQ(24, game.getNumberOfStates());
EXPECT_EQ(16, game.getBottomStates().getNonZeroCount());
}
@ -662,7 +662,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
EXPECT_EQ(2656, game.getNumberOfTransitions());
EXPECT_EQ(2744, game.getNumberOfTransitions());
EXPECT_EQ(24, game.getNumberOfStates());
EXPECT_EQ(16, game.getBottomStates().getNonZeroCount());
}

Write Preview
|||||||
100:0
Loading…
Cancel
Save