From 7c9c55b09c90944efa6115199ad327ae217db629 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 9 Sep 2016 14:42:56 +0200
Subject: [PATCH] added 'superclass' for PRISM program and JANI model so they
 can be handled as symbolic model descriptions

Former-commit-id: 748069c151a8157867c5a8358476c0266c2d52b9 [formerly 2c3e462958903cf0ec2f00e3d19802694af7c73e]
Former-commit-id: e8d3ceb693377f5f39cc57bae2a2f23b85ec4312
---
 src/storage/SymbolicModelDescription.cpp | 43 +++++++++++++++++++-----
 src/storage/SymbolicModelDescription.h   | 35 +++++++++++++------
 2 files changed, 59 insertions(+), 19 deletions(-)

diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp
index 9451c6a08..3bf4bf121 100644
--- a/src/storage/SymbolicModelDescription.cpp
+++ b/src/storage/SymbolicModelDescription.cpp
@@ -1,9 +1,36 @@
-//
-//  SymbolicModelDescription.cpp
-//  storm
-//
-//  Created by Christian Dehnert on 09/09/16.
-//
-//
+#include "src/storage/SymbolicModelDescription.h"
 
-#include "SymbolicModelDescription.hpp"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace storage {
+        
+        SymbolicModelDescription::SymbolicModelDescription(storm::jani::Model const& model) {
+            // Intentionally left empty.
+        }
+        
+        SymbolicModelDescription::SymbolicModelDescription(storm::prism::Program const& program) {
+            // Intentionally left empty.
+        }
+                
+        bool SymbolicModelDescription::isJaniModel() const {
+            return modelDescription.which() == 0;
+        }
+        
+        bool SymbolicModelDescription::isPrismProgram() const {
+            return modelDescription.which() == 1;
+        }
+        
+        storm::jani::Model const& SymbolicModelDescription::asJaniModel() const {
+            STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type.");
+            return boost::get<storm::jani::Model>(modelDescription);
+        }
+        
+        storm::prism::Program const& SymbolicModelDescription::asPrismProgram() const {
+            STORM_LOG_THROW(isPrismProgram(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type.");
+            return boost::get<storm::prism::Program>(modelDescription);
+        }
+        
+    }
+}
\ No newline at end of file
diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h
index f73dce810..1679ef1df 100644
--- a/src/storage/SymbolicModelDescription.h
+++ b/src/storage/SymbolicModelDescription.h
@@ -1,14 +1,27 @@
-//
-//  SymbolicModelDescription.hpp
-//  storm
-//
-//  Created by Christian Dehnert on 09/09/16.
-//
-//
+#pragma once
 
-#ifndef SymbolicModelDescription_hpp
-#define SymbolicModelDescription_hpp
+#include <boost/variant.hpp>
 
-#include <stdio.h>
+#include "src/storage/jani/Model.h"
+#include "src/storage/prism/Program.h"
 
-#endif /* SymbolicModelDescription_hpp */
+namespace storm {
+    namespace storage {
+        
+        class SymbolicModelDescription {
+        public:
+            SymbolicModelDescription(storm::jani::Model const& model);
+            SymbolicModelDescription(storm::prism::Program const& program);
+
+            bool isJaniModel() const;
+            bool isPrismProgram() const;
+            
+            storm::jani::Model const& asJaniModel() const;
+            storm::prism::Program const& asPrismProgram() const;
+            
+        private:
+            boost::variant<storm::jani::Model, storm::prism::Program> modelDescription;
+        };
+        
+    }
+}
\ No newline at end of file