Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables.

Former-commit-id: 86439306b9

src/adapters/ExplicitModelAdapter.h

@@ -168,7 +168,14 @@ namespace storm {
                     setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState));
                 }
                 for (auto variableAssignmentPair : update.getIntegerAssignments()) {
-                    setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsInt(baseState));
+                    int_fast64_t newVariableValue = variableAssignmentPair.second.getExpression()->getValueAsInt(baseState);
+                    bool isLegalValueForVariable = newVariableValue >= variableInformation.lowerBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)) && newVariableValue <= variableInformation.upperBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first));
+                    
+                    if (!isLegalValueForVariable) {
+                        throw storm::exceptions::InvalidStateException() << "Invalid value '" << newVariableValue << "' for variable \"" << variableInformation.integerVariables.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)).getName() << "\". Please strengthen the guards if necessary or enlarge the domains of the variables.";
+                    }
+                    
+                    setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), newVariableValue);
                 }
                 return newState;
             }

src/parser/prismparser/BooleanExpressionGrammar.cpp

@@ -22,7 +22,7 @@ namespace storm {
                 notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
                 notExpression.name("boolean expression");
                 
-                atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
+                atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | this->state->constantBooleanFormulas_ | this->state->booleanFormulas_ | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
                 atomicBooleanExpression.name("boolean expression");
                 
                 relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];

src/parser/prismparser/ConstBooleanExpressionGrammar.cpp

@@ -21,7 +21,7 @@ namespace prism {
 		constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
 		constantNotExpression.name("constant boolean expression");
 
-		constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
+		constantAtomicBooleanExpression %= (constantRelativeExpression | this->state->constantBooleanFormulas_ | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
 		constantAtomicBooleanExpression.name("constant boolean expression");
 
 		constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];

src/parser/prismparser/ConstDoubleExpressionGrammar.cpp

@@ -18,7 +18,7 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<Varia
 			[qi::_val = phoenix::bind(&BaseGrammar::createDoubleMult, this, qi::_val, qi::_a, qi::_1)];
 	constantDoubleMultExpression.name("constant double expression");
 
-	constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
+	constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | this->state->constantDoubleFormulas_ | this->state->constantIntegerFormulas_ | doubleConstantExpression);
 	constantAtomicDoubleExpression.name("constant double expression");
 
 	doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression);

src/parser/prismparser/ConstIntegerExpressionGrammar.cpp

@@ -19,7 +19,7 @@ namespace storm {
                 [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
                 constantIntegerMultExpression.name("constant integer expression");
                 
-                constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
+                constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | this->state->constantIntegerFormulas_ | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
                 constantAtomicIntegerExpression.name("constant integer expression");
                 
                 constantIntegerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(",") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)];

src/parser/prismparser/IntegerExpressionGrammar.cpp

@@ -19,7 +19,7 @@ namespace storm {
                 integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
                 integerMultExpression.name("integer expression");
                 
-                atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state));
+                atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | this->state->constantIntegerFormulas_ | this->state->integerFormulas_ | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state));
                 atomicIntegerExpression.name("integer expression");
                 
                 integerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(",") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)];

src/parser/prismparser/PrismGrammar.cpp

