From e6d9c85749964659472384a2fe5d40ddaf26de01 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 19:33:40 +0200
Subject: [PATCH] fixed some bugs related to simplifaction of PRISM programs
Former-commit-id: 3c81bcac8d34b9a88180a0542c7b1e1f305848b3
---
src/generator/JaniNextStateGenerator.cpp | 3 +
src/generator/PrismNextStateGenerator.cpp | 9 ++-
src/parser/PrismParser.cpp | 2 +
src/storage/prism/Module.h | 1 -
src/storage/prism/Program.cpp | 72 ++++++++++++++++++-----
src/storage/prism/RewardModel.cpp | 18 ++++++
src/storage/prism/RewardModel.h | 9 +++
src/utility/storm.cpp | 2 +-
8 files changed, 95 insertions(+), 21 deletions(-)
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index cfb08fb79..0b2fad41a 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -161,6 +161,9 @@ namespace storm {
}
// Block the current initial state to search for the next one.
+ if (!blockingExpression.isInitialized()) {
+ break;
+ }
solver->add(blockingExpression);
}
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index c0026a98d..7eb2291c5 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -23,8 +23,9 @@ namespace storm {
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels() {
+ STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program);
STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
-
+
// Only after checking validity of the program, we initialize the variable information.
this->checkValid(program);
this->variableInformation = VariableInformation(program);
@@ -166,6 +167,9 @@ namespace storm {
initialStateIndices.push_back(id);
// Block the current initial state to search for the next one.
+ if (!blockingExpression.isInitialized()) {
+ break;
+ }
solver->add(blockingExpression);
}
@@ -314,7 +318,7 @@ namespace storm {
template<typename ValueType, typename StateType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
-
+
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
@@ -445,7 +449,6 @@ namespace storm {
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::prism::Command const& command = *iteratorList[i];
-
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
storm::prism::Update const& update = command.getUpdate(j);
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 7d54f18c6..f9f4350b9 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -65,6 +65,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
}
+ STORM_LOG_TRACE("Parsed PRISM input: " << result);
+
return result;
}
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 620432580..df8a61c21 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -104,7 +104,6 @@ namespace storm {
*/
std::set<storm::expressions::Variable> getAllExpressionVariables() const;
-
/*!
* Retrieves a list of expressions that characterize the legal ranges of all variables declared by this
* module.
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 4962157eb..acb17a17e 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -734,6 +734,12 @@ 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());
@@ -757,6 +763,9 @@ 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;
@@ -773,7 +782,37 @@ namespace storm {
newLabels.emplace_back(label.substitute(constantSubstitution));
}
- return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
+ // 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());
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1153,17 +1192,19 @@ namespace storm {
}
Program Program::simplify() {
+ // Start by substituting the constants, because this will potentially erase some commands or even actions.
+ Program substitutedProgram = this->substituteConstants();
+
std::vector<Module> newModules;
- std::vector<Constant> newConstants = this->getConstants();
- for (auto const& module : this->getModules()) {
- // Remove identity assignments from the updates
+ std::vector<Constant> newConstants = substitutedProgram.getConstants();
+ for (auto const& module : substitutedProgram.getModules()) {
+ // Remove identity assignments from the updates.
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
}
- // Substitute Variables by Global constants if possible.
-
+ // Substitute variables by global constants if possible.
std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
for (auto const& variable : module.getBooleanVariables()) {
@@ -1179,11 +1220,11 @@ namespace storm {
// Check all assignments.
for (auto const& assignment : update.getAssignments()) {
auto bit = booleanVars.find(assignment.getVariable());
- if(bit != booleanVars.end()) {
+ if (bit != booleanVars.end()) {
booleanVars.erase(bit);
} else {
auto iit = integerVars.find(assignment.getVariable());
- if(iit != integerVars.end()) {
+ if (iit != integerVars.end()) {
integerVars.erase(iit);
}
}
@@ -1192,31 +1233,30 @@ namespace storm {
}
std::vector<storm::prism::BooleanVariable> newBVars;
- for(auto const& variable : module.getBooleanVariables()) {
- if(booleanVars.count(variable.getExpressionVariable()) == 0) {
+ for (auto const& variable : module.getBooleanVariables()) {
+ if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
newBVars.push_back(variable);
}
}
std::vector<storm::prism::IntegerVariable> newIVars;
- for(auto const& variable : module.getIntegerVariables()) {
- if(integerVars.count(variable.getExpressionVariable()) == 0) {
+ for (auto const& variable : module.getIntegerVariables()) {
+ if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
newIVars.push_back(variable);
}
}
newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
- for(auto const& entry : booleanVars) {
+ for (auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
}
- for(auto const& entry : integerVars) {
+ for (auto const& entry : integerVars) {
newConstants.emplace_back(entry.first, entry.second);
}
}
- return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants();
-
+ return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants);
}
Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 30c43728c..52ef5dc67 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -81,6 +81,24 @@ namespace storm {
return true;
}
+ RewardModel RewardModel::restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const {
+ std::vector<StateActionReward> newStateActionRewards;
+ for (auto const& stateActionReward : this->getStateActionRewards()) {
+ if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+ newStateActionRewards.emplace_back(stateActionReward);
+ }
+ }
+
+ std::vector<TransitionReward> newTransitionRewards;
+ for (auto const& transitionReward : this->getTransitionRewards()) {
+ if (actionIndicesToKeep.find(transitionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+ newTransitionRewards.emplace_back(transitionReward);
+ }
+ }
+
+ return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
+ }
+
std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
stream << "rewards";
if (rewardModel.getName() != "") {
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index c62aff61a..01ab69508 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -4,6 +4,7 @@
#include <string>
#include <vector>
#include <map>
+#include <boost/container/flat_set.hpp>
#include "src/storage/prism/StateReward.h"
#include "src/storage/prism/StateActionReward.h"
@@ -108,6 +109,14 @@ namespace storm {
*/
bool containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+ /*!
+ * Restricts all action-related rewards of the reward model to the ones with an action index in the provided set.
+ *
+ * @param actionIndicesToKeep The set of action indices to keep.
+ * @return The resulting reward model.
+ */
+ RewardModel restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const;
+
friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
private:
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index 5956e72c9..c6d2f9c65 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -10,7 +10,7 @@
namespace storm {
storm::prism::Program parseProgram(std::string const& path) {
- storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify();
+ storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify();
program.checkValidity();
return program;
}