sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

prism/Program: Integer variables can now have no lower and/or upper bound.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
aa5bb9cb7d
commit
5c2b9c503c
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
6 changed files with 168 additions and 65 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 54
      src/storm/storage/prism/IntegerVariable.cpp
  2. 19
      src/storm/storage/prism/IntegerVariable.h
  3. 17
      src/storm/storage/prism/Module.cpp
  4. 5
      src/storm/storage/prism/Module.h
  5. 133
      src/storm/storage/prism/Program.cpp
  6. 5
      src/storm/storage/prism/Program.h

54
src/storm/storage/prism/IntegerVariable.cpp
View File

@ -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<storm::expressions::Variable, storm::expressions::Expression> 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();
}

19
src/storm/storage/prism/IntegerVariable.h
View File

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

17
src/storm/storage/prism/Module.cpp
View File

@ -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<storm::expressions::Expression> Module::getAllRangeExpressions() const {
std::vector<storm::expressions::Expression> 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;
}
}

5
src/storm/storage/prism/Module.h
View File

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

133
src/storm/storage/prism/Program.cpp
View File

@ -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<storm::expressions::Expression> Program::getAllRangeExpressions() const {
std::vector<storm::expressions::Expression> 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<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasLowerBoundExpression()) {
std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasUpperBoundExpression()) {
std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasLowerBoundExpression()) {
std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasUpperBoundExpression()) {
std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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();
}
}

5
src/storm/storage/prism/Program.h
View File

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

Write Preview
Loading…
Cancel
Save