@@ -242,12 +242,28 @@ namespace storm {
                 constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
                 constantDefinitionList.name("constant declaration list");
                 
+                constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)];
+                constantBooleanFormulaDefinition.name("constant boolean formula definition");
+                booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)];
+                booleanFormulaDefinition.name("boolean formula definition");
+                constantIntegerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantIntegerFormulas_.add, qi::_1, qi::_2)];
+                constantIntegerFormulaDefinition.name("constant integer formula definition");
+                integerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> IntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerFormulas_.add, qi::_1, qi::_2)];
+                integerFormulaDefinition.name("integer formula definition");
+                constantDoubleFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantDoubleFormulas_.add, qi::_1, qi::_2)];
+                constantDoubleFormulaDefinition.name("constant double formula definition");
+                formulaDefinition = constantBooleanFormulaDefinition | booleanFormulaDefinition | constantIntegerFormulaDefinition | integerFormulaDefinition | constantDoubleFormulaDefinition;
+                formulaDefinition.name("formula definition");
+                formulaDefinitionList = *formulaDefinition;
+                formulaDefinitionList.name("formula definition list");
+
                 // This block defines all entities that are needed for parsing a program.
                 modelTypeDefinition = modelType_;
                 modelTypeDefinition.name("model type");
                 start = (qi::eps >
                          modelTypeDefinition >
                          constantDefinitionList(qi::_a, qi::_b, qi::_c) >
+                         formulaDefinitionList >
                          globalVariableDefinitionList(qi::_d) >
                          moduleDefinitionList >
                          rewardDefinitionList(qi::_e) >

src/parser/prismparser/PrismGrammar.h

@@ -139,6 +139,15 @@ namespace storm {
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
                 
+                // Rules for formula definitions.
+                qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinitionList;
+                qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinition;
+                qi::rule<Iterator, qi::unused_type(), Skipper> constantIntegerFormulaDefinition;
+                qi::rule<Iterator, qi::unused_type(), Skipper> integerFormulaDefinition;
+                qi::rule<Iterator, qi::unused_type(), Skipper> constantDoubleFormulaDefinition;
+                qi::rule<Iterator, qi::unused_type(), Skipper> constantBooleanFormulaDefinition;
+                qi::rule<Iterator, qi::unused_type(), Skipper> booleanFormulaDefinition;
+
                 // Rules for variable recognition.
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;

src/parser/prismparser/VariableState.cpp

@@ -149,11 +149,18 @@ namespace storm {
             }
             
             bool VariableState::isFreeIdentifier(std::string const& identifier) const {
+            	if (this->booleanVariableNames_.find(identifier) != nullptr) return false;
                 if (this->integerVariableNames_.find(identifier) != nullptr) return false;
                 if (this->allConstantNames_.find(identifier) != nullptr) return false;
                 if (this->labelNames_.find(identifier) != nullptr) return false;
                 if (this->moduleNames_.find(identifier) != nullptr) return false;
                 if (this->keywords.find(identifier) != nullptr) return false;
+                if (this->booleanFormulas_.find(identifier) != nullptr) return false;
+                if (this->integerFormulas_.find(identifier) != nullptr) return false;
+                if (this->doubleFormulas_.find(identifier) != nullptr) return false;
+                if (this->constantBooleanFormulas_.find(identifier) != nullptr) return false;
+                if (this->constantIntegerFormulas_.find(identifier) != nullptr) return false;
+                if (this->constantDoubleFormulas_.find(identifier) != nullptr) return false;
                 return true;
             }
             

src/parser/prismparser/VariableState.h

@@ -124,7 +124,7 @@ namespace storm {
                 // Structures mapping variable and constant names to the corresponding expression nodes of
                 // the intermediate representation.
                 struct qi::symbols<char, std::shared_ptr<VariableExpression>> integerVariables_, booleanVariables_;
-                struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
+                struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_, booleanFormulas_, constantBooleanFormulas_, integerFormulas_, constantIntegerFormulas_, doubleFormulas_, constantDoubleFormulas_;
                 
                 // A structure representing the identity function over identifier names.
                 struct variableNamesStruct : qi::symbols<char, std::string> { }

src/utility/IRUtility.h

@@ -272,6 +272,12 @@ namespace storm {
                 // List of all integer variables.
                 std::vector<storm::ir::IntegerVariable> integerVariables;
                 
+                // List of all lower bounds for integer variables.
+                std::vector<int_fast64_t> lowerBounds;
+                
+                // List of all upper bounds for integer variables.
+                std::vector<int_fast64_t> upperBounds;
+                
                 // A mapping of integer variable names to their indices.
                 std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
             };
@@ -299,6 +305,8 @@ namespace storm {
                 // Resize the variable vectors appropriately.
                 result.booleanVariables.resize(numberOfBooleanVariables);
                 result.integerVariables.resize(numberOfIntegerVariables);
+                result.lowerBounds.resize(numberOfIntegerVariables);
+                result.upperBounds.resize(numberOfIntegerVariables);
                 
                 // Create variables.
                 for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) {
@@ -310,6 +318,8 @@ namespace storm {
                     storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i);
                     result.integerVariables[var.getGlobalIndex()] = var;
                     result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
+                    result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr);
+                    result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr);
                 }
                 for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
                     storm::ir::Module const& module = program.getModule(i);
@@ -323,6 +333,8 @@ namespace storm {
                         storm::ir::IntegerVariable const& var = module.getIntegerVariable(j);
                         result.integerVariables[var.getGlobalIndex()] = var;
                         result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
+                        result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr);
+                        result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr);
                     }
                 }