Jani: Allowing bounded types for constants as pointed out in GitHub issue #37

CHANGELOG.md

@@ -9,6 +9,7 @@ Version 1.3.x
 
 ### Version 1.3.1 (under development)
 - Added support for multi-dimensional quantile queries
+- Allow bounded types for constants in JANI.
 - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
 
 ### Version 1.3.0 (2018/12)

src/storm-parsers/parser/JaniParser.cpp

@@ -648,67 +648,45 @@ namespace storm {
             // TODO check existance of name.
             // TODO store prefix in variable.
             std::string exprManagerName = name;
-            STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration.");
             size_t valueCount = constantStructure.count("value");
-            storm::expressions::Expression initExpr;
+            storm::expressions::Expression definingExpression;
             STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name +  "'  (scope: " + scope.description + ") must be given at most once.");
             if (valueCount == 1) {
                 // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment.
-                initExpr = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name));
-                assert(initExpr.isInitialized());
+                definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name));
+                assert(definingExpression.isInitialized());
             }
-
-            if (constantStructure.at("type").is_object()) {
-//                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scope.description << ")  kind must be given");
-//                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scope.description + ") ");
-//                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: " << scope.description << ") lower-bound must be given");
-//                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scope.description + ")");
-//                    assert(lowerboundExpr.isInitialized());
-//                    STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scope.description << ") upper-bound must be given");
-//                    storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scope.description + ")");
-//                    assert(upperboundExpr.isInitialized());
-//                    STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scope.description << ") base must be given");
-//                    std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name  + "(scope: " + scope.description + ") ");
-//                    if(basictype == "int") {
-//                        STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scope.description << ") must be integer-typed");
-//                        STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scope.description << ") must be integer-typed");
-//                        return std::make_shared<storm::jani::BoundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr);
-//                    } else {
-//                        STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scope.description << ") ");
-//                    }
-//                } else {
-//                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scope.description << ") ");
-//                }
-             }
-             else if(constantStructure.at("type").is_string()) {
-                if(constantStructure.at("type") == "real") {
-                    if(initExpr.isInitialized()) {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareRationalVariable(exprManagerName), initExpr);
-                    } else {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareRationalVariable(exprManagerName));
-                    }
-                } else if(constantStructure.at("type") == "bool") {
-                    if(initExpr.isInitialized()) {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareBooleanVariable(exprManagerName), initExpr);
-                    } else {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareBooleanVariable(exprManagerName));
-                    }
-
-                } else if(constantStructure.at("type") == "int") {
-                    if(initExpr.isInitialized()) {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareIntegerVariable(exprManagerName), initExpr);
-                    } else {
-                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareIntegerVariable(exprManagerName));
+            
+            STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration.");
+            ParsedType type;
+            parseType(type, constantStructure.at("type"), name, scope);
+            
+            STORM_LOG_THROW(type.basicType.is_initialized(), storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") has unexpected type");
+            storm::expressions::Variable var;
+            switch (type.basicType.get()) {
+                case ParsedType::BasicType::Bool:
+                    var = expressionManager->declareBooleanVariable(exprManagerName);
+                    break;
+                case ParsedType::BasicType::Int:
+                    var = expressionManager->declareIntegerVariable(exprManagerName);
+                    break;
+                case ParsedType::BasicType::Real:
+                    var = expressionManager->declareRationalVariable(exprManagerName);
+                    break;
+            }
+            storm::expressions::Expression constraintExpression;
+            if (type.bounds) {
+                if (type.bounds->first.isInitialized()) {
+                    constraintExpression = var.getExpression() >= type.bounds->first;
+                    if (type.bounds->second.isInitialized()) {
+                        constraintExpression = constraintExpression && (var.getExpression() <= type.bounds->second);
                     }
-                } else {
-                    // TODO clocks.
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump()  << " for constant '" << name << "' (scope: " << scope.description << ")");
+                } else if (type.bounds->second.isInitialized()) {
+                    constraintExpression = var.getExpression() <= type.bounds->second;
                 }
             }
