Browse Source

update to game-based abstraction refinement

tempestpy_adaptions
dehnert 7 years ago
parent
commit
efbd899e46
  1. 28
      src/storm/abstraction/MenuGameAbstractor.cpp
  2. 18
      src/storm/abstraction/MenuGameAbstractor.h
  3. 41
      src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
  4. 37
      src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
  5. 1
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  6. 10
      src/storm/settings/modules/AbstractionSettings.cpp
  7. 8
      src/storm/settings/modules/AbstractionSettings.h
  8. 35
      src/storm/utility/dd.cpp
  9. 5
      src/storm/utility/dd.h

28
src/storm/abstraction/MenuGameAbstractor.cpp

@ -4,6 +4,9 @@
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/utility/dd.h"
@ -15,6 +18,11 @@
namespace storm {
namespace abstraction {
template <storm::dd::DdType DdType, typename ValueType>
MenuGameAbstractor<DdType, ValueType>::MenuGameAbstractor() : restrictToRelevantStates(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isRestrictToRelevantStatesSet()) {
// Intentionally left empty.
}
template <typename ValueType>
std::string getStateName(std::pair<storm::expressions::SimpleValuation, ValueType> const& stateValue, std::set<storm::expressions::Variable> const& locationVariables, std::set<storm::expressions::Variable> const& predicateVariables, storm::expressions::Variable const& bottomVariable) {
std::stringstream stateName;
@ -45,6 +53,11 @@ namespace storm {
return stateName.str();
}
template <storm::dd::DdType DdType, typename ValueType>
bool MenuGameAbstractor<DdType, ValueType>::isRestrictToRelevantStatesSet() const {
return restrictToRelevantStates;
}
template <storm::dd::DdType DdType, typename ValueType>
void MenuGameAbstractor<DdType, ValueType>::exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
@ -135,6 +148,21 @@ namespace storm {
storm::utility::closeFile(out);
}
template <storm::dd::DdType DdType, typename ValueType>
void MenuGameAbstractor<DdType, ValueType>::setTargetStates(storm::expressions::Expression const& targetStateExpression) {
this->targetStateExpression = targetStateExpression;
}
template <storm::dd::DdType DdType, typename ValueType>
storm::expressions::Expression const& MenuGameAbstractor<DdType, ValueType>::getTargetStateExpression() const {
return this->targetStateExpression;
}
template <storm::dd::DdType DdType, typename ValueType>
bool MenuGameAbstractor<DdType, ValueType>::hasTargetStateExpression() const {
return this->targetStateExpression.isInitialized();
}
template class MenuGameAbstractor<storm::dd::DdType::CUDD, double>;
template class MenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

18
src/storm/abstraction/MenuGameAbstractor.h

@ -24,6 +24,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
class MenuGameAbstractor {
public:
MenuGameAbstractor();
virtual ~MenuGameAbstractor() = default;
/// Retrieves the abstraction.
@ -58,8 +59,25 @@ namespace storm {
*/
virtual void addTerminalStates(storm::expressions::Expression const& expression) = 0;
/*!
* Sets the expression characterizing the target states. For this to work, appropriate predicates must have
* been used to refine the abstraction, otherwise this will fail.
*/
void setTargetStates(storm::expressions::Expression const& targetStateExpression);
storm::expressions::Expression const& getTargetStateExpression() const;
bool hasTargetStateExpression() const;
protected:
bool isRestrictToRelevantStatesSet() const;
void exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const;
private:
bool restrictToRelevantStates;
// An expression characterizing the target states.
storm::expressions::Expression targetStateExpression;
};
}

41
src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@ -17,6 +17,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/dd.h"
#include "storm/utility/macros.h"
#include "storm/utility/solver.h"
@ -154,18 +155,48 @@ namespace storm {
auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
// Compute which states are non-terminal.
storm::utility::Stopwatch relevantStatesWatch(true);
storm::dd::Bdd<DdType> nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne();
for (auto const& expression : this->terminalStateExpressions) {
nonTerminalStates &= !this->getStates(expression);
if (this->isRestrictToRelevantStatesSet()) {
// Compute which states are non-terminal.
for (auto const& expression : this->terminalStateExpressions) {
nonTerminalStates &= !this->getStates(expression);
}
if (this->hasTargetStateExpression()) {
nonTerminalStates &= !this->getStates(this->getTargetStateExpression());
}
}
relevantStatesWatch.stop();
// Do a reachability analysis on the raw transition relation.
storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
storm::dd::Bdd<DdType> initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates();
initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
relevantStatesWatch.start();
if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {
// Cut transition relation to the reachable states for backward search.
transitionRelation &= reachableStates;
// Get the target state BDD.
storm::dd::Bdd<DdType> targetStates = reachableStates && this->getStates(this->getTargetStateExpression());
// In the presence of target states, we keep only states that can reach the target states.
reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates;
// Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self-
// loops of (now) deadlock states.
transitionRelation &= reachableStates;
// Include all successors of reachable states, because the backward search otherwise potentially
// cuts probability 0 choices of these states.
reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
relevantStatesWatch.stop();
STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms.");
}
// Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states,
// as the bottom states are not contained in the reachable states.
storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
@ -223,7 +254,7 @@ namespace storm {
void JaniMenuGameAbstractor<DdType, ValueType>::addTerminalStates(storm::expressions::Expression const& expression) {
terminalStateExpressions.emplace_back(expression);
}
// Explicitly instantiate the class.
template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;

37
src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@ -15,6 +15,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/dd.h"
#include "storm/utility/macros.h"
#include "storm/utility/solver.h"
@ -147,11 +148,18 @@ namespace storm {
auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
// Compute which states are non-terminal.
storm::utility::Stopwatch relevantStatesWatch(true);
storm::dd::Bdd<DdType> nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne();
for (auto const& expression : this->terminalStateExpressions) {
nonTerminalStates &= !this->getStates(expression);
if (this->isRestrictToRelevantStatesSet()) {
// Compute which states are non-terminal.
for (auto const& expression : this->terminalStateExpressions) {
nonTerminalStates &= !this->getStates(expression);
}
if (this->hasTargetStateExpression()) {
nonTerminalStates &= !this->getStates(this->getTargetStateExpression());
}
}
relevantStatesWatch.stop();
// Do a reachability analysis on the raw transition relation.
storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
@ -159,6 +167,29 @@ namespace storm {
initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
relevantStatesWatch.start();
if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {
// Cut transition relation to the reachable states for backward search.
transitionRelation &= reachableStates;
// Get the target state BDD.
storm::dd::Bdd<DdType> targetStates = reachableStates && this->getStates(this->getTargetStateExpression());
// In the presence of target states, we keep only states that can reach the target states.
reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates;
// Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self-
// loops of (now) deadlock states.
transitionRelation &= reachableStates;
// Include all successors of reachable states, because the backward search otherwise potentially
// cuts probability 0 choices of these states.
reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
relevantStatesWatch.stop();
STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms.");
}
// Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states,
// as the bottom states are not contained in the reachable states.
storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());

1
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -346,6 +346,7 @@ namespace storm {
abstractor->addTerminalStates(!constraintExpression);
}
abstractor->addTerminalStates(targetStateExpression);
abstractor->setTargetStates(targetStateExpression);
// Create a refiner that can be used to refine the abstraction when needed.
storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));

10
src/storm/settings/modules/AbstractionSettings.cpp

@ -21,6 +21,7 @@ namespace storm {
const std::string AbstractionSettings::precisionOptionName = "precision";
const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic";
const std::string AbstractionSettings::reuseResultsOptionName = "reuse";
const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant";
AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@ -64,6 +65,11 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
.setDefaultValueString("all").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, restrictToRelevantStatesOptionName, true, "Sets whether to restrict to relevant states during the abstraction.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
.setDefaultValueString("off").build())
.build());
}
AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
@ -104,6 +110,10 @@ namespace storm {
return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on";
}
bool AbstractionSettings::isRestrictToRelevantStatesSet() const {
return this->getOption(restrictToRelevantStatesOptionName).getArgumentByName("value").getValueAsString() == "on";
}
double AbstractionSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}

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

@ -93,6 +93,13 @@ namespace storm {
*/
ReuseMode getReuseMode() const;
/*!
* Retrieves whether only relevant states are to be considered.
*
* @return True iff the option was set.
*/
bool isRestrictToRelevantStatesSet() const;
const static std::string moduleName;
private:
@ -104,6 +111,7 @@ namespace storm {
const static std::string precisionOptionName;
const static std::string pivotHeuristicOptionName;
const static std::string reuseResultsOptionName;
const static std::string restrictToRelevantStatesOptionName;
};
}

35
src/storm/utility/dd.cpp

@ -45,6 +45,38 @@ namespace storm {
return reachableStates;
}
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> computeBackwardsReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) {
STORM_LOG_TRACE("Computing backwards reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states).");
auto start = std::chrono::high_resolution_clock::now();
storm::dd::Bdd<Type> reachableStates = initialStates;
// Perform the BFS to discover all reachable states.
bool changed = true;
uint_fast64_t iteration = 0;
do {
changed = false;
storm::dd::Bdd<Type> tmp = reachableStates.inverseRelationalProduct(transitions, rowMetaVariables, columnMetaVariables);
storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates) && constraintStates;
// Check whether new states were indeed discovered.
if (!newReachableStates.isZero()) {
changed = true;
}
reachableStates |= newReachableStates;
++iteration;
STORM_LOG_TRACE("Iteration " << iteration << " of (backward) reachability computation completed: " << reachableStates.getNonZeroCount() << " reachable states found.");
} while (changed);
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Backward reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms).");
return reachableStates;
}
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
return ddManager.getIdentity(rowColumnMetaVariablePairs, false);
@ -53,6 +85,9 @@ namespace storm {
template storm::dd::Bdd<storm::dd::DdType::CUDD> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template storm::dd::Bdd<storm::dd::DdType::Sylvan> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template storm::dd::Bdd<storm::dd::DdType::CUDD> computeBackwardsReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& constraintStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template storm::dd::Bdd<storm::dd::DdType::Sylvan> computeBackwardsReachableStates(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& initialStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& constraintStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template storm::dd::Bdd<storm::dd::DdType::CUDD> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::CUDD> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);
template storm::dd::Bdd<storm::dd::DdType::Sylvan> getRowColumnDiagonal(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);

5
src/storm/utility/dd.h

@ -25,7 +25,10 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> computeReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> computeBackwardsReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);
template <storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs);

Loading…
Cancel
Save