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

in the spirit of JP: up 

Former-commit-id: 3d7982c083
main
dehnert 10 years ago
parent
e3c4f5fa72
commit
ecfff3d2f9
5 changed files with 220 additions and 332 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 236
      src/modelchecker/AbstractModelChecker.cpp
  2. 50
      src/modelchecker/AbstractModelChecker.h
  3. 129
      src/modelchecker/CheckTask.cpp
  4. 124
      src/modelchecker/CheckTask.h
  5. 13
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

236
src/modelchecker/AbstractModelChecker.cpp
View File

@ -11,138 +11,144 @@
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::check(CheckTask<storm::logic::Formula> const& checkTask) {
storm::logic::Formula const& formula = checkTask.getFormula();
STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
CheckSettings<double> newCheckSettings = checkSettings ? checkSettings.get() : CheckSettings<double>::fromNestedFormula(formula);
if (formula.isStateFormula()) { if (formula.isStateFormula()) {
return this->checkStateFormula(formula.asStateFormula(), newCheckSettings);
return this->checkStateFormula(checkTask.replaceFormula(formula.asStateFormula()));
} else if (formula.isPathFormula()) { } else if (formula.isPathFormula()) {
return this->computeProbabilities(formula.asPathFormula(), newCheckSettings);
return this->computeProbabilities(checkTask.replaceFormula(formula.asPathFormula()));
} else if (formula.isRewardPathFormula()) { } else if (formula.isRewardPathFormula()) {
return this->computeRewards(formula.asRewardPathFormula(), newCheckSettings);
return this->computeRewards(checkTask.replaceFormula(formula.asRewardPathFormula()));
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(CheckTask<storm::logic::PathFormula> const& checkTask) {
storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
if (pathFormula.isBoundedUntilFormula()) { if (pathFormula.isBoundedUntilFormula()) {
return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), checkSettings);
return this->computeBoundedUntilProbabilities(checkTask.replaceFormula(pathFormula.asBoundedUntilFormula()));
} else if (pathFormula.isConditionalPathFormula()) { } else if (pathFormula.isConditionalPathFormula()) {
return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), checkSettings);
return this->computeConditionalProbabilities(checkTask.replaceFormula(pathFormula.asConditionalPathFormula()));
} else if (pathFormula.isEventuallyFormula()) { } else if (pathFormula.isEventuallyFormula()) {
return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), checkSettings);
return this->computeEventuallyProbabilities(checkTask.replaceFormula(pathFormula.asEventuallyFormula()));
} else if (pathFormula.isGloballyFormula()) { } else if (pathFormula.isGloballyFormula()) {
return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), checkSettings);
return this->computeGloballyProbabilities(checkTask.replaceFormula(pathFormula.asGloballyFormula()));
} else if (pathFormula.isUntilFormula()) { } else if (pathFormula.isUntilFormula()) {
return this->computeUntilProbabilities(pathFormula.asUntilFormula(), checkSettings);
return this->computeUntilProbabilities(checkTask.replaceFormula(pathFormula.asUntilFormula()));
} else if (pathFormula.isNextFormula()) { } else if (pathFormula.isNextFormula()) {
return this->computeNextProbabilities(pathFormula.asNextFormula(), checkSettings);
return this->computeNextProbabilities(checkTask.replaceFormula(pathFormula.asNextFormula()));
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid.");
} }
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::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
return this->computeUntilProbabilities(newFormula, checkSettings);
return this->computeUntilProbabilities(checkTask.replaceFormula(newFormula));
} }
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::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::RewardPathFormula> const& checkTask) {
storm::logic::RewardPathFormula const& rewardPathFormula = checkTask.getFormula();
if (rewardPathFormula.isCumulativeRewardFormula()) { if (rewardPathFormula.isCumulativeRewardFormula()) {
return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), checkSettings);
return this->computeCumulativeRewards(checkTask.replaceFormula(rewardPathFormula.asCumulativeRewardFormula()));
} else if (rewardPathFormula.isInstantaneousRewardFormula()) { } else if (rewardPathFormula.isInstantaneousRewardFormula()) {
return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), checkSettings);
return this->computeInstantaneousRewards(checkTask.replaceFormula(rewardPathFormula.asInstantaneousRewardFormula()));
} else if (rewardPathFormula.isReachabilityRewardFormula()) { } else if (rewardPathFormula.isReachabilityRewardFormula()) {
return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), checkSettings);
return this->computeReachabilityRewards(checkTask.replaceFormula(rewardPathFormula.asReachabilityRewardFormula()));
} else if (rewardPathFormula.isLongRunAverageRewardFormula()) { } else if (rewardPathFormula.isLongRunAverageRewardFormula()) {
return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), checkSettings);
return this->computeLongRunAverageRewards(checkTask.replaceFormula(rewardPathFormula.asLongRunAverageRewardFormula()));
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
} }
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::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
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::computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(CheckTask<storm::logic::StateFormula> const& checkTask) {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
if (stateFormula.isBinaryBooleanStateFormula()) { if (stateFormula.isBinaryBooleanStateFormula()) {
return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula(), checkSettings);
return this->checkBinaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asBinaryBooleanStateFormula()));
} else if (stateFormula.isUnaryBooleanStateFormula()) { } else if (stateFormula.isUnaryBooleanStateFormula()) {
return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula(), checkSettings);
return this->checkUnaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asUnaryBooleanStateFormula()));
} else if (stateFormula.isBooleanLiteralFormula()) { } else if (stateFormula.isBooleanLiteralFormula()) {
return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings);
return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula()));
} else if (stateFormula.isProbabilityOperatorFormula()) { } else if (stateFormula.isProbabilityOperatorFormula()) {
return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula(), checkSettings);
return this->checkProbabilityOperatorFormula(checkTask.replaceFormula(stateFormula.asProbabilityOperatorFormula()));
} else if (stateFormula.isRewardOperatorFormula()) { } else if (stateFormula.isRewardOperatorFormula()) {
return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula(), checkSettings);
return this->checkRewardOperatorFormula(checkTask.replaceFormula(stateFormula.asRewardOperatorFormula()));
} else if (stateFormula.isExpectedTimeOperatorFormula()) { } else if (stateFormula.isExpectedTimeOperatorFormula()) {
return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula(), checkSettings);
return this->checkExpectedTimeOperatorFormula(checkTask.replaceFormula(stateFormula.asExpectedTimeOperatorFormula()));
} else if (stateFormula.isLongRunAverageOperatorFormula()) { } else if (stateFormula.isLongRunAverageOperatorFormula()) {
return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula(), checkSettings);
return this->checkLongRunAverageOperatorFormula(checkTask.replaceFormula(stateFormula.asLongRunAverageOperatorFormula()));
} else if (stateFormula.isAtomicExpressionFormula()) { } else if (stateFormula.isAtomicExpressionFormula()) {
return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula(), checkSettings);
return this->checkAtomicExpressionFormula(checkTask.replaceFormula(stateFormula.asAtomicExpressionFormula()));
} else if (stateFormula.isAtomicLabelFormula()) { } else if (stateFormula.isAtomicLabelFormula()) {
return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula(), checkSettings);
return this->checkAtomicLabelFormula(checkTask.replaceFormula(stateFormula.asAtomicLabelFormula()));
} else if (stateFormula.isBooleanLiteralFormula()) { } else if (stateFormula.isBooleanLiteralFormula()) {
return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula(), checkSettings);
return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula()));
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(CheckTask<storm::logic::AtomicExpressionFormula> const& checkTask) {
storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula();
std::stringstream stream; std::stringstream stream;
stream << stateFormula.getExpression(); stream << stateFormula.getExpression();
return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()), checkSettings);
return this->checkAtomicLabelFormula(checkTask.replaceFormula(storm::logic::AtomicLabelFormula(stream.str())));
} }
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::checkAtomicLabelFormula(CheckTask<storm::logic::AtomicLabelFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkBinaryBooleanStateFormula(CheckTask<storm::logic::BinaryBooleanStateFormula> const& checkTask) {
storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); 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());
std::unique_ptr<CheckResult> rightResult = this->check(stateFormula.getRightSubformula().asStateFormula());
std::unique_ptr<CheckResult> leftResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getLeftSubformula().asStateFormula()));
std::unique_ptr<CheckResult> rightResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getRightSubformula().asStateFormula()));
STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results."); STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results.");
@ -157,35 +163,15 @@ namespace storm {
return leftResult; return leftResult;
} }
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::checkBooleanLiteralFormula(CheckTask<storm::logic::BooleanLiteralFormula> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) {
storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
CheckSettings<double> newCheckSettings =
// If the probability bound is 0 or 1, is suffices to do qualitative model checking.
bool qualitative = false;
if (stateFormula.hasBound()) {
if (storm::utility::isZero(stateFormula.getBound()) || storm::utility::isOne(stateFormula.getBound())) {
qualitative = true;
}
}
std::unique_ptr<CheckResult> result;
if (stateFormula.hasOptimalityType()) {
result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType());
} else if (stateFormula.hasBound()) {
if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Maximize);
} else {
result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, OptimizationDirection::Minimize);
}
} else {
result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative);
}
std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asPathFormula()));
if (stateFormula.hasBound()) { if (stateFormula.hasBound()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@ -195,95 +181,51 @@ namespace storm {
} }
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); 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.
bool qualitative = false;
if (stateFormula.hasBound()) {
if (storm::utility::isZero(stateFormula.getBound())) {
qualitative = true;
}
}
std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.replaceFormula(stateFormula.getSubformula().asRewardPathFormula()));
std::unique_ptr<CheckResult> result;
if (stateFormula.hasOptimalityType()) {
result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, stateFormula.getOptimalityType());
} else if (stateFormula.hasBound()) {
if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Maximize);
} else {
result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative, OptimizationDirection::Minimize);
}
} else {
result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), stateFormula.getOptionalRewardModelName(), qualitative);
}
if (stateFormula.hasBound()) {
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue());
} else { } else {
return result; return result;
} }
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask) {
storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); 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.
bool qualitative = false;
if (stateFormula.hasBound()) {
if (storm::utility::isZero(stateFormula.getBound())) {
qualitative = true;
}
}
std::unique_ptr<CheckResult> result;
if (stateFormula.hasOptimalityType()) {
result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType());
} else if (stateFormula.hasBound()) {
if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Maximize);
} else {
result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, OptimizationDirection::Minimize);
}
} else {
result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative);
}
std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.replaceFormula(stateFormula.getSubformula().asEventuallyFormula()));
if (stateFormula.hasBound()) {
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue());
} else { } else {
return result; return result;
} }
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula, boost::optional<CheckSettings<double>> checkSettings) {
std::unique_ptr<CheckResult> AbstractModelChecker::checkLongRunAverageOperatorFormula(CheckTask<storm::logic::LongRunAverageOperatorFormula> const& checkTask) {
storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
std::unique_ptr<CheckResult> result;
if (stateFormula.hasOptimalityType()) {
result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType());
} else if (stateFormula.hasBound()) {
if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Maximize);
} else {
result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false, OptimizationDirection::Minimize);
}
} else {
result = this->computeLongRunAverageProbabilities(stateFormula.getSubformula().asStateFormula(), false);
}
std::unique_ptr<CheckResult> result = this->computeLongRunAverageProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asStateFormula()));
if (stateFormula.hasBound()) {
return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue());
} else { } else {
return result; return result;
} }
} }
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());
std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask<storm::logic::UnaryBooleanStateFormula> const& checkTask) {
storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getSubformula()));
STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
if (stateFormula.isNot()) { if (stateFormula.isNot()) {
subResult->asQualitativeCheckResult().complement(); subResult->asQualitativeCheckResult().complement();

50
src/modelchecker/AbstractModelChecker.h
View File

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

129
src/modelchecker/CheckTask.cpp
View File

@ -1,129 +0,0 @@
#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>;
}
}

124
src/modelchecker/CheckTask.h
View File

@ -3,6 +3,9 @@
#include <boost/optional.hpp> #include <boost/optional.hpp>
#include "src/logic/Formulas.h"
#include "src/utility/constants.h"
#include "src/solver/OptimizationDirection.h" #include "src/solver/OptimizationDirection.h"
#include "src/logic/ComparisonType.h" #include "src/logic/ComparisonType.h"
@ -22,74 +25,157 @@ namespace storm {
/*! /*!
* Creates an empty task object with the default options. * Creates an empty task object with the default options.
*/ */
CheckTask();
CheckTask() : CheckTask(boost::none, boost::none, boost::none, false, boost::none, false, false) {
// Intentionally left empty.
}
/*! /*!
* Creates a task object with the default options for the given formula. * Creates a task object with the default options for the given formula.
*/ */
CheckTask(FormulaType const& formula);
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;
}
}
}
}
/*! /*!
* Converts the check task object to one with the given new formula type.
* 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.
*/ */
template<typename NewFormulaType> template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> convert();
CheckTask<NewFormulaType, ValueType> replaceFormula(NewFormulaType const& newFormula) const {
return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->initialStatesBound, this->qualitative, this->produceStrategies);
}
/*! /*!
* Retrieves whether this task is associated with a formula. * Retrieves whether this task is associated with a formula.
*/ */
bool hasFormula() const;
bool hasFormula() const {
return static_cast<bool>(formula);
}
/*! /*!
* Retrieves the formula from this task. * Retrieves the formula from this task.
*/ */
FormulaType const& getFormula() const;
FormulaType const& getFormula() const {
return formula.get().get();
}
/*! /*!
* Retrieves whether an optimization direction was set. * Retrieves whether an optimization direction was set.
*/ */
bool isOptimizationDirectionSet() const;
bool isOptimizationDirectionSet() const {
return static_cast<bool>(optimizationDirection);
}
/*! /*!
* Retrieves the optimization direction (if set). * Retrieves the optimization direction (if set).
*/ */
storm::OptimizationDirection const& getOptimizationDirection() const;
storm::OptimizationDirection const& getOptimizationDirection() const {
return optimizationDirection.get();
}
/*! /*!
* Retrieves whether a reward model was set. * Retrieves whether a reward model was set.
*/ */
bool isRewardModelSet() const;
bool isRewardModelSet() const {
return static_cast<bool>(rewardModel);
}
/*! /*!
* Retrieves the reward model over which to perform the checking (if set). * Retrieves the reward model over which to perform the checking (if set).
*/ */
std::string const& getRewardModel() const;
std::string const& getRewardModel() const {
return rewardModel.get();
}
/*! /*!
* Retrieves whether only the initial states are relevant in the computation. * Retrieves whether only the initial states are relevant in the computation.
*/ */
bool isOnlyInitialStatesRelevantSet() const;
bool isOnlyInitialStatesRelevantSet() const {
return onlyInitialStatesRelevant;
}
/*! /*!
* Retrieves whether there is a bound with which the values for the initial states will be compared.
* Retrieves whether there is a bound with which the values for the states will be compared.
*/ */
bool isInitialStatesBoundSet() const;
bool isBoundSet() const {
return static_cast<bool>(bound);
}
/*!
* Retrieves the value of the bound (if set).
*/
ValueType const& getBoundValue() const {
return bound.get().second;
}
/*!
* Retrieves the comparison type of the bound (if set).
*/
storm::logic::ComparisonType const& getBoundComparisonType() const {
return bound.get().first;
}
/*! /*!
* Retrieves the bound for the initial states (if set). * Retrieves the bound for the initial states (if set).
*/ */
std::pair<storm::logic::ComparisonType, ValueType> const& getInitialStatesBound() const;
std::pair<storm::logic::ComparisonType, ValueType> const& getBound() const {
return bound.get();
}
/*! /*!
* Retrieves whether the computation only needs to be performed qualitatively, because the values will only * Retrieves whether the computation only needs to be performed qualitatively, because the values will only
* be compared to 0/1. * be compared to 0/1.
*/ */
bool isQualitativeSet() const;
bool isQualitativeSet() const {
return qualitative;
}
/*! /*!
* Retrieves whether strategies are to be produced (if supported). * Retrieves whether strategies are to be produced (if supported).
*/ */
bool isProduceStrategiesSet() const;
bool isProduceStrategiesSet() const {
return produceStrategies;
}
private: private:
/*! /*!
@ -107,7 +193,9 @@ namespace storm {
* @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve * @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. * a value will be produced if this flag is set.
*/ */
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);
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& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) {
// Intentionally left empty.
}
// The formula that is to be checked. // The formula that is to be checked.
boost::optional<std::reference_wrapper<FormulaType>> formula; boost::optional<std::reference_wrapper<FormulaType>> formula;
@ -122,7 +210,7 @@ namespace storm {
bool onlyInitialStatesRelevant; bool onlyInitialStatesRelevant;
// The bound with which the initial states will be compared. // The bound with which the initial states will be compared.
boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> bound;
// A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1.
bool qualitative; bool qualitative;

13
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -8,16 +8,6 @@
#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h"
namespace storm { namespace storm {
namespace counterexamples {
template<typename ValueType>
class SMTMinimalCommandSetGenerator;
template<typename ValueType>
class MILPMinimalLabelSetGenerator;
}
namespace modelchecker { namespace modelchecker {
template<class SparseMdpModelType> template<class SparseMdpModelType>
class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker<SparseMdpModelType> { class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker<SparseMdpModelType> {
@ -25,9 +15,6 @@ namespace storm {
typedef typename SparseMdpModelType::ValueType ValueType; typedef typename SparseMdpModelType::ValueType ValueType;
typedef typename SparseMdpModelType::RewardModelType RewardModelType; typedef typename SparseMdpModelType::RewardModelType RewardModelType;
friend class storm::counterexamples::SMTMinimalCommandSetGenerator<ValueType>;
friend class storm::counterexamples::MILPMinimalLabelSetGenerator<ValueType>;
explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model); explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model);
explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& MinMaxLinearEquationSolverFactory); explicit SparseMdpPrctlModelChecker(SparseMdpModelType const& model, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType>>&& MinMaxLinearEquationSolverFactory);

Write Preview
Loading…
Cancel
Save