initial value support for booleans, some extra error messages)

Former-commit-id: bb857b0923 [formerly 80b90ed08e]
Former-commit-id: d529e6b9d2

src/parser/JaniParser.cpp

@@ -20,6 +20,8 @@ namespace storm {
         // Defaults
         ////////////
         const bool JaniParser::defaultVariableTransient = false;
+        const bool JaniParser::defaultBooleanInitialValue = false;
+        const int64_t JaniParser::defaultIntegerInitialValue = 0;
         const std::set<std::string> JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc",
                                                          "sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"});
 
@@ -221,7 +223,7 @@ namespace storm {
                 if(kind == "bounded") {
                     // First do the bounds, that makes the code a bit more streamlined
                     STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
-                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scopeDescription + ")");
+                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")");
                     assert(lowerboundExpr.isInitialized());
                     STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
                     storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")");
@@ -237,6 +239,9 @@ namespace storm {
                     }
                     std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name  + "(scope: " + scopeDescription + ") ");
                     if(basictype == "int") {
+                        if(initVal) {
+                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+                        }
                         STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
                         STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
                         return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr);
@@ -252,6 +257,14 @@ namespace storm {
                     // expressionManager->declareRationalVariable(name);
                     // TODO something.
                 } else if(variableStructure.at("type") == "bool") {
+                    if(initvalcount == 1) {
+                        if(variableStructure.at("initial-value").is_null()) {
+                            initVal = expressionManager->boolean(defaultBooleanInitialValue);
+                        } else {
+                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+                        }
+                        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") {
                     return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar);

src/parser/JaniParser.h

@@ -71,6 +71,9 @@ namespace storm {
             //   Default values -- assumptions from JANI.
             //////////
             static const bool defaultVariableTransient;
+            
+            static const bool defaultBooleanInitialValue;
+            static const int64_t defaultIntegerInitialValue;
 
             static const std::set<std::string> unsupportedOpstrings;
 

src/storage/jani/BooleanVariable.cpp

@@ -7,6 +7,11 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+            // Intentionally left empty.
+        }
+        
+        
         bool BooleanVariable::isBooleanVariable() const {
             return true;
         }

src/storage/jani/BooleanVariable.h

@@ -7,11 +7,17 @@ namespace storm {
         
         class BooleanVariable : public Variable {
         public:
+            
             /*!
-             * Creates a boolean variable.
+             * Creates a Boolean variable with initial value
              */
             BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
             
+            /*!
+             * Creates a Boolean variable with initial value
+             */
+            BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue, bool transient=false);
+            
             virtual bool isBooleanVariable() const override;
         };