Model:

-Actions
-Const correctness
-Constructor takes a name

Former-commit-id: 0023152cae

src/storage/jani/Model.cpp

@@ -1,17 +1,35 @@
+#include <src/exceptions/InvalidJaniException.h>
 #include "src/storage/jani/Model.h"
 
 namespace storm {
     namespace jani {
         
-        Model::Model(ModelType const& modelType, uint64_t version) : modelType(modelType), version(version) {
+        Model::Model(std::string const& name, ModelType const& modelType, uint64_t version) : name(name), modelType(modelType), version(version) {
             // Intentionally left empty.
         }
 
-        void Model::checkSupported() {
+        uint64_t Model::addAction(Action const& act) {
+            STORM_LOG_THROW(actionToIndex.count(act.getName()) == 0, storm::exceptions::InvalidJaniException, "Action with name " + act.getName() + " already exists");
+            actionToIndex.emplace(act.getName(), actions.size());
+            actions.push_back(act);
+            return actions.size() - 1;
+        }
+
+        bool Model::hasAction(std::string const &name) const {
+            return actionToIndex.count(name) != 0;
+        }
+
+        uint64_t Model::getActionIndex(std::string const& name) const {
+            assert(this->hasAction(name));
+            return actionToIndex.at(name);
+        }
+
+
+        void Model::checkSupported() const {
             //TODO
         }
 
-        bool Model::checkValidity(bool logdbg) {
+        bool Model::checkValidity(bool logdbg) const {
             // TODO switch to exception based return value.
 
             if (version == 0) {

src/storage/jani/Model.h

@@ -2,6 +2,7 @@
 
 #include "src/utility/macros.h"
 
+#include "src/storage/jani/Action.h"
 #include "src/storage/jani/ModelType.h"
 #include "src/storage/jani/Automaton.h"
 
@@ -13,8 +14,29 @@ namespace storm {
             /*!
              * Creates an empty model with the given type.
              */
-            Model(ModelType const& modelType, uint64_t version = 1);
+            Model(std::string const& name, ModelType const& modelType, uint64_t version = 1);
+
+            /**
+             * Checks whether the model has an action with the given name.
+             * 
+             * @param name The name to look for. 
+             */
+            bool hasAction(std::string const& name) const;
+            
+            /**
+             * Get the index of the action
+             * @param the name of the model
+             * @return the index of the (unique) action with the given name, undefined if no such action is present.
+             */
+            uint64_t getActionIndex(std::string const& name) const;
             
+            /**
+             * Adds an action to the model.
+             *
+             * @return the index for this action.
+             */
+            uint64_t addAction(Action const& act);
+
             /*!
              *  Does some simple checks to determine whether the model is supported by Prism.
              *  Mainly checks abscence of features the parser supports.
@@ -22,23 +44,29 @@ namespace storm {
              *  Throws UnsupportedModelException if something is wrong
              */
             // TODO add engine as argument to check this for several engines.
-            void checkSupported();
+            void checkSupported() const;
 
              /*!
              *  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);
+             bool checkValidity(bool logdbg = true) const;
         private:
+            /// The model name
+            std::string name;
             /// The list of automata
             std::vector<Automaton> automata;
             /// A mapping from names to automata indices
-            std::map<std::string, size_t> automatonIndex;
+            std::unordered_map<std::string, size_t> automatonToIndex;
+            /// The list with actions
+            std::vector<Action> actions;
+            /// A mapping from names to action indices
+            std::unordered_map<std::string, uint64_t> actionToIndex;
+
             /// The type of the model.
             ModelType modelType;
             /// The JANI-version used to specify the model.
             uint64_t version;
-            /// The model name
-            std::string name;
+
 
         };
     }