Implemented retrieval of jani model information with a traverser. Also determine the size of the state domain.

src/storm/storage/jani/Model.cpp

@@ -20,6 +20,7 @@
 #include "storm/storage/jani/FunctionEliminator.h"
 #include "storm/storage/jani/VariablesToConstantsTransformer.h"
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
+#include "storm/storage/jani/traverser/InformationCollector.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 
@@ -684,6 +685,10 @@ namespace storm {
             return res;
         }
 
+        InformationObject Model::getModelInformation() const {
+            return collectModelInformation(*this);
+        }
+        
         Variable const& Model::addVariable(Variable const& variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());

src/storm/storage/jani/Model.h

@@ -36,6 +36,7 @@ namespace storm {
         class SynchronizationVector;
         struct ArrayEliminatorData;
         class Property;
+        struct InformationObject;
         
         class Model {
         public:
@@ -390,6 +391,10 @@ namespace storm {
              */
             std::size_t getTotalNumberOfNonTransientVariables() const;
 
+            /*!
+             * Returns various information of this model.
+             */
+            InformationObject getModelInformation() const;
 
             /*!
              * Sets the system composition expression of the JANI model.

src/storm/storage/jani/traverser/InformationCollector.cpp

@@ -5,16 +5,94 @@
 namespace storm {
     namespace jani {
         namespace detail {
-
+            class InformationCollector : public ConstJaniTraverser {
+            public:
+                InformationObject collect(Model const& model) {
+                    info = InformationObject();
+                    this->traverse(model, boost::any());
+                    return info;
+                }
+                
+                virtual void traverse(Model const& model, boost::any const& data) override {
+                    info.modelType = model.getModelType();
+                    info.nrAutomata = model.getNumberOfAutomata();
+                    ConstJaniTraverser::traverse(model, data);
+                }
+                
+                virtual void traverse(Automaton const& automaton, boost::any const& data) override {
+                    info.nrLocations += automaton.getNumberOfLocations();
+                    info.stateDomainSize *= automaton.getNumberOfLocations();
+                    info.nrEdges += automaton.getNumberOfEdges();
+                    ConstJaniTraverser::traverse(automaton, data);
+                }
+                
+                virtual void traverse(VariableSet const& variableSet, boost::any const& data) override {
+                    info.nrVariables += variableSet.getNumberOfNontransientVariables();
+                    ConstJaniTraverser::traverse(variableSet, data);
+                }
+                
+                virtual void traverse(BooleanVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        info.stateDomainSize *= 2;
+                    }
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+                virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        if (variable.hasLowerBound() && variable.hasUpperBound() && !variable.getLowerBound().containsVariables() && !variable.getUpperBound().containsVariables()) {
+                            info.stateDomainSize *= (variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt());
+                        } else {
+                            info.stateDomainSize = 0; // i.e. unknown
+                        }
+                    }
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+                virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        info.stateDomainSize = 0; // i.e. unknown
+                    }
+                    
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+                virtual void traverse(RealVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        info.stateDomainSize = 0; // i.e. unknown
+                    }
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+                virtual void traverse(ArrayVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        info.stateDomainSize = 0; // i.e. unknown
+                    }
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+                virtual void traverse(ClockVariable const& variable, boost::any const& data) override {
+                    if (!variable.isTransient()) {
+                        info.stateDomainSize = 0; // i.e. unknown
+                    }
+                    ConstJaniTraverser::traverse(variable, data);
+                }
+                
+            private:
+                InformationObject info;
+                
+            };
+            
+            
+        }
+        
+        InformationObject::InformationObject() : nrVariables(0), nrAutomata(0),  nrEdges(0), nrLocations(0), stateDomainSize(1) {
+            // Intentionally left empty
         }
+        
 
-        InformationObject collect(Model const& model) {
-            InformationObject result;
-            result.modelType = model.getModelType();
-            result.nrAutomata = model.getNumberOfAutomata();
-            result.nrEdges = model.getNumberOfEdges();
-            result.nrVariables = model.getTotalNumberOfNonTransientVariables();
-            return result;
+        InformationObject collectModelInformation(Model const& model) {
+            return detail::InformationCollector().collect(model);
         }
     }
 }

src/storm/storage/jani/traverser/InformationCollector.h

@@ -1,20 +1,27 @@
 #pragma once
+
+#include <string>
+
 #include "storm/storage/jani/ModelType.h"
 
+
 namespace storm {
     namespace jani {
 
         class Model;
 
         struct InformationObject {
-            storm::jani::ModelType modelType;
-            uint64_t nrVariables;
-            uint64_t nrAutomata;
-            uint64_t nrEdges;
-            uint64_t nrLocations;
+            InformationObject();
+            storm::jani::ModelType modelType; /// The type of the model
+            uint64_t nrVariables; /// The number of non-transient variables in the model
+            uint64_t nrAutomata; /// The number of automata in the model
+            uint64_t nrEdges; /// The number of edges in the model
+            uint64_t nrLocations; /// The numer of all locations of all automata of the model
+            uint64_t stateDomainSize; /// The size of the domain of the states (i.e., the product of the range of all variables times the number of locations).
+                                    /// Here, 0 means that the state domain size is unknown.
         };
 
-        InformationObject collect(Model const& model);
+        InformationObject collectModelInformation(Model const& model);
     }
 }