From b1498ef0bb61056273d0f697f166d9d84e70af6e Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Fri, 22 Feb 2013 15:11:36 +0100
Subject: [PATCH] moved model from specific model checkers to
AbstractModelChecker
---
src/modelchecker/AbstractModelChecker.h | 23 +++++++++++++++++++
src/modelchecker/DtmcPrctlModelChecker.h | 21 +++++++++++------
src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 6 +++--
src/modelchecker/MdpPrctlModelChecker.h | 23 +++++++++++--------
4 files changed, 55 insertions(+), 18 deletions(-)
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 244b35df1..698aaa466 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -15,6 +15,7 @@ template <class Type> class AbstractModelChecker;
#include "src/exceptions/InvalidPropertyException.h"
#include "src/formula/Formulas.h"
#include "src/storage/BitVector.h"
+#include "src/models/AbstractModel.h"
#include <iostream>
@@ -50,6 +51,15 @@ class AbstractModelChecker :
public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
public:
+ explicit AbstractModelChecker(storm::models::AbstractModel<Type>& model)
+ : model(model) {
+ // Nothing to do here...
+ }
+
+ explicit AbstractModelChecker(AbstractModelChecker<Type>* modelChecker)
+ : model(modelChecker->model) {
+ }
+
template <template <class T> class Target>
const Target<Type>* as() const {
try {
@@ -154,6 +164,19 @@ public:
delete quantitativeResult;
return result;
}
+
+ void setModel(storm::models::AbstractModel<Type>& model) {
+ this->model = model;
+ }
+
+ template <class Model>
+ Model& getModel() const {
+ return *dynamic_cast<Model*>(&this->model);
+ }
+
+private:
+ storm::models::AbstractModel<Type>& model;
+
};
} //namespace modelChecker
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index 61a9b2ffd..a31caac13 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -39,14 +39,22 @@ namespace modelChecker {
*/
template<class Type>
class DtmcPrctlModelChecker :
- public virtual AbstractModelChecker<Type> {
+ public AbstractModelChecker<Type> {
+
+private:
+ /*!
+ * Make default constructor private.
+ */
+ explicit DtmcPrctlModelChecker() {}
+
public:
/*!
* Constructor
*
* @param model The dtmc model which is checked.
*/
- explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : model(model) {
+ explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model)
+ : AbstractModelChecker<Type>(model) {
// Intentionally left empty.
}
@@ -55,8 +63,7 @@ public:
*
* @param modelChecker The model checker that is copied.
*/
- explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) {
- this->model = new storm::models::Dtmc<Type>(modelChecker->getModel());
+ explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) {
}
/*!
@@ -70,7 +77,7 @@ public:
* @returns A reference to the dtmc of the model checker.
*/
storm::models::Dtmc<Type>& getModel() const {
- return this->model;
+ return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>();
}
/*!
@@ -78,7 +85,7 @@ public:
* @param model
*/
void setModel(storm::models::Dtmc<Type>& model) {
- this->model = &model;
+ AbstractModelChecker<Type>::setModel(model);
}
/*!
@@ -268,7 +275,7 @@ public:
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
private:
- storm::models::Dtmc<Type>& model;
+// storm::models::Dtmc<Type>& model;
};
} //namespace modelChecker
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index fdd246843..d4aeef764 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -36,10 +36,12 @@ namespace modelChecker {
* A model checking engine that makes use of the gmm++ backend.
*/
template <class Type>
-class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
+class GmmxxDtmcPrctlModelChecker
+ : public DtmcPrctlModelChecker<Type> {
public:
- explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
+ explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc)
+ : DtmcPrctlModelChecker<Type>(dtmc) {
// Intentionally left empty.
}
diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/MdpPrctlModelChecker.h
index c2fad0b21..319efd12a 100644
--- a/src/modelchecker/MdpPrctlModelChecker.h
+++ b/src/modelchecker/MdpPrctlModelChecker.h
@@ -40,15 +40,22 @@ namespace modelChecker {
*/
template<class Type>
class MdpPrctlModelChecker :
- public virtual AbstractModelChecker<Type> {
+ public AbstractModelChecker<Type> {
+
+private:
+ /*!
+ * Make default constructor private.
+ */
+ explicit MdpPrctlModelChecker() {}
+
public:
/*!
* Constructor
*
* @param model The dtmc model which is checked.
*/
- explicit MdpPrctlModelChecker(storm::models::Mdp<Type>& model) : model(model), minimumOperatorStack() {
-
+ explicit MdpPrctlModelChecker(storm::models::Mdp<Type>& model)
+ : AbstractModelChecker<Type>(model), minimumOperatorStack() {
}
/*!
@@ -56,7 +63,8 @@ public:
*
* @param modelChecker The model checker that is copied.
*/
- explicit MdpPrctlModelChecker(const storm::modelChecker::MdpPrctlModelChecker<Type>* modelChecker) : model(new storm::models::Mdp<Type>(modelChecker->getModel())), minimumOperatorStack() {
+ explicit MdpPrctlModelChecker(const storm::modelChecker::MdpPrctlModelChecker<Type>* modelChecker)
+ : AbstractModelChecker<Type>(modelChecker), minimumOperatorStack() {
}
@@ -71,7 +79,7 @@ public:
* @returns A reference to the dtmc of the model checker.
*/
storm::models::Mdp<Type>& getModel() const {
- return this->model;
+ return AbstractModelChecker<Type>::template getModel<storm::models::Mdp<Type>>();
}
/*!
@@ -79,7 +87,7 @@ public:
* @param model
*/
void setModel(storm::models::Mdp<Type>& model) {
- this->model = &model;
+ AbstractModelChecker<Type>::setModel(model);
}
/*!
@@ -273,9 +281,6 @@ public:
*/
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
-private:
- storm::models::Mdp<Type>& model;
-
protected:
mutable std::stack<bool> minimumOperatorStack;
};