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

CheckTask may now hold info about shielding query

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
d4d3c0d9ea
commit
102b26b933
1 changed files with 72 additions and 42 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. 114
      src/storm/modelchecker/CheckTask.h

114
src/storm/modelchecker/CheckTask.h
View File

@ -10,6 +10,7 @@
#include "storm/solver/OptimizationDirection.h"
#include "storm/logic/ComparisonType.h"
#include "storm/logic/PlayerCoalition.h"
#include "storm/logic/ShieldExpression.h"
#include "storm/modelchecker/hints/ModelCheckerHint.h"
#include "storm/exceptions/InvalidOperationException.h"
@ -19,13 +20,13 @@ namespace storm {
namespace logic {
class Formula;
}
namespace modelchecker {
enum class CheckType {
Probabilities, Rewards
};
/*
* This class is used to customize the checking process of a formula.
*/
@ -34,7 +35,7 @@ namespace storm {
public:
template<typename OtherFormulaType, typename OtherValueType>
friend class CheckTask;
/*!
* Creates a task object with the default options for the given formula.
*/
@ -42,10 +43,10 @@ namespace storm {
this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
this->produceSchedulers = false;
this->qualitative = false;
updateOperatorInformation();
}
/*!
* Copies the check task from the source while replacing the formula with the new one. In particular, this
* changes the formula type of the check task object.
@ -56,7 +57,7 @@ namespace storm {
result.updateOperatorInformation();
return result;
}
/*!
* If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula.
* Calling this method has no effect if the provided formula is not an operator formula.
@ -67,20 +68,20 @@ namespace storm {
if (operatorFormula.hasOptimalityType()) {
this->optimizationDirection = operatorFormula.getOptimalityType();
}
if (operatorFormula.hasBound()) {
this->bound = operatorFormula.getBound();
}
if (operatorFormula.hasOptimalityType()) {
this->optimizationDirection = operatorFormula.getOptimalityType();
} else if (operatorFormula.hasBound()) {
this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
if (formula.get().isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.get().asProbabilityOperatorFormula();
if (probabilityOperatorFormula.hasBound()) {
if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
@ -89,7 +90,7 @@ namespace storm {
} else if (formula.get().isRewardOperatorFormula()) {
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.get().asRewardOperatorFormula();
this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
if (rewardOperatorFormula.hasBound()) {
if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
@ -107,49 +108,49 @@ namespace storm {
CheckTask<FormulaType, NewValueType> convertValueType() const {
return CheckTask<FormulaType, NewValueType>(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint);
}
/*!
* Retrieves the formula from this task.
*/
FormulaType const& getFormula() const {
return formula.get();
}
/*!
* Retrieves whether an optimization direction was set.
*/
bool isOptimizationDirectionSet() const {
return static_cast<bool>(optimizationDirection);
}
/*!
* Retrieves the optimization direction (if set).
*/
storm::OptimizationDirection const& getOptimizationDirection() const {
return optimizationDirection.get();
}
/*!
* Sets the optimization direction.
*/
void setOptimizationDirection(storm::OptimizationDirection const& dir) {
optimizationDirection = dir;
}
/*!
* Retrieves whether a player coalition was set.
*/
bool isPlayerCoalitionSet() const {
return static_cast<bool>(playerCoalition);
}
/*!
* Retrieves the player coalition (if set).
*/
storm::logic::PlayerCoalition const& getPlayerCoalition() const {
return playerCoalition.get();
}
/*!
* Sets the player coalition.
*/
@ -157,28 +158,28 @@ namespace storm {
playerCoalition = coalition;
return *this;
}
/*!
* Retrieves whether a reward model was set.
*/
bool isRewardModelSet() const {
return static_cast<bool>(rewardModel);
}
/*!
* Retrieves the reward model over which to perform the checking (if set).
*/
std::string const& getRewardModel() const {
return rewardModel.get();
}
/*!
* Retrieves whether only the initial states are relevant in the computation.
*/
bool isOnlyInitialStatesRelevantSet() const {
return onlyInitialStatesRelevant;
}
/*!
* Sets whether only initial states are relevant.
*/
@ -186,14 +187,37 @@ namespace storm {
this->onlyInitialStatesRelevant = value;
return *this;
}
/*
* TODO
*/
bool isShieldingTask() const {
return static_cast<bool>(shieldingExpression);
}
/*
* TODO
*/
std::shared_ptr<storm::logic::ShieldExpression const> getShieldingExpression() const {
return shieldingExpression.get();
}
/*
* TODO
*/
CheckTask<FormulaType, ValueType>& setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
this->shieldingExpression = shieldingExpression;
this->produceSchedulers = true;
return *this;
}
/*!
* Retrieves whether there is a bound with which the values for the states will be compared.
*/
bool isBoundSet() const {
return static_cast<bool>(bound);
}
/*!
* Retrieves the value of the bound (if set).
*/
@ -201,14 +225,14 @@ namespace storm {
STORM_LOG_THROW(!bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << bound.get().threshold << "' as it contains undefined constants.");
return storm::utility::convertNumber<ValueType>(bound.get().threshold.evaluateAsRational());
}
/*!
* Retrieves the comparison type of the bound (if set).
*/
storm::logic::ComparisonType const& getBoundComparisonType() const {
return bound.get().comparisonType;
}
/*!
* Retrieves the bound (if set).
*/
@ -238,46 +262,46 @@ namespace storm {
void setQualitative(bool value) {
qualitative = value;
}
/*!
* Sets whether to produce schedulers (if supported).
*/
void setProduceSchedulers(bool produceSchedulers = true) {
this->produceSchedulers = produceSchedulers;
}
/*!
* Retrieves whether scheduler(s) are to be produced (if supported).
*/
bool isProduceSchedulersSet() const {
return produceSchedulers;
}
/*!
* sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
*/
void setHint(std::shared_ptr<ModelCheckerHint> const& hint) {
this->hint = hint;
}
/*!
* Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
*/
ModelCheckerHint const& getHint() const {
return *hint;
}
ModelCheckerHint& getHint() {
return *hint;
}
/*!
* Conversion operator that strips the type of the formula.
*/
operator CheckTask<storm::logic::Formula, ValueType>() const {
return this->substituteFormula<storm::logic::Formula>(this->getFormula());
}
private:
/*!
* Creates a task object with the given options.
@ -297,36 +321,42 @@ namespace storm {
CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::PlayerCoalition> playerCoalition, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound> const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr<ModelCheckerHint> const& hint) : formula(formula), optimizationDirection(optimizationDirection), playerCoalition(playerCoalition), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) {
// Intentionally left empty.
}
// The formula that is to be checked.
std::reference_wrapper<FormulaType const> formula;
// If set, the probabilities will be minimized/maximized.
boost::optional<storm::OptimizationDirection> optimizationDirection;
// If set, the given coalitions of players will be assumed.
boost::optional<storm::logic::PlayerCoalition> playerCoalition;
// If set, the reward property has to be interpreted over this model.
boost::optional<std::string> rewardModel;
// If set to true, the model checker may decide to only compute the values for the initial states.
bool onlyInitialStatesRelevant;
// If set to true, we will create the appropriate shield.
bool shieldingTask = false;
// The according ShieldExpression.
boost::optional<std::shared_ptr<storm::logic::ShieldExpression const>> shieldingExpression;
// The bound with which the states will be compared.
boost::optional<storm::logic::Bound> bound;
// A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1.
bool qualitative;
// If supported by the model checker and the model formalism, schedulers to achieve a value will be produced
// if this flag is set.
bool produceSchedulers;
// A hint that might contain information that speeds up the modelchecking process (if supported by the model checker)
std::shared_ptr<ModelCheckerHint> hint;
};
}
}

Write Preview
Loading…
Cancel
Save