Browse Source

adding needed methods for more formula classes

tempestpy_adaptions
gereon 12 years ago
parent
commit
8077952331
  1. 7
      src/formula/And.h
  2. 5
      src/formula/BoundOperator.h
  3. 5
      src/formula/BoundedEventually.h
  4. 5
      src/formula/CumulativeReward.h
  5. 5
      src/formula/Globally.h
  6. 5
      src/formula/InstantaneousReward.h
  7. 5
      src/formula/Next.h
  8. 7
      src/formula/Or.h
  9. 2
      src/formula/ProbabilisticBoundOperator.h
  10. 1
      src/formula/RewardBoundOperator.h

7
src/formula/And.h

@ -9,6 +9,7 @@
#define STORM_FORMULA_AND_H_
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include <string>
@ -149,9 +150,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
private:
AbstractStateFormula<T>* left;

5
src/formula/BoundOperator.h

@ -10,6 +10,7 @@
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include "src/utility/ConstTemplates.h"
@ -157,6 +158,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->pathFormula);
}
private:
ComparisonType comparisonOperator;

5
src/formula/BoundedEventually.h

@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
#include "src/modelChecker/AbstractModelChecker.h"
@ -147,6 +148,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
private:
AbstractStateFormula<T>* child;

5
src/formula/CumulativeReward.h

@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -111,6 +112,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
private:
uint_fast64_t bound;

5
src/formula/Globally.h

@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@ -121,6 +122,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
private:
AbstractStateFormula<T>* child;

5
src/formula/InstantaneousReward.h

@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -111,6 +112,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
private:
uint_fast64_t bound;

5
src/formula/Next.h

@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@ -123,6 +124,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
private:
AbstractStateFormula<T>* child;

7
src/formula/Or.h

@ -8,7 +8,8 @@
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
#include "AbstractStateFormula.h"
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
namespace formula {
@ -150,6 +151,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
private:
AbstractStateFormula<T>* left;

2
src/formula/ProbabilisticBoundOperator.h

@ -45,10 +45,12 @@ public:
/*!
* Empty constructor
*/
//! TODO: this constructor should give a comparisontype as first argument
ProbabilisticBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
// Intentionally left empty
}
/*!
* Constructor
*

1
src/formula/RewardBoundOperator.h

@ -44,6 +44,7 @@ public:
/*!
* Empty constructor
*/
//! TODO: this constructor should give a comparisontype as first argument
RewardBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
// Intentionally left empty
}

Loading…
Cancel
Save