From 422da8f48138a4c701f19b2d04e06dece92335e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 Oct 2013 17:09:39 +0200 Subject: [PATCH] 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: ac9993eab25e1c0b9300e8f8ede12b1b86dfeb6d --- src/adapters/ExplicitModelAdapter.h | 12 +- .../MILPMinimalLabelSetGenerator.h | 20 +- .../SMTMinimalCommandSetGenerator.h | 128 +++++----- src/ir/Module.cpp | 4 +- src/ir/Module.h | 3 +- src/ir/Program.cpp | 2 +- src/ir/Program.h | 3 +- src/models/AbstractDeterministicModel.h | 6 +- src/models/AbstractModel.h | 19 +- src/models/AbstractNondeterministicModel.h | 6 +- src/models/Ctmc.h | 4 +- src/models/Ctmdp.h | 7 +- src/models/Dtmc.h | 4 +- src/models/Mdp.h | 14 +- src/parser/DeterministicModelParser.cpp | 4 +- src/parser/NondeterministicModelParser.cpp | 4 +- src/storage/LabeledValues.h | 18 +- src/storage/VectorSet.h | 225 ++++++++++++++++++ src/utility/IRUtility.h | 10 +- src/utility/counterexamples.h | 33 +-- 20 files changed, 380 insertions(+), 146 deletions(-) create mode 100644 src/storage/VectorSet.h diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 188653d55..a2924c97e 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -77,7 +77,7 @@ namespace storm { storm::storage::SparseMatrix transitionRewardMatrix; // A vector that stores a labeling for each choice. - std::vector> choiceLabeling; + std::vector> 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 newLabelSet = valueLabelSetPair.second; + storm::storage::VectorSet 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>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { + static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { std::vector nondeterministicChoiceIndices; - std::vector> choiceLabels; + std::vector> choiceLabels; // Initialize a queue and insert the initial state. std::queue stateQueue; @@ -488,7 +488,7 @@ namespace storm { if (deterministicModel) { Choice globalChoice(""); std::map stateToRewardMap; - std::set allChoiceLabels; + storm::storage::VectorSet 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>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); + std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first); modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 0eed58615..aa24cb073 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -66,8 +66,8 @@ namespace storm { struct ChoiceInformation { std::unordered_map> relevantChoicesForRelevantStates; std::unordered_map> problematicChoicesForProblematicStates; - std::set allRelevantLabels; - std::set knownLabels; + storm::storage::VectorSet allRelevantLabels; + storm::storage::VectorSet knownLabels; }; /*! @@ -126,7 +126,7 @@ namespace storm { ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> 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 createLabelVariables(GRBenv* env, GRBmodel* model, std::set const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) { + static std::unordered_map createLabelVariables(GRBenv* env, GRBmodel* model, storm::storage::VectorSet const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) { int error = 0; std::stringstream variableNameBuffer; std::unordered_map resultingMap; @@ -671,7 +671,7 @@ namespace storm { static uint_fast64_t assertChoicesImplyLabels(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; int error = 0; - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); for (auto state : stateInformation.relevantStates) { std::list::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 getUsedLabelsInSolution(GRBenv* env, GRBmodel* model, VariableInformation const& variableInformation) { + static storm::storage::VectorSet 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 result; + storm::storage::VectorSet result; double value = 0; for (auto labelVariablePair : variableInformation.labelToVariableIndexMap) { @@ -1265,7 +1265,7 @@ namespace storm { public: - static std::set getMinimalLabelSet(storm::models::Mdp 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 getMinimalLabelSet(storm::models::Mdp 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 usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation); + storm::storage::VectorSet 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 usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true); + storm::storage::VectorSet 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(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 52bc3d8d4..807011964 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -43,10 +43,10 @@ namespace storm { storm::storage::BitVector relevantStates; // The set of relevant labels. - std::set relevantLabels; + storm::storage::VectorSet relevantLabels; // A set of labels that is definitely known to be taken in the final solution. - std::set knownLabels; + storm::storage::VectorSet knownLabels; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; @@ -94,7 +94,7 @@ namespace storm { // Retrieve some references for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> 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 remainingLabels; - std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.begin())); + storm::storage::VectorSet 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 const& relevantLabels) { + static VariableInformation createExpressionsForRelevantLabels(z3::context& context, storm::storage::VectorSet 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 initialLabels; - std::map> precedingLabels; - std::set targetLabels; - std::map> followingLabels; - std::map>> synchronizingLabels; + storm::storage::VectorSet initialLabels; + std::map> precedingLabels; + storm::storage::VectorSet targetLabels; + std::map> followingLabels; + std::map>> synchronizingLabels; // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); storm::storage::SparseMatrix 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 synchSet(choiceLabeling[currentChoice]); + storm::storage::VectorSet synchSet(choiceLabeling[currentChoice]); synchSet.erase(label); synchronizingLabels[label].emplace(std::move(synchSet)); } @@ -289,10 +289,11 @@ namespace storm { std::vector 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 intersection; - std::set_intersection(initialLabels.begin(), initialLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.begin())); + storm::storage::VectorSet 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 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>> precedingLabelSets; + std::map, std::set>> precedingLabelSets; // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); storm::storage::SparseMatrix 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>> backwardImplications; + std::map, std::set>> 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 const& commandSet, VariableInformation const& variableInformation) { + static void ruleOutSolution(z3::context& context, z3::solver& solver, storm::storage::VectorSet 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 getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) { - std::set result; + static storm::storage::VectorSet getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) { + storm::storage::VectorSet 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 findSmallestCommandSet(z3::context& context, z3::solver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { + static storm::storage::VectorSet 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 const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeZeroProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::VectorSet 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 const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); + std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); // Now determine which states and labels are actually reachable. - std::set reachableLabels; + storm::storage::VectorSet 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> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels); + std::vector> 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> const& choiceLabeling = originalMdp.getChoiceLabeling(); - std::set> cutLabels; + std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); + std::set> 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::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 currentLabelSet; + storm::storage::VectorSet currentLabelSet; for (auto label : choiceLabeling[currentChoice]) { - if (commandSet.find(label) == commandSet.end()) { + if (!commandSet.contains(label)) { currentLabelSet.insert(label); } } - std::set 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 formulae; - std::set unknownReachableLabels; - std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.begin())); + storm::storage::VectorSet 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 const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::VectorSet 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 const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); + std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); // Now determine which states and labels are actually reachable. - std::set reachableLabels; + storm::storage::VectorSet 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> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels); + std::vector> 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> const& choiceLabeling = originalMdp.getChoiceLabeling(); - std::set> cutLabels; + std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); + std::set> cutLabels; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!storm::utility::set::isSubsetOf(choiceLabeling[currentChoice], commandSet)) { - std::set currentLabelSet; + if (!choiceLabeling[currentChoice].subsetOf(commandSet)) { + storm::storage::VectorSet currentLabelSet; for (auto label : choiceLabeling[currentChoice]) { - if (commandSet.find(label) == commandSet.end()) { + if (!commandSet.contains(label)) { currentLabelSet.insert(label); } } - std::set 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 formulae; - std::set unknownReachableLabels; - std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.begin())); + storm::storage::VectorSet 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 getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false) { + static storm::storage::VectorSet getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp 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 commandSet(relevancyInformation.relevantLabels); + storm::storage::VectorSet commandSet(relevancyInformation.relevantLabels); bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index c8790d2f4..23ed343c8 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -186,10 +186,10 @@ namespace storm { } } - void Module::restrictCommands(std::set const& indexSet) { + void Module::restrictCommands(storm::storage::VectorSet const& indexSet) { std::vector newCommands; for (auto const& command : commands) { - if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { + if (indexSet.contains(command.getGlobalIndex())) { newCommands.push_back(std::move(command)); } } diff --git a/src/ir/Module.h b/src/ir/Module.h index d0bcec060..4ee60c5f3 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -20,6 +20,7 @@ #include #include +#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 const& indexSet); + void restrictCommands(storm::storage::VectorSet const& indexSet); private: /*! diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index e7b6accad..94006f92d 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -290,7 +290,7 @@ namespace storm { return this->globalIntegerVariableToIndexMap.at(variableName); } - void Program::restrictCommands(std::set const& indexSet) { + void Program::restrictCommands(storm::storage::VectorSet const& indexSet) { for (auto& module : modules) { module.restrictCommands(indexSet); } diff --git a/src/ir/Program.h b/src/ir/Program.h index 01bd25d04..6a1f1bf8b 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -13,6 +13,7 @@ #include #include +#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 const& indexSet); + void restrictCommands(storm::storage::VectorSet const& indexSet); private: // The type of the model. ModelType modelType; diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index d2e24cbbd..0ba5166f6 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel { */ AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { } @@ -43,7 +43,7 @@ class AbstractDeterministicModel: public AbstractModel { */ AbstractDeterministicModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { @@ -116,7 +116,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return void */ virtual void setStateIdBasedChoiceLabeling() override { - std::vector> newChoiceLabeling; + std::vector> newChoiceLabeling; size_t stateCount = this->getNumberOfStates(); newChoiceLabeling.resize(stateCount); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index deffd9999..3518bcea4 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -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 #include #include +#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(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling) { if (optionalStateRewardVector) { @@ -95,7 +96,7 @@ class AbstractModel: public std::enable_shared_from_this> { */ AbstractModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) : + boost::optional>>&& 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> { * Returns the labels for the choices of the model, if there are any. * @return The labels for the choices of the model. */ - std::vector> const& getChoiceLabeling() const { + std::vector> const& getChoiceLabeling() const { return choiceLabeling.get(); } @@ -538,7 +539,7 @@ protected: storm::storage::SparseMatrix transitionMatrix; /*! The labeling that is associated with the choices for each state. */ - boost::optional>> choiceLabeling; + boost::optional>> choiceLabeling; private: /*! The labeling of the states of the model. */ storm::models::AtomicPropositionsLabeling stateLabeling; diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index c4569473f..d45e2a51a 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -32,7 +32,7 @@ namespace storm { std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { this->nondeterministicChoiceIndices = nondeterministicChoiceIndices; } @@ -51,7 +51,7 @@ namespace storm { std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractModel(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> newChoiceLabeling; + std::vector> newChoiceLabeling; size_t stateCount = this->getNumberOfStates(); size_t choiceCount = this->getNumberOfChoices(); diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 787649540..2385ce2cf 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -37,7 +37,7 @@ public: */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { // Intentionally left empty. } @@ -52,7 +52,7 @@ public: */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index c8966357c..b8d3145e2 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -42,7 +42,7 @@ public: std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { @@ -65,10 +65,9 @@ public: std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractNondeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), - std::move(optionalChoiceLabeling)) { + : AbstractNondeterministicModel(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."; diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 7b012803d..024d6eae0 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -43,7 +43,7 @@ public: */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -69,7 +69,7 @@ public: */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 17620e194..5507ddfb2 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -49,7 +49,7 @@ public: std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -77,7 +77,7 @@ public: std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractNondeterministicModel(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 restrictChoiceLabels(std::set const& enabledChoiceLabels) const { + Mdp restrictChoiceLabels(storm::storage::VectorSet 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> const& choiceLabeling = this->getChoiceLabeling(); + std::vector> const& choiceLabeling = this->getChoiceLabeling(); storm::storage::SparseMatrix transitionMatrix; transitionMatrix.initialize(); std::vector nondeterministicChoiceIndices; - std::vector> newChoiceLabeling; + std::vector> 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 restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional>(this->getStateRewardVector()) : boost::optional>(), this->hasTransitionRewards() ? boost::optional>(this->getTransitionRewardMatrix()) : boost::optional>(), boost::optional>>(newChoiceLabeling)); + Mdp restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional>(this->getStateRewardVector()) : boost::optional>(), this->hasTransitionRewards() ? boost::optional>(this->getTransitionRewardMatrix()) : boost::optional>(), boost::optional>>(newChoiceLabeling)); return restrictedMdp; } diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index ec357b3bf..2637f1be0 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -58,7 +58,7 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & t storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 536a6ec88..beabf456b 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -58,7 +58,7 @@ NondeterministicModelParserResultContainer parseNondeterministicModel(st storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h index 8ebb5ec45..f69e37029 100644 --- a/src/storage/LabeledValues.h +++ b/src/storage/LabeledValues.h @@ -9,7 +9,7 @@ #define STORM_STORAGE_LABELEDVALUES_H #include -#include +#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& addValue(ValueType value) { - valueLabelList.emplace_back(value, std::set()); + storm::storage::VectorSet& addValue(ValueType value) { + valueLabelList.emplace_back(value, storm::storage::VectorSet()); 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& addValue(ValueType value, std::set const& labels) { + storm::storage::VectorSet& addValue(ValueType value, storm::storage::VectorSet 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>>::iterator begin() { + typename std::list>>::iterator begin() { return valueLabelList.begin(); } @@ -76,7 +76,7 @@ namespace storm { * * @return An iterator pointing past the last labeled probability. */ - typename std::list>>::const_iterator end() { + typename std::list>>::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>>::const_iterator begin() const { + typename std::list>>::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>>::const_iterator end() const { + typename std::list>>::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>> valueLabelList; + std::list>> valueLabelList; /*! * Returns the sum of the values. diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h new file mode 100644 index 000000000..1371eda30 --- /dev/null +++ b/src/storage/VectorSet.h @@ -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 +#include + +namespace storm { + namespace storage { + + template + class VectorSet { + public: + typedef T* difference_type; + typedef T value_type; + typedef T* pointer; + typedef T& reference; + typedef typename std::vector::iterator iterator; + typedef typename std::vector::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 const& data) : data(data), dirty(true) { + ensureSet(); + } + + VectorSet(std::set const& data) : dirty(false) { + this->data.reserve(data.size()); + for (auto const& element : data) { + this->data.push_back(element); + } + } + + template + 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 + iterator insert(InputIterator first, InputIterator last) { + return data.insert(data.end(), first, last); + } + + template + 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 data; + mutable bool dirty; + }; + } +} + +namespace std { + +} + + +#endif /* STORM_STORAGE_VECTORSET_H */ diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h index fdcf473a9..b3f79a380 100644 --- a/src/utility/IRUtility.h +++ b/src/utility/IRUtility.h @@ -160,7 +160,7 @@ namespace storm { * * @param labelSet The label set to associate with this choice. */ - void addChoiceLabels(std::set const& labelSet) { + void addChoiceLabels(storm::storage::VectorSet 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 const& getChoiceLabels() const { + storm::storage::VectorSet const& getChoiceLabels() const { return choiceLabels; } @@ -224,7 +224,7 @@ namespace storm { std::string actionLabel; // The labels that are associated with this choice. - std::set choiceLabels; + storm::storage::VectorSet choiceLabels; }; /*! @@ -238,7 +238,7 @@ namespace storm { * is ignored by this particular function but not by the overloaded functions. */ template - void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, storm::storage::VectorSet 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 - void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, storm::storage::VectorSet const& labels) { auto& labeledEntry = choice.getOrAddEntry(state); labeledEntry.addValue(probability, labels); } diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index 218daf964..f3e0742a5 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -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 - std::vector> getGuaranteedLabelSets(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, std::set const& relevantLabels) { + std::vector> getGuaranteedLabelSets(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, storm::storage::VectorSet const& relevantLabels) { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); storm::storage::SparseMatrix 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> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels); + std::vector> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels); std::queue> 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 intersection; + storm::storage::VectorSet intersection(analysisInformation[currentState]); for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { + storm::storage::VectorSet tmpIntersection; + storm::storage::VectorSet tmpUnion; + bool choiceTargetsTargetState = false; for (typename storm::storage::SparseMatrix::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 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 - std::set getGuaranteedLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, std::set const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels); + storm::storage::VectorSet getGuaranteedLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, storm::storage::VectorSet const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels); - std::set knownLabels(relevantLabels); - std::set tempIntersection; + storm::storage::VectorSet knownLabels(relevantLabels); + storm::storage::VectorSet 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;