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. *