Browse Source

bugfix for PRISM program: only check initial values of variables if they have one

Former-commit-id: c5c548bd62 [formerly c27c72bd59]
Former-commit-id: 97acb66693
main
dehnert 8 years ago
parent
commit
ba0d81ca52
  1. 4
      src/storage/prism/Module.cpp

4
src/storage/prism/Module.cpp

@ -196,12 +196,12 @@ namespace storm {
bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
for (auto const& booleanVariable : this->getBooleanVariables()) {
if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& integerVariable : this->getIntegerVariables()) {
if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {

Loading…
Cancel
Save