From 79761d049256986ac9e8d84df6c67d9e5ff7b283 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Mon, 3 Dec 2012 11:18:10 +0100
Subject: [PATCH] Added copy constructor to model checker

---
 src/modelChecker/DtmcPrctlModelChecker.cpp |  5 ++++
 src/modelChecker/DtmcPrctlModelChecker.h   | 30 ++++++++++++++--------
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp
index 2af9ee50d..f5a884921 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.cpp
+++ b/src/modelChecker/DtmcPrctlModelChecker.cpp
@@ -21,6 +21,11 @@ DtmcPrctlModelChecker<T>::~DtmcPrctlModelChecker() {
    delete this->dtmc;
 }
 
+template<class T>
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	this->dtmc = new mrmc::models::Dtmc<T>(modelChecker->getDtmc());
+}
+
 
 } //namespace modelChecker
 
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index 7c6932ccb..979d8d93d 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -54,28 +54,33 @@ namespace modelChecker {
  */
 template<class T>
 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
        */
       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
        * other edges from these states)
@@ -185,6 +190,9 @@ class DtmcPrctlModelChecker {
        * @returns for each state the probability that the path formula holds.
        */
       virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0;
+
+   private:
+      mrmc::models::Dtmc<T>* dtmc;
 };
 
 } //namespace modelChecker