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(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(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 -#include +#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 modelDescription; + }; + + } +} \ No newline at end of file