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

Added set class with an underlying vector container. Adapted code in counterexample generators to use the new set class. Still bugs in it though. 

Former-commit-id: ac9993eab2
tempestpy_adaptions
dehnert 11 years ago
parent
58fa1a46a0
commit
422da8f481
20 changed files with 380 additions and 146 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. 12
      src/adapters/ExplicitModelAdapter.h
  2. 20
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  3. 128
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  4. 4
      src/ir/Module.cpp
  5. 3
      src/ir/Module.h
  6. 2
      src/ir/Program.cpp
  7. 3
      src/ir/Program.h
  8. 6
      src/models/AbstractDeterministicModel.h
  9. 19
      src/models/AbstractModel.h
  10. 6
      src/models/AbstractNondeterministicModel.h
  11. 4
      src/models/Ctmc.h
  12. 7
      src/models/Ctmdp.h
  13. 4
      src/models/Dtmc.h
  14. 14
      src/models/Mdp.h
  15. 4
      src/parser/DeterministicModelParser.cpp
  16. 4
      src/parser/NondeterministicModelParser.cpp
  17. 18
      src/storage/LabeledValues.h
  18. 225
      src/storage/VectorSet.h
  19. 10
      src/utility/IRUtility.h
  20. 33
      src/utility/counterexamples.h

12
src/adapters/ExplicitModelAdapter.h
View File

