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

replace in model checker interface (part 3) 

Former-commit-id: c550b8198f
tempestpy_adaptions
dehnert 9 years ago
parent
16be4f9adc
commit
5dd2dff92a
2 changed files with 25 additions and 24 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. 29
      src/modelchecker/AbstractModelChecker.cpp
  2. 20
      src/modelchecker/AbstractModelChecker.h

29
src/modelchecker/AbstractModelChecker.cpp
View File

@ -13,29 +13,30 @@ namespace storm {
namespace modelchecker {
std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula, boost::optional<CheckSettings<double>> const& 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);
if (formula.isStateFormula()) {
return this->checkStateFormula(formula.asStateFormula());
return this->checkStateFormula(formula.asStateFormula(), settingsToUse);
} else if (formula.isPathFormula()) {
return this->computeProbabilities(formula.asPathFormula());
return this->computeProbabilities(formula.asPathFormula(), settingsToUse);
} else if (formula.isRewardPathFormula()) {
return this->computeRewards(formula.asRewardPathFormula());
return this->computeRewards(formula.asRewardPathFormula(), settingsToUse);
}
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) {
if (pathFormula.isBoundedUntilFormula()) {
return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), qualitative, optimalityType);
return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), checkSettings);
} else if (pathFormula.isConditionalPathFormula()) {
return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), qualitative, optimalityType);
return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), checkSettings);
} else if (pathFormula.isEventuallyFormula()) {
return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), qualitative, optimalityType);
return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), checkSettings);
} else if (pathFormula.isGloballyFormula()) {
return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), qualitative, optimalityType);
return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), checkSettings);
} else if (pathFormula.isUntilFormula()) {
return this->computeUntilProbabilities(pathFormula.asUntilFormula(), qualitative, optimalityType);
return this->computeUntilProbabilities(pathFormula.asUntilFormula(), checkSettings);
} else if (pathFormula.isNextFormula()) {
return this->computeNextProbabilities(pathFormula.asNextFormula(), qualitative, optimalityType);
return this->computeNextProbabilities(pathFormula.asNextFormula(), checkSettings);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid.");
}
@ -50,7 +51,7 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
return this->computeUntilProbabilities(newFormula, qualitative, optimalityType);
return this->computeUntilProbabilities(newFormula, checkSettings);
}
std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, CheckSettings<double> const& checkSettings) {
@ -67,13 +68,13 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, CheckSettings<double> const& checkSettings) {
if (rewardPathFormula.isCumulativeRewardFormula()) {
return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), rewardModelName, qualitative, optimalityType);
return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), checkSettings);
} else if (rewardPathFormula.isInstantaneousRewardFormula()) {
return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), rewardModelName, qualitative, optimalityType);
return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), checkSettings);
} else if (rewardPathFormula.isReachabilityRewardFormula()) {
return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), rewardModelName, qualitative, optimalityType);
return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), checkSettings);
} else if (rewardPathFormula.isLongRunAverageRewardFormula()) {
return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), rewardModelName, qualitative, optimalityType);
return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), checkSettings);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
}

20
src/modelchecker/AbstractModelChecker.h
View File

@ -56,16 +56,16 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, CheckSettings<double> const& checkSettings);
// The methods to check state formulas.
virtual std::unique_ptr<CheckResult> checkStateFormula(storm::logic::StateFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula);
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula);
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);
};
}
}

Write Preview
Loading…
Cancel
Save