-
-            STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump()  << " for Variable '" << name << "' (scope: " << scope.description << ")");
+            
+            return std::make_shared<storm::jani::Constant>(name, std::move(var), definingExpression, constraintExpression);
         }
         
         void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, Scope const& scope) {
@@ -753,6 +731,15 @@ namespace storm {
                         result.basicType = ParsedType::BasicType::Int;
                         result.expressionType = expressionManager->getIntegerType();
                         result.bounds = std::make_pair(lowerboundExpr, upperboundExpr);
+                    } else if (basictype == "real") {
+                        STORM_LOG_THROW(!lowerboundExpr.isInitialized() || lowerboundExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded real variable " << variableName << "(scope: " << scope.description << ") must be numeric");
+                        STORM_LOG_THROW(!upperboundExpr.isInitialized() || upperboundExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded real variable " << variableName << "(scope: " << scope.description << ") must be numeric");
+                        if (lowerboundExpr.isInitialized() && upperboundExpr.isInitialized() && !lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) {
+                            STORM_LOG_THROW(lowerboundExpr.evaluateAsRational() <= upperboundExpr.evaluateAsRational(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable "  << variableName << "(scope: " << scope.description << ")");
+                        }
+                        result.basicType = ParsedType::BasicType::Real;
+                        result.expressionType = expressionManager->getRationalType();
+                        result.bounds = std::make_pair(lowerboundExpr, upperboundExpr);
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scope.description << ") ");
                     }
@@ -835,6 +822,7 @@ namespace storm {
             if (type.basicType) {
                 switch (type.basicType.get()) {
                     case ParsedType::BasicType::Real:
+                        STORM_LOG_WARN_COND(!type.bounds.is_initialized(), "Bounds for rational variable " + name + "(scope " + scope.description + ") will be ignored.");
                         if (setInitValFromDefault) {
                             initVal = expressionManager->rational(defaultRationalInitialValue);
                         }

src/storm/storage/jani/Constant.cpp

@@ -1,10 +1,25 @@
 #include "storm/storage/jani/Constant.h"
+#include "storm/utility/solver.h"
+#include "storm/solver/SmtSolver.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidJaniException.h"
 
 namespace storm {
     namespace jani {
+
+        bool checkDefiningExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& definingExpression, storm::expressions::Expression const& constaintExpression) {
+            auto manager = var.getManager().clone();
+            auto smtSolver = storm::utility::solver::getSmtSolver(*manager);
+            smtSolver->add(var.getExpression().changeManager(*manager) == definingExpression.changeManager(*manager));
+            smtSolver->add(constaintExpression.changeManager(*manager));
+            return smtSolver->check() == storm::solver::SmtSolver::CheckResult::Sat;
+        }
         
-        Constant::Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> const& expression) : name(name), variable(variable), expression(expression) {
-            // Intentionally left empty.
+        Constant::Constant(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& definingExpression, storm::expressions::Expression const& constraintExpression) : name(name), variable(variable), definingExpression(definingExpression), constraintExpression(constraintExpression) {
+            if (definingExpression.isInitialized() && constraintExpression.isInitialized()) {
+                STORM_LOG_THROW(checkDefiningExpression(variable, definingExpression, constraintExpression), storm::exceptions::InvalidJaniException, "The constant '" << name << "' was set to '" << definingExpression << "' which violates the constraint given for this constant: '" << constraintExpression << "'.");
+            }
         }
         
         std::string const& Constant::getName() const {
@@ -12,11 +27,14 @@ namespace storm {
         }
         
         bool Constant::isDefined() const {
-            return static_cast<bool>(expression);
+            return definingExpression.isInitialized();
         }
         
         void Constant::define(storm::expressions::Expression const& expression) {
-            this->expression = expression;
+            if (hasConstraint()) {
+                STORM_LOG_THROW(checkDefiningExpression(getExpressionVariable(), expression, constraintExpression), storm::exceptions::InvalidJaniException, "The constant '" << name << "' was set to '" << expression << "' which violates the constraint given for this constant: '" << constraintExpression << "'.");
+            }
+            this->definingExpression = expression;
         }
         
         storm::expressions::Type const& Constant::getType() const {
@@ -40,7 +58,24 @@ namespace storm {
         }
         
         storm::expressions::Expression const& Constant::getExpression() const {
-            return expression.get();
+            STORM_LOG_ASSERT(isDefined(), "Tried to get the constant definition of undefined constant '" << variable.getName() << "'.");
+            return definingExpression;
+        }
+        
+        bool Constant::hasConstraint() const {
+            return constraintExpression.isInitialized();
+        }
+        
+        storm::expressions::Expression const& Constant::getConstraintExpression() const {
+            STORM_LOG_ASSERT(hasConstraint(), "Tried to get the constant constraint of unconstrained constant '" << variable.getName() << "'.");
+            return constraintExpression;
+        }
+        
+        void Constant::setConstraintExpression(storm::expressions::Expression const& expression) {
+            if (isDefined()) {
+                STORM_LOG_THROW(checkDefiningExpression(getExpressionVariable(), definingExpression, expression), storm::exceptions::InvalidJaniException, "The constant '" << name << "' was set to '" << definingExpression << "' which violates the constraint given for this constant: '" << expression << "'.");
+            }
+            constraintExpression = expression;
         }
         
     }

src/storm/storage/jani/Constant.h

@@ -15,7 +15,7 @@ namespace storm {
             /*!
              * Creates a constant.
              */
-            Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> const& expression = boost::none);
+            Constant(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& definingExpression = storm::expressions::Expression(), storm::expressions::Expression const& constraintExpression = storm::expressions::Expression());
             
             /*!
              * Retrieves the name of the constant.
@@ -29,6 +29,7 @@ namespace storm {
             
             /*!
              * Defines the constant with the given expression.
+             * If a constraintExpression is set, it is checked whether the constant definition satisfies the given constraint.
              */
             void define(storm::expressions::Expression const& expression);
             
@@ -62,6 +63,21 @@ namespace storm {
              */
             storm::expressions::Expression const& getExpression() const;
             
+            /*!
+             * Retrieves whether there is a constraint for the possible values of this constant
+             */
+             bool hasConstraint() const;
+             
+             /*!
+              * Retrieves the expression that constraints the possible values of this constant (if any).
+              */
+            storm::expressions::Expression const& getConstraintExpression() const;
+             
+             /*!
+              * Sets a constraint expression. An exception is thrown if this constant is defined and the definition violates the given constraint.
+              */
+             void setConstraintExpression(storm::expressions::Expression const& expression);
+            
         private:
             // The name of the constant.
             std::string name;
@@ -70,7 +86,10 @@ namespace storm {
             storm::expressions::Variable variable;
 
             // The expression defining the constant (if any).
-            boost::optional<storm::expressions::Expression> expression;
+            storm::expressions::Expression definingExpression;
+
+            // The expression constraining possible values of the constant (if any).
+            storm::expressions::Expression constraintExpression;
         };
         
     }

src/storm/storage/jani/JSONExporter.cpp

@@ -796,7 +796,46 @@ namespace storm {
             
         }
         
-
+        modernjson::json buildTypeDescription(storm::expressions::Type const& type) {
+            modernjson::json typeDescr;
+            if (type.isIntegerType()) {
+                typeDescr = "int";
+            } else if (type.isRationalType()) {
+                typeDescr = "real";
+            } else if (type.isBooleanType()) {
+                typeDescr = "bool";
+            } else if (type.isArrayType()) {
+                typeDescr["kind"] = "array";
+                typeDescr["base"] = buildTypeDescription(type.getElementType());
+            } else {
+                assert(false);
+            }
+            return typeDescr;
+        }
+        
+        void getBoundsFromConstraints(modernjson::json& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector<storm::jani::Constant> const& constants) {
+            if (constraint.getBaseExpression().isBinaryBooleanFunctionExpression() && constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::And) {
+                getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(0), constants);
+                getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(1), constants);
+            } else if (constraint.getBaseExpression().isBinaryRelationExpression()) {
+                bool leq = constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::LessOrEqual;
+                bool geq = constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::GreaterOrEqual;
+                std::vector<bool> varOps(2, false);
+                for (int i : {0,1}) {
+                    varOps[i] = constraint.getOperand(i).isVariable() && constraint.getOperand(i).getBaseExpression().asVariableExpression().getVariable() == var;
+                }
+                storm::expressions::Expression boundExpr = varOps[0] ? constraint.getOperand(1) : constraint.getOperand(0);
+                if ((leq && varOps[0]) || geq && varOps[1]) {
+                    typeDesc["upper-bound"] = buildExpression(boundExpr, constants);
+                } else if ((leq && varOps[1] || geq && varOps[0])) {
+                    typeDesc["lower-bound"] = buildExpression(boundExpr, constants);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani Export for constant constraint " << constraint << " is not supported.");
+                }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani Export for constant constraint " << constraint << " is not supported.");
+            }
+        }
         
         modernjson::json buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
             std::vector<modernjson::json> constantDeclarations;
@@ -804,13 +843,12 @@ namespace storm {
                 modernjson::json constantEntry;
                 constantEntry["name"] = constant.getName();
                 modernjson::json typeDesc;
-                if(constant.isBooleanConstant()) {
-                    typeDesc = "bool";
-                } else if(constant.isRealConstant()) {
-                    typeDesc = "real";
+                if (constant.hasConstraint()) {
+                    typeDesc["kind"] = "bounded";
+                    typeDesc["base"] = buildTypeDescription(constant.getType());
+                    getBoundsFromConstraints(typeDesc, constant.getExpressionVariable(), constant.getConstraintExpression(), constants);
                 } else {
-                    assert(constant.isIntegerConstant());
-                    typeDesc = "int";
+                    typeDesc = buildTypeDescription(constant.getType());
                 }
                 constantEntry["type"] = typeDesc;
                 if(constant.isDefined()) {
@@ -880,24 +918,7 @@ namespace storm {
             }
             return variableDeclarations;
         }
-        
-        modernjson::json buildTypeDescription(storm::expressions::Type const& type) {
-            modernjson::json typeDescr;
-            if (type.isIntegerType()) {
-                typeDescr = "int";
-            } else if (type.isRationalType()) {
-                typeDescr = "real";
-            } else if (type.isBooleanType()) {
-                typeDescr = "bool";
-            } else if (type.isArrayType()) {
-                typeDescr["kind"] = "array";
-                typeDescr["base"] = buildTypeDescription(type.getElementType());
-            } else {
-                assert(false);
-            }
-            return typeDescr;
-        }
-        
+
         modernjson::json buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
             modernjson::json functionDeclarations = std::vector<modernjson::json>();
             for (auto const& nameFunDef : functionDefinitions) {

src/storm/storage/jani/Model.cpp

@@ -1022,6 +1022,9 @@ namespace storm {
             // Gather all defining expressions of constants.
             std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
             for (auto& constant : result.getConstants()) {
+                if (constant.hasConstraint()) {
+                    constant.setConstraintExpression(substituteJaniExpression(constant.getConstraintExpression(), constantSubstitution));
+                }
                 if (constant.isDefined()) {
                     constant.define(substituteJaniExpression(constant.getExpression(), constantSubstitution));
                     constantSubstitution[constant.getExpressionVariable()] = constant.getExpression();
@@ -1079,6 +1082,9 @@ namespace storm {
         void Model::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             // substitute in all defining expressions of constants
             for (auto& constant : this->getConstants()) {
+                if (constant.hasConstraint()) {
+                    constant.setConstraintExpression(substituteJaniExpression(constant.getConstraintExpression(), substitution));
+                }
                 if (constant.isDefined()) {
                     constant.define(substituteJaniExpression(constant.getExpression(), substitution));
                 }

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

@@ -48,6 +48,9 @@ namespace storm {
             if (constant.isDefined()) {
                 traverse(constant.getExpression(), data);
             }
+            if (constant.hasConstraint()) {
+                traverse(constant.getConstraintExpression(), data);
+            }
         }
         
         void JaniTraverser::traverse(FunctionDefinition& functionDefinition, boost::any const& data) {
@@ -226,6 +229,9 @@ namespace storm {
             if (constant.isDefined()) {
                 traverse(constant.getExpression(), data);
             }
+            if (constant.hasConstraint()) {
+                traverse(constant.getConstraintExpression(), data);
+            }
         }
         
         void ConstJaniTraverser::traverse(FunctionDefinition const& functionDefinition, boost::any const& data) {

src/storm/storage/prism/ToJaniConverter.cpp

@@ -48,7 +48,7 @@ namespace storm {
             
             // Add all constants of the PRISM program to the JANI model.
             for (auto const& constant : program.getConstants()) {
-                janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional<storm::expressions::Expression>(constant.getExpression()) : boost::none));
+                janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? constant.getExpression() : storm::expressions::Expression()));
             }
             
             // Maintain a mapping of each variable to a flag that is true if the variable will be made global.