diff --git a/CHANGELOG.md b/CHANGELOG.md index 65e10cd4b..8ffc256d4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,4 @@ + Changelog ============== @@ -8,6 +9,7 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- ## Version 1.6.4 (20xx/xx) +- Added support for PRISM models that use unbounded integer variables. - Added an export of check results to json. Use `--exportresult` in the command line interface. - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface. - Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now. diff --git a/resources/examples/testfiles/mdp/unbounded.nm b/resources/examples/testfiles/mdp/unbounded.nm new file mode 100644 index 000000000..235caa982 --- /dev/null +++ b/resources/examples/testfiles/mdp/unbounded.nm @@ -0,0 +1,8 @@ +mdp +const int N; +module main + x : int; + [] x<=0 -> (x'=x+1); + [] x>0 -> (x'=N*x); +endmodule + diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 609bd8d50..6459be5d1 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -423,13 +423,11 @@ namespace storm { // Then add the constraints for bounds of the integer variables. for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } for (auto const& module : program.getModules()) { for (auto const& integerVariable : module.getIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } } } else { diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 36a01f05f..771578f17 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -151,7 +151,13 @@ namespace storm { booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - integerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition.name("bounded integer variable definition"); + + unboundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("int")) > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, storm::expressions::Expression(), storm::expressions::Expression(), qi::_a)]; + unboundedIntegerVariableDefinition.name("unbounded integer variable definition"); + + integerVariableDefinition = boundedIntegerVariableDefinition | unboundedIntegerVariableDefinition; integerVariableDefinition.name("integer variable definition"); clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)]; diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 2a1d5beeb..0554d088f 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -240,8 +240,6 @@ namespace storm { // Rules for global variable definitions. qi::rule globalVariableDefinition; - qi::rule globalBooleanVariableDefinition; - qi::rule globalIntegerVariableDefinition; // Rules for modules definition. qi::rule knownModuleName; @@ -254,6 +252,8 @@ namespace storm { qi::rule&, std::vector&, std::vector&), Skipper> variableDefinition; qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; + qi::rule, Skipper> boundedIntegerVariableDefinition; + qi::rule, Skipper> unboundedIntegerVariableDefinition; qi::rule, Skipper> clockVariableDefinition; // Rules for command definitions. diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 79c7fb8a3..6a879d9ba 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -541,7 +541,7 @@ namespace storm { template bool DdPrismModelBuilder::canHandle(storm::prism::Program const& program) { - return program.getModelType() != storm::prism::Program::ModelType::PTA; + return !program.hasUnboundedVariables() && (program.getModelType() != storm::prism::Program::ModelType::PTA); } template @@ -1311,6 +1311,7 @@ namespace storm { stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); } + STORM_LOG_THROW(!program.hasUnboundedVariables(), storm::exceptions::InvalidArgumentException, "Program contains unbounded variables which is not supported by the DD engine."); STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index ead36e763..5bad7e1ba 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -33,7 +33,7 @@ namespace storm { // Only after checking validity of the program, we initialize the variable information. this->checkValid(); - this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet()); + this->variableInformation = VariableInformation(program, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet()); // Create a proper evalator. this->evaluator = std::make_unique>(program.getManager()); diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 91dcf30ee..7fc2c3403 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -34,7 +34,47 @@ namespace storm { // Intentionally left empty. } - VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { + /*! + * Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range + * @pre If has[Lower,Upper]Bound is true, [lower,upper]Bound must be set to the corresponding bound. + * @post lowerBound and upperBound are set to the considered bound for this variable + * @param hasLowerBound shall be true iff there is a lower bound given + * @param lowerBound a reference to the lower bound value + * @param hasUpperBound shall be true iff there is an upper bound given + * @param upperBound a reference to the upper bound + * @param reservedBitsForUnboundedVariables the number of bits that shall be used to represent unbounded variables + * @return the number of bits required to represent the final variable range + */ + uint64_t getBitWidthLowerUpperBound(bool const& hasLowerBound, int64_t& lowerBound, bool const& hasUpperBound, int64_t& upperBound, uint64_t const& reservedBitsForUnboundedVariables) { + if (hasLowerBound) { + if (hasUpperBound) { + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); + // We do not have to set any bounds in this case. + // Return the number of bits required to store all the values between lower and upper bound + return static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + } else { + // We only have a lower bound. Find the largest upper bound we can store with the given number of bits. + upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); + } + } else { + if (hasUpperBound) { + // We only have an upper bound. Find the smallest lower bound we can store with the given number of bits + lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); + } else { + // We neither have a lower nor an upper bound. Take the usual n-bit integer values for lower/upper bounds + lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); // = -2^(reservedBits-1) + upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; // = 2^(reservedBits-1) - 1 + } + } + // If we reach this point, it means that the variable is unbounded. + // Lets check for potential overflows. + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound. Has there been an integer over-/underflow?"); + // By choice of the lower/upper bound, the number of reserved bits must coincide with the bitwidth + STORM_LOG_ASSERT(reservedBitsForUnboundedVariables == static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))), "Unexpected bitwidth for unbounded variable."); + return reservedBitsForUnboundedVariables; + } + + VariableInformation::VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { outOfBoundsBit = 0; ++totalBitOffset; @@ -47,11 +87,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } for (auto const& module : program.getModules()) { @@ -60,11 +104,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : module.getIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } } @@ -81,22 +129,6 @@ namespace storm { for (auto const& automaton : model.getAutomata()) { STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); } -// -// for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { -// if (!variable.isTransient()) { -// booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true); -// ++totalBitOffset; -// } -// } -// for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { -// if (!variable.isTransient()) { -// int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); -// int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); -// uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); -// integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true); -// totalBitOffset += bitwidth; -// } -// } if (outOfBoundsState) { outOfBoundsBit = 0; @@ -181,30 +213,24 @@ namespace storm { } for (auto const& variable : variableSet.getBoundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound; - int64_t upperBound; + int64_t lowerBound, upperBound; + STORM_LOG_ASSERT(variable.hasLowerBound() || variable.hasUpperBound(), "Bounded integer variable has neither a lower nor an upper bound."); if (variable.hasLowerBound()) { lowerBound = variable.getLowerBound().evaluateAsInt(); - if (variable.hasUpperBound()) { - upperBound = variable.getUpperBound().evaluateAsInt(); - } else { - upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); - } - } else { - STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); + } + if (variable.hasUpperBound()) { upperBound = variable.getUpperBound().evaluateAsInt(); - lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); } - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + uint64_t bitwidth = getBitWidthLowerUpperBound(variable.hasLowerBound(), lowerBound, variable.hasUpperBound(), upperBound, reservedBitsForUnboundedVariables); integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, !variable.hasLowerBound() || !variable.hasUpperBound()); totalBitOffset += bitwidth; } } for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); - int64_t upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true, true); + int64_t lowerBound, upperBound; + uint64_t bitwidth = getBitWidthLowerUpperBound(false, lowerBound, false, upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, true); totalBitOffset += reservedBitsForUnboundedVariables; } } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index be97290f8..7c2586dbb 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -98,7 +98,7 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { - VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false); + VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState = false); VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState); VariableInformation() = default; diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.cpp b/src/storm/storage/jani/UnboundedIntegerVariable.cpp index a57d3acde..bbb88e307 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storm/storage/jani/UnboundedIntegerVariable.cpp @@ -19,5 +19,14 @@ namespace storm { return true; } + std::shared_ptr makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient) { + if (initValue) { + return std::make_shared(name, variable, initValue.get(), transient); + } else { + assert(!transient); + return std::make_shared(name, variable); + } + } + } } diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.h b/src/storm/storage/jani/UnboundedIntegerVariable.h index fe0649ce5..8ea5d52bd 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.h +++ b/src/storm/storage/jani/UnboundedIntegerVariable.h @@ -21,5 +21,10 @@ namespace storm { virtual bool isUnboundedIntegerVariable() const override; }; + /** + * Convenience function to call the appropriate constructor and return a shared pointer to the variable. + */ + std::shared_ptr makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient); + } } diff --git a/src/storm/storage/prism/IntegerVariable.cpp b/src/storm/storage/prism/IntegerVariable.cpp index d53ea618b..125df94d5 100644 --- a/src/storm/storage/prism/IntegerVariable.cpp +++ b/src/storm/storage/prism/IntegerVariable.cpp @@ -1,35 +1,81 @@ #include "storm/storage/prism/IntegerVariable.h" +#include "storm/storage/expressions/ExpressionManager.h" + namespace storm { namespace prism { IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, observable, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } + bool IntegerVariable::hasLowerBoundExpression() const { + return this->lowerBoundExpression.isInitialized(); + } + storm::expressions::Expression const& IntegerVariable::getLowerBoundExpression() const { + STORM_LOG_ASSERT(hasLowerBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from below."); return this->lowerBoundExpression; } + bool IntegerVariable::hasUpperBoundExpression() const { + return this->upperBoundExpression.isInitialized(); + } + storm::expressions::Expression const& IntegerVariable::getUpperBoundExpression() const { + STORM_LOG_ASSERT(hasUpperBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from above."); return this->upperBoundExpression; } storm::expressions::Expression IntegerVariable::getRangeExpression() const { - return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + if (hasLowerBoundExpression()) { + if (hasUpperBoundExpression()) { + return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + } else { + return this->getLowerBoundExpression() <= this->getExpressionVariable(); + } + } else { + if (hasUpperBoundExpression()) { + return this->getExpressionVariable() <= this->getUpperBoundExpression(); + } else { + return this->getExpressionVariable().getManager().boolean(true); + } + } } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getExpressionVariable(), + this->hasLowerBoundExpression() ? this->getLowerBoundExpression().substitute(substitution) : storm::expressions::Expression(), + this->hasUpperBoundExpression() ? this->getUpperBoundExpression().substitute(substitution) : storm::expressions::Expression(), + this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), + this->isObservable(), this->getFilename(), this->getLineNumber()); } void IntegerVariable::createMissingInitialValue() { if (!this->hasInitialValue()) { - this->setInitialValueExpression(this->getLowerBoundExpression()); + if (this->hasLowerBoundExpression()) { + this->setInitialValueExpression(this->getLowerBoundExpression()); + } else { + this->setInitialValueExpression(this->getExpressionVariable().getManager().integer(0)); + } } } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]"; + stream << variable.getName() << ": "; + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + // The syntax for the case where there is only one bound is not standardized, yet. + std::cout << "["; + if (variable.hasLowerBoundExpression()) { + std::cout << variable.getLowerBoundExpression(); + } + std::cout << ".."; + if (variable.hasUpperBoundExpression()) { + std::cout << variable.getUpperBoundExpression(); + } + std::cout << "]"; + } else { + std::cout << "int"; + } if (variable.hasInitialValue()) { stream << " init " << variable.getInitialValueExpression(); } diff --git a/src/storm/storage/prism/IntegerVariable.h b/src/storm/storage/prism/IntegerVariable.h index 67618f6eb..a4faba92a 100644 --- a/src/storm/storage/prism/IntegerVariable.h +++ b/src/storm/storage/prism/IntegerVariable.h @@ -28,23 +28,36 @@ namespace storm { * @param lineNumber The line number in which the variable is defined. */ IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + /*! + * @return true if a lower bound for this integer variable is defined + */ + bool hasLowerBoundExpression() const; /*! * Retrieves an expression defining the lower bound for this integer variable. - * + * @pre A lower bound for this integer variable is defined * @return An expression defining the lower bound for this integer variable. */ storm::expressions::Expression const& getLowerBoundExpression() const; - + + /*! + * @return true if an upper bound for this integer variable is defined + */ + bool hasUpperBoundExpression() const; + /*! * Retrieves an expression defining the upper bound for this integer variable. - * + * @pre An upper bound for this integer variable is defined * @return An expression defining the upper bound for this integer variable. */ storm::expressions::Expression const& getUpperBoundExpression() const; + /*! * Retrieves an expression characterizing the legal range of the variable. + * Only bounds that are defined will be considered in this expression. + * If neither a lower nor an upper bound is defined, this expression will be equivalent to true. * * @return An expression characterizing the legal range of the variable. */ diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 512985ded..bd2e05976 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -15,6 +15,15 @@ namespace storm { this->createMappings(); } + bool Module::hasUnboundedVariables() const { + for (auto const& integerVariable : this->integerVariables) { + if (!integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()) { + return true; + } + } + return false; + } + std::size_t Module::getNumberOfBooleanVariables() const { return this->booleanVariables.size(); } @@ -74,7 +83,9 @@ namespace storm { std::vector Module::getAllRangeExpressions() const { std::vector result; for (auto const& integerVariable : this->integerVariables) { - result.push_back(integerVariable.getRangeExpression()); + if (integerVariable.hasLowerBoundExpression() || integerVariable.hasUpperBoundExpression()) { + result.push_back(integerVariable.getRangeExpression()); + } } return result; } @@ -246,10 +257,10 @@ namespace storm { if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } } diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 138dfbe09..2f19ecec7 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -57,6 +57,11 @@ namespace storm { Module(Module&& other) = default; Module& operator=(Module&& other) = default; + /*! + * @return True iff the module contains at least one variable with infinite domain + */ + bool hasUnboundedVariables() const; + /*! * Retrieves the number of boolean variables in the module. * diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 0a892e20c..46db1067a 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -207,7 +207,21 @@ namespace storm { } return res; } - + + bool Program::hasUnboundedVariables() const { + for (auto const& globalIntegerVariable : this->globalIntegerVariables) { + if (!globalIntegerVariable.hasLowerBoundExpression() || !globalIntegerVariable.hasUpperBoundExpression()) { + return true; + } + } + for (auto const& module : modules) { + if (module.hasUnboundedVariables()) { + return true; + } + } + return false; + } + bool Program::hasUndefinedConstants() const { for (auto const& constant : this->getConstants()) { if (!constant.isDefined()) { @@ -254,10 +268,10 @@ namespace storm { return false; } } - if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } } @@ -437,7 +451,9 @@ namespace storm { std::vector Program::getAllRangeExpressions() const { std::vector result; for (auto const& globalIntegerVariable : this->globalIntegerVariables) { - result.push_back(globalIntegerVariable.getRangeExpression()); + if (globalIntegerVariable.hasLowerBoundExpression() || globalIntegerVariable.hasUpperBoundExpression()) { + result.push_back(globalIntegerVariable.getRangeExpression()); + } } for (auto const& module : modules) { @@ -1065,37 +1081,43 @@ namespace storm { } for (auto const& variable : this->getGlobalIntegerVariables()) { // Check that bound expressions of the range. - std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasLowerBoundExpression()) { + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasUpperBoundExpression()) { + std::set containedVariables = variable.getUpperBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } if (variable.hasInitialValue()) { STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present."); // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); + bool isValid = illegalVariables.empty(); if (!isValid) { std::vector illegalVariableNames; for (auto const& var : illegalVariables) { @@ -1138,38 +1160,45 @@ namespace storm { } for (auto const& variable : module.getIntegerVariables()) { // Check that bound expressions of the range. - std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasLowerBoundExpression()) { + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - - containedVariables = variable.getLowerBoundExpression().getVariables(); - illegalVariables.clear(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + + if (variable.hasUpperBoundExpression()) { + std::set containedVariables = variable.getUpperBoundExpression().getVariables(); + std::set illegalVariables; + + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } if (variable.hasInitialValue()) { STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present."); // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; illegalVariables.clear(); std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); + bool isValid = illegalVariables.empty(); if (!isValid) { std::vector illegalVariableNames; for (auto const& var : illegalVariables) { @@ -1623,8 +1652,7 @@ namespace storm { // Assert the bounds of the global variables. for (auto const& variable : this->getGlobalIntegerVariables()) { - solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); - solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + solver->add(variable.getRangeExpression()); } // Make the global variables local, such that the resulting module covers all occurring variables. Note that @@ -1642,8 +1670,7 @@ namespace storm { allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end()); for (auto const& variable : module.getIntegerVariables()) { - solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); - solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + solver->add(variable.getRangeExpression()); } if (module.hasInvariant()) { @@ -1987,14 +2014,10 @@ namespace storm { void Program::createMissingInitialValues() { for (auto& variable : globalBooleanVariables) { - if (!variable.hasInitialValue()) { - variable.setInitialValueExpression(manager->boolean(false)); - } + variable.createMissingInitialValue(); } for (auto& variable : globalIntegerVariables) { - if (!variable.hasInitialValue()) { - variable.setInitialValueExpression(variable.getLowerBoundExpression()); - } + variable.createMissingInitialValue(); } } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 496ac7bf8..49db27835 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -92,6 +92,11 @@ namespace storm { */ bool isPartiallyObservable() const; + /*! + * @return True iff the program contains at least one variable with infinite domain + */ + bool hasUnboundedVariables() const; + /*! * Retrieves whether there are undefined constants of any type in the program. * diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index f6097aaec..1baa10e59 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -129,11 +129,21 @@ namespace storm { // Add all global variables of the PRISM program to the JANI model. for (auto const& variable : program.getGlobalIntegerVariables()) { - if (variable.hasInitialValue()) { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false, + variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none, + variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newBoundedIntegerVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false); + storm::jani::UnboundedIntegerVariable const& createdVariable = janiModel.addVariable(newUnboundedIntegerVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -344,21 +354,35 @@ namespace storm { storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix)); for (auto const& variable : module.getIntegerVariables()) { - storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable()); if (findRes != variablesToMakeGlobal.end()) { bool makeVarGlobal = findRes->second; - storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newIntegerVariable) : automaton.addVariable(newIntegerVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false, + variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none, + variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none); + storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBoundedIntegerVariable) : automaton.addVariable(newBoundedIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else { + storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false); + storm::jani::UnboundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newUnboundedIntegerVariable) : automaton.addVariable(newUnboundedIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } } else { STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used."); } } for (auto const& variable : module.getBooleanVariables()) { - storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable()); if (findRes != variablesToMakeGlobal.end()) { bool makeVarGlobal = findRes->second; + storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); storm::jani::BooleanVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBooleanVariable) : automaton.addVariable(newBooleanVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index fef10b9a3..b64e2d277 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -319,3 +319,14 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(21ul, mdp->getNumberOfChoices()); } +TEST(UnboundedTest_Sylvan, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} + +TEST(UnboundedTest_Cudd, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} \ No newline at end of file diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index f654d28f1..d7d324112 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -94,6 +94,12 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) { model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); + + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + program = modelDescription.preprocess("N=-7").asPrismProgram(); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(9ul, model->getNumberOfStates()); + EXPECT_EQ(9ul, model->getNumberOfTransitions()); } TEST(ExplicitPrismModelBuilderTest, Ma) { @@ -125,3 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, FailComposition) { STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); } + +TEST(ExplicitPrismModelBuilderTest, FailUnbounded) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=7").asPrismProgram(); + STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); +} diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 9caba734f..ad509af46 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -28,6 +28,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); testInput = R"(mdp @@ -44,6 +45,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); } TEST(PrismParser, ComplexTest) { @@ -97,8 +99,23 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(3ul, result.getNumberOfModules()); EXPECT_EQ(2ul, result.getNumberOfRewardModels()); EXPECT_EQ(1ul, result.getNumberOfLabels()); + EXPECT_FALSE(result.hasUnboundedVariables()); } +TEST(PrismParser, UnboundedTest) { + std::string testInput = + R"(mdp + module main + b : int; + [a] true -> 1: (b'=b+1); + endmodule)"; + + storm::prism::Program result; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); + EXPECT_EQ(1ul, result.getNumberOfModules()); + EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_TRUE(result.hasUnboundedVariables()); +} TEST(PrismParser, POMDPInputTest) { std::string testInput = diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index dc3ba04b6..73f019e30 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -1,5 +1,5 @@ -#include "test/storm_gtest.h" #include "storm-config.h" +#include "test/storm_gtest.h" #include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" @@ -163,4 +163,7 @@ TEST(PrismProgramTest, ConvertToJani) { ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm")); ASSERT_NO_THROW(janiModel = prismProgram.toJani()); + + ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm")); + ASSERT_NO_THROW(janiModel = prismProgram.toJani()); }