Browse Source
Merge branch 'interfacelogic'
Merge branch 'interfacelogic'
Conflicts: src/models/Mdp.h src/parser/NonDeterministicSparseTransitionParser.cpp src/parser/NonDeterministicSparseTransitionParser.htempestpy_adaptions
gereon
12 years ago
32 changed files with 1225 additions and 355 deletions
-
73src/formula/AbstractFormula.h
-
56src/formula/AbstractFormulaChecker.h
-
31src/formula/AbstractPathFormula.h
-
30src/formula/AbstractStateFormula.h
-
65src/formula/And.h
-
51src/formula/Ap.h
-
60src/formula/BoundOperator.h
-
60src/formula/BoundedEventually.h
-
211src/formula/BoundedNaryUntil.h
-
67src/formula/BoundedUntil.h
-
53src/formula/CumulativeReward.h
-
61src/formula/Eventually.h
-
8src/formula/Formulas.h
-
61src/formula/Globally.h
-
53src/formula/InstantaneousReward.h
-
59src/formula/Next.h
-
63src/formula/NoBoundOperator.h
-
58src/formula/Not.h
-
66src/formula/Or.h
-
48src/formula/PctlFormula.h
-
46src/formula/PrctlFormulaChecker.h
-
22src/formula/ProbabilisticBoundOperator.h
-
20src/formula/ProbabilisticNoBoundOperator.h
-
64src/formula/ReachabilityReward.h
-
19src/formula/RewardBoundOperator.h
-
20src/formula/RewardNoBoundOperator.h
-
66src/formula/Until.h
-
57src/modelChecker/AbstractModelChecker.h
-
19src/modelChecker/DtmcPrctlModelChecker.h
-
2src/parser/NonDeterministicSparseTransitionParser.h
-
6src/parser/PrctlParser.cpp
-
5src/parser/PrctlParser.h
@ -0,0 +1,73 @@ |
|||
/* |
|||
* 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" |
|||
#include "src/formula/AbstractFormulaChecker.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(). |
|||
* |
|||
* This is the base class for every formula class in every logic. |
|||
*/ |
|||
template <class T> |
|||
class AbstractFormula { |
|||
|
|||
public: |
|||
/*! |
|||
* Virtual destructor. |
|||
*/ |
|||
virtual ~AbstractFormula() { } |
|||
|
|||
/*! |
|||
* @brief Return string representation of this formula. |
|||
* |
|||
* @note very subclass must implement this method. |
|||
* |
|||
* @returns a string representation of the formula |
|||
*/ |
|||
virtual std::string toString() const = 0; |
|||
|
|||
/*! |
|||
* @brief Checks if all subtrees are valid in some logic. |
|||
* |
|||
* @note Every subclass must implement this method. |
|||
* |
|||
* This method is given a checker object that knows which formula |
|||
* classes are allowed within the logic the checker represents. Every |
|||
* subclass is supposed to call checker.conforms() for all child |
|||
* formulas and return true if and only if all those calls returned |
|||
* true. |
|||
* |
|||
* @param checker Checker object. |
|||
* @return true iff all subtrees are valid. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0; |
|||
}; |
|||
|
|||
} // namespace formula |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */ |
|||
@ -0,0 +1,56 @@ |
|||
#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ |
|||
#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ |
|||
|
|||
#include "src/formula/AbstractFormula.h" |
|||
|
|||
namespace storm { |
|||
namespace formula { |
|||
|
|||
/*! |
|||
* @brief Base class for all formula checkers. |
|||
* |
|||
* A formula checker is used to check if a given formula is valid in some |
|||
* logic. Hence, this pure virtual base class should be subclassed for |
|||
* every logic we support. |
|||
* |
|||
* Every subclass must implement conforms(). It gets a pointer to an |
|||
* AbstractFormula object and should return if the subtree represented by |
|||
* this formula is valid in the logic. |
|||
* |
|||
* Usually, this will be implemented like this: |
|||
* @code |
|||
* if ( |
|||
* dynamic_cast<const And<T>*>(formula) || |
|||
* dynamic_cast<const Not<T>*>(formula) || |
|||
* dynamic_cast<const Or<T>*>(formula) |
|||
* ) { |
|||
* return formula->conforms(*this); |
|||
* } else return false; |
|||
* @endcode |
|||
* |
|||
* Every formula class implements a conforms() method itself which calls |
|||
* conforms() on the given checker for every child in the formula tree. |
|||
* |
|||
* If the formula structure is not an actual tree, but an directed acyclic |
|||
* graph, the shared subtrees will be checked twice. If we have directed |
|||
* cycles, we will have infinite recursions. |
|||
*/ |
|||
template <class T> |
|||
class AbstractFormulaChecker { |
|||
public: |
|||
/*! |
|||
* @brief Checks if the given formula is valid in some logic. |
|||
* |
|||
* Every subclass must implement this method and check, if the |
|||
* formula object is valid in the logic of the subclass. |
|||
* |
|||
* @param formula A pointer to some formula object. |
|||
* @return true iff the formula is valid. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormula<T>* formula) const = 0; |
|||
}; |
|||
|
|||
} // namespace formula |
|||
} // namespace storm |
|||
|
|||
#endif |
|||
@ -0,0 +1,211 @@ |
|||
/* |
|||
* BoundedNaryUntil.h |
|||
* |
|||
* Created on: 19.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_ |
|||
#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_ |
|||
|
|||
#include "src/formula/AbstractPathFormula.h" |
|||
#include "src/formula/AbstractStateFormula.h" |
|||
#include "src/modelChecker/AbstractModelChecker.h" |
|||
#include "boost/integer/integer_mask.hpp" |
|||
#include <string> |
|||
#include <vector> |
|||
#include <tuple> |
|||
#include <sstream> |
|||
#include "src/formula/AbstractFormulaChecker.h" |
|||
|
|||
namespace storm { |
|||
namespace formula { |
|||
|
|||
template <class T> class BoundedNaryUntil; |
|||
|
|||
/*! |
|||
* @brief Interface class for model checkers that support BoundedNaryUntil. |
|||
* |
|||
* All model checkers that support the formula class BoundedNaryUntil must inherit |
|||
* this pure virtual class. |
|||
*/ |
|||
template <class T> |
|||
class IBoundedNaryUntilModelChecker { |
|||
public: |
|||
/*! |
|||
* @brief Evaluates BoundedNaryUntil formula within a model checker. |
|||
* |
|||
* @param obj Formula object with subformulas. |
|||
* @return Result of the formula for every node. |
|||
*/ |
|||
virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj) const = 0; |
|||
}; |
|||
|
|||
/*! |
|||
* @brief |
|||
* Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root. |
|||
* |
|||
* Has at least two Abstract state formulas as sub formulas and an interval |
|||
* associated with all but the first sub formula. We'll call the first one |
|||
* \e left and all other one \e right. |
|||
* |
|||
* @par Semantics |
|||
* The formula holds iff \e left holds until eventually any of the \e right |
|||
* formulas holds after a number of steps contained in the interval |
|||
* associated with this 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 AbstractPathFormula |
|||
* @see AbstractFormula |
|||
*/ |
|||
template <class T> |
|||
class BoundedNaryUntil : public AbstractPathFormula<T> { |
|||
|
|||
public: |
|||
/*! |
|||
* Empty constructor |
|||
*/ |
|||
BoundedNaryUntil() { |
|||
this->left = NULL; |
|||
this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>(); |
|||
} |
|||
|
|||
/*! |
|||
* Constructor |
|||
* |
|||
* @param left The left formula subtree |
|||
* @param right The left formula subtree |
|||
* @param bound The maximal number of steps |
|||
*/ |
|||
BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) { |
|||
this->left = left; |
|||
this->right = right; |
|||
} |
|||
|
|||
/*! |
|||
* Destructor. |
|||
* |
|||
* Also deletes the subtrees. |
|||
* (this behaviour can be prevented by setting the subtrees to NULL before deletion) |
|||
*/ |
|||
virtual ~BoundedNaryUntil() { |
|||
if (left != NULL) { |
|||
delete left; |
|||
} |
|||
if (right != NULL) { |
|||
delete right; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Sets the left child node. |
|||
* |
|||
* @param newLeft the new left child. |
|||
*/ |
|||
void setLeft(AbstractStateFormula<T>* newLeft) { |
|||
left = newLeft; |
|||
} |
|||
|
|||
void setRight(std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newRight) { |
|||
right = newRight; |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Sets the right child node. |
|||
* |
|||
* @param newRight the new right child. |
|||
*/ |
|||
void addRight(AbstractStateFormula<T>* newRight, T upperBound, T lowerBound) { |
|||
this->right->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(newRight, upperBound, lowerBound)); |
|||
} |
|||
|
|||
/*! |
|||
* @returns a pointer to the left child node |
|||
*/ |
|||
const AbstractStateFormula<T>& getLeft() const { |
|||
return *left; |
|||
} |
|||
|
|||
/*! |
|||
* @returns a pointer to the right child nodes. |
|||
*/ |
|||
const std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>& getRight() const { |
|||
return *right; |
|||
} |
|||
|
|||
/*! |
|||
* @returns a string representation of the formula |
|||
*/ |
|||
virtual std::string toString() const { |
|||
std::stringstream result; |
|||
result << "( " << left->toString(); |
|||
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|||
result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString(); |
|||
} |
|||
result << ")"; |
|||
return result.str(); |
|||
} |
|||
|
|||
/*! |
|||
* Clones the called object. |
|||
* |
|||
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones |
|||
* |
|||
* @returns a new BoundedNaryUntil-object that is identical the called object. |
|||
*/ |
|||
virtual AbstractPathFormula<T>* clone() const { |
|||
BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>(); |
|||
if (left != NULL) { |
|||
result->setLeft(left->clone()); |
|||
} |
|||
if (right != NULL) { |
|||
std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>(); |
|||
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|||
newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it))); |
|||
} |
|||
result->setRight(newright); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Calls the model checker to check this formula. |
|||
* Needed to infer the correct type of formula class. |
|||
* |
|||
* @note This function should only be called in a generic check function of a model checker class. For other uses, |
|||
* the methods of the model checker should be used. |
|||
* |
|||
* @returns A vector indicating the probability that the formula holds for each state. |
|||
*/ |
|||
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const { |
|||
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this); |
|||
} |
|||
|
|||
/*! |
|||
* @brief Checks if all subtrees conform to some logic. |
|||
* |
|||
* @param checker Formula checker object. |
|||
* @return true iff all subtrees conform to some logic. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
|||
bool res = checker.conforms(this->left); |
|||
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|||
res &= checker.conforms(std::get<0>(*it)); |
|||
} |
|||
return res; |
|||
} |
|||
|
|||
private: |
|||
AbstractStateFormula<T>* left; |
|||
std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right; |
|||
}; |
|||
|
|||
} //namespace formula |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */ |
|||
@ -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_ */ |
|||
@ -0,0 +1,46 @@ |
|||
#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_ |
|||
#define STORM_FORMULA_PRCTLFORMULACHECKER_H_ |
|||
|
|||
#include "src/formula/AbstractFormulaChecker.h" |
|||
#include "src/formula/Formulas.h" |
|||
|
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace formula { |
|||
|
|||
/*! |
|||
* @brief Checks formulas if they are within PRCTL. |
|||
* |
|||
* This class implements AbstractFormulaChecker to check if a given formula |
|||
* is part of PRCTL logic. |
|||
*/ |
|||
template <class T> |
|||
class PrctlFormulaChecker : public AbstractFormulaChecker<T> { |
|||
public: |
|||
/*! |
|||
* Implementation of AbstractFormulaChecker::conforms() using code |
|||
* looking exactly like the sample code given there. |
|||
* |
|||
* We currently allow And, Ap, Eventually, Not, Or, |
|||
* ProbabilisticNoBoundOperator. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormula<T>* formula) const { |
|||
if ( |
|||
dynamic_cast<const And<T>*>(formula) || |
|||
dynamic_cast<const Ap<T>*>(formula) || |
|||
dynamic_cast<const Eventually<T>*>(formula) || |
|||
dynamic_cast<const Not<T>*>(formula) || |
|||
dynamic_cast<const Or<T>*>(formula) || |
|||
dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula) |
|||
) { |
|||
return formula->conforms(*this); |
|||
} |
|||
return false; |
|||
} |
|||
}; |
|||
|
|||
} // namespace formula |
|||
} // namespace storm |
|||
|
|||
#endif |
|||
@ -0,0 +1,57 @@ |
|||
/* |
|||
* 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" |
|||
|
|||
#include <iostream> |
|||
|
|||
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> |
|||
{ |
|||
|
|||
public: |
|||
template <template <class T> class Target> |
|||
const Target<Type>* as() const { |
|||
try { |
|||
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
std::cerr << "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << std::endl; |
|||
} |
|||
return nullptr; |
|||
} |
|||
}; |
|||
|
|||
} //namespace modelChecker |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue