|
@ -54,28 +54,33 @@ namespace modelChecker { |
|
|
*/ |
|
|
*/ |
|
|
template<class T> |
|
|
template<class T> |
|
|
class DtmcPrctlModelChecker { |
|
|
class DtmcPrctlModelChecker { |
|
|
private: |
|
|
|
|
|
mrmc::models::Dtmc<T>* dtmc; |
|
|
|
|
|
|
|
|
|
|
|
protected: |
|
|
|
|
|
|
|
|
public: |
|
|
/*! |
|
|
/*! |
|
|
* @returns A reference to the dtmc of the model checker. |
|
|
|
|
|
|
|
|
* Constructor |
|
|
|
|
|
* |
|
|
|
|
|
* @parameter Dtmc The dtmc model which is checked. |
|
|
*/ |
|
|
*/ |
|
|
mrmc::models::Dtmc<T>* getDtmc() const { |
|
|
|
|
|
return this->dtmc; |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* Dtmc); |
|
|
|
|
|
|
|
|
public: |
|
|
|
|
|
/*! |
|
|
/*! |
|
|
* Constructor |
|
|
|
|
|
|
|
|
* Copy constructor |
|
|
|
|
|
* |
|
|
|
|
|
* @parameter modelChecker The model checker that is copied. |
|
|
*/ |
|
|
*/ |
|
|
explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC); |
|
|
|
|
|
|
|
|
explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker); |
|
|
|
|
|
|
|
|
/*! |
|
|
/*! |
|
|
* Destructor |
|
|
* Destructor |
|
|
*/ |
|
|
*/ |
|
|
virtual ~DtmcPrctlModelChecker(); |
|
|
virtual ~DtmcPrctlModelChecker(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
|
|
* @returns A reference to the dtmc of the model checker. |
|
|
|
|
|
*/ |
|
|
|
|
|
mrmc::models::Dtmc<T>* getDtmc() const { |
|
|
|
|
|
return this->dtmc; |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
/*! |
|
|
/*! |
|
|
* Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all |
|
|
* Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all |
|
|
* other edges from these states) |
|
|
* other edges from these states) |
|
@ -185,6 +190,9 @@ class DtmcPrctlModelChecker { |
|
|
* @returns for each state the probability that the path formula holds. |
|
|
* @returns for each state the probability that the path formula holds. |
|
|
*/ |
|
|
*/ |
|
|
virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0; |
|
|
virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0; |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
|
|
mrmc::models::Dtmc<T>* dtmc; |
|
|
}; |
|
|
}; |
|
|
|
|
|
|
|
|
} //namespace modelChecker |
|
|
} //namespace modelChecker |
|
|