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

more options and bugfix

tempestpy_adaptions
dehnert 8 years ago
parent
24eede3e19
commit
26320049a6
8 changed files with 83 additions and 63 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/abstraction/MenuGameAbstractor.h
  2. 38
      src/storm/abstraction/MenuGameRefiner.cpp
  3. 11
      src/storm/abstraction/MenuGameRefiner.h
  4. 11
      src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
  5. 9
      src/storm/abstraction/prism/PrismMenuGameAbstractor.h
  6. 46
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  7. 11
      src/storm/settings/modules/AbstractionSettings.cpp
  8. 18
      src/storm/settings/modules/AbstractionSettings.h

2
src/storm/abstraction/MenuGameAbstractor.h
View File

@ -29,7 +29,7 @@ namespace storm {
virtual std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0;
/// Methods to refine the abstraction.
virtual void refine(std::vector<RefinementCommand> const& commands) = 0;
virtual void refine(RefinementCommand const& command) = 0;
/// Exports a representation of the current abstraction state in the dot format.
virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const = 0;

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

@ -12,7 +12,7 @@ namespace storm {
namespace abstraction {
template<storm::dd::DdType Type, typename ValueType>
MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()), splitter(), equivalenceChecker(std::move(smtSolver)) {
MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()), splitGuards(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitGuardsSet()), splitter(), equivalenceChecker(std::move(smtSolver)) {
if (storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
std::vector<storm::expressions::Expression> guards;
@ -21,7 +21,7 @@ namespace storm {
for (uint64_t index = player1Choices.first; index < player1Choices.second; ++index) {
guards.push_back(this->abstractor.get().getGuard(index));
}
performRefinement(createGlobalRefinement(guards));
performRefinement(createGlobalRefinement(preprocessPredicates(guards, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitInitialGuardsSet())));
}
}
@ -74,9 +74,10 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
storm::expressions::Expression MenuGameRefiner<Type, ValueType>::derivePredicateFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const {
std::pair<storm::expressions::Expression, bool> MenuGameRefiner<Type, ValueType>::derivePredicateFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const {
// Prepare result.
storm::expressions::Expression newPredicate;
bool fromGuard = false;
// Get abstraction informatin for easier access.
AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
@ -95,6 +96,7 @@ namespace storm {
if (buttomStateSuccessor) {
STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate.");
newPredicate = abstractor.get().getGuard(player1Index);
fromGuard = true;
STORM_LOG_DEBUG("Derived new predicate (based on guard): " << newPredicate);
} else {
STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
@ -130,7 +132,7 @@ namespace storm {
for (auto const& predicate : abstractionInformation.getPredicates()) {
STORM_LOG_TRACE(predicate);
}
return newPredicate;
return std::make_pair(newPredicate, fromGuard);
}
template<storm::dd::DdType Type>
@ -169,7 +171,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
storm::expressions::Expression MenuGameRefiner<Type, ValueType>::derivePredicateFromPivotState(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
std::pair<storm::expressions::Expression, bool> MenuGameRefiner<Type, ValueType>::derivePredicateFromPivotState(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
// 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());
@ -182,7 +184,7 @@ namespace storm {
STORM_LOG_TRACE("Refining based on lower choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
std::pair<storm::expressions::Expression, bool> newPredicate = derivePredicateFromDifferingChoices(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 newPredicate;
@ -195,7 +197,7 @@ namespace storm {
if (upperChoicesDifferent) {
STORM_LOG_TRACE("Refining based on upper choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
std::pair<storm::expressions::Expression, bool> newPredicate = derivePredicateFromDifferingChoices(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 newPredicate;
@ -234,8 +236,8 @@ namespace storm {
storm::dd::Bdd<Type> pivotState = pickPivotStateWithMinimalDistance<Type, ValueType>(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates);
// Derive predicate based on the selected pivot state.
storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates({newPredicate});
std::pair<storm::expressions::Expression, bool> newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates({newPredicate.first}, (newPredicate.second && splitGuards) || (!newPredicate.second && splitPredicates));
performRefinement(createGlobalRefinement(preparedPredicates));
return true;
}
@ -262,15 +264,15 @@ namespace storm {
storm::dd::Bdd<Type> pivotState = pickPivotStateWithMinimalDistance<Type, ValueType>(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates);
// Derive predicate based on the selected pivot state.
storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates({newPredicate});
std::pair<storm::expressions::Expression, bool> newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates({newPredicate.first}, (newPredicate.second && splitGuards) || (!newPredicate.second && splitPredicates));
performRefinement(createGlobalRefinement(preparedPredicates));
return true;
}
template<storm::dd::DdType Type, typename ValueType>
std::vector<storm::expressions::Expression> MenuGameRefiner<Type, ValueType>::preprocessPredicates(std::vector<storm::expressions::Expression> const& predicates) const {
if (splitPredicates) {
std::vector<storm::expressions::Expression> MenuGameRefiner<Type, ValueType>::preprocessPredicates(std::vector<storm::expressions::Expression> const& predicates, bool split) const {
if (split) {
std::vector<storm::expressions::Expression> cleanedAtoms;
for (auto const& predicate : predicates) {
@ -314,19 +316,15 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::vector<RefinementCommand> MenuGameRefiner<Type, ValueType>::createGlobalRefinement(std::vector<storm::expressions::Expression> const& predicates) const {
std::vector<RefinementCommand> commands;
// std::pair<uint64_t, uint64_t> player1Choices = abstractor.get().getPlayer1ChoiceRange();
// for (uint64_t index = player1Choices.first; index < player1Choices.second; ++index) {
// commands.emplace_back(index, predicates);
// }
commands.emplace_back(predicates);
return commands;
}
template<storm::dd::DdType Type, typename ValueType>
void MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<RefinementCommand> const& refinementCommands) const {
abstractor.get().refine(refinementCommands);
for (auto const& command : refinementCommands) {
abstractor.get().refine(command);
}
}
template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;

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

@ -53,13 +53,13 @@ namespace storm {
bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const;
private:
storm::expressions::Expression derivePredicateFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const;
storm::expressions::Expression derivePredicateFromPivotState(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
std::pair<storm::expressions::Expression, bool> derivePredicateFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const;
std::pair<storm::expressions::Expression, bool> derivePredicateFromPivotState(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
/*!
* Preprocesses the predicates.
*/
std::vector<storm::expressions::Expression> preprocessPredicates(std::vector<storm::expressions::Expression> const& predicates) const;
std::vector<storm::expressions::Expression> preprocessPredicates(std::vector<storm::expressions::Expression> const& predicates, bool allowSplits) const;
/*!
* Creates a set of refinement commands that amounts to splitting all player 1 choices with the given set of predicates.
@ -73,7 +73,10 @@ namespace storm {
/// A flag indicating whether predicates shall be split before using them for refinement.
bool splitPredicates;
/// A flag indicating whether predicates shall be split before using them for refinement.
bool splitGuards;
/// An object that can be used for splitting predicates.
mutable storm::expressions::PredicateSplitter splitter;

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

@ -72,15 +72,6 @@ namespace storm {
commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
}
template <storm::dd::DdType DdType, typename ValueType>
void PrismMenuGameAbstractor<DdType, ValueType>::refine(std::vector<RefinementCommand> const& commands) {
for (auto const& command : commands) {
STORM_LOG_THROW(!command.refersToPlayer1Choice(), storm::exceptions::NotSupportedException, "Currently only global refinement is supported.");
refine(command);
refinementPerformed |= !command.getPredicates().empty();
}
}
template <storm::dd::DdType DdType, typename ValueType>
void PrismMenuGameAbstractor<DdType, ValueType>::refine(RefinementCommand const& command) {
// Add the predicates to the global list of predicates and gather their indices.
@ -97,6 +88,8 @@ namespace storm {
// Refine initial state abstractor.
initialStateAbstractor.refine(predicateIndices);
refinementPerformed |= !command.getPredicates().empty();
}
template <storm::dd::DdType DdType, typename ValueType>

9
src/storm/abstraction/prism/PrismMenuGameAbstractor.h
View File

@ -93,19 +93,12 @@ namespace storm {
*/
storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& predicate);
/*!
* Performs the given refinement commands.
*
* @param commands The commands to perform.
*/
virtual void refine(std::vector<RefinementCommand> const& commands) override;
/*!
* Performs the given refinement command.
*
* @param command The command to perform.
*/
void refine(RefinementCommand const& command);
virtual void refine(RefinementCommand const& command) override;
/*!
* Exports the current state of the abstraction in the dot format to the given file.

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

@ -211,14 +211,32 @@ namespace storm {
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) {
bool min = player2Direction == storm::OptimizationDirection::Minimize;
QuantitativeResult<Type, ValueType> result;
// The minimal value after qualitative checking can only be zero. If it was 1, we could have given
// the result right away. Similarly, the maximal value can only be one at this point.
ValueType initialStateValue = min ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>();
result.initialStateValue = min ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>();
QuantitativeResult<Type, ValueType> result;
// We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative
// preprocessing if possible.
storm::dd::Bdd<Type> combinedPlayer1QualitativeStrategies;
storm::dd::Bdd<Type> combinedPlayer2QualitativeStrategies;
if (min) {
combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy());
combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer2Strategy() || qualitativeResult.prob1Min.getPlayer2Strategy());
} else {
combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer1Strategy() || qualitativeResult.prob1Max.getPlayer1Strategy());
combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy());
}
result.player1Strategy = combinedPlayer1QualitativeStrategies;
result.player2Strategy = combinedPlayer2QualitativeStrategies;
result.values = game.getManager().template getAddZero<ValueType>();
auto start = std::chrono::high_resolution_clock::now();
if (!maybeStates.isZero()) {
STORM_LOG_TRACE("Solving " << maybeStates.getNonZeroCount() << " maybe states.");
// Solve the quantitative values of maybe states.
result = solveMaybeStates(player1Direction, player2Direction, game, maybeStates, min ? qualitativeResult.prob1Min.getPlayer1States() : qualitativeResult.prob1Max.getPlayer1States(), startInfo);
@ -233,24 +251,12 @@ namespace storm {
storm::dd::Add<Type, ValueType> initialStateValueAdd = initialStatesAdd * result.values;
// For min, we can only require a non-zero count of *at most* one, because the result may actually be 0.
STORM_LOG_ASSERT((!min || initialStateValueAdd.getNonZeroCount() == 1) && (min || initialStateValueAdd.getNonZeroCount() <= 1), "Wrong number of results for initial states. Expected " << (min ? "<= 1" : "1") << ", but got " << initialStateValueAdd.getNonZeroCount() << ".");
result.initialStateValue = initialStateValue = initialStateValueAdd.getMax();
// Finally, we fix the strategies. That is, we take the decisions of the strategies obtained in the
// qualitiative preprocessing if possible.
storm::dd::Bdd<Type> combinedPlayer1QualitativeStrategies;
storm::dd::Bdd<Type> combinedPlayer2QualitativeStrategies;
if (min) {
combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy());
combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer2Strategy() || qualitativeResult.prob1Min.getPlayer2Strategy());
} else {
combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer1Strategy() || qualitativeResult.prob1Max.getPlayer1Strategy());
combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy());
}
result.initialStateValue = result.initialStateValue = initialStateValueAdd.getMax();
result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy);
result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy);
} else {
result = QuantitativeResult<Type, ValueType>(initialStateValue, game.getManager().template getAddZero<ValueType>(), game.getManager().getBddZero(), game.getManager().getBddZero());
STORM_LOG_TRACE("No maybe states.");
}
auto end = std::chrono::high_resolution_clock::now();
@ -369,10 +375,10 @@ namespace storm {
}
// Make sure that all strategies are still valid strategies.
STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.isZero() || quantitativeResult.min.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.isZero() || quantitativeResult.max.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.isZero() || quantitativeResult.min.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.isZero() || quantitativeResult.max.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
// (10) If we arrived at this point, it means that we have all qualitative and quantitative
// information about the game, but we could not yet answer the query. In this case, we need to refine.

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

@ -10,10 +10,14 @@ namespace storm {
const std::string AbstractionSettings::moduleName = "abstraction";
const std::string AbstractionSettings::addAllGuardsOptionName = "allguards";
const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds";
const std::string AbstractionSettings::splitInitialGuardsOptionName = "split-init-guards";
const std::string AbstractionSettings::splitGuardsOptionName = "split-guards";
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());
this->addOption(storm::settings::OptionBuilder(moduleName, splitInitialGuardsOptionName, true, "Sets whether the initial guards are split into atoms before they are added.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, splitGuardsOptionName, true, "Sets whether the guards are split into atoms before they are added.").build());
}
bool AbstractionSettings::isAddAllGuardsSet() const {
@ -23,7 +27,14 @@ namespace storm {
bool AbstractionSettings::isSplitPredicatesSet() const {
return this->getOption(splitPredicatesOptionName).getHasOptionBeenSet();
}
bool AbstractionSettings::isSplitInitialGuardsSet() const {
return this->getOption(splitInitialGuardsOptionName).getHasOptionBeenSet();
}
bool AbstractionSettings::isSplitGuardsSet() const {
return this->getOption(splitGuardsOptionName).getHasOptionBeenSet();
}
}
}
}

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

@ -29,12 +29,28 @@ namespace storm {
* @return True iff the option was set.
*/
bool isSplitPredicatesSet() const;
/*!
* Retrieves whether the option to split the initially added guards to atoms was set.
*
* @return True iff the option was set.
*/
bool isSplitInitialGuardsSet() const;
/*!
* Retrieves whether the option to split guards derived later to atoms was set.
*
* @return True iff the option was set.
*/
bool isSplitGuardsSet() const;
const static std::string moduleName;
private:
const static std::string addAllGuardsOptionName;
const static std::string splitPredicatesOptionName;
const static std::string splitInitialGuardsOptionName;
const static std::string splitGuardsOptionName;
};
}

Write Preview
Loading…
Cancel
Save