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

Added a probabilistic operator class that checks whether the probability 

that the path formula holds is equal to one single number, instead of
comparing it to a lower and upper bound.
tempestpy_adaptions
Lanchid 12 years ago
parent
f80a7bcab3
commit
1c088c1ca6
5 changed files with 229 additions and 73 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. 1
      src/formula/Formulas.h
  2. 176
      src/formula/ProbabilisticIntervalOperator.h
  3. 98
      src/formula/ProbabilisticOperator.h
  4. 25
      src/modelChecker/DtmcPrctlModelChecker.h
  5. 2
      src/modelChecker/GmmxxDtmcPrctlModelChecker.h

1
src/formula/Formulas.h
View File

@ -18,6 +18,7 @@
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "ProbabilisticOperator.h"
#include "ProbabilisticIntervalOperator.h"
#include "Until.h"
#endif /* FORMULAS_H_ */

176
src/formula/ProbabilisticIntervalOperator.h
View File

@ -0,0 +1,176 @@
/*
* ProbabilisticOperator.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
#ifndef PROBABILISTICINTERVALOPERATOR_H_
#define PROBABILISTICINTERVALOPERATOR_H_
#include "PCTLStateFormula.h"
#include "PCTLPathFormula.h"
#include "utility/const_templates.h"
namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
* If the probability interval consist just of one single value (i.e. it is [x,x] for some
* real number x), the class ProbabilisticOperator should be used instead.
*
*
* Has one PCTL path formula as sub formula/tree.
*
* @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
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
* @see PCTLStateFormula
* @see PCTLPathFormula
* @see ProbabilisticOperator
* @see PCTLFormula
*/
template<class T>
class ProbabilisticIntervalOperator : public PCTLStateFormula<T> {
public:
/*!
* Empty constructor
*/
ProbabilisticIntervalOperator() {
upper = mrmc::utility::constGetZero(upper);
lower = mrmc::utility::constGetZero(lower);
pathFormula = NULL;
}
/*!
* Constructor
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula<T>& pathFormula) {
this->lower = lowerBound;
this->upper = upperBound;
this->pathFormula = &pathFormula;
}
/*!
* Destructor
*
* The subtree is deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~ProbabilisticIntervalOperator() {
if (pathFormula != NULL) {
delete pathFormula;
}
}
/*!
* @returns the child node (representation of a PCTL path formula)
*/
const PCTLPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
/*!
* @returns the lower bound for the probability
*/
const T& getLowerBound() const {
return lower;
}
/*!
* @returns the upper bound for the probability
*/
const T& getUpperBound() const {
return upper;
}
/*!
* Sets the child node
*
* @param pathFormula the path formula that becomes the new child node
*/
void setPathFormula(PCTLPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
/*!
* Sets the interval in which the probability that the path formula holds may lie in.
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
*/
void setInterval(T lowerBound, T upperBound) {
this->lower = lowerBound;
this->upper = upperBound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = "(";
result += " P[";
result += lower;
result += ";";
result += upper;
result += "] ";
result += pathFormula->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 AND-object that is identical the called object.
*/
virtual PCTLStateFormula<T>* clone() const {
ProbabilisticIntervalOperator<T>* result = new ProbabilisticIntervalOperator<T>();
result->setInterval(lower, upper);
if (pathFormula != NULL) {
result->setPathFormula(pathFormula->clone());
}
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 bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkProbabilisticIntervalOperator(this);
}
private:
T lower;
T upper;
PCTLPathFormula<T>* pathFormula;
};
} //namespace formula
} //namespace mrmc
#endif /* PROBABILISTICINTERVALOPERATOR_H_ */

98
src/formula/ProbabilisticOperator.h
View File

@ -1,7 +1,7 @@
/*
* ProbabilisticOperator.h
*
* Created on: 19.10.2012
* Created on: 07.12.2012
* Author: Thomas Heinemann
*/
@ -9,53 +9,54 @@
#define PROBABILISTICOPERATOR_H_
#include "PCTLStateFormula.h"
#include "PCTLPathFormula.h"
#include "utility/const_templates.h"
namespace mrmc {
namespace formula {
/*!
* @brief
* Class for a PCTL formula tree with a P (probablistic) operator node as root.
* Class for a PCTL formula tree with a P (probablistic) operator node over a single real valued
* probability as root.
*
* If the probability interval consist just of one single value (i.e. it is [x,x] for some
* real number x), the class ProbabilisticOperator should be used instead.
*
*
* Has one PCTL path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds specified in this operator
* The formula holds iff the probability that the path formula holds is equal to the probablility
* 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 PCTLStateFormula
* @see PCTLPathFormula
* @see ProbabilisticOperator
* @see PCTLFormula
*/
template<class T>
class ProbabilisticOperator : public PCTLStateFormula<T> {
class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula<T> {
public:
/*!
* Empty constructor
*/
ProbabilisticOperator() {
upper = mrmc::utility::constGetZero(upper);
lower = mrmc::utility::constGetZero(lower);
pathFormula = NULL;
// TODO Auto-generated constructor stub
}
/*!
* Constructor
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
* @param pathFormula The child node (can be omitted, is then set to NULL)
* @param bound The expected value for path formulas
* @param pathFormula The child node
*/
ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
this->lower = lowerBound;
this->upper = upperBound;
this->pathFormula = pathFormula;
ProbabilisticOperator(T bound, PCTLPathFormula<T>& pathFormula) {
this->bound = bound;
this->pathFormula = &pathFormula;
}
/*!
@ -65,9 +66,7 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~ProbabilisticOperator() {
if (pathFormula != NULL) {
delete pathFormula;
}
// TODO Auto-generated destructor stub
}
/*!
@ -81,14 +80,7 @@ public:
* @returns the lower bound for the probability
*/
const T& getLowerBound() const {
return lower;
}
/*!
* @returns the upper bound for the probability
*/
const T& getUpperBound() const {
return upper;
return bound;
}
/*!
@ -101,29 +93,12 @@ public:
}
/*!
* Sets the interval in which the probability that the path formula holds may lie.
* Sets the expected probability that the path formula holds.
*
* @param lowerBound The lower bound for the probability
* @param upperBound The upper bound for the probability
* @param bound The bound for the probability
*/
void setInterval(T lowerBound, T upperBound) {
this->lower = lowerBound;
this->upper = upperBound;
}
/*!
* @returns a string representation of the formula
*/
virtual std::string toString() const {
std::string result = "(";
result += " P[";
result += lower;
result += ";";
result += upper;
result += "] ";
result += pathFormula->toString();
result += ")";
return result;
void setInterval(T bound) {
this->bound = bound;
}
/*!
@ -131,11 +106,11 @@ public:
*
* 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.
* @returns a new ProbabilisticOperator-object that is identical to the called object.
*/
virtual PCTLStateFormula<T>* clone() const {
ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
result->setInterval(lower, upper);
result->setBound(bound);
if (pathFormula != NULL) {
result->setPathFormula(pathFormula->clone());
}
@ -146,23 +121,22 @@ public:
* 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 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.
* @returns A bit vector indicating all states that satisfy the formula represented by the
* called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual mrmc::storage::BitVector *check(
const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
return modelChecker.checkProbabilisticOperator(this);
}
private:
T lower;
T upper;
T bound;
PCTLPathFormula<T>* pathFormula;
};
} //namespace formula
} //namespace mrmc
} /* namespace formula */
} /* namespace mrmc */
#endif /* PROBABILISTICOPERATOR_H_ */

25
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -26,14 +26,7 @@ class DtmcPrctlModelChecker;
#include "src/formula/PCTLPathFormula.h"
#include "src/formula/PCTLStateFormula.h"
#include "src/formula/And.h"
#include "src/formula/AP.h"
#include "src/formula/BoundedUntil.h"
#include "src/formula/Next.h"
#include "src/formula/Not.h"
#include "src/formula/Or.h"
#include "src/formula/ProbabilisticOperator.h"
#include "src/formula/Until.h"
#include "src/formula/Formulas.h"
#include "src/models/Dtmc.h"
#include "src/storage/BitVector.h"
@ -163,12 +156,24 @@ public:
}
/*!
* The check method for a state formula with a probabilistic operator node as root in its formula tree
* 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(const mrmc::formula::ProbabilisticOperator<T>& formula) const = 0;
virtual mrmc::storage::BitVector* checkProbabilisticOperator(
const mrmc::formula::ProbabilisticOperator<T>& formula) const = 0;
/*!
* The check method for a state formula with a probabilistic interval 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* checkProbabilisticIntervalOperator(
const mrmc::formula::ProbabilisticIntervalOperator<T>& formula) const = 0;
/*!
* The check method for a path formula; Will infer the actual type of formula and delegate it

2
src/modelChecker/GmmxxDtmcPrctlModelChecker.h
View File

@ -37,7 +37,7 @@ public:
virtual ~GmmxxDtmcPrctlModelChecker() { }
virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator<Type>& formula) const {
virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticIntervalOperator<Type>& formula) const {
std::vector<Type>* probabilisticResult = this->checkPathFormula(formula.getPathFormula());
mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates());

Write Preview
Loading…
Cancel
Save