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

Documentation of ModelChecker (new) and improved doc of formula classes

tempestpy_adaptions
Lanchid 12 years ago
parent
f5d2205352
commit
a1854b26a5
12 changed files with 140 additions and 12 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. 2
      src/formula/AP.h
  2. 2
      src/formula/And.h
  3. 4
      src/formula/BoundedUntil.h
  4. 4
      src/formula/Next.h
  5. 2
      src/formula/Not.h
  6. 2
      src/formula/Or.h
  7. 2
      src/formula/PCTLPathFormula.h
  8. 2
      src/formula/PCTLStateFormula.h
  9. 2
      src/formula/PCTLformula.h
  10. 4
      src/formula/ProbabilisticOperator.h
  11. 6
      src/formula/Until.h
  12. 114
      src/modelChecker/DtmcPrctlModelChecker.h

2
src/formula/AP.h
View File

@ -15,7 +15,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
* @see PCTLStateFormula

2
src/formula/And.h
View File

@ -16,7 +16,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with AND node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
*
* As AND is commutative, the order is \e theoretically not important, but will influence the order in which

4
src/formula/BoundedUntil.h
View File

@ -19,10 +19,12 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL (path) formula tree with a BoundedUntil node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
*
* \par Semantics
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
* \e left holds.
*

4
src/formula/Next.h
View File

@ -16,10 +16,12 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL (path) formula tree with a Next node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
*
* \par Semantics
* @par Semantics
* The formula holds iff in the next step, \e child holds
*
* The subtree is seen as part of the object and deleted with the object

2
src/formula/Not.h
View File

@ -15,7 +15,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with NOT node as root.
*
* Has one PCTL state formula as sub formula/tree.
*
* The subtree is seen as part of the object and deleted with the object

2
src/formula/Or.h
View File

@ -15,7 +15,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with OR node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
*
* As OR is commutative, the order is \e theoretically not important, but will influence the order in which

2
src/formula/PCTLPathFormula.h
View File

@ -17,7 +17,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Abstract base class for PCTL 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
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method

2
src/formula/PCTLStateFormula.h
View File

@ -17,7 +17,9 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Abstract base class for PCTL 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
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method

2
src/formula/PCTLformula.h
View File

@ -17,7 +17,9 @@ 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

4
src/formula/ProbabilisticOperator.h
View File

@ -17,10 +17,12 @@ namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator node as root.
*
* Has one PCTL path formula as sub formula/tree.
*
* \par Semantics
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds specified in this operator
*
* The subtree is seen as part of the object and deleted with it

6
src/formula/Until.h
View File

@ -16,10 +16,12 @@ namespace mrmc {
namespace formula {
/*!
* Class for a PCTL (path) formula tree with a BoundedUntil node as root.
* @brief
* Class for a PCTL (path) formula tree with an Until node as root.
*
* Has two PCTL state formulas as sub formulas/trees.
*
* \par Semantics
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
* \e left holds always.
*

114
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -43,41 +43,147 @@ namespace mrmc {
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 T>
class DtmcPrctlModelChecker {
private:
mrmc::models::Dtmc<T>* dtmc;
protected:
/*!
* @returns A reference to the dtmc of the model checker.
*/
mrmc::models::Dtmc<T>* getDtmc() const {
return this->dtmc;
}
public:
/*!
* Constructor
*/
explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
/*!
* Destructor
*/
virtual ~DtmcPrctlModelChecker();
virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0;
virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0;
virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
/*!
* Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all
* other edges from these states)
*
* @param states A bit vector representing a set of states that should become absorbing.
*/
virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0;
/*!
* Returns all states that are labeled with a given atomic proposition.
*
* @param ap A string representing an atomic proposition.
* @returns The set of states labeled with the atomic proposition ap.
*/
virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0;
/*!
* Multiplies the matrix with a given vector; the result again is a vector.
*
* @param vector The vector to multiply the matrix with.
* @returns The result of multiplying the transition probability matrix with vector.
*/
virtual std::vector<T> multiplyMatrixVector(std::vector<T>* vector) = 0;
/*!
* The check method for a state formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula<T>* formula) {
return formula->check(this);
}
/*!
* The check method for a state formula with an And node as root in its formula tree
*
* @param formula The And formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And<T>* formula) = 0;
virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And<T>*) = 0;
/*!
* The check method for a formula with an AP node as root in its formula tree
*
* @param formula The AP state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP<T>*) = 0;
/*!
* The check method for a formula with a Not node as root in its formula tree
*
* @param formula The Not state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not<T>*) = 0;
/*!
* The check method for a state formula with an Or node as root in its formula tree
*
* @param formula The Or state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or<T>*) = 0;
/*!
* The check method for a state formula with a probabilistic operator node as root in its formula tree
*
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
/*!
* The check method for a path formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>* formula) {
return formula->check(this);
}
/*!
* The check method for a path formula with a Bounded Until operator node as root in its formula tree
*
* @param formula The Bounded Until path formula to check
* @returns for each state the probability that the path formula holds.
*/
virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil<T>*) = 0;
/*!
* The check method for a path formula with a Next operator node as root in its formula tree
*
* @param formula The Next path formula to check
* @returns for each state the probability that the path formula holds.
*/
virtual std::vector<T> checkNext(mrmc::formula::Next<T>*) = 0;
/*!
* The check method for a path formula with an Until operator node as root in its formula tree
*
* @param formula The Until path formula to check
* @returns for each state the probability that the path formula holds.
*/
virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0;
};

Write Preview
Loading…
Cancel
Save