@ -77,7 +77,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> transitionRewardMatrix;
// A vector that stores a labeling for each choice.
std::vector<std::set<uint_fast64_t>> choiceLabeling;
std::vector<storm::storage::VectorSet<uint_fast64_t>> choiceLabeling;
};
/*!
@ -344,7 +344,7 @@ namespace storm {
double updateProbability = update.getLikelihoodExpression()->getValueAsDouble(currentState);
for (auto const& valueLabelSetPair : stateProbabilityPair.second) {
// Copy the label set, so we can modify it.
std::set<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
storm::storage::VectorSet<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
newLabelSet.insert(update.getGlobalIndex());
newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet);
@ -448,9 +448,9 @@ namespace storm {
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
static std::pair<std::vector<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector<storm::ir::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::SparseMatrix<ValueType>& transitionRewardMatrix) {
static std::pair<std::vector<uint_fast64_t>, std::vector<storm::storage::VectorSet<uint_fast64_t>>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector<storm::ir::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::SparseMatrix<ValueType>& transitionRewardMatrix) {
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
std::vector<std::set<uint_fast64_t>> choiceLabels;
std::vector<storm::storage::VectorSet<uint_fast64_t>> choiceLabels;
// Initialize a queue and insert the initial state.
std::queue<uint_fast64_t> stateQueue;
@ -488,7 +488,7 @@ namespace storm {
if (deterministicModel) {
Choice<ValueType> globalChoice("");
std::map<uint_fast64_t, ValueType> stateToRewardMap;
std::set<uint_fast64_t> allChoiceLabels;
storm::storage::VectorSet<uint_fast64_t> allChoiceLabels;
// Combine all the choices and scale them with the total number of choices of the current state.
for (auto const& choice : allUnlabeledChoices) {
@ -637,7 +637,7 @@ namespace storm {
bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC;
// Build the transition and reward matrices.
std::pair<std::vector<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix);
std::pair<std::vector<uint_fast64_t>, std::vector<storm::storage::VectorSet<uint_fast64_t>>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix);
modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first);
modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second);

20
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -66,8 +66,8 @@ namespace storm {
struct ChoiceInformation {
std::unordered_map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
std::unordered_map<uint_fast64_t, std::list<uint_fast64_t>> problematicChoicesForProblematicStates;
std::set<uint_fast64_t> allRelevantLabels;
std::set<uint_fast64_t> knownLabels;
storm::storage::VectorSet<uint_fast64_t> allRelevantLabels;
storm::storage::VectorSet<uint_fast64_t> knownLabels;
};
/*!
@ -126,7 +126,7 @@ namespace storm {
ChoiceInformation result;
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
// Now traverse all choices of all relevant states and check whether there is a relevant target state.
// If so, the associated labels become relevant. Also, if a choice of relevant state has at least one
@ -296,7 +296,7 @@ namespace storm {
* variables, this value is increased.
* @return A mapping from labels to variable indices.
*/
static std::unordered_map<uint_fast64_t, uint_fast64_t> createLabelVariables(GRBenv* env, GRBmodel* model, std::set<uint_fast64_t> const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) {
static std::unordered_map<uint_fast64_t, uint_fast64_t> createLabelVariables(GRBenv* env, GRBmodel* model, storm::storage::VectorSet<uint_fast64_t> const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) {
int error = 0;
std::stringstream variableNameBuffer;
std::unordered_map<uint_fast64_t, uint_fast64_t> resultingMap;
@ -671,7 +671,7 @@ namespace storm {
static uint_fast64_t assertChoicesImplyLabels(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
int error = 0;
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
for (auto state : stateInformation.relevantStates) {
std::list<uint_fast64_t>::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin();
for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) {
@ -1147,12 +1147,12 @@ namespace storm {
* @param model The Gurobi model.
* @param variableInformation A struct with information about the variables of the model.
*/
static std::set<uint_fast64_t> getUsedLabelsInSolution(GRBenv* env, GRBmodel* model, VariableInformation const& variableInformation) {
static storm::storage::VectorSet<uint_fast64_t> getUsedLabelsInSolution(GRBenv* env, GRBmodel* model, VariableInformation const& variableInformation) {
int error = 0;
// Check whether the model was optimized, so we can read off the solution.
if (checkGurobiModelIsOptimized(env, model)) {
std::set<uint_fast64_t> result;
storm::storage::VectorSet<uint_fast64_t> result;
double value = 0;
for (auto labelVariablePair : variableInformation.labelToVariableIndexMap) {
@ -1265,7 +1265,7 @@ namespace storm {
public:
static std::set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
static storm::storage::VectorSet<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
#ifdef STORM_HAVE_GUROBI
// (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabels()) {
@ -1311,7 +1311,7 @@ namespace storm {
optimizeModel(environmentModelPair.first, environmentModelPair.second);
// (4.5) Read off result from variables.
std::set<uint_fast64_t> usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation);
storm::storage::VectorSet<uint_fast64_t> usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation);
usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end());
// Display achieved probability.
@ -1375,7 +1375,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
std::set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true);
storm::storage::VectorSet<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true);
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

128
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -43,10 +43,10 @@ namespace storm {
storm::storage::BitVector relevantStates;
// The set of relevant labels.
std::set<uint_fast64_t> relevantLabels;
storm::storage::VectorSet<uint_fast64_t> relevantLabels;
// A set of labels that is definitely known to be taken in the final solution.
std::set<uint_fast64_t> knownLabels;
storm::storage::VectorSet<uint_fast64_t> knownLabels;
// A list of relevant choices for each relevant state.
std::map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
@ -94,7 +94,7 @@ namespace storm {
// Retrieve some references for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
// Now traverse all choices of all relevant states and check whether there is a successor target state.
// If so, the associated labels become relevant. Also, if a choice of relevant state has at least one
@ -124,8 +124,8 @@ namespace storm {
// Compute the set of labels that are known to be taken in any case.
relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, relevancyInformation.relevantLabels);
if (!relevancyInformation.knownLabels.empty()) {
std::set<uint_fast64_t> remainingLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.begin()));
storm::storage::VectorSet<uint_fast64_t> remainingLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end()));
relevancyInformation.relevantLabels = remainingLabels;
}
@ -142,7 +142,7 @@ namespace storm {
* @param relevantCommands A set of relevant labels for which to create the expressions.
* @return A mapping from relevant labels to their corresponding expressions.
*/
static VariableInformation createExpressionsForRelevantLabels(z3::context& context, std::set<uint_fast64_t> const& relevantLabels) {
static VariableInformation createExpressionsForRelevantLabels(z3::context& context, storm::storage::VectorSet<uint_fast64_t> const& relevantLabels) {
VariableInformation variableInformation;
// Create stringstream to build expression names.
@ -202,17 +202,17 @@ namespace storm {
// * identify labels that directly reach a target state
// * identify labels that can directly follow a given action
std::set<uint_fast64_t> initialLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> precedingLabels;
std::set<uint_fast64_t> targetLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> followingLabels;
std::map<uint_fast64_t, std::set<std::set<uint_fast64_t>>> synchronizingLabels;
storm::storage::VectorSet<uint_fast64_t> initialLabels;
std::map<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>> precedingLabels;
storm::storage::VectorSet<uint_fast64_t> targetLabels;
std::map<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>> followingLabels;
std::map<uint_fast64_t, std::set<storm::storage::VectorSet<uint_fast64_t>>> synchronizingLabels;
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
for (auto currentState : relevancyInformation.relevantStates) {
@ -221,7 +221,7 @@ namespace storm {
// If the choice is a synchronization choice, we need to record it.
if (choiceLabeling[currentChoice].size() > 1) {
for (auto label : choiceLabeling[currentChoice]) {
std::set<uint_fast64_t> synchSet(choiceLabeling[currentChoice]);
storm::storage::VectorSet<uint_fast64_t> synchSet(choiceLabeling[currentChoice]);
synchSet.erase(label);
synchronizingLabels[label].emplace(std::move(synchSet));
}
@ -289,10 +289,11 @@ namespace storm {
std::vector<z3::expr> formulae;
LOG4CPLUS_DEBUG(logger, "Asserting initial label is taken.");
// Start by asserting that we take at least one initial label. We may do so only if there is no initial
// label that is already known. Otherwise this condition would be too strong.
std::set<uint_fast64_t> intersection;
std::set_intersection(initialLabels.begin(), initialLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.begin()));
storm::storage::VectorSet<uint_fast64_t> intersection;
std::set_intersection(initialLabels.begin(), initialLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection,intersection.end()));
if (intersection.empty()) {
for (auto label : initialLabels) {
formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
@ -306,7 +307,7 @@ namespace storm {
LOG4CPLUS_DEBUG(logger, "Asserting target label is taken.");
// Likewise, if no target label is known, we may assert that there is at least one.
std::set_intersection(targetLabels.begin(), targetLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.begin()));
std::set_intersection(targetLabels.begin(), targetLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.end()));
if (intersection.empty()) {
for (auto label : targetLabels) {
formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
@ -321,13 +322,16 @@ namespace storm {
// Now assert that for each non-target label, we take a following label.
for (auto const& labelSetPair : followingLabels) {
formulae.clear();
if (targetLabels.find(labelSetPair.first) == targetLabels.end()) {
if (!targetLabels.contains(labelSetPair.first)) {
// Also, if there is a known label that may follow the current label, we don't need to assert
// anything here.
std::set_intersection(labelSetPair.second.begin(), labelSetPair.second.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.begin()));
std::set_intersection(labelSetPair.second.begin(), labelSetPair.second.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.end()));
if (intersection.empty()) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSetPair.first)));
if (!relevancyInformation.knownLabels.contains(labelSetPair.first)) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSetPair.first)));
}
for (auto followingLabel : labelSetPair.second) {
std::cout << "2 " << followingLabel << std::endl;
if (followingLabel != labelSetPair.first) {
formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(followingLabel)));
}
@ -347,7 +351,7 @@ namespace storm {
// the label appears in.
for (auto const& labelSynchronizingSetsPair : synchronizingLabels) {
formulae.clear();
if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) {
if (!relevancyInformation.knownLabels.contains(labelSynchronizingSetsPair.first)) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first)));
}
@ -358,7 +362,7 @@ namespace storm {
z3::expr currentCombination = context.bool_val(true);
bool allImplicantsKnownForCurrentSet = true;
for (auto label : synchronizingSet) {
if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
if (!relevancyInformation.knownLabels.contains(label)) {
currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
}
}
@ -388,11 +392,11 @@ namespace storm {
static void assertSymbolicCuts(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) {
// A container storing the label sets that may precede a given label set.
std::map<std::set<uint_fast64_t>, std::set<std::set<uint_fast64_t>>> precedingLabelSets;
std::map<storm::storage::VectorSet<uint_fast64_t>, std::set<storm::storage::VectorSet<uint_fast64_t>>> precedingLabelSets;
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
// Compute the set of labels that may precede a given action.
@ -460,7 +464,7 @@ namespace storm {
}
// Store the found implications in a container similar to the preceding label sets.
std::map<std::set<uint_fast64_t>, std::set<std::set<uint_fast64_t>>> backwardImplications;
std::map<storm::storage::VectorSet<uint_fast64_t>, std::set<storm::storage::VectorSet<uint_fast64_t>>> backwardImplications;
// Now check for possible backward cuts.
for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) {
@ -474,7 +478,7 @@ namespace storm {
storm::ir::Command const& command = module.getCommand(commandIndex);
// If the current command is one of the commands we need to consider, store a reference to it in the container.
if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) {
if (labelSetAndPrecedingLabelSetsPair.first.contains(command.getGlobalIndex())) {
currentCommandVector.push_back(command);
}
}
@ -543,7 +547,7 @@ namespace storm {
storm::ir::Command const& command = module.getCommand(commandIndex);
// If the current command is one of the commands we need to consider, store a reference to it in the container.
if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) {
if (precedingLabelSet.contains(command.getGlobalIndex())) {
currentPrecedingCommandVector.push_back(command);
}
}
@ -612,7 +616,7 @@ namespace storm {
// Create the first part of the implication.
for (auto label : labelSetImplicationsPair.first) {
if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
if (!relevancyInformation.knownLabels.contains(label)) {
implicationExpression.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
}
@ -621,7 +625,7 @@ namespace storm {
for (auto const& implicationSet : labelSetImplicationsPair.second) {
implicationExpression.push_back(context.bool_val(true));
for (auto label : implicationSet) {
if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
if (!relevancyInformation.knownLabels.contains(label)) {
implicationExpression.back() = implicationExpression.back() && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
}
}
@ -915,10 +919,10 @@ namespace storm {
* @param commandSet The command set to rule out as a solution.
* @param variableInformation A structure with information about the variables for the labels.
*/
static void ruleOutSolution(z3::context& context, z3::solver& solver, std::set<uint_fast64_t> const& commandSet, VariableInformation const& variableInformation) {
static void ruleOutSolution(z3::context& context, z3::solver& solver, storm::storage::VectorSet<uint_fast64_t> const& commandSet, VariableInformation const& variableInformation) {
z3::expr blockSolutionExpression = context.bool_val(false);
for (auto labelIndexPair : variableInformation.labelToIndexMap) {
if (commandSet.find(labelIndexPair.first) == commandSet.end()) {
if (commandSet.contains(labelIndexPair.first)) {
blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second];
}
}
@ -933,8 +937,8 @@ namespace storm {
* @param model The Z3 model from which to extract the information.
* @param variableInformation A structure with information about the variables of the solver.
*/
static std::set<uint_fast64_t> getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) {
std::set<uint_fast64_t> result;
static storm::storage::VectorSet<uint_fast64_t> getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) {
storm::storage::VectorSet<uint_fast64_t> result;
for (auto const& labelIndexPair : variableInformation.labelToIndexMap) {
z3::expr auxValue = model.eval(variableInformation.labelVariables.at(labelIndexPair.second));
@ -986,7 +990,7 @@ namespace storm {
* in order to satisfy the constraint system.
* @return The smallest set of labels such that the constraint system of the solver is satisfiable.
*/
static std::set<uint_fast64_t> findSmallestCommandSet(z3::context& context, z3::solver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) {
static storm::storage::VectorSet<uint_fast64_t> findSmallestCommandSet(z3::context& context, z3::solver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) {
// Check if we can find a solution with the current bound.
z3::expr assumption = !variableInformation.auxiliaryVariables.back();
@ -1016,7 +1020,7 @@ namespace storm {
* @param commandSet The currently chosen set of commands.
* @param variableInformation A structure with information about the variables of the solver.
*/
static void analyzeZeroProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
static void analyzeZeroProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::VectorSet<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
storm::storage::BitVector reachableStates(subMdp.getNumberOfStates());
// Initialize the stack for the DFS.
@ -1030,10 +1034,10 @@ namespace storm {
storm::storage::SparseMatrix<T> const& transitionMatrix = subMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices();
std::vector<std::set<uint_fast64_t>> const& subChoiceLabeling = subMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& subChoiceLabeling = subMdp.getChoiceLabeling();
// Now determine which states and labels are actually reachable.
std::set<uint_fast64_t> reachableLabels;
storm::storage::VectorSet<uint_fast64_t> reachableLabels;
while (!stack.empty()) {
uint_fast64_t currentState = stack.back();
stack.pop_back();
@ -1070,16 +1074,18 @@ namespace storm {
storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates;
storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp, subMdp.getBackwardTransitions(), phiStates, psiStates);
std::vector<std::set<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
std::vector<storm::storage::VectorSet<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
LOG4CPLUS_DEBUG(logger, "Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states.");
// Search for states on the border of the reachable state space, i.e. states that are still reachable
// and possess a (disabled) option to leave the reachable part of the state space.
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = originalMdp.getChoiceLabeling();
std::set<std::set<uint_fast64_t>> cutLabels;
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = originalMdp.getChoiceLabeling();
std::set<storm::storage::VectorSet<uint_fast64_t>> cutLabels;
for (auto state : reachableStates) {
bool isBorderState = false;
for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) {
if (!storm::utility::set::isSubsetOf(choiceLabeling[currentChoice], commandSet)) {
if (!choiceLabeling[currentChoice].subsetOf(commandSet)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = originalMdp.getTransitionMatrix().constColumnIteratorBegin(currentChoice), successorIte = originalMdp.getTransitionMatrix().constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (unreachableRelevantStates.get(*successorIt)) {
isBorderState = true;
@ -1087,15 +1093,13 @@ namespace storm {
}
if (isBorderState) {
std::set<uint_fast64_t> currentLabelSet;
storm::storage::VectorSet<uint_fast64_t> currentLabelSet;
for (auto label : choiceLabeling[currentChoice]) {
if (commandSet.find(label) == commandSet.end()) {
if (!commandSet.contains(label)) {
currentLabelSet.insert(label);
}
}
std::set<uint_fast64_t> notTakenImpliedChoices;
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(notTakenImpliedChoices, notTakenImpliedChoices.begin()));
currentLabelSet.insert(notTakenImpliedChoices.begin(), notTakenImpliedChoices.end());
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end()));
cutLabels.insert(currentLabelSet);
}
@ -1105,8 +1109,8 @@ namespace storm {
// Given the results of the previous analysis, we construct the implications
std::vector<z3::expr> formulae;
std::set<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.begin()));
storm::storage::VectorSet<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
for (auto label : unknownReachableLabels) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
@ -1137,7 +1141,7 @@ namespace storm {
* @param commandSet The currently chosen set of commands.
* @param variableInformation A structure with information about the variables of the solver.
*/
static void analyzeInsufficientProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
static void analyzeInsufficientProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::VectorSet<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
// ruleOutSolution(context, solver, commandSet, variableInformation);
storm::storage::BitVector reachableStates(subMdp.getNumberOfStates());
@ -1153,10 +1157,10 @@ namespace storm {
storm::storage::SparseMatrix<T> const& transitionMatrix = subMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices();
std::vector<std::set<uint_fast64_t>> const& subChoiceLabeling = subMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& subChoiceLabeling = subMdp.getChoiceLabeling();
// Now determine which states and labels are actually reachable.
std::set<uint_fast64_t> reachableLabels;
storm::storage::VectorSet<uint_fast64_t> reachableLabels;
while (!stack.empty()) {
uint_fast64_t currentState = stack.back();
stack.pop_back();
@ -1187,23 +1191,21 @@ namespace storm {
storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates;
storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp, subMdp.getBackwardTransitions(), phiStates, psiStates);
std::vector<std::set<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
std::vector<storm::storage::VectorSet<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
// Search for states for which we could enable another option and possibly improve the reachability probability.
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = originalMdp.getChoiceLabeling();
std::set<std::set<uint_fast64_t>> cutLabels;
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = originalMdp.getChoiceLabeling();
std::set<storm::storage::VectorSet<uint_fast64_t>> cutLabels;
for (auto state : reachableStates) {
for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) {
if (!storm::utility::set::isSubsetOf(choiceLabeling[currentChoice], commandSet)) {
std::set<uint_fast64_t> currentLabelSet;
if (!choiceLabeling[currentChoice].subsetOf(commandSet)) {
storm::storage::VectorSet<uint_fast64_t> currentLabelSet;
for (auto label : choiceLabeling[currentChoice]) {
if (commandSet.find(label) == commandSet.end()) {
if (!commandSet.contains(label)) {
currentLabelSet.insert(label);
}
}
std::set<uint_fast64_t> notTakenImpliedChoices;
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(notTakenImpliedChoices, notTakenImpliedChoices.begin()));
currentLabelSet.insert(notTakenImpliedChoices.begin(), notTakenImpliedChoices.end());
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end()));
cutLabels.insert(currentLabelSet);
@ -1213,8 +1215,8 @@ namespace storm {
// Given the results of the previous analysis, we construct the implications
std::vector<z3::expr> formulae;
std::set<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.begin()));
storm::storage::VectorSet<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
for (auto label : unknownReachableLabels) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
@ -1248,7 +1250,7 @@ namespace storm {
* @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check
* is made and fails, an exception is thrown.
*/
static std::set<uint_fast64_t> getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false) {
static storm::storage::VectorSet<uint_fast64_t> getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false) {
#ifdef STORM_HAVE_Z3
// Set up all clocks used for time measurement.
auto totalClock = std::chrono::high_resolution_clock::now();
@ -1320,7 +1322,7 @@ namespace storm {
// the solver.
// Set up some variables for the iterations.
std::set<uint_fast64_t> commandSet(relevancyInformation.relevantLabels);
storm::storage::VectorSet<uint_fast64_t> commandSet(relevancyInformation.relevantLabels);
bool done = false;
uint_fast64_t iterations = 0;
uint_fast64_t currentBound = 0;

4
src/ir/Module.cpp
View File

@ -186,10 +186,10 @@ namespace storm {
}
}
void Module::restrictCommands(std::set<uint_fast64_t> const& indexSet) {
void Module::restrictCommands(storm::storage::VectorSet<uint_fast64_t> const& indexSet) {
std::vector<storm::ir::Command> newCommands;
for (auto const& command : commands) {
if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) {
if (indexSet.contains(command.getGlobalIndex())) {
newCommands.push_back(std::move(command));
}
}

3
src/ir/Module.h
View File

@ -20,6 +20,7 @@
#include <vector>
#include <memory>
#include "src/storage/VectorSet.h"
#include "BooleanVariable.h"
#include "IntegerVariable.h"
#include "Command.h"
@ -186,7 +187,7 @@ namespace storm {
*
* @param indexSet The set of indices for which to keep the commands.
*/
void restrictCommands(std::set<uint_fast64_t> const& indexSet);
void restrictCommands(storm::storage::VectorSet<uint_fast64_t> const& indexSet);
private:
/*!

2
src/ir/Program.cpp
View File

@ -290,7 +290,7 @@ namespace storm {
return this->globalIntegerVariableToIndexMap.at(variableName);
}
void Program::restrictCommands(std::set<uint_fast64_t> const& indexSet) {
void Program::restrictCommands(storm::storage::VectorSet<uint_fast64_t> const& indexSet) {
for (auto& module : modules) {
module.restrictCommands(indexSet);
}

3
src/ir/Program.h
View File

@ -13,6 +13,7 @@
#include <memory>
#include <set>
#include "src/storage/VectorSet.h"
#include "expressions/BaseExpression.h"
#include "expressions/BooleanConstantExpression.h"
#include "expressions/IntegerConstantExpression.h"
@ -266,7 +267,7 @@ namespace storm {
*
* @param indexSet The set of indices for which to keep the commands.
*/
void restrictCommands(std::set<uint_fast64_t> const& indexSet);
void restrictCommands(storm::storage::VectorSet<uint_fast64_t> const& indexSet);
private:
// The type of the model.
ModelType modelType;

6
src/models/AbstractDeterministicModel.h
View File

@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
*/
AbstractDeterministicModel(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
}
@ -43,7 +43,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
*/
AbstractDeterministicModel(storm::storage::SparseMatrix<T>&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
@ -116,7 +116,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
* @return void
*/
virtual void setStateIdBasedChoiceLabeling() override {
std::vector<std::set<uint_fast64_t>> newChoiceLabeling;
std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling;
size_t stateCount = this->getNumberOfStates();
newChoiceLabeling.resize(stateCount);

19
src/models/AbstractModel.h
View File

@ -1,16 +1,17 @@
#ifndef STORM_MODELS_ABSTRACTMODEL_H_
#define STORM_MODELS_ABSTRACTMODEL_H_
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/storage/BitVector.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/Hash.h"
#include <memory>
#include <vector>
#include <boost/optional.hpp>
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/storage/BitVector.h"
#include "src/storage/SparseMatrix.h"
#include "src/storage/VectorSet.h"
#include "src/utility/Hash.h"
namespace storm {
namespace models {
@ -71,7 +72,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
*/
AbstractModel(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: transitionMatrix(transitionMatrix), stateLabeling(stateLabeling) {
if (optionalStateRewardVector) {
@ -95,7 +96,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
*/
AbstractModel(storm::storage::SparseMatrix<T>&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling) :
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling) :
transitionMatrix(std::move(transitionMatrix)), choiceLabeling(std::move(optionalChoiceLabeling)),
stateLabeling(std::move(stateLabeling)), stateRewardVector(std::move(optionalStateRewardVector)),
transitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) {
@ -359,7 +360,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* Returns the labels for the choices of the model, if there are any.
* @return The labels for the choices of the model.
*/
std::vector<std::set<uint_fast64_t>> const& getChoiceLabeling() const {
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& getChoiceLabeling() const {
return choiceLabeling.get();
}
@ -538,7 +539,7 @@ protected:
storm::storage::SparseMatrix<T> transitionMatrix;
/*! The labeling that is associated with the choices for each state. */
boost::optional<std::vector<std::set<uint_fast64_t>>> choiceLabeling;
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> choiceLabeling;
private:
/*! The labeling of the states of the model. */
storm::models::AtomicPropositionsLabeling stateLabeling;

6
src/models/AbstractNondeterministicModel.h
View File

@ -32,7 +32,7 @@ namespace storm {
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
this->nondeterministicChoiceIndices = nondeterministicChoiceIndices;
}
@ -51,7 +51,7 @@ namespace storm {
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)), nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) {
@ -221,7 +221,7 @@ namespace storm {
* @return void
*/
virtual void setStateIdBasedChoiceLabeling() override {
std::vector<std::set<uint_fast64_t>> newChoiceLabeling;
std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling;
size_t stateCount = this->getNumberOfStates();
size_t choiceCount = this->getNumberOfChoices();

4
src/models/Ctmc.h
View File

@ -37,7 +37,7 @@ public:
*/
Ctmc(storm::storage::SparseMatrix<T> const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
// Intentionally left empty.
}
@ -52,7 +52,7 @@ public:
*/
Ctmc(storm::storage::SparseMatrix<T>&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractDeterministicModel<T>(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {

7
src/models/Ctmdp.h
View File

@ -42,7 +42,7 @@ public:
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix,
optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
@ -65,10 +65,9 @@ public:
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractNondeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
: AbstractNondeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";

4
src/models/Dtmc.h
View File

@ -43,7 +43,7 @@ public:
*/
Dtmc(storm::storage::SparseMatrix<T> const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@ -69,7 +69,7 @@ public:
*/
Dtmc(storm::storage::SparseMatrix<T>&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractDeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {

14
src/models/Mdp.h
View File

@ -49,7 +49,7 @@ public:
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@ -77,7 +77,7 @@ public:
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<std::set<uint_fast64_t>>>&& optionalChoiceLabeling)
boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
@ -134,25 +134,25 @@ public:
* and which ones need to be ignored.
* @return A restricted version of the current MDP that only uses choice labels from the given set.
*/
Mdp<T> restrictChoiceLabels(std::set<uint_fast64_t> const& enabledChoiceLabels) const {
Mdp<T> restrictChoiceLabels(storm::storage::VectorSet<uint_fast64_t> const& enabledChoiceLabels) const {
// Only perform this operation if the given model has choice labels.
if (!this->hasChoiceLabels()) {
throw storm::exceptions::InvalidArgumentException() << "Restriction to label set is impossible for unlabeled model.";
}
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
storm::storage::SparseMatrix<T> transitionMatrix;
transitionMatrix.initialize();
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
std::vector<std::set<uint_fast64_t>> newChoiceLabeling;
std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling;
// Check for each choice of each state, whether the choice labels are fully contained in the given label set.
uint_fast64_t currentRow = 0;
for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
bool stateHasValidChoice = false;
for (uint_fast64_t choice = this->getNondeterministicChoiceIndices()[state]; choice < this->getNondeterministicChoiceIndices()[state + 1]; ++choice) {
bool choiceValid = storm::utility::set::isSubsetOf(choiceLabeling[choice], enabledChoiceLabels);
bool choiceValid = choiceLabeling[choice].subsetOf(enabledChoiceLabels);
// If the choice is valid, copy over all its elements.
if (choiceValid) {
@ -180,7 +180,7 @@ public:
transitionMatrix.finalize(true);
nondeterministicChoiceIndices.push_back(currentRow);
Mdp<T> restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<std::set<uint_fast64_t>>>(newChoiceLabeling));
Mdp<T> restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>(newChoiceLabeling));
return restrictedMdp;
}

4
src/parser/DeterministicModelParser.cpp
View File

@ -58,7 +58,7 @@ DeterministicModelParserResultContainer<double> parseDeterministicModel(std::str
storm::models::Dtmc<double> DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParserResultContainer<double> parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Dtmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<std::set<uint_fast64_t>>>());
return storm::models::Dtmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
}
/*!
@ -69,7 +69,7 @@ storm::models::Dtmc<double> DeterministicModelParserAsDtmc(std::string const & t
storm::models::Ctmc<double> DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParserResultContainer<double> parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Ctmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<std::set<uint_fast64_t>>>());
return storm::models::Ctmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
}
} /* namespace parser */

4
src/parser/NondeterministicModelParser.cpp
View File

@ -58,7 +58,7 @@ NondeterministicModelParserResultContainer<double> parseNondeterministicModel(st
storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<std::set<uint_fast64_t>>>());
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
}
/*!
@ -69,7 +69,7 @@ storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const &
storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<std::set<uint_fast64_t>>>());
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
}
} /* namespace parser */

18
src/storage/LabeledValues.h
View File

@ -9,7 +9,7 @@
#define STORM_STORAGE_LABELEDVALUES_H
#include <list>
#include <set>
#include "src/storage/VectorSet.h"
namespace storm {
namespace utility {
@ -45,8 +45,8 @@ namespace storm {
* @param value The value to add.
* @return A reference to the list of labels that is associated with the given value.
*/
std::set<uint_fast64_t>& addValue(ValueType value) {
valueLabelList.emplace_back(value, std::set<uint_fast64_t>());
storm::storage::VectorSet<uint_fast64_t>& addValue(ValueType value) {
valueLabelList.emplace_back(value, storm::storage::VectorSet<uint_fast64_t>());
return valueLabelList.back().second;
}
@ -57,7 +57,7 @@ namespace storm {
* @param labels The labels to associate with this value.
* @return A reference to the list of labels that is associated with the given value.
*/
std::set<uint_fast64_t>& addValue(ValueType value, std::set<uint_fast64_t> const& labels) {
storm::storage::VectorSet<uint_fast64_t>& addValue(ValueType value, storm::storage::VectorSet<uint_fast64_t> const& labels) {
valueLabelList.emplace_back(value, labels);
return valueLabelList.back().second;
}
@ -67,7 +67,7 @@ namespace storm {
*
* @return An iterator pointing to the first labeled probability.
*/
typename std::list<std::pair<ValueType, std::set<uint_fast64_t>>>::iterator begin() {
typename std::list<std::pair<ValueType, storm::storage::VectorSet<uint_fast64_t>>>::iterator begin() {
return valueLabelList.begin();
}
@ -76,7 +76,7 @@ namespace storm {
*
* @return An iterator pointing past the last labeled probability.
*/
typename std::list<std::pair<ValueType, std::set<uint_fast64_t>>>::const_iterator end() {
typename std::list<std::pair<ValueType, storm::storage::VectorSet<uint_fast64_t>>>::const_iterator end() {
return valueLabelList.end();
}
@ -85,7 +85,7 @@ namespace storm {
*
* @return A const iterator pointing to the first labeled probability.
*/
typename std::list<std::pair<ValueType, std::set<uint_fast64_t>>>::const_iterator begin() const {
typename std::list<std::pair<ValueType, storm::storage::VectorSet<uint_fast64_t>>>::const_iterator begin() const {
return valueLabelList.begin();
}
@ -94,7 +94,7 @@ namespace storm {
*
* @return A const iterator pointing past the last labeled probability.
*/
typename std::list<std::pair<ValueType, std::set<uint_fast64_t>>>::const_iterator end() const {
typename std::list<std::pair<ValueType, storm::storage::VectorSet<uint_fast64_t>>>::const_iterator end() const {
return valueLabelList.end();
}
@ -178,7 +178,7 @@ namespace storm {
private:
// The actual storage used to store the list of values and the associated labels.
std::list<std::pair<ValueType, std::set<uint_fast64_t>>> valueLabelList;
std::list<std::pair<ValueType, storm::storage::VectorSet<uint_fast64_t>>> valueLabelList;
/*!
* Returns the sum of the values.

225
src/storage/VectorSet.h
View File

@ -0,0 +1,225 @@
/*
* VectorSet.h
*
* Created on: 23.10.2013
* Author: Christian Dehnert
*/
#ifndef STORM_STORAGE_VECTORSET_H
#define STORM_STORAGE_VECTORSET_H
#include <algorithm>
#include <iostream>
namespace storm {
namespace storage {
template<typename T>
class VectorSet {
public:
typedef T* difference_type;
typedef T value_type;
typedef T* pointer;
typedef T& reference;
typedef typename std::vector<T>::iterator iterator;
typedef typename std::vector<T>::const_iterator const_iterator;
VectorSet() : data(), dirty(false) {
// Intentionally left empty.
}
VectorSet(uint_fast64_t size) : data(), dirty(false) {
data.reserve(size);
}
VectorSet(std::vector<T> const& data) : data(data), dirty(true) {
ensureSet();
}
VectorSet(std::set<T> const& data) : dirty(false) {
this->data.reserve(data.size());
for (auto const& element : data) {
this->data.push_back(element);
}
}
template<typename InputIterator>
VectorSet(InputIterator first, InputIterator last) : data(first, last), dirty(true) {
ensureSet();
}
VectorSet(VectorSet const& other) : data(other.data), dirty(other.dirty) {
// Intentionally left empty.
}
VectorSet& operator=(VectorSet const& other) {
data = other.data;
dirty = other.dirty;
return *this;
}
VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) {
// Intentionally left empty.
}
VectorSet& operator=(VectorSet&& other) {
data = std::move(other.data);
dirty = std::move(other.dirty);
return *this;
}
bool operator==(VectorSet const& other) const {
if (this->size() != other.size()) return false;
return std::equal(data.begin(), data.end(), other.begin(), other.end());
}
bool operator<(VectorSet const& other) const {
if (this->size() < other.size()) return true;
if (this->size() > other.size()) return false;
for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) {
if (*it1 < *it2) return true;
if (*it1 > *it2) return false;
}
return false;
}
void ensureSet() const {
if (dirty) {
std::sort(data.begin(), data.end());
data.erase(std::unique(data.begin(), data.end()), data.end());
dirty = false;
}
}
bool contains(T const& element) const {
ensureSet();
return std::binary_search(data.begin(), data.end(), element);
}
bool subsetOf(VectorSet const& other) const {
ensureSet();
other.ensureSet();
return std::includes(other.begin(), other.end(), data.begin(), data.end());
}
bool supersetOf(VectorSet const& other) const {
ensureSet();
return other.subsetOf(*this);
}
VectorSet intersect(VectorSet const& other) {
ensureSet();
other.ensureSet();
VectorSet result;
std::set_intersection(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end()));
return result;
}
VectorSet join(VectorSet const& other) {
ensureSet();
other.ensureSet();
VectorSet result;
std::set_union(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end()));
return result;
}
iterator begin() {
ensureSet();
return data.begin();
}
iterator end() {
ensureSet();
return data.end();
}
const_iterator begin() const {
ensureSet();
return data.begin();
}
const_iterator end() const {
ensureSet();
return data.end();
}
void insert(T const& element) {
data.push_back(element);
dirty = true;
}
template<typename InputIterator>
iterator insert(InputIterator first, InputIterator last) {
return data.insert(data.end(), first, last);
}
template<typename InputIterator>
iterator insert(InputIterator pos, T element) {
return data.insert(pos, element);
}
bool empty() const {
ensureSet();
return data.empty();
}
size_t size() const {
ensureSet();
return data.size();
}
void clear() {
data.clear();
dirty = false;
}
bool erase(T const& element) {
ensureSet();
uint_fast64_t lowerBound = 0;
uint_fast64_t upperBound = data.size();
while (lowerBound != upperBound) {
uint_fast64_t currentPosition = (upperBound - lowerBound) / 2;
bool searchInLowerHalf = element < data[currentPosition];
if (searchInLowerHalf) {
upperBound = currentPosition;
} else {
bool searchInRightHalf = element > data[currentPosition];
if (searchInRightHalf) {
lowerBound = currentPosition + 1;
} else {
// At this point we have found the element.
data.erase(data.begin() + currentPosition);
return true;
}
}
}
return false;
}
friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set) {
set.ensureSet();
stream << "VectorSet(" << set.size() << ") { ";
if (set.size() > 0) {
for (uint_fast64_t index = 0; index < set.size() - 1; ++index) {
stream << set.data[index] << ", ";
}
stream << set.data[set.size() - 1] << " }";
} else {
stream << "}";
}
return stream;
}
private:
mutable std::vector<T> data;
mutable bool dirty;
};
}
}
namespace std {
}
#endif /* STORM_STORAGE_VECTORSET_H */

10
src/utility/IRUtility.h
View File

@ -160,7 +160,7 @@ namespace storm {
*
* @param labelSet The label set to associate with this choice.
*/
void addChoiceLabels(std::set<uint_fast64_t> const& labelSet) {
void addChoiceLabels(storm::storage::VectorSet<uint_fast64_t> const& labelSet) {
for (uint_fast64_t label : labelSet) {
addChoiceLabel(label);
}
@ -171,7 +171,7 @@ namespace storm {
*
* @return The set of labels associated with this choice.
*/
std::set<uint_fast64_t> const& getChoiceLabels() const {
storm::storage::VectorSet<uint_fast64_t> const& getChoiceLabels() const {
return choiceLabels;
}
@ -224,7 +224,7 @@ namespace storm {
std::string actionLabel;
// The labels that are associated with this choice.
std::set<uint_fast64_t> choiceLabels;
storm::storage::VectorSet<uint_fast64_t> choiceLabels;
};
/*!
@ -238,7 +238,7 @@ namespace storm {
* is ignored by this particular function but not by the overloaded functions.
*/
template<typename ValueType>
void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> const& labels) {
void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, storm::storage::VectorSet<uint_fast64_t> const& labels) {
choice.getOrAddEntry(state) += probability;
}
@ -252,7 +252,7 @@ namespace storm {
* @param labels A set of labels that is supposed to be associated with this state and probability.
*/
template<typename ValueType>
void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> const& labels) {
void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, storm::storage::VectorSet<uint_fast64_t> const& labels) {
auto& labeledEntry = choice.getOrAddEntry(state);
labeledEntry.addValue(probability, labels);
}

33
src/utility/counterexamples.h
View File

@ -20,15 +20,15 @@ namespace storm {
* @return The set of action labels that is visited on all paths from any state to a target state.
*/
template <typename T>
std::vector<std::set<uint_fast64_t>> getGuaranteedLabelSets(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, std::set<uint_fast64_t> const& relevantLabels) {
std::vector<storm::storage::VectorSet<uint_fast64_t>> getGuaranteedLabelSets(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, storm::storage::VectorSet<uint_fast64_t> const& relevantLabels) {
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
// Now we compute the set of labels that is present on all paths from the initial to the target states.
std::vector<std::set<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);
std::vector<storm::storage::VectorSet<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);
std::queue<std::pair<uint_fast64_t, uint_fast64_t>> worklist;
// Initially, put all predecessors of target states in the worklist and empty the analysis information them.
@ -50,19 +50,25 @@ namespace storm {
uint_fast64_t targetState = currentStateTargetStatePair.second;
// Iterate over the successor states for all choices and compute new analysis information.
std::set<uint_fast64_t> intersection;
storm::storage::VectorSet<uint_fast64_t> intersection(analysisInformation[currentState]);
for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) {
storm::storage::VectorSet<uint_fast64_t> tmpIntersection;
storm::storage::VectorSet<uint_fast64_t> tmpUnion;
bool choiceTargetsTargetState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
// If we can reach the target state with this choice, we need to intersect the current
// analysis information with the union of the new analysis information of the target state
// and the choice labels.
if (*successorIt == targetState) {
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[targetState].begin(), analysisInformation[targetState].end(), std::inserter(intersection, intersection.begin()));
std::set<uint_fast64_t> choiceLabelIntersection;
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(intersection, intersection.begin()));
choiceTargetsTargetState = true;
std::set_union(analysisInformation[targetState].begin(), analysisInformation[targetState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpUnion, tmpUnion.end()));
break;
}
}
if (choiceTargetsTargetState) {
std::set_intersection(intersection.begin(), intersection.end(), tmpUnion.begin(), tmpUnion.end(), std::inserter(tmpIntersection, tmpIntersection.end()));
std::swap(intersection, tmpIntersection);
}
}
// If the analysis information changed, we need to update it and put all the predecessors of this
@ -87,15 +93,14 @@ namespace storm {
* @return The set of action labels that is visited on all paths from an initial state to a target state.
*/
template <typename T>
std::set<uint_fast64_t> getGuaranteedLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, std::set<uint_fast64_t> const& relevantLabels) {
std::vector<std::set<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels);
storm::storage::VectorSet<uint_fast64_t> getGuaranteedLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, storm::storage::VectorSet<uint_fast64_t> const& relevantLabels) {
std::vector<storm::storage::VectorSet<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels);
std::set<uint_fast64_t> knownLabels(relevantLabels);
std::set<uint_fast64_t> tempIntersection;
storm::storage::VectorSet<uint_fast64_t> knownLabels(relevantLabels);
storm::storage::VectorSet<uint_fast64_t> tempIntersection;
for (auto initialState : labeledMdp.getInitialStates()) {
std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.begin()));
tempIntersection = knownLabels.intersect(guaranteedLabels[initialState]);
std::swap(knownLabels, tempIntersection);
tempIntersection.clear();
}
return knownLabels;

Write Preview
Loading…
Cancel
Save