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

tests working again 

Former-commit-id: 58e97ea35b
main
dehnert 9 years ago
parent
dc8a5b11e0
commit
7b643fe166
7 changed files with 35 additions and 32 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. 2
      src/logic/FormulaInformation.cpp
  2. 5
      src/logic/FormulaInformation.h
  3. 12
      src/logic/FragmentChecker.cpp
  4. 4
      src/logic/FragmentSpecification.cpp
  5. 34
      src/modelchecker/AbstractModelChecker.cpp
  6. 2
      src/modelchecker/AbstractModelChecker.h
  7. 8
      src/storage/bisimulation/BisimulationDecomposition.h

2
src/logic/FormulaInformation.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
} }
bool FormulaInformation::containsBoundedUntilFormula() const { bool FormulaInformation::containsBoundedUntilFormula() const {
return this-mContainsBoundedUntilFormula;
return this->mContainsBoundedUntilFormula;
} }
FormulaInformation FormulaInformation::join(FormulaInformation const& other) { FormulaInformation FormulaInformation::join(FormulaInformation const& other) {

5
src/logic/FormulaInformation.h
View File

@ -7,6 +7,11 @@ namespace storm {
class FormulaInformation { class FormulaInformation {
public: public:
FormulaInformation(); 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 containsRewardOperator() const;
bool containsNextFormula() const; bool containsNextFormula() const;
bool containsBoundedUntilFormula() const; bool containsBoundedUntilFormula() const;

12
src/logic/FragmentChecker.cpp
View File

@ -99,7 +99,7 @@ namespace storm {
result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed(); result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed();
result = result && f.getSubformula().isStateFormula(); result = result && f.getSubformula().isStateFormula();
} }
result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result; return result;
} }
@ -108,7 +108,7 @@ namespace storm {
bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed(); bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed();
result = result && f.getSubformula().isExpectedTimePathFormula(); result = result && f.getSubformula().isExpectedTimePathFormula();
if (!inherited.getSpecification().areNestedOperatorsAllowed()) { if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else { } else {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }
@ -135,7 +135,7 @@ namespace storm {
bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed(); bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed();
result = result && f.getSubformula().isStateFormula(); result = result && f.getSubformula().isStateFormula();
if (!inherited.getSpecification().areNestedOperatorsAllowed()) { if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else { } else {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }
@ -160,9 +160,9 @@ namespace storm {
boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); bool result = inherited.getSpecification().areProbabilityOperatorsAllowed();
result = result && f.getSubformula().isProbabilityPathFormula();
result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula());
if (!inherited.getSpecification().areNestedOperatorsAllowed()) { if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else { } else {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }
@ -174,7 +174,7 @@ namespace storm {
bool result = inherited.getSpecification().areRewardOperatorsAllowed(); bool result = inherited.getSpecification().areRewardOperatorsAllowed();
result = result && f.getSubformula().isRewardPathFormula(); result = result && f.getSubformula().isRewardPathFormula();
if (!inherited.getSpecification().areNestedOperatorsAllowed()) { if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else { } else {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }

4
src/logic/FragmentSpecification.cpp
View File

@ -1,5 +1,7 @@
#include "src/logic/FragmentSpecification.h" #include "src/logic/FragmentSpecification.h"
#include <iostream>
namespace storm { namespace storm {
namespace logic { namespace logic {
@ -50,7 +52,7 @@ namespace storm {
} }
FragmentSpecification csrl() { FragmentSpecification csrl() {
FragmentSpecification csrl;
FragmentSpecification csrl = csl();
csrl.setRewardOperatorsAllowed(true); csrl.setRewardOperatorsAllowed(true);
csrl.setCumulativeRewardFormulasAllowed(true); csrl.setCumulativeRewardFormulasAllowed(true);

34
src/modelchecker/AbstractModelChecker.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
} else if (formula.isPathFormula()) { } else if (formula.isPathFormula()) {
if (formula.isProbabilityPathFormula()) { if (formula.isProbabilityPathFormula()) {
return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula()));
return this->computeProbabilities(checkTask);
} else if (formula.isRewardPathFormula()) { } else if (formula.isRewardPathFormula()) {
return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula())); 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."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
} }
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(CheckTask<storm::logic::PathFormula> 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<CheckResult> AbstractModelChecker::computeProbabilities(CheckTask<storm::logic::Formula> 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<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) { std::unique_ptr<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) {
@ -78,7 +80,7 @@ namespace storm {
return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula())); return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula()));
} else if (rewardPathFormula.isInstantaneousRewardFormula()) { } else if (rewardPathFormula.isInstantaneousRewardFormula()) {
return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula())); return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula()));
} else if (rewardPathFormula.isEventuallyFormula()) {
} else if (rewardPathFormula.isReachabilityRewardFormula()) {
return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula())); return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula()));
} else if (rewardPathFormula.isLongRunAverageRewardFormula()) { } else if (rewardPathFormula.isLongRunAverageRewardFormula()) {
return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula())); return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula()));
@ -177,7 +179,7 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) { std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) {
storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula(); storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula()));
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.");

2
src/modelchecker/AbstractModelChecker.h
View File

@ -35,7 +35,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> check(CheckTask<storm::logic::Formula> const& checkTask); 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(CheckTask<storm::logic::PathFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeProbabilities(CheckTask<storm::logic::Formula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask); virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask); virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask);
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask); virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);

8
src/storage/bisimulation/BisimulationDecomposition.h
View File

@ -139,10 +139,7 @@ namespace storm {
private: private:
boost::optional<OptimizationDirection> optimalityType; boost::optional<OptimizationDirection> optimalityType;
/// A flag that indicates whether or not the state-rewards of the model are to be respected (and should /// 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). /// be kept in the quotient model, if one is built).
bool keepRewards; bool keepRewards;
@ -154,9 +151,6 @@ namespace storm {
/// when computing strong bisimulation equivalence. /// when computing strong bisimulation equivalence.
bool bounded; bool bounded;
/*! /*!
* Sets the options under the assumption that the given formula is the only one that is to be checked. * Sets the options under the assumption that the given formula is the only one that is to be checked.
* *

Write Preview
Loading…
Cancel
Save