diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index e69de29bb..337dd7c39 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -0,0 +1,15 @@ +#include "src/storage/jani/Model.h" + +namespace storm { + namespace jani { + + Model::Model(ModelType const& modelType, uint64_t version) : modelType(modelType), version(version) { + // Intentionally left empty. + } + + bool Model::isValid(bool logDebug) const { + // TODO. + } + + } +} \ No newline at end of file diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index f287ab066..ab2ac4ed4 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -1,24 +1,20 @@ #pragma once -#include "Automaton.h" #include "src/utility/macros.h" +#include "src/storage/jani/ModelType.h" +#include "src/storage/jani/Automaton.h" namespace storm { namespace jani { - - enum class JaniModelType {UNSPECIFED = 0, - DTMC = 1, - CTMC = 2, - MDP = 3}; - class Model { - size_t janiVersion = 0; - JaniModelType modelType; - std::map automata; - public: + /*! + * Creates an empty model with the given type. + */ + Model(ModelType const& modelType, uint64_t version = 1); + /*! * Does some simple checks to determine whether the model is supported by Prism. * Mainly checks abscence of features the parser supports. @@ -26,32 +22,24 @@ namespace storm { * Throws UnsupportedModelException if something is wrong */ // TODO add engine as argument to check this for several engines. - void checkSupported() { + void checkSupported(); - } - - /*! + /*! * Checks if the model is valid JANI, which should be verified before any further operations are applied to a model. */ - bool checkValidity(bool logdbg = true) { - if (janiVersion == 0) { - if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified"); - return false; - } - - if(modelType == JaniModelType::UNSPECIFED) { - if(logdbg) STORM_LOG_DEBUG("Model type is unspecified"); - return false; - } - - if(automata.empty()) { - if(logdbg) STORM_LOG_DEBUG("No automata specified"); - return false; - } - // All checks passed. - return true; + bool checkValidity(bool logdbg = true); + private: + /// The list of automata + std::vector automata; + /// A mapping from names to automata indices + std::map automatonIndex; + /// The type of the model. + ModelType modelType; + /// The JANI-version used to specify the model. + uint64_t version; + /// The model name + std::string name; - } }; } } diff --git a/src/storage/jani/ModelType.cpp b/src/storage/jani/ModelType.cpp new file mode 100644 index 000000000..243d69515 --- /dev/null +++ b/src/storage/jani/ModelType.cpp @@ -0,0 +1,28 @@ +#include "src/storage/jani/ModelType.h" + +namespace storm { + namespace jani { + + std::ostream& operator<<(std::ostream& stream, ModelType const& type) { + switch (type) { + case ModelType::UNDEFINED: + stream << "undefined"; + break; + case ModelType::DTMC: + stream << "dtmc"; + break; + case ModelType::CTMC: + stream << "ctmc"; + break; + case ModelType::MDP: + stream << "mdp"; + break; + case ModelType::MA: + stream << "ma"; + break; + } + return stream; + } + + } +} diff --git a/src/storage/jani/ModelType.h b/src/storage/jani/ModelType.h new file mode 100644 index 000000000..47568355e --- /dev/null +++ b/src/storage/jani/ModelType.h @@ -0,0 +1,13 @@ +#pragma once + +#include + +namespace storm { + namespace jani { + + enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, MA = 4}; + + std::ostream& operator<<(std::ostream& stream, ModelType const& type); + + } +} \ No newline at end of file