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

moved deletion of commands (if guard becomes false) from Program::substitute to Program::simplify 

Former-commit-id: ec5b4d4a57
tempestpy_adaptions
dehnert 8 years ago
parent
3ea11188b7
commit
bcb13a4fe1
3 changed files with 61 additions and 71 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. 5
      src/storage/prism/Module.cpp
  2. 119
      src/storage/prism/Program.cpp
  3. 8
      src/storage/prism/Program.h

5
src/storage/prism/Module.cpp
View File

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

119
src/storage/prism/Program.cpp
View File

@ -717,7 +717,7 @@ namespace storm {
}
Program Program::substituteConstants() const {
// We start by creating the appropriate substitution
// We start by creating the appropriate substitution.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
std::vector<Constant> newConstants(this->getConstants());
for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) {
@ -734,12 +734,6 @@ namespace storm {
}
}
// As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
// maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
// commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
// remove the forced synchronization that was there before.
std::set<uint_fast64_t> actionIndicesToDelete;
// Now we can substitute the constants in all expressions appearing in the program.
std::vector<BooleanVariable> newBooleanVariables;
newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
@ -763,9 +757,6 @@ namespace storm {
newModules.reserve(this->getNumberOfModules());
for (auto const& module : this->getModules()) {
newModules.emplace_back(module.substitute(constantSubstitution));
// Determine the set of action indices that have been deleted entirely.
std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
}
std::vector<RewardModel> newRewardModels;
@ -782,37 +773,7 @@ namespace storm {
newLabels.emplace_back(label.substitute(constantSubstitution));
}
// If we have to delete whole actions, do so now.
std::map<std::string, uint_fast64_t> newActionToIndexMap;
if (!actionIndicesToDelete.empty()) {
boost::container::flat_set<uint_fast64_t> actionsToKeep;
std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
// Insert the silent action as this is not contained in the synchronizing action indices.
actionsToKeep.insert(0);
std::vector<Module> cleanedModules;
cleanedModules.reserve(this->getNumberOfModules());
for (auto const& module : newModules) {
cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
}
newModules = std::move(cleanedModules);
std::vector<RewardModel> cleanedRewardModels;
cleanedRewardModels.reserve(this->getNumberOfRewardModels());
for (auto const& rewardModel : newRewardModels) {
cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
}
newRewardModels = std::move(cleanedRewardModels);
for (auto const& entry : this->getActionNameToIndexMapping()) {
if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
newActionToIndexMap.emplace(entry.first, entry.second);
}
}
}
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@ -1195,13 +1156,22 @@ namespace storm {
// Start by substituting the constants, because this will potentially erase some commands or even actions.
Program substitutedProgram = this->substituteConstants();
// As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
// maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
// commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
// remove the forced synchronization that was there before.
std::set<uint_fast64_t> actionIndicesToDelete;
std::vector<Module> newModules;
std::vector<Constant> newConstants = substitutedProgram.getConstants();
for (auto const& module : substitutedProgram.getModules()) {
// Remove identity assignments from the updates.
// Discard all commands with a guard equivalent to false and remove identity assignments from the updates.
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
if (!command.getGuardExpression().isFalse()) {
newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
}
}
// Substitute variables by global constants if possible.
@ -1214,38 +1184,44 @@ namespace storm {
integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
// Collect all variables that are being written. These variables cannot be turned to constants.
for (auto const& command : newCommands) {
// Check all updates.
for (auto const& update : command.getUpdates()) {
// Check all assignments.
for (auto const& assignment : update.getAssignments()) {
auto bit = booleanVars.find(assignment.getVariable());
if (bit != booleanVars.end()) {
booleanVars.erase(bit);
if (assignment.getVariable().getType().isBooleanType()) {
auto it = booleanVars.find(assignment.getVariable());
if (it != booleanVars.end()) {
booleanVars.erase(it);
}
} else {
auto iit = integerVars.find(assignment.getVariable());
if (iit != integerVars.end()) {
integerVars.erase(iit);
auto it = integerVars.find(assignment.getVariable());
if (it != integerVars.end()) {
integerVars.erase(it);
}
}
}
}
}
std::vector<storm::prism::BooleanVariable> newBVars;
std::vector<storm::prism::BooleanVariable> newBooleanVars;
for (auto const& variable : module.getBooleanVariables()) {
if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
newBVars.push_back(variable);
newBooleanVars.push_back(variable);
}
}
std::vector<storm::prism::IntegerVariable> newIVars;
std::vector<storm::prism::IntegerVariable> newIntegerVars;
for (auto const& variable : module.getIntegerVariables()) {
if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
newIVars.push_back(variable);
newIntegerVars.push_back(variable);
}
}
newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands);
// Determine the set of action indices that have been deleted entirely.
std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
for (auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
@ -1256,11 +1232,36 @@ namespace storm {
}
}
return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants);
}
Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
// If we have to delete whole actions, do so now.
std::map<std::string, uint_fast64_t> newActionToIndexMap;
std::vector<RewardModel> newRewardModels;
if (!actionIndicesToDelete.empty()) {
boost::container::flat_set<uint_fast64_t> actionsToKeep;
std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
// Insert the silent action as this is not contained in the synchronizing action indices.
actionsToKeep.insert(0);
std::vector<Module> cleanedModules;
cleanedModules.reserve(newModules.size());
for (auto const& module : newModules) {
cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
}
newModules = std::move(cleanedModules);
newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels());
for (auto const& rewardModel : substitutedProgram.getRewardModels()) {
newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
}
for (auto const& entry : this->getActionNameToIndexMapping()) {
if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
newActionToIndexMap.emplace(entry.first, entry.second);
}
}
}
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
}
Program Program::flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {

8
src/storage/prism/Program.h
View File

@ -661,14 +661,6 @@ namespace storm {
// A mapping from variable names to the modules in which they were declared.
std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
/**
* Takes the current program and replaces all modules. As we reuse the expression manager, we recommend to not use the original program any further.
* @param newModules the modules which replace the old modules.
* @param newConstants the constants which replace the old constants.
* @return A program with the new modules and constants.
*/
Program replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants);
};
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);

Write Preview
Loading…
Cancel
Save