Browse Source
renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...)
renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...)
renamed modelChecker to modelcheckermain
gereon
12 years ago
28 changed files with 461 additions and 69 deletions
-
2src/formula/AbstractFormula.h
-
2src/formula/AbstractPathFormula.h
-
4src/formula/AbstractStateFormula.h
-
2src/formula/And.h
-
2src/formula/Ap.h
-
6src/formula/BoundedEventually.h
-
9src/formula/BoundedNaryUntil.h
-
2src/formula/BoundedUntil.h
-
6src/formula/Eventually.h
-
4src/formula/Formulas.h
-
6src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
28src/formula/PathBoundOperator.h
-
14src/formula/ProbabilisticBoundOperator.h
-
2src/formula/ReachabilityReward.h
-
12src/formula/RewardBoundOperator.h
-
197src/formula/StateBoundOperator.h
-
161src/formula/SteadyStateOperator.h
-
0src/modelchecker/AbstractModelChecker.h
-
4src/modelchecker/DtmcPrctlModelChecker.h
-
2src/modelchecker/EigenDtmcPrctlModelChecker.h
-
0src/modelchecker/ForwardDeclarations.h
-
2src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
16src/parser/PrctlParser.cpp
-
4src/storm.cpp
-
4test/parser/PrctlParserTest.cpp
-
35test/parser/output.dot
-
2test/storm-tests.cpp
@ -0,0 +1,197 @@ |
|||
/* |
|||
* 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 { |
|||
|
|||
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 formula |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */ |
|||
@ -0,0 +1,161 @@ |
|||
/* |
|||
* SteadyState.h |
|||
* |
|||
* Created on: 19.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ |
|||
#define STORM_FORMULA_STEADYSTATEOPERATOR_H_ |
|||
|
|||
#include "AbstractPathFormula.h" |
|||
#include "AbstractStateFormula.h" |
|||
#include "BoundOperator.h" |
|||
#include "src/formula/AbstractFormulaChecker.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace formula { |
|||
|
|||
template <class T> class SteadyStateOperator; |
|||
|
|||
/*! |
|||
* @brief Interface class for model checkers that support SteadyStateOperator. |
|||
* |
|||
* All model checkers that support the formula class SteadyStateOperator must inherit |
|||
* this pure virtual class. |
|||
*/ |
|||
template <class T> |
|||
class ISteadyStateOperatorModelChecker { |
|||
public: |
|||
/*! |
|||
* @brief Evaluates SteadyStateOperator formula within a model checker. |
|||
* |
|||
* @param obj Formula object with subformulas. |
|||
* @return Result of the formula for every node. |
|||
*/ |
|||
virtual storm::storage::BitVector* checkSteadyStateOperator(const SteadyStateOperator<T>& obj) const = 0; |
|||
}; |
|||
|
|||
/*! |
|||
* @brief |
|||
* Class for a Abstract (path) formula tree with a SteadyStateOperator node as root. |
|||
* |
|||
* Has two Abstract state formulas as sub formulas/trees. |
|||
* |
|||
* @par Semantics |
|||
* The formula holds iff \e child holds SteadyStateOperator step, \e child holds |
|||
* |
|||
* 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 AbstractPathFormula |
|||
* @see AbstractFormula |
|||
*/ |
|||
template <class T> |
|||
class SteadyStateOperator : public BoundOperator<T> { |
|||
|
|||
public: |
|||
/*! |
|||
* Empty constructor |
|||
*/ |
|||
SteadyStateOperator() : BoundOperator<T> |
|||
(BoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) { |
|||
// Intentionally left empty |
|||
} |
|||
|
|||
/*! |
|||
* Constructor |
|||
* |
|||
* @param child The child node |
|||
*/ |
|||
SteadyStateOperator( |
|||
BoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* child) { |
|||
this->child = child; |
|||
} |
|||
|
|||
/*! |
|||
* Constructor. |
|||
* |
|||
* Also deletes the subtree. |
|||
* (this behaviour can be prevented by setting the subtrees to NULL before deletion) |
|||
*/ |
|||
virtual ~SteadyStateOperator() { |
|||
if (child != NULL) { |
|||
delete child; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* @returns the child node |
|||
*/ |
|||
const AbstractStateFormula<T>& getChild() const { |
|||
return *child; |
|||
} |
|||
|
|||
/*! |
|||
* Sets the subtree |
|||
* @param child the new child node |
|||
*/ |
|||
void setChild(AbstractStateFormula<T>* child) { |
|||
this->child = child; |
|||
} |
|||
|
|||
/*! |
|||
* @returns a string representation of the formula |
|||
*/ |
|||
virtual std::string toString() const { |
|||
std::string result = "("; |
|||
result += " S "; |
|||
result += child->toString(); |
|||
result += ")"; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* 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 BoundedUntil-object that is identical the called object. |
|||
*/ |
|||
virtual AbstractPathFormula<T>* clone() const { |
|||
SteadyStateOperator<T>* result = new SteadyStateOperator<T>(); |
|||
if (child != NULL) { |
|||
result->setChild(child); |
|||
} |
|||
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 storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const { |
|||
return modelChecker.template as<ISteadyStateOperatorModelChecker>()->checkSteadyStateOperator(*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->child); |
|||
} |
|||
|
|||
private: |
|||
AbstractStateFormula<T>* child; |
|||
}; |
|||
|
|||
} //namespace formula |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */ |
|||
@ -0,0 +1,35 @@ |
|||
digraph dtmc { |
|||
1[label="1\n{ phi }"]; |
|||
2[label="2\n{ phi }"]; |
|||
3[label="3\n{ phi }"]; |
|||
4[label="4\n{ smth }"]; |
|||
5[label="5\n{ phi,smth }"]; |
|||
6[label="6\n{ psi }"]; |
|||
7[label="7\n{ phi,psi }"]; |
|||
8[label="8\n{ phi,psi }"]; |
|||
9[label="9\n{ phi }"]; |
|||
10[label="10\n{ phi }"]; |
|||
11[label="11\n{ phi }"]; |
|||
0 -> 0 [label=1] |
|||
1 -> 3 [label=0.5] |
|||
1 -> 4 [label=0.5] |
|||
2 -> 1 [label=0.3] |
|||
2 -> 7 [label=0.7] |
|||
3 -> 2 [label=0.05] |
|||
3 -> 3 [label=0.7] |
|||
3 -> 6 [label=0.05] |
|||
3 -> 8 [label=0.2] |
|||
4 -> 1 [label=0.3] |
|||
4 -> 5 [label=0.3] |
|||
4 -> 6 [label=0.4] |
|||
5 -> 4 [label=1] |
|||
6 -> 7 [label=1] |
|||
7 -> 2 [label=0.2] |
|||
7 -> 6 [label=0.8] |
|||
8 -> 9 [label=1] |
|||
9 -> 8 [label=0.3] |
|||
9 -> 9 [label=0.7] |
|||
10 -> 4 [label=1] |
|||
11 -> 5 [label=0.7] |
|||
11 -> 9 [label=0.3] |
|||
} |
|||
Reference in new issue
xxxxxxxxxx