Browse Source

Simplification of program when substituting constants.

Former-commit-id: d5ecb355f8
tempestpy_adaptions
dehnert 10 years ago
parent
commit
8bc646ccb8
  1. 2
      src/storage/prism/Command.cpp
  2. 5
      src/storage/prism/Module.cpp

2
src/storage/prism/Command.cpp

@ -41,7 +41,7 @@ namespace storm {
newUpdates.emplace_back(update.substitute(substitution));
}
return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
}
bool Command::isLabeled() const {

5
src/storage/prism/Module.cpp

@ -161,7 +161,10 @@ namespace storm {
std::vector<Command> newCommands;
newCommands.reserve(this->getNumberOfCommands());
for (auto const& command : this->getCommands()) {
newCommands.emplace_back(command.substitute(substitution));
Command newCommand = command.substitute(substitution);
if (!newCommand.getGuardExpression().isFalse()) {
newCommands.emplace_back(newCommand);
}
}
return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());

Loading…
Cancel
Save