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

more work on customizing checking process 

Former-commit-id: 93e5895f77
tempestpy_adaptions
dehnert 9 years ago
parent
280af18341
commit
e3c4f5fa72
7 changed files with 215 additions and 208 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. 4
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 2
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  3. 58
      src/modelchecker/AbstractModelChecker.cpp
  4. 52
      src/modelchecker/AbstractModelChecker.h
  5. 127
      src/modelchecker/CheckSettings.cpp
  6. 129
      src/modelchecker/CheckTask.cpp
  7. 51
      src/modelchecker/CheckTask.h

4
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -264,6 +264,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
#endif
}
if (!std::is_same<ValueType, double>::value) {
doMagic<ValueType>(iasdfasdpfoy);
}
// If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
if (options.labelsToBuild) {

2
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -957,8 +957,6 @@ namespace storm {
// (4.2) Construct constraint system.
buildConstraintSystem(*solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts);
solver->writeModelToFile("model.lp");
// (4.3) Optimize the model.
solver->optimize();

58
src/modelchecker/AbstractModelChecker.cpp
View File

@ -11,20 +11,20 @@
namespace storm {
namespace modelchecker {
std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
CheckSettings<double> settingsToUse = checkSettings ? checkSettings.get() : CheckSettings<double>::fromToplevelFormula(formula);
CheckSettings<double> newCheckSettings = checkSettings ? checkSettings.get() : CheckSettings<double>::fromNestedFormula(formula);
if (formula.isStateFormula()) {
return this->checkStateFormula(formula.asStateFormula(), settingsToUse);
return this->checkStateFormula(formula.asStateFormula(), newCheckSettings);
} else if (formula.isPathFormula()) {
return this->computeProbabilities(formula.asPathFormula(), settingsToUse);
return this->computeProbabilities(formula.asPathFormula(), newCheckSettings);
} else if (formula.isRewardPathFormula()) {
return this->computeRewards(formula.asRewardPathFormula(), settingsToUse);
return this->computeRewards(formula.asRewardPathFormula(), newCheckSettings);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
if (pathFormula.isBoundedUntilFormula()) {
return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), checkSettings);
} else if (pathFormula.isConditionalPathFormula()) {
@ -41,32 +41,32 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
return this->computeUntilProbabilities(newFormula, checkSettings);
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
if (rewardPathFormula.isCumulativeRewardFormula()) {
return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), checkSettings);
} else if (rewardPathFormula.isInstantaneousRewardFormula()) {
@ -79,31 +79,31 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& eventuallyFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& eventuallyFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
if (stateFormula.isBinaryBooleanStateFormula()) {
return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula(), checkSettings);
} else if (stateFormula.isUnaryBooleanStateFormula()) {
@ -128,17 +128,17 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::stringstream stream;
stream << stateFormula.getExpression();
return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()), checkSettings);
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
std::unique_ptr<CheckResult> leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula());
@ -157,11 +157,11 @@ namespace storm {
return leftResult;
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << ".");
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
CheckSettings<double> newCheckSettings =
@ -195,7 +195,7 @@ namespace storm {
}
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
// If the reward bound is 0, is suffices to do qualitative model checking.
@ -227,7 +227,7 @@ namespace storm {
}
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
// If the reward bound is 0, is suffices to do qualitative model checking.
@ -259,7 +259,7 @@ namespace storm {
}
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
std::unique_ptr<CheckResult> result;
@ -282,7 +282,7 @@ namespace storm {
}
}
std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, CheckSettings<double> const& checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> subResult = this->check(stateFormula.getSubformula());
STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
if (stateFormula.isNot()) {

52
src/modelchecker/AbstractModelChecker.h
View File

@ -3,7 +3,7 @@
#include <boost/optional.hpp>
#include "src/modelchecker/CheckSettings.h"
#include "src/modelchecker/CheckTask.h"
#include "src/logic/Formulas.h"
#include "src/solver/OptimizationDirection.h"
@ -33,39 +33,39 @@ namespace storm {
* @param checkSettings If provided, this object is used to customize the checking process.
* @return The verification result.
*/
virtual std::unique_ptr<CheckResult> check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> const& checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> check(CheckTask<> storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
// The methods to compute probabilities for path formulas.
virtual std::unique_ptr<CheckResult> computeProbabilities(storm::logic::PathFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
// The methods to compute the rewards for path formulas.
virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
// The methods to compute the long-run average and expected time.
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
// The methods to check state formulas.
virtual std::unique_ptr<CheckResult> checkStateFormula(storm::logic::StateFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, CheckSettings<double> const& checkSettings);
virtual std::unique_ptr<CheckResult> checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings);
virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings = boost::none);
};
}
}

127
src/modelchecker/CheckSettings.cpp
View File

@ -1,127 +0,0 @@
#include "src/modelchecker/CheckSettings.h"
#include "src/logic/Formulas.h"
#include "src/utility/constants.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
CheckSettings<ValueType>::CheckSettings() : CheckSettings(boost::none, boost::none, false, boost::none, false, false) {
// Intentionally left empty.
}
template<typename ValueType>
CheckSettings<ValueType>::CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies) : optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) {
// Intentionally left empty.
}
template<typename ValueType>
CheckSettings<ValueType> CheckSettings<ValueType>::fromToplevelFormula(storm::logic::Formula const& formula) {
return fromFormula(formula, true);
}
template<typename ValueType>
CheckSettings<ValueType> CheckSettings<ValueType>::fromNestedFormula(storm::logic::Formula const& formula) {
return fromFormula(formula, false);
}
template<typename ValueType>
CheckSettings<ValueType> CheckSettings<ValueType>::fromFormula(storm::logic::Formula const& formula, bool toplevel) {
boost::optional<storm::OptimizationDirection> optimizationDirection;
boost::optional<std::string> rewardModel;
boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
bool qualitative = false;
bool onlyInitialStatesRelevant = !toplevel;
bool produceStrategies = false;
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
if (probabilityOperatorFormula.hasOptimalityType()) {
optimizationDirection = probabilityOperatorFormula.getOptimalityType();
}
if (probabilityOperatorFormula.hasBound()) {
if (onlyInitialStatesRelevant) {
initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast<ValueType>(probabilityOperatorFormula.getBound()));
}
if (probabilityOperatorFormula.getBound() == storm::utility::zero<ValueType>() || probabilityOperatorFormula.getBound() == storm::utility::one<ValueType>()) {
qualitative = true;
}
if (!optimizationDirection) {
optimizationDirection = probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
}
} else if (formula.isRewardOperatorFormula()) {
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
if (rewardOperatorFormula.hasOptimalityType()) {
optimizationDirection = rewardOperatorFormula.getOptimalityType();
}
if (rewardOperatorFormula.hasBound()) {
if (onlyInitialStatesRelevant) {
initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast<ValueType>(rewardOperatorFormula.getBound()));
}
if (rewardOperatorFormula.getBound() == storm::utility::zero<ValueType>()) {
qualitative = true;
}
if (!optimizationDirection) {
optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
}
}
return CheckSettings<ValueType>(optimizationDirection, rewardModel, onlyInitialStatesRelevant, initialStatesBound, qualitative, produceStrategies);
}
template<typename ValueType>
bool CheckSettings<ValueType>::isOptimizationDirectionSet() const {
return static_cast<bool>(optimizationDirection);
}
template<typename ValueType>
storm::OptimizationDirection const& CheckSettings<ValueType>::getOptimizationDirection() const {
return optimizationDirection.get();
}
template<typename ValueType>
bool CheckSettings<ValueType>::isRewardModelSet() const {
return static_cast<bool>(rewardModel);
}
template<typename ValueType>
std::string const& CheckSettings<ValueType>::getRewardModel() const {
return rewardModel.get();
}
template<typename ValueType>
bool CheckSettings<ValueType>::isOnlyInitialStatesRelevantSet() const {
return onlyInitialStatesRelevant;
}
template<typename ValueType>
bool CheckSettings<ValueType>::isInitialStatesBoundSet() const {
return static_cast<bool>(initialStatesBound);
}
template<typename ValueType>
std::pair<storm::logic::ComparisonType, ValueType> const& CheckSettings<ValueType>::getInitialStatesBound() const {
return initialStatesBound.get();
}
template<typename ValueType>
bool CheckSettings<ValueType>::isQualitativeSet() const {
return qualitative;
}
template<typename ValueType>
bool CheckSettings<ValueType>::isProduceStrategiesSet() const {
return produceStrategies;
}
template class CheckSettings<double>;
}
}

129
src/modelchecker/CheckTask.cpp
View File

@ -0,0 +1,129 @@
#include "src/modelchecker/CheckTask.h"
#include "src/logic/Formulas.h"
#include "src/utility/constants.h"
namespace storm {
namespace modelchecker {
template<typename FormulaType, typename ValueType>
CheckTask<FormulaType, ValueType>::CheckTask() : CheckTask(boost::none, boost::none, boost::none, false, boost::none, false, false) {
// Intentionally left empty.
}
template<typename FormulaType, typename ValueType>
CheckTask<FormulaType, ValueType>::CheckTask(boost::optional<std::reference_wrapper<FormulaType>> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) {
// Intentionally left empty.
}
template<typename FormulaType, typename ValueType>
CheckTask<FormulaType, ValueType>::CheckTask(FormulaType const& formula) {
this->onlyInitialStatesRelevant = false;
this->produceStrategies = true;
this->qualitative = false;
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
if (probabilityOperatorFormula.hasOptimalityType()) {
this->optimizationDirection = probabilityOperatorFormula.getOptimalityType();
}
if (probabilityOperatorFormula.hasBound()) {
if (onlyInitialStatesRelevant) {
this->initialStatesBound = std::make_pair(probabilityOperatorFormula.getComparisonType(), static_cast<ValueType>(probabilityOperatorFormula.getBound()));
}
if (probabilityOperatorFormula.getBound() == storm::utility::zero<ValueType>() || probabilityOperatorFormula.getBound() == storm::utility::one<ValueType>()) {
this->qualitative = true;
}
if (!optimizationDirection) {
this->optimizationDirection = probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || probabilityOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
}
} else if (formula.isRewardOperatorFormula()) {
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
if (rewardOperatorFormula.hasOptimalityType()) {
this->optimizationDirection = rewardOperatorFormula.getOptimalityType();
}
if (rewardOperatorFormula.hasBound()) {
if (onlyInitialStatesRelevant) {
this->initialStatesBound = std::make_pair(rewardOperatorFormula.getComparisonType(), static_cast<ValueType>(rewardOperatorFormula.getBound()));
}
if (rewardOperatorFormula.getBound() == storm::utility::zero<ValueType>()) {
this->qualitative = true;
}
if (!optimizationDirection) {
this->optimizationDirection = rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || rewardOperatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
}
}
}
template<typename FormulaType, typename ValueType>
template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> CheckTask<FormulaType, ValueType>::convert() {
return CheckTask<NewFormulaType, ValueType>();
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::hasFormula() const {
return static_cast<bool>(formula);
}
template<typename FormulaType, typename ValueType>
FormulaType const& CheckTask<FormulaType, ValueType>::getFormula() const {
return formula.get().get();
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isOptimizationDirectionSet() const {
return static_cast<bool>(optimizationDirection);
}
template<typename FormulaType, typename ValueType>
storm::OptimizationDirection const& CheckTask<FormulaType, ValueType>::getOptimizationDirection() const {
return optimizationDirection.get();
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isRewardModelSet() const {
return static_cast<bool>(rewardModel);
}
template<typename FormulaType, typename ValueType>
std::string const& CheckTask<FormulaType, ValueType>::getRewardModel() const {
return rewardModel.get();
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isOnlyInitialStatesRelevantSet() const {
return onlyInitialStatesRelevant;
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isInitialStatesBoundSet() const {
return static_cast<bool>(initialStatesBound);
}
template<typename FormulaType, typename ValueType>
std::pair<storm::logic::ComparisonType, ValueType> const& CheckTask<FormulaType, ValueType>::getInitialStatesBound() const {
return initialStatesBound.get();
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isQualitativeSet() const {
return qualitative;
}
template<typename FormulaType, typename ValueType>
bool CheckTask<FormulaType, ValueType>::isProduceStrategiesSet() const {
return produceStrategies;
}
template class CheckTask<storm::logic::ProbabilityOperatorFormula, double>;
}
}

51
src/modelchecker/CheckSettings.h → src/modelchecker/CheckTask.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_MODELCHECKER_CHECKSETTINGS_H_
#define STORM_MODELCHECKER_CHECKSETTINGS_H_
#ifndef STORM_MODELCHECKER_CHECKTASK_H_
#define STORM_MODELCHECKER_CHECKTASK_H_
#include <boost/optional.hpp>
@ -16,27 +16,34 @@ namespace storm {
/*
* This class is used to customize the checking process of a formula.
*/
template<typename ValueType>
class CheckSettings {
template<typename FormulaType, typename ValueType = double>
class CheckTask {
public:
/*!
* Creates a settings object with the default options.
* Creates an empty task object with the default options.
*/
CheckSettings();
CheckTask();
/*!
* Creates a settings object for the given top-level formula.
*
* @param formula The formula for which to create the settings.
* Creates a task object with the default options for the given formula.
*/
static CheckSettings fromToplevelFormula(storm::logic::Formula const& formula);
CheckTask(FormulaType const& formula);
/*!
* Creates a settings object for the given formula that is nested within another formula.
*
* @param formula The formula for which to create the settings.
* Converts the check task object to one with the given new formula type.
*/
template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> convert();
/*!
* Retrieves whether this task is associated with a formula.
*/
static CheckSettings fromNestedFormula(storm::logic::Formula const& formula);
bool hasFormula() const;
/*!
* Retrieves the formula from this task.
*/
FormulaType const& getFormula() const;
/*!
* Retrieves whether an optimization direction was set.
@ -86,8 +93,9 @@ namespace storm {
private:
/*!
* Creates a settings object with the given options.
* Creates a task object with the given options.
*
* @param formula The formula to attach to the task.
* @param optimizationDirection If set, the probabilities will be minimized/maximized.
* @param rewardModelName If given, the checking has to be done wrt. to this reward model.
* @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values
@ -99,15 +107,10 @@ namespace storm {
* @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve
* a value will be produced if this flag is set.
*/
CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
CheckTask(boost::optional<std::reference_wrapper<FormulaType>> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
/*!
* Creates a settings object for the given formula.
*
* @param formula The formula for which to create the settings.
* @param toplevel Indicates whether this formula is the top-level formula.
*/
static CheckSettings fromFormula(storm::logic::Formula const& formula, bool toplevel);
// The formula that is to be checked.
boost::optional<std::reference_wrapper<FormulaType>> formula;
// If set, the probabilities will be minimized/maximized.
boost::optional<storm::OptimizationDirection> optimizationDirection;
@ -132,4 +135,4 @@ namespace storm {
}
}
#endif /* STORM_MODELCHECKER_CHECKSETTINGS_H_ */
#endif /* STORM_MODELCHECKER_CHECKTASK_H_ */
Write Preview
Loading…
Cancel
Save