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

first "kind of working" version.

main
gereon 12 years ago
parent
3a73e0838c
commit
df91728da0
28 changed files with 525 additions and 324 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. 65
      src/formula/AbstractFormula.h
  2. 32
      src/formula/AbstractPathFormula.h
  3. 31
      src/formula/AbstractStateFormula.h
  4. 39
      src/formula/And.h
  5. 25
      src/formula/Ap.h
  6. 38
      src/formula/BoundOperator.h
  7. 34
      src/formula/BoundedEventually.h
  8. 40
      src/formula/BoundedUntil.h
  9. 26
      src/formula/CumulativeReward.h
  10. 39
      src/formula/Eventually.h
  11. 7
      src/formula/Formulas.h
  12. 36
      src/formula/Globally.h
  13. 26
      src/formula/InstantaneousReward.h
  14. 34
      src/formula/Next.h
  15. 38
      src/formula/NoBoundOperator.h
  16. 32
      src/formula/Not.h
  17. 41
      src/formula/Or.h
  18. 48
      src/formula/PctlFormula.h
  19. 18
      src/formula/ProbabilisticBoundOperator.h
  20. 18
      src/formula/ProbabilisticNoBoundOperator.h
  21. 36
      src/formula/ReachabilityReward.h
  22. 16
      src/formula/RewardBoundOperator.h
  23. 18
      src/formula/RewardNoBoundOperator.h
  24. 40
      src/formula/Until.h
  25. 43
      src/modelChecker/AbstractModelChecker.h
  26. 18
      src/modelChecker/DtmcPrctlModelChecker.h
  27. 6
      src/parser/PrctlParser.cpp
  28. 5
      src/parser/PrctlParser.h

65
src/formula/AbstractFormula.h
View File

@ -0,0 +1,65 @@
/*
* Abstractformula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
#ifndef STORM_FORMULA_AbstractFORMULA_H_
#define STORM_FORMULA_AbstractFORMULA_H_
#include <string>
namespace storm { namespace formula {
template <class T> class AbstractFormula;
}}
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
//abstract
/*!
* @brief
* Abstract base class for Abstract formulas in general.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
* AbstractPathFormula and AbstractStateFormula offer the method clone().
*/
template <class T>
class AbstractFormula {
public:
/*!
* virtual destructor
*/
virtual ~AbstractFormula() { }
/*!
* @note This function is not implemented in this class.
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
template <template <class Type> class MC>
const MC<T>* cast(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
try {
const MC<T>& mc = dynamic_cast<const MC<T>&>(modelChecker);
return &mc;
} catch (std::bad_cast& bc) {
std::cerr << "Bad cast: tried to cast " << typeid(modelChecker).name() << " to " << typeid(MC<T>).name() << std::endl;
}
return nullptr;
}
};
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_AbstractFORMULA_H_ */

32
src/formula/PctlPathFormula.h → src/formula/AbstractPathFormula.h
View File

@ -1,16 +1,23 @@
/*
* PctlPathFormula.h
* AbstractPathFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
#ifndef STORM_FORMULA_PCTLPATHFORMULA_H_
#define STORM_FORMULA_PCTLPATHFORMULA_H_
#ifndef STORM_FORMULA_AbstractPATHFORMULA_H_
#define STORM_FORMULA_AbstractPATHFORMULA_H_
#include "PctlFormula.h"
#include "modelChecker/DtmcPrctlModelChecker.h"
namespace storm { namespace formula {
template <class T> class AbstractPathFormula;
}}
#include "src/formula/AbstractFormula.h"
#include "modelChecker/AbstractModelChecker.h"
#include <vector>
#include <iostream>
#include <typeinfo>
namespace storm {
@ -18,7 +25,7 @@ namespace formula {
/*!
* @brief
* Abstract base class for PCTL path formulas.
* Abstract base class for Abstract path formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@ -26,13 +33,13 @@ namespace formula {
* clone().
*/
template <class T>
class PctlPathFormula : public PctlFormula<T> {
class AbstractPathFormula : public virtual AbstractFormula<T> {
public:
/*!
* empty destructor
*/
virtual ~PctlPathFormula() { }
virtual ~AbstractPathFormula() { }
/*!
* Clones the called object.
@ -42,7 +49,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const = 0;
virtual AbstractPathFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@ -55,11 +62,14 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
return nullptr;
}
};
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */
#endif /* STORM_FORMULA_AbstractPATHFORMULA_H_ */

31
src/formula/PctlStateFormula.h → src/formula/AbstractStateFormula.h
View File

@ -1,16 +1,20 @@
/*
* PctlStateFormula.h
* AbstractStateFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
#ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_
#define STORM_FORMULA_PCTLSTATEFORMULA_H_
#ifndef STORM_FORMULA_AbstractSTATEFORMULA_H_
#define STORM_FORMULA_AbstractSTATEFORMULA_H_
#include "PctlFormula.h"
#include "storage/BitVector.h"
#include "modelChecker/DtmcPrctlModelChecker.h"
namespace storm { namespace formula {
template <class T> class AbstractStateFormula;
}}
#include "AbstractFormula.h"
#include "src/storage/BitVector.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@ -18,7 +22,7 @@ namespace formula {
/*!
* @brief
* Abstract base class for PCTL state formulas.
* Abstract base class for Abstract state formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@ -26,13 +30,13 @@ namespace formula {
* clone().
*/
template <class T>
class PctlStateFormula : public PctlFormula<T> {
class AbstractStateFormula : public AbstractFormula<T> {
public:
/*!
* empty destructor
*/
virtual ~PctlStateFormula() { }
virtual ~AbstractStateFormula() { }
/*!
* Clones the called object.
@ -42,7 +46,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const = 0;
virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@ -55,7 +59,10 @@ 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::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
return nullptr;
}
};
} //namespace formula
@ -63,4 +70,4 @@ public:
} //namespace storm
#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */
#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */

39
src/formula/And.h
View File

@ -8,18 +8,25 @@
#ifndef STORM_FORMULA_AND_H_
#define STORM_FORMULA_AND_H_
#include "PctlStateFormula.h"
#include "AbstractStateFormula.h"
#include <string>
namespace storm {
namespace formula {
template <class T> class And;
template <class T>
class IAndModelChecker {
public:
virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with AND node as root.
* Class for a Abstract formula tree with AND node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
* Has two Abstract state formulas as sub formulas/trees.
*
* As AND is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@ -27,11 +34,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlStateFormula
* @see PctlFormula
* @see AbstractStateFormula
* @see AbstractFormula
*/
template <class T>
class And : public PctlStateFormula<T> {
class And : public AbstractStateFormula<T> {
public:
/*!
@ -50,7 +57,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
And(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@ -75,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
void setLeft(PctlStateFormula<T>* newLeft) {
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@ -84,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
void setRight(PctlStateFormula<T>* newRight) {
void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const PctlStateFormula<T>& getLeft() const {
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const PctlStateFormula<T>& getRight() const {
const AbstractStateFormula<T>& getRight() const {
return *right;
}
@ -121,7 +128,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
And<T>* result = new And();
if (this->left != NULL) {
result->setLeft(left->clone());
@ -141,13 +148,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::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const IAndModelChecker<T>& modelChecker) const {
return modelChecker.checkAnd(*this);
}
private:
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
};
} //namespace formula

25
src/formula/Ap.h
View File

@ -8,23 +8,32 @@
#ifndef STORM_FORMULA_AP_H_
#define STORM_FORMULA_AP_H_
#include "PctlStateFormula.h"
#include "AbstractStateFormula.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
template <class T> class Ap;
template <class T>
class IApModelChecker {
public:
virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with atomic proposition as root.
* Class for a Abstract formula tree with atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
* @see PctlStateFormula
* @see PctlFormula
* @see AbstractStateFormula
* @see AbstractFormula
*/
template <class T>
class Ap : public PctlStateFormula<T> {
class Ap : public AbstractStateFormula<T> {
public:
/*!
@ -64,7 +73,7 @@ public:
*
* @returns a new Ap-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
return new Ap(ap);
}
@ -77,8 +86,8 @@ 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::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkAp(*this);
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return this->template cast<IApModelChecker>(modelChecker)->checkAp(*this);
}
private:

38
src/formula/BoundOperator.h
View File

@ -8,20 +8,28 @@
#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
#define STORM_FORMULA_BOUNDOPERATOR_H_
#include "PctlStateFormula.h"
#include "PctlPathFormula.h"
#include "AbstractStateFormula.h"
#include "AbstractPathFormula.h"
#include "utility/ConstTemplates.h"
namespace storm {
namespace formula {
template <class T> class BoundUntil;
template <class T>
class IBoundUntilModelChecker {
public:
virtual storm::storage::BitVector* checkBoundUntil(const BoundUntil<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
* Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
* Has one PCTL path formula as sub formula/tree.
* Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@ -31,14 +39,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
* @see PctlFormula
* @see AbstractFormula
*/
template<class T>
class BoundOperator : public PctlStateFormula<T> {
class BoundOperator : public AbstractStateFormula<T> {
public:
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@ -50,7 +58,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula<T>* pathFormula)
BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
// Intentionally left empty
}
@ -68,9 +76,9 @@ public:
}
/*!
* @returns the child node (representation of a PCTL path formula)
* @returns the child node (representation of a Abstract path formula)
*/
const PctlPathFormula<T>& getPathFormula () const {
const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@ -79,7 +87,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(PctlPathFormula<T>* pathFormula) {
void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@ -134,7 +142,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const = 0;
virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@ -145,14 +153,14 @@ 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::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const IBoundUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundOperator(*this);
}
private:
ComparisonType comparisonOperator;
T bound;
PctlPathFormula<T>* pathFormula;
AbstractPathFormula<T>* pathFormula;
};
} //namespace formula

34
src/formula/BoundedEventually.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -17,11 +17,19 @@ namespace storm {
namespace formula {
template <class T> class BoundedEventually;
template <class T>
class IBoundedEventuallyModelChecker {
public:
virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a BoundedEventually node as root.
* Class for a Abstract (path) formula tree with a BoundedEventually node as root.
*
* Has one PCTL state formulas as sub formula/tree.
* Has one Abstract state formulas as sub formula/tree.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e child holds.
@ -29,11 +37,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class BoundedEventually : public PctlPathFormula<T> {
class BoundedEventually : public AbstractPathFormula<T> {
public:
/*!
@ -50,7 +58,7 @@ public:
* @param child The child formula subtree
* @param bound The maximal number of steps
*/
BoundedEventually(PctlStateFormula<T>* child, uint_fast64_t bound) {
BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) {
this->child = child;
this->bound = bound;
}
@ -70,7 +78,7 @@ public:
/*!
* @returns the child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -78,7 +86,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -116,7 +124,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
BoundedEventually<T>* result = new BoundedEventually<T>();
result->setBound(bound);
if (child != nullptr) {
@ -135,12 +143,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IBoundedEventuallyModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedEventually(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
uint_fast64_t bound;
};

40
src/formula/BoundedUntil.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
#define STORM_FORMULA_BOUNDEDUNTIL_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -17,11 +17,19 @@ namespace storm {
namespace formula {
template <class T> class BoundedUntil;
template <class T>
class IBoundedUntilModelChecker {
public:
virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a BoundedUntil node as root.
* Class for a Abstract (path) formula tree with a BoundedUntil node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
* Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
@ -30,11 +38,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class BoundedUntil : public PctlPathFormula<T> {
class BoundedUntil : public AbstractPathFormula<T> {
public:
/*!
@ -53,7 +61,7 @@ public:
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
BoundedUntil(PctlStateFormula<T>* left, PctlStateFormula<T>* right,
BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
uint_fast64_t bound) {
this->left = left;
this->right = right;
@ -80,7 +88,7 @@ public:
*
* @param newLeft the new left child.
*/
void setLeft(PctlStateFormula<T>* newLeft) {
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@ -89,21 +97,21 @@ public:
*
* @param newRight the new right child.
*/
void setRight(PctlStateFormula<T>* newRight) {
void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const PctlStateFormula<T>& getLeft() const {
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const PctlStateFormula<T>& getRight() const {
const AbstractStateFormula<T>& getRight() const {
return *right;
}
@ -144,7 +152,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil<T>();
result->setBound(bound);
if (left != NULL) {
@ -166,13 +174,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IBoundedUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedUntil(*this);
}
private:
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
uint_fast64_t bound;
};

26
src/formula/CumulativeReward.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_CUMULATIVEREWARD_H_
#define STORM_FORMULA_CUMULATIVEREWARD_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -17,18 +17,26 @@ namespace storm {
namespace formula {
template <class T> class CumulativeReward;
template <class T>
class ICumulativeRewardModelChecker {
public:
virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a Cumulative Reward node as root.
* Class for a Abstract (path) formula tree with a Cumulative Reward node as root.
*
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class CumulativeReward : public PctlPathFormula<T> {
class CumulativeReward : public AbstractPathFormula<T> {
public:
/*!
@ -84,9 +92,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
* @returns a new CumulativeReward-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
return new CumulativeReward(bound);
}
@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const ICumulativeRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkCumulativeReward(*this);
}

39
src/formula/Eventually.h
View File

@ -8,18 +8,27 @@
#ifndef STORM_FORMULA_EVENTUALLY_H_
#define STORM_FORMULA_EVENTUALLY_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
template <class T> class Eventually;
template <class T>
class IEventuallyModelChecker {
public:
virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with an Eventually node as root.
* Class for a Abstract (path) formula tree with an Eventually node as root.
*
* Has one PCTL state formula as sub formula/tree.
* Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff eventually \e child holds.
@ -27,11 +36,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class Eventually : public PctlPathFormula<T> {
class Eventually : public AbstractPathFormula<T> {
public:
/*!
@ -46,7 +55,7 @@ public:
*
* @param child The child node
*/
Eventually(PctlStateFormula<T>* child) {
Eventually(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -65,7 +74,7 @@ public:
/*!
* @returns the child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -73,7 +82,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -91,9 +100,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
* @returns a new Eventually-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
Eventually<T>* result = new Eventually<T>();
if (child != nullptr) {
result->setChild(child);
@ -110,12 +119,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkEventually(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return this->template cast<IEventuallyModelChecker>(modelChecker)->checkEventually(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
};
} //namespace formula

7
src/formula/Formulas.h
View File

@ -8,15 +8,16 @@
#ifndef STORM_FORMULA_FORMULAS_H_
#define STORM_FORMULA_FORMULAS_H_
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "And.h"
#include "Ap.h"
#include "BoundedUntil.h"
#include "Next.h"
#include "Not.h"
#include "Or.h"
#include "PctlFormula.h"
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "ProbabilisticNoBoundOperator.h"
#include "ProbabilisticBoundOperator.h"
#include "Until.h"

36
src/formula/Globally.h
View File

@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_GLOBALLY_H_
#define STORM_FORMULA_GLOBALLY_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class Globally;
template <class T>
class IGloballyModelChecker {
public:
virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a Globally node as root.
* Class for a Abstract (path) formula tree with a Globally node as root.
*
* Has one PCTL state formula as sub formula/tree.
* Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff globally \e child holds.
@ -27,11 +35,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class Globally : public PctlPathFormula<T> {
class Globally : public AbstractPathFormula<T> {
public:
/*!
@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
Globally(PctlStateFormula<T>* child) {
Globally(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -91,9 +99,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
* @returns a new Globally-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != nullptr) {
result->setChild(child);
@ -110,12 +118,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IGloballyModelChecker<T>& modelChecker) const {
return modelChecker.checkGlobally(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
};
} //namespace formula

26
src/formula/InstantaneousReward.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_INSTANTANEOUSREWARD_H_
#define STORM_FORMULA_INSTANTANEOUSREWARD_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@ -17,18 +17,26 @@ namespace storm {
namespace formula {
template <class T> class InstantaneousReward;
template <class T>
class IInstantaneousRewardModelChecker {
public:
virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a Instantaneous Reward node as root.
* Class for a Abstract (path) formula tree with a Instantaneous Reward node as root.
*
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class InstantaneousReward : public PctlPathFormula<T> {
class InstantaneousReward : public AbstractPathFormula<T> {
public:
/*!
@ -84,9 +92,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
* @returns a new InstantaneousReward-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
return new InstantaneousReward(bound);
}
@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IInstantaneousRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkInstantaneousReward(*this);
}

34
src/formula/Next.h
View File

@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_NEXT_H_
#define STORM_FORMULA_NEXT_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class Next;
template <class T>
class INextModelChecker {
public:
virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with a Next node as root.
* Class for a Abstract (path) formula tree with a Next node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
* Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in the next step, \e child holds
@ -27,11 +35,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class Next : public PctlPathFormula<T> {
class Next : public AbstractPathFormula<T> {
public:
/*!
@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
Next(PctlStateFormula<T>* child) {
Next(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -95,7 +103,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
@ -112,12 +120,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const INextModelChecker<T>& modelChecker) const {
return modelChecker.checkNext(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
};
} //namespace formula

38
src/formula/NoBoundOperator.h
View File

@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
#define STORM_FORMULA_NOBOUNDOPERATOR_H_
#include "PctlFormula.h"
#include "PctlPathFormula.h"
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
namespace storm {
namespace formula {
template <class T> class NoBoundOperator;
template <class T>
class INoBoundOperatorModelChecker {
public:
virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities
* Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
* Has one PCTL path formula as sub formula/tree.
* Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@ -39,14 +47,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
* @see PctlFormula
* @see AbstractFormula
*/
template <class T>
class NoBoundOperator: public storm::formula::PctlFormula<T> {
class NoBoundOperator: public storm::formula::AbstractFormula<T> {
public:
/*!
* Empty constructor
@ -60,7 +68,7 @@ public:
*
* @param pathFormula The child node.
*/
NoBoundOperator(PctlPathFormula<T>* pathFormula) {
NoBoundOperator(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@ -74,9 +82,9 @@ public:
}
/*!
* @returns the child node (representation of a PCTL path formula)
* @returns the child node (representation of a Abstract path formula)
*/
const PctlPathFormula<T>& getPathFormula () const {
const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@ -85,7 +93,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(PctlPathFormula<T>* pathFormula) {
void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating all states that satisfy the formula represented by the called object.
*/
virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T>* check(const INoBoundOperatorModelChecker<T>& modelChecker) const {
return modelChecker.checkNoBoundOperator(*this);
}
@ -110,7 +118,7 @@ public:
virtual std::string toString() const = 0;
private:
PctlPathFormula<T>* pathFormula;
AbstractPathFormula<T>* pathFormula;
};
} /* namespace formula */

32
src/formula/Not.h
View File

@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOT_H_
#define STORM_FORMULA_NOT_H_
#include "PctlStateFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class Not;
template <class T>
class INotModelChecker {
public:
virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with NOT node as root.
* Class for a Abstract formula tree with NOT node as root.
*
* Has one PCTL state formula as sub formula/tree.
* Has one Abstract state formula as sub formula/tree.
*
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlStateFormula
* @see PctlFormula
* @see AbstractStateFormula
* @see AbstractFormula
*/
template <class T>
class Not : public PctlStateFormula<T> {
class Not : public AbstractStateFormula<T> {
public:
/*!
@ -41,7 +49,7 @@ public:
* Constructor
* @param child The child node
*/
Not(PctlStateFormula<T>* child) {
Not(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -60,7 +68,7 @@ public:
/*!
* @returns The child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -68,7 +76,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -88,7 +96,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child);
@ -105,12 +113,12 @@ 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::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const INotModelChecker<T>& modelChecker) const {
return modelChecker.checkNot(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
};
} //namespace formula

41
src/formula/Or.h
View File

@ -8,17 +8,24 @@
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
#include "PctlStateFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class Or;
template <class T>
class IOrModelChecker {
public:
virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL formula tree with OR node as root.
* Class for a Abstract formula tree with OR node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
* Has two Abstract state formulas as sub formulas/trees.
*
* As OR is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@ -26,11 +33,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlStateFormula
* @see PctlFormula
* @see AbstractStateFormula
* @see AbstractFormula
*/
template <class T>
class Or : public PctlStateFormula<T> {
class Or : public AbstractStateFormula<T> {
public:
/*!
@ -49,7 +56,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
Or(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@ -74,7 +81,7 @@ public:
*
* @param newLeft the new left child.
*/
void setLeft(PctlStateFormula<T>* newLeft) {
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@ -83,21 +90,21 @@ public:
*
* @param newRight the new right child.
*/
void setRight(PctlStateFormula<T>* newRight) {
void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const PctlStateFormula<T>& getLeft() const {
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const PctlStateFormula<T>& getRight() const {
const AbstractStateFormula<T>& getRight() const {
return *right;
}
@ -120,7 +127,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
Or<T>* result = new Or();
if (this->left != NULL) {
result->setLeft(left->clone());
@ -130,7 +137,7 @@ public:
}
return result;
}
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
@ -140,13 +147,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::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const IOrModelChecker<T>& modelChecker) const {
return modelChecker.checkOr(*this);
}
private:
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
};
} //namespace formula

48
src/formula/PctlFormula.h
View File

@ -1,48 +0,0 @@
/*
* Pctlformula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
#ifndef STORM_FORMULA_PCTLFORMULA_H_
#define STORM_FORMULA_PCTLFORMULA_H_
#include <string>
namespace storm {
namespace formula {
//abstract
/*!
* @brief
* Abstract base class for PCTL formulas in general.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
* PctlPathFormula and PctlStateFormula offer the method clone().
*/
template <class T>
class PctlFormula {
public:
/*!
* virtual destructor
*/
virtual ~PctlFormula() { }
/*!
* @note This function is not implemented in this class.
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
};
} //namespace formula
} //namespace storm
#endif /* STORM_FORMULA_PCTLFORMULA_H_ */

18
src/formula/ProbabilisticBoundOperator.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#include "PctlStateFormula.h"
#include "PctlPathFormula.h"
#include "AbstractStateFormula.h"
#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@ -19,10 +19,10 @@ namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
* Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
* Has one PCTL path formula as sub formula/tree.
* Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@ -32,11 +32,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
* @see PctlFormula
* @see AbstractFormula
*/
template<class T>
class ProbabilisticBoundOperator : public BoundOperator<T> {
@ -56,7 +56,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
ProbabilisticBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@ -81,7 +81,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
result->setInterval(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());

18
src/formula/ProbabilisticNoBoundOperator.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#include "PctlFormula.h"
#include "PctlPathFormula.h"
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities
* Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
* Has one PCTL path formula as sub formula/tree.
* Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
* @see PctlFormula
* @see AbstractFormula
*/
template <class T>
class ProbabilisticNoBoundOperator: public NoBoundOperator<T> {
@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
ProbabilisticNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}

36
src/formula/ReachabilityReward.h
View File

@ -8,27 +8,35 @@
#ifndef STORM_FORMULA_REACHABILITYREWARD_H_
#define STORM_FORMULA_REACHABILITYREWARD_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class ReachabilityReward;
template <class T>
class IReachabilityRewardModelChecker {
public:
virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with an Reachability Reward node as root.
* Class for a Abstract (path) formula tree with an Reachability Reward node as root.
*
* Has one PCTL state formula as sub formula/tree.
* Has one Abstract state formula as sub formula/tree.
*
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class ReachabilityReward : public PctlPathFormula<T> {
class ReachabilityReward : public AbstractPathFormula<T> {
public:
/*!
@ -43,7 +51,7 @@ public:
*
* @param child The child node
*/
ReachabilityReward(PctlStateFormula<T>* child) {
ReachabilityReward(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -62,7 +70,7 @@ public:
/*!
* @returns the child node
*/
const PctlStateFormula<T>& getChild() const {
const AbstractStateFormula<T>& getChild() const {
return *child;
}
@ -70,7 +78,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
void setChild(PctlStateFormula<T>* child) {
void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@ -88,9 +96,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
* @returns a new BoundedUntil-object that is identical the called object.
* @returns a new ReachabilityReward-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
ReachabilityReward<T>* result = new ReachabilityReward<T>();
if (child != nullptr) {
result->setChild(child);
@ -107,12 +115,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IReachabilityRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkReachabilityReward(*this);
}
private:
PctlStateFormula<T>* child;
AbstractStateFormula<T>* child;
};
} //namespace formula

16
src/formula/RewardBoundOperator.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_
#include "PctlStateFormula.h"
#include "PctlPathFormula.h"
#include "AbstractStateFormula.h"
#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@ -19,7 +19,7 @@ namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root.
* Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
*
* Has a reward path formula as sub formula/tree.
*
@ -31,11 +31,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
* @see PctlFormula
* @see AbstractFormula
*/
template<class T>
class RewardBoundOperator : public BoundOperator<T> {
@ -55,7 +55,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
RewardBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@ -80,7 +80,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
virtual PctlStateFormula<T>* clone() const {
virtual AbstractStateFormula<T>* clone() const {
RewardBoundOperator<T>* result = new RewardBoundOperator<T>();
result->setBound(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());

18
src/formula/RewardNoBoundOperator.h
View File

@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
#include "PctlFormula.h"
#include "PctlPathFormula.h"
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a R (reward) operator without declaration of reward values
* Class for a Abstract formula tree with a R (reward) operator without declaration of reward values
* as root.
*
* Checking a formula with this operator as root returns the reward for the reward path formula for
* each state
*
* Has one PCTL path formula as sub formula/tree.
* Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
* Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PctlStateFormula
* @see PctlPathFormula
* @see AbstractStateFormula
* @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
* @see PctlFormula
* @see AbstractFormula
*/
template <class T>
class RewardNoBoundOperator: public NoBoundOperator<T> {
@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
RewardNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}

40
src/formula/Until.h
View File

@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_UNTIL_H_
#define STORM_FORMULA_UNTIL_H_
#include "PctlPathFormula.h"
#include "PctlStateFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
template <class T> class Until;
template <class T>
class IUntilModelChecker {
public:
virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
};
/*!
* @brief
* Class for a PCTL (path) formula tree with an Until node as root.
* Class for a Abstract (path) formula tree with an Until node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
* Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
@ -28,11 +36,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
* @see PctlPathFormula
* @see PctlFormula
* @see AbstractPathFormula
* @see AbstractFormula
*/
template <class T>
class Until : public PctlPathFormula<T> {
class Until : public AbstractPathFormula<T> {
public:
/*!
@ -49,7 +57,7 @@ public:
* @param left The left formula subtree
* @param right The left formula subtree
*/
Until(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@ -74,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
void setLeft(PctlStateFormula<T>* newLeft) {
void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@ -83,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
void setRight(PctlStateFormula<T>* newRight) {
void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
const PctlStateFormula<T>& getLeft() const {
const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
const PctlStateFormula<T>& getRight() const {
const AbstractStateFormula<T>& getRight() const {
return *right;
}
@ -120,7 +128,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
virtual PctlPathFormula<T>* clone() const {
virtual AbstractPathFormula<T>* clone() const {
Until<T>* result = new Until();
if (left != NULL) {
result->setLeft(left->clone());
@ -140,13 +148,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const IUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkUntil(*this);
}
private:
PctlStateFormula<T>* left;
PctlStateFormula<T>* right;
AbstractStateFormula<T>* left;
AbstractStateFormula<T>* right;
};
} //namespace formula

43
src/modelChecker/AbstractModelChecker.h
View File

@ -0,0 +1,43 @@
/*
* DtmcPrctlModelChecker.h
*
* Created on: 22.10.2012
* Author: Thomas Heinemann
*/
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
namespace storm { namespace modelChecker {
template <class Type> class AbstractModelChecker;
}}
//#include "src/formula/Formulas.h"
#include "src/formula/Or.h"
#include "src/formula/Ap.h"
#include "src/storage/BitVector.h"
namespace storm {
namespace modelChecker {
/*!
* @brief
* Interface for model checker classes.
*
* This class provides basic functions that are the same for all subclasses, but mainly only declares
* abstract methods that are to be implemented in concrete instances.
*
* @attention This class is abstract.
*/
template<class Type>
class AbstractModelChecker :
public virtual storm::formula::IOrModelChecker<Type>,
public virtual storm::formula::IApModelChecker<Type>
{
};
} //namespace modelChecker
} //namespace storm
#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */

18
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -23,15 +23,13 @@ class DtmcPrctlModelChecker;
}
#include "src/formula/PctlPathFormula.h"
#include "src/formula/PctlStateFormula.h"
#include "src/formula/Formulas.h"
#include "src/models/Dtmc.h"
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/utility/Vector.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include <vector>
#include "log4cplus/logger.h"
@ -53,7 +51,11 @@ namespace modelChecker {
* @attention This class is abstract.
*/
template<class Type>
class DtmcPrctlModelChecker {
class DtmcPrctlModelChecker :
public virtual AbstractModelChecker<Type>,
public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
public virtual storm::formula::IEventuallyModelChecker<Type>
{
public:
/*!
* Constructor
@ -100,7 +102,7 @@ public:
* states.
* @param stateFormula The formula to be checked.
*/
void check(const storm::formula::PctlStateFormula<Type>& stateFormula) const {
void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
@ -160,7 +162,7 @@ public:
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkStateFormula(const storm::formula::PctlStateFormula<Type>& formula) const {
storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula<Type>& formula) const {
return formula.check(*this);
}
@ -216,7 +218,7 @@ public:
* @param formula The Or state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
virtual storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
storm::storage::BitVector* result = checkStateFormula(formula.getLeft());
storm::storage::BitVector* right = checkStateFormula(formula.getRight());
(*result) |= (*right);
@ -269,7 +271,7 @@ public:
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
std::vector<Type>* checkPathFormula(const storm::formula::PctlPathFormula<Type>& formula) const {
std::vector<Type>* checkPathFormula(const storm::formula::AbstractPathFormula<Type>& formula) const {
return formula.check(*this);
}

6
src/parser/PrctlParser.cpp
View File

@ -58,7 +58,7 @@ namespace
/*!
* @brief Resulting formula.
*/
storm::formula::PctlFormula<double>* result;
//storm::formula::PctlFormula<double>* result;
struct dump
{
@ -141,7 +141,7 @@ storm::parser::PrctlParser::PrctlParser(const char* filename)
std::cout << "File was parsed" << std::endl;
std::string rest(data, file.dataend);
std::cout << "Rest: " << rest << std::endl;
this->formula = p.result;
//this->formula = p.result;
}
else this->formula = NULL;
//else this->formula = NULL;
}

5
src/parser/PrctlParser.h
View File

@ -1,7 +1,7 @@
#ifndef STORM_PARSER_PRCTLPARSER_H_
#define STORM_PARSER_PRCTLPARSER_H_
#include "src/formula/PctlFormula.h"
// #include "src/formula/PctlFormula.h"
#include "src/parser/Parser.h"
namespace storm {
@ -18,13 +18,14 @@ class PrctlParser : Parser
/*!
* @brief return formula object parsed from file.
*/
storm::formula::PctlFormula<double>* getFormula()
/* storm::formula::PctlFormula<double>* getFormula()
{
return this->formula;
}
private:
storm::formula::PctlFormula<double>* formula;
*/
};
} // namespace parser

Write Preview
Loading…
Cancel
Save