diff --git a/src/logic/FormulaInformation.cpp b/src/logic/FormulaInformation.cpp index b49f4a23b..3cbca1323 100644 --- a/src/logic/FormulaInformation.cpp +++ b/src/logic/FormulaInformation.cpp @@ -17,7 +17,7 @@ namespace storm { } bool FormulaInformation::containsBoundedUntilFormula() const { - return this-mContainsBoundedUntilFormula; + return this->mContainsBoundedUntilFormula; } FormulaInformation FormulaInformation::join(FormulaInformation const& other) { diff --git a/src/logic/FormulaInformation.h b/src/logic/FormulaInformation.h index 53269696c..6dfc90b8e 100644 --- a/src/logic/FormulaInformation.h +++ b/src/logic/FormulaInformation.h @@ -7,6 +7,11 @@ namespace storm { class FormulaInformation { public: FormulaInformation(); + FormulaInformation(FormulaInformation const& other) = default; + FormulaInformation(FormulaInformation&& other) = default; + FormulaInformation& operator=(FormulaInformation const& other) = default; + FormulaInformation& operator=(FormulaInformation&& other) = default; + bool containsRewardOperator() const; bool containsNextFormula() const; bool containsBoundedUntilFormula() const; diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 405b75a27..8e701cedd 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -99,7 +99,7 @@ namespace storm { result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed(); result = result && f.getSubformula().isStateFormula(); } - result && boost::any_cast(f.getSubformula().accept(*this, data)); + result = result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; } @@ -108,7 +108,7 @@ namespace storm { bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed(); result = result && f.getSubformula().isExpectedTimePathFormula(); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { - result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { result = result && boost::any_cast(f.getSubformula().accept(*this, data)); } @@ -135,7 +135,7 @@ namespace storm { bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed(); result = result && f.getSubformula().isStateFormula(); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { - result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { result = result && boost::any_cast(f.getSubformula().accept(*this, data)); } @@ -160,9 +160,9 @@ namespace storm { boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); - result = result && f.getSubformula().isProbabilityPathFormula(); + result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula()); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { - result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { result = result && boost::any_cast(f.getSubformula().accept(*this, data)); } @@ -174,7 +174,7 @@ namespace storm { bool result = inherited.getSpecification().areRewardOperatorsAllowed(); result = result && f.getSubformula().isRewardPathFormula(); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { - result = result && boost::any_cast(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false))); + result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { result = result && boost::any_cast(f.getSubformula().accept(*this, data)); } diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index d8c02a18e..378fe3a88 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -1,5 +1,7 @@ #include "src/logic/FragmentSpecification.h" +#include + namespace storm { namespace logic { @@ -50,7 +52,7 @@ namespace storm { } FragmentSpecification csrl() { - FragmentSpecification csrl; + FragmentSpecification csrl = csl(); csrl.setRewardOperatorsAllowed(true); csrl.setCumulativeRewardFormulasAllowed(true); diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index e7fabdec1..8f7a7b2f5 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -18,7 +18,7 @@ namespace storm { return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); } else if (formula.isPathFormula()) { if (formula.isProbabilityPathFormula()) { - return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula())); + return this->computeProbabilities(checkTask); } else if (formula.isRewardPathFormula()) { return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula())); } @@ -30,20 +30,22 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } - std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { - storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); - if (pathFormula.isBoundedUntilFormula()) { - return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(pathFormula.asBoundedUntilFormula())); - } else if (pathFormula.isEventuallyFormula()) { - return this->computeEventuallyProbabilities(checkTask.substituteFormula(pathFormula.asEventuallyFormula())); - } else if (pathFormula.isGloballyFormula()) { - return this->computeGloballyProbabilities(checkTask.substituteFormula(pathFormula.asGloballyFormula())); - } else if (pathFormula.isUntilFormula()) { - return this->computeUntilProbabilities(checkTask.substituteFormula(pathFormula.asUntilFormula())); - } else if (pathFormula.isNextFormula()) { - return this->computeNextProbabilities(checkTask.substituteFormula(pathFormula.asNextFormula())); + std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { + storm::logic::Formula const& formula = checkTask.getFormula(); + if (formula.isBoundedUntilFormula()) { + return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula())); + } else if (formula.isEventuallyFormula()) { + return this->computeEventuallyProbabilities(checkTask.substituteFormula(formula.asEventuallyFormula())); + } else if (formula.isGloballyFormula()) { + return this->computeGloballyProbabilities(checkTask.substituteFormula(formula.asGloballyFormula())); + } else if (formula.isUntilFormula()) { + return this->computeUntilProbabilities(checkTask.substituteFormula(formula.asUntilFormula())); + } else if (formula.isNextFormula()) { + return this->computeNextProbabilities(checkTask.substituteFormula(formula.asNextFormula())); + } else if (formula.isConditionalProbabilityFormula()) { + return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula())); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { @@ -78,7 +80,7 @@ namespace storm { return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula())); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula())); - } else if (rewardPathFormula.isEventuallyFormula()) { + } else if (rewardPathFormula.isReachabilityRewardFormula()) { return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula())); } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula())); @@ -177,7 +179,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); + std::unique_ptr result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula())); if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index c79302808..fc7fe2fdd 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -35,7 +35,7 @@ namespace storm { virtual std::unique_ptr check(CheckTask const& checkTask); // The methods to compute probabilities for path formulas. - virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); + virtual std::unique_ptr computeProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask); virtual std::unique_ptr computeEventuallyProbabilities(CheckTask const& checkTask); diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 420d528c9..dc1c73261 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -139,10 +139,7 @@ namespace storm { private: boost::optional optimalityType; - - - - + /// A flag that indicates whether or not the state-rewards of the model are to be respected (and should /// be kept in the quotient model, if one is built). bool keepRewards; @@ -154,9 +151,6 @@ namespace storm { /// when computing strong bisimulation equivalence. bool bounded; - - - /*! * Sets the options under the assumption that the given formula is the only one that is to be checked. *