diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index fec849628..a476e2fd9 100644 --- a/src/storage/prism/Command.cpp +++ b/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 { diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index bc40cbd78..e6adf07b1 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -161,7 +161,10 @@ namespace storm { std::vector 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());