Lanchid
12 years ago
21 changed files with 149 additions and 718 deletions
-
6src/formula/Prctl/AbstractPathFormula.h
-
6src/formula/Prctl/AbstractStateFormula.h
-
6src/formula/Prctl/BoundedEventually.h
-
6src/formula/Prctl/BoundedNaryUntil.h
-
6src/formula/Prctl/BoundedUntil.h
-
6src/formula/Prctl/CumulativeReward.h
-
6src/formula/Prctl/Eventually.h
-
6src/formula/Prctl/Globally.h
-
6src/formula/Prctl/InstantaneousReward.h
-
6src/formula/Prctl/Next.h
-
60src/formula/Prctl/Not.h
-
94src/formula/Prctl/Or.h
-
35src/formula/Prctl/ProbabilisticBoundOperator.h
-
27src/formula/Prctl/ProbabilisticNoBoundOperator.h
-
66src/formula/Prctl/ReachabilityReward.h
-
50src/formula/Prctl/RewardBoundOperator.h
-
15src/formula/Prctl/RewardNoBoundOperator.h
-
199src/formula/Prctl/StateBoundOperator.h
-
150src/formula/Prctl/StateNoBoundOperator.h
-
29src/formula/Prctl/SteadyStateReward.h
-
82src/formula/Prctl/Until.h
@ -1,199 +0,0 @@ |
|||
/* |
|||
* BoundOperator.h |
|||
* |
|||
* Created on: 27.12.2012 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_ |
|||
#define STORM_FORMULA_STATEBOUNDOPERATOR_H_ |
|||
|
|||
#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" |
|||
|
|||
namespace storm { |
|||
namespace formula { |
|||
namespace prctl { |
|||
|
|||
template <class T> class StateBoundOperator; |
|||
|
|||
/*! |
|||
* @brief Interface class for model checkers that support StateBoundOperator. |
|||
* |
|||
* All model checkers that support the formula class StateBoundOperator must inherit |
|||
* this pure virtual class. |
|||
*/ |
|||
template <class T> |
|||
class IStateBoundOperatorModelChecker { |
|||
public: |
|||
virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0; |
|||
}; |
|||
|
|||
/*! |
|||
* @brief |
|||
* Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval |
|||
* as root. |
|||
* |
|||
* Has one Abstract state formula as sub formula/tree. |
|||
* |
|||
* @par Semantics |
|||
* The formula holds iff the probability that the state formula holds is inside the bounds |
|||
* specified in this operator |
|||
* |
|||
* The subtree is seen as part of the object and deleted with it |
|||
* (this behavior can be prevented by setting them to NULL before deletion) |
|||
* |
|||
* |
|||
* @see AbstractStateFormula |
|||
* @see AbstractPathFormula |
|||
* @see ProbabilisticOperator |
|||
* @see ProbabilisticNoBoundsOperator |
|||
* @see AbstractFormula |
|||
*/ |
|||
template<class T> |
|||
class StateBoundOperator : public AbstractStateFormula<T> { |
|||
|
|||
public: |
|||
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; |
|||
|
|||
/*! |
|||
* Constructor |
|||
* |
|||
* @param comparisonOperator The relation for the bound. |
|||
* @param bound The bound for the probability |
|||
* @param stateFormula The child node |
|||
*/ |
|||
StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula) |
|||
: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { |
|||
// Intentionally left empty |
|||
} |
|||
|
|||
/*! |
|||
* Destructor |
|||
* |
|||
* The subtree is deleted with the object |
|||
* (this behavior can be prevented by setting them to NULL before deletion) |
|||
*/ |
|||
virtual ~StateBoundOperator() { |
|||
if (stateFormula != nullptr) { |
|||
delete stateFormula; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* @returns the child node (representation of a Abstract state formula) |
|||
*/ |
|||
const AbstractStateFormula<T>& getStateFormula () const { |
|||
return *stateFormula; |
|||
} |
|||
|
|||
/*! |
|||
* Sets the child node |
|||
* |
|||
* @param stateFormula the state formula that becomes the new child node |
|||
*/ |
|||
void setStateFormula(AbstractStateFormula<T>* stateFormula) { |
|||
this->stateFormula = stateFormula; |
|||
} |
|||
|
|||
/*! |
|||
* @returns the comparison relation |
|||
*/ |
|||
const ComparisonType getComparisonOperator() const { |
|||
return comparisonOperator; |
|||
} |
|||
|
|||
void setComparisonOperator(ComparisonType comparisonOperator) { |
|||
this->comparisonOperator = comparisonOperator; |
|||
} |
|||
|
|||
/*! |
|||
* @returns the bound for the measure |
|||
*/ |
|||
const T& getBound() const { |
|||
return bound; |
|||
} |
|||
|
|||
/*! |
|||
* Sets the interval in which the probability that the path formula holds may lie in. |
|||
* |
|||
* @param bound The bound for the measure |
|||
*/ |
|||
void setBound(T bound) { |
|||
this->bound = bound; |
|||
} |
|||
|
|||
/*! |
|||
* @returns a string representation of the formula |
|||
*/ |
|||
virtual std::string toString() const { |
|||
std::string result = " "; |
|||
switch (comparisonOperator) { |
|||
case LESS: result += "< "; break; |
|||
case LESS_EQUAL: result += "<= "; break; |
|||
case GREATER: result += "> "; break; |
|||
case GREATER_EQUAL: result += ">= "; break; |
|||
} |
|||
result += std::to_string(bound); |
|||
result += " ["; |
|||
result += stateFormula->toString(); |
|||
result += "]"; |
|||
return result; |
|||
} |
|||
|
|||
bool meetsBound(T value) const { |
|||
switch (comparisonOperator) { |
|||
case LESS: return value < bound; break; |
|||
case LESS_EQUAL: return value <= bound; break; |
|||
case GREATER: return value > bound; break; |
|||
case GREATER_EQUAL: return value >= bound; break; |
|||
default: return false; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* 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 AND-object that is identical the called object. |
|||
*/ |
|||
virtual AbstractStateFormula<T>* clone() const = 0; |
|||
|
|||
/*! |
|||
* 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 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) const { |
|||
return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this); |
|||
} |
|||
|
|||
/*! |
|||
* @brief Checks if the subtree conforms to some logic. |
|||
* |
|||
* @param checker Formula checker object. |
|||
* @return true iff the subtree conforms to some logic. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
|||
return checker.conforms(this->stateFormula); |
|||
} |
|||
|
|||
private: |
|||
ComparisonType comparisonOperator; |
|||
T bound; |
|||
AbstractStateFormula<T>* stateFormula; |
|||
}; |
|||
|
|||
} //namespace prctl |
|||
} //namespace formula |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */ |
|||
@ -1,150 +0,0 @@ |
|||
/* |
|||
* StateNoBoundOperator.h |
|||
* |
|||
* Created on: 09.04.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_ |
|||
#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_ |
|||
|
|||
#include "src/formula/AbstractFormula.h" |
|||
#include "src/formula/AbstractPathFormula.h" |
|||
#include "src/formula/AbstractFormulaChecker.h" |
|||
|
|||
#include "src/modelchecker/ForwardDeclarations.h" |
|||
|
|||
namespace storm { |
|||
namespace formula { |
|||
namespace prctl { |
|||
|
|||
template <class T> class StateNoBoundOperator; |
|||
|
|||
/*! |
|||
* @brief Interface class for model checkers that support PathNoBoundOperator. |
|||
* |
|||
* All model checkers that support the formula class NoBoundOperator must inherit |
|||
* this pure virtual class. |
|||
*/ |
|||
template <class T> |
|||
class IStateNoBoundOperatorModelChecker { |
|||
public: |
|||
/*! |
|||
* @brief Evaluates NoBoundOperator formula within a model checker. |
|||
* |
|||
* @param obj Formula object with subformulas. |
|||
* @return Result of the formula for every node. |
|||
*/ |
|||
virtual std::vector<T>* checkStateNoBoundOperator(const StateNoBoundOperator<T>& obj) const = 0; |
|||
}; |
|||
|
|||
|
|||
/*! |
|||
* @brief |
|||
* Class for a Abstract formula tree with an 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 Abstract state 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 AbstractFormula. |
|||
* |
|||
* @note |
|||
* This class does not contain a check() method like the other formula classes. |
|||
* The check method should only be called by the model checker to infer the correct check function for sub |
|||
* formulas. As this operator can only appear at the root, the method is not useful here. |
|||
* Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead. |
|||
* |
|||
* The subtree is seen as part of the object and deleted with it |
|||
* (this behavior can be prevented by setting them to NULL before deletion) |
|||
* |
|||
* |
|||
* @see AbstractStateFormula |
|||
* @see AbstractPathFormula |
|||
* @see SteadyStateNoBoundOperator |
|||
* @see AbstractFormula |
|||
*/ |
|||
template <class T> |
|||
class StateNoBoundOperator: public storm::formula::AbstractFormula<T> { |
|||
public: |
|||
/*! |
|||
* Empty constructor |
|||
*/ |
|||
StateNoBoundOperator() { |
|||
stateFormula = nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Constructor |
|||
*/ |
|||
StateNoBoundOperator(AbstractStateFormula<T>* stateFormula) { |
|||
this->stateFormula = stateFormula; |
|||
} |
|||
|
|||
/*! |
|||
* Destructor |
|||
* |
|||
* Deletes the subtree |
|||
*/ |
|||
virtual ~StateNoBoundOperator() { |
|||
if (stateFormula != nullptr) { |
|||
delete stateFormula; |
|||
} |
|||
} |
|||
|
|||
const AbstractStateFormula<T>& getStateFormula() const { |
|||
return *(this->stateFormula); |
|||
} |
|||
|
|||
void setStateFormula(AbstractStateFormula<T>* stateFormula) { |
|||
this->stateFormula = stateFormula; |
|||
} |
|||
|
|||
/*! |
|||
* 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. |
|||
* |
|||
* @note This function is not implemented in this class. |
|||
* |
|||
* @returns A vector indicating all states that satisfy the formula represented by the called object. |
|||
*/ |
|||
virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const { |
|||
return modelChecker.template as<IStateNoBoundOperatorModelChecker>()->checkStateNoBoundOperator(*this); |
|||
} |
|||
|
|||
/*! |
|||
* @returns a string representation of the formula |
|||
*/ |
|||
virtual std::string toString() const { |
|||
std::string result; |
|||
result += " = ? ["; |
|||
result += this->getStateFormula().toString(); |
|||
result += "]"; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* @brief Checks if the subtree conforms to some logic. |
|||
* |
|||
* @param checker Formula checker object. |
|||
* @return true iff the subtree conforms to some logic. |
|||
*/ |
|||
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
|||
return checker.conforms(this->stateFormula); |
|||
} |
|||
|
|||
private: |
|||
AbstractStateFormula<T>* stateFormula; |
|||
}; |
|||
|
|||
} //namespace prctl |
|||
} //namespace formula |
|||
} //namespace storm |
|||
#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue