initial value support unbounded integers, some extra error messages)

Former-commit-id: 72a35269f3 [formerly 243d50b5af]
Former-commit-id: 9c7e2bd9eb

src/parser/JaniParser.cpp

@@ -262,19 +262,29 @@ namespace storm {
                             initVal = expressionManager->boolean(defaultBooleanInitialValue);
                         } else {
                             initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
                         }
                         return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
                     }
                     return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar);
                 } else if(variableStructure.at("type") == "int") {
+                    if(initvalcount == 1) {
+                        if(variableStructure.at("initial-value").is_null()) {
+                            initVal = expressionManager->integer(defaultIntegerInitialValue);
+                        } else {
+                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+                        }
+                        return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
+                    }
                     return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar);
                 } else {
                     // TODO clocks.
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump()  << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
                 }
             }
 
-            STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump()  << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
         }
 
         /**

src/storage/jani/UnboundedIntegerVariable.cpp

@@ -3,6 +3,10 @@
 namespace storm {
     namespace jani {
         
+        UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+            // Intentionally left empty.
+        }
+        
         UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) {
             // Intentionally left empty.
         }

src/storage/jani/UnboundedIntegerVariable.h

@@ -8,9 +8,14 @@ namespace storm {
         class UnboundedIntegerVariable : public Variable {
         public:
             /*!
-             * Creates an unbounded integer variable.
+             * Creates an unbounded integer variable without initial value.
              */
             UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
+            /*!
+             * Creates an unbounded integer variable with initial value.
+             */
+            UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const&, bool transient=false);
+
             
             virtual bool isUnboundedIntegerVariable() const override;
         };