diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 36c1bbe01..be446333d 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -14,6 +14,7 @@ #include #include #include +#include #include "src/ir/Program.h" #include "src/ir/RewardModel.h" @@ -77,7 +78,7 @@ namespace storm { storm::storage::SparseMatrix transitionRewardMatrix; // A vector that stores a labeling for each choice. - std::vector> choiceLabeling; + std::vector> choiceLabeling; }; /*! @@ -294,10 +295,9 @@ namespace storm { // Update the choice by adding the probability/target state to it. double probabilityToAdd = update.getLikelihoodExpression()->getValueAsDouble(currentState); probabilitySum += probabilityToAdd; - std::set lables; - lables.insert(update.getGlobalIndex()); - //addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, {update.getGlobalIndex()}); - addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, lables); + boost::container::flat_set labels; + labels.insert(update.getGlobalIndex()); + addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, labels); } // Check that the resulting distribution is in fact a distribution. @@ -351,7 +351,7 @@ namespace storm { double updateProbability = update.getLikelihoodExpression()->getValueAsDouble(currentState); for (auto const& valueLabelSetPair : stateProbabilityPair.second) { // Copy the label set, so we can modify it. - storm::storage::VectorSet newLabelSet = valueLabelSetPair.second; + boost::container::flat_set newLabelSet = valueLabelSetPair.second; newLabelSet.insert(update.getGlobalIndex()); newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet); @@ -455,9 +455,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::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { + static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { std::vector nondeterministicChoiceIndices; - std::vector> choiceLabels; + std::vector> choiceLabels; // Initialize a queue and insert the initial state. std::queue stateQueue; @@ -492,7 +492,7 @@ namespace storm { if (deterministicModel) { Choice globalChoice(""); std::map stateToRewardMap; - storm::storage::VectorSet allChoiceLabels; + boost::container::flat_set allChoiceLabels; // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { @@ -633,7 +633,7 @@ namespace storm { // Build the transition and reward matrices. storm::storage::SparseMatrixBuilder transitionMatrixBuilder; storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; - std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); + std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); 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 bb135b43f..6fff846aa 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -57,8 +57,8 @@ namespace storm { struct ChoiceInformation { std::unordered_map> relevantChoicesForRelevantStates; std::unordered_map> problematicChoicesForProblematicStates; - storm::storage::VectorSet allRelevantLabels; - storm::storage::VectorSet knownLabels; + boost::container::flat_set allRelevantLabels; + boost::container::flat_set knownLabels; }; /*! @@ -116,7 +116,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 @@ -168,7 +168,7 @@ namespace storm { * @param relevantLabels The set of relevant labels of the model. * @return A mapping from labels to variable indices. */ - static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, storm::storage::VectorSet const& relevantLabels) { + static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { int error = 0; std::stringstream variableNameBuffer; std::unordered_map resultingMap; @@ -482,7 +482,7 @@ namespace storm { static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 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)) { @@ -888,8 +888,8 @@ namespace storm { * @param solver The MILP solver. * @param variableInformation A struct with information about the variables of the model. */ - static storm::storage::VectorSet getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { - storm::storage::VectorSet result; + static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + boost::container::flat_set result; for (auto labelVariablePair : variableInformation.labelToVariableIndexMap) { bool labelTaken = solver.getBinaryValue(labelVariablePair.second); @@ -951,7 +951,7 @@ namespace storm { public: - 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) { + static boost::container::flat_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) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; @@ -987,8 +987,8 @@ namespace storm { solver->optimize(); // (4.4) Read off result from variables. - storm::storage::VectorSet usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); - usedLabelSet.insert(choiceInformation.knownLabels); + boost::container::flat_set usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); + usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); // Display achieved probability. std::pair initialStateProbabilityPair = getReachabilityProbability(*solver, labeledMdp, variableInformation); @@ -1044,7 +1044,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - storm::storage::VectorSet usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true); + boost::container::flat_set 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 e8bedf243..136045173 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. - storm::storage::VectorSet relevantLabels; + boost::container::flat_set relevantLabels; // A set of labels that is definitely known to be taken in the final solution. - storm::storage::VectorSet knownLabels; + boost::container::flat_set knownLabels; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; @@ -112,7 +112,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 @@ -141,7 +141,7 @@ 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()) { - storm::storage::VectorSet remainingLabels; + boost::container::flat_set remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); relevancyInformation.relevantLabels = remainingLabels; } @@ -282,19 +282,19 @@ namespace storm { // * identify labels that directly reach a target state // * identify labels that can directly follow a given action - storm::storage::VectorSet initialLabels; - std::set> initialCombinations; - std::map> precedingLabels; - storm::storage::VectorSet targetLabels; - storm::storage::VectorSet> targetCombinations; - std::map, std::set>> followingLabels; - std::map>> synchronizingLabels; + boost::container::flat_set initialLabels; + std::set> initialCombinations; + std::map> precedingLabels; + boost::container::flat_set targetLabels; + boost::container::flat_set> targetCombinations; + std::map, std::set>> 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) { @@ -309,7 +309,7 @@ namespace storm { // If the state is initial, we need to add all the choice labels to the initial label set. if (initialStates.get(currentState)) { - initialLabels.insert(choiceLabeling[currentChoice]); + initialLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); initialCombinations.insert(choiceLabeling[currentChoice]); } @@ -327,7 +327,7 @@ namespace storm { // If the choice can reach a target state directly, we add all the labels to the target label set. if (canReachTargetState) { - targetLabels.insert(choiceLabeling[currentChoice]); + targetLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); targetCombinations.insert(choiceLabeling[currentChoice]); } } @@ -368,7 +368,7 @@ namespace storm { // combination that is already known. Otherwise this condition would be too strong. bool initialCombinationKnown = false; for (auto const& combination : initialCombinations) { - storm::storage::VectorSet tmpSet; + boost::container::flat_set tmpSet; std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { initialCombinationKnown = true; @@ -393,7 +393,7 @@ namespace storm { // Likewise, if no target combination is known, we may assert that there is at least one. bool targetCombinationKnown = false; for (auto const& combination : targetCombinations) { - storm::storage::VectorSet tmpSet; + boost::container::flat_set tmpSet; std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { targetCombinationKnown = true; @@ -412,10 +412,10 @@ namespace storm { } // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. - storm::storage::VectorSet> hasKnownSuccessor; + boost::container::flat_set> hasKnownSuccessor; for (auto const& labelSetFollowingSetsPair : followingLabels) { for (auto const& set : labelSetFollowingSetsPair.second) { - if (set.subsetOf(relevancyInformation.knownLabels)) { + if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { hasKnownSuccessor.insert(set); break; } @@ -429,17 +429,17 @@ namespace storm { // Only build a constraint if the combination does not lead to a target state and // no successor set is already known. - if (!targetCombinations.contains(labelSetFollowingSetsPair.first) && !hasKnownSuccessor.contains(labelSetFollowingSetsPair.first)) { + if (targetCombinations.find(labelSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(labelSetFollowingSetsPair.first) == hasKnownSuccessor.end()) { // Compute the set of unknown labels on the left-hand side of the implication. - storm::storage::VectorSet unknownLhsLabels; + boost::container::flat_set unknownLhsLabels; std::set_difference(labelSetFollowingSetsPair.first.begin(), labelSetFollowingSetsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); for (auto label : unknownLhsLabels) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } for (auto const& followingSet : labelSetFollowingSetsPair.second) { - storm::storage::VectorSet tmpSet; + boost::container::flat_set tmpSet; // Check which labels of the current following set are not known. This set must be non-empty, because // otherwise a successor combination would already be known and control cannot reach this point. @@ -461,7 +461,7 @@ namespace storm { z3::expr finalDisjunct = context.bool_val(false); for (auto label : labelSetFollowingSetsPair.first) { z3::expr alternativeExpressionForLabel = context.bool_val(false); - std::set> const& synchsForCommand = synchronizingLabels.at(label); + std::set> const& synchsForCommand = synchronizingLabels.at(label); for (auto const& synchSet : synchsForCommand) { z3::expr alternativeExpression = context.bool_val(true); @@ -471,9 +471,9 @@ namespace storm { // Now that we have the labels that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known successor or leads directly to a target state. - if (!hasKnownSuccessor.contains(synchSet) && !targetCombinations.contains(synchSet)) { + if (hasKnownSuccessor.find(synchSet) == hasKnownSuccessor.end() && targetCombinations.find(synchSet) == targetCombinations.end()) { // If not, we can assert that we take one of its possible successors. - storm::storage::VectorSet unknownSynchs; + boost::container::flat_set unknownSynchs; std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); unknownSynchs.erase(label); @@ -485,7 +485,7 @@ namespace storm { for (auto successorSet : followingLabels.at(synchSet)) { z3::expr conjunctionOverLabels = context.bool_val(true); for (auto label : successorSet) { - if (!relevancyInformation.knownLabels.contains(label)) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } @@ -516,7 +516,7 @@ namespace storm { for (auto const& labelSynchronizingSetsPair : synchronizingLabels) { std::vector formulae; - if (!relevancyInformation.knownLabels.contains(labelSynchronizingSetsPair.first)) { + if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first))); } @@ -527,7 +527,7 @@ namespace storm { z3::expr currentCombination = context.bool_val(true); bool allImplicantsKnownForCurrentSet = true; for (auto label : synchronizingSet) { - if (!relevancyInformation.knownLabels.contains(label) && label != labelSynchronizingSetsPair.first) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end() && label != labelSynchronizingSetsPair.first) { currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } @@ -557,14 +557,14 @@ 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; // A container that maps labels to their reachable synchronization sets. - std::map>> synchronizingLabels; + std::map>> synchronizingLabels; // 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. @@ -640,7 +640,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) { @@ -654,7 +654,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.contains(command.getGlobalIndex())) { + if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) { currentCommandVector.push_back(command); } } @@ -723,7 +723,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.contains(command.getGlobalIndex())) { + if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) { currentPrecedingCommandVector.push_back(command); } } @@ -789,10 +789,10 @@ namespace storm { } // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. - storm::storage::VectorSet> hasKnownPredecessor; + boost::container::flat_set> hasKnownPredecessor; for (auto const& labelSetImplicationsPair : backwardImplications) { for (auto const& set : labelSetImplicationsPair.second) { - if (set.subsetOf(relevancyInformation.knownLabels)) { + if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { hasKnownPredecessor.insert(set); break; } @@ -805,17 +805,17 @@ namespace storm { std::vector formulae; // Only build a constraint if the combination no predecessor set is already known. - if (!hasKnownPredecessor.contains(labelSetImplicationsPair.first)) { + if (hasKnownPredecessor.find(labelSetImplicationsPair.first) == hasKnownPredecessor.end()) { // Compute the set of unknown labels on the left-hand side of the implication. - storm::storage::VectorSet unknownLhsLabels; + boost::container::flat_set unknownLhsLabels; std::set_difference(labelSetImplicationsPair.first.begin(), labelSetImplicationsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); for (auto label : unknownLhsLabels) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } for (auto const& precedingSet : labelSetImplicationsPair.second) { - storm::storage::VectorSet tmpSet; + boost::container::flat_set tmpSet; // Check which labels of the current following set are not known. This set must be non-empty, because // otherwise a predecessor combination would already be known and control cannot reach this point. @@ -837,7 +837,7 @@ namespace storm { z3::expr finalDisjunct = context.bool_val(false); for (auto label : labelSetImplicationsPair.first) { z3::expr alternativeExpressionForLabel = context.bool_val(false); - std::set> const& synchsForCommand = synchronizingLabels.at(label); + std::set> const& synchsForCommand = synchronizingLabels.at(label); for (auto const& synchSet : synchsForCommand) { z3::expr alternativeExpression = context.bool_val(true); @@ -847,9 +847,9 @@ namespace storm { // Now that we have the labels that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known predecessor. - if (!hasKnownPredecessor.contains(synchSet)) { + if (hasKnownPredecessor.find(synchSet) == hasKnownPredecessor.end()) { // If not, we can assert that we take one of its possible predecessors. - storm::storage::VectorSet unknownSynchs; + boost::container::flat_set unknownSynchs; std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); unknownSynchs.erase(label); @@ -863,7 +863,7 @@ namespace storm { for (auto precedingSet : precedingLabelSetsIterator->second) { z3::expr conjunctionOverLabels = context.bool_val(true); for (auto label : precedingSet) { - if (!relevancyInformation.knownLabels.contains(label)) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } @@ -901,7 +901,7 @@ namespace storm { // 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(); // First, we add the formulas that encode @@ -911,14 +911,14 @@ namespace storm { for (auto relevantState : relevancyInformation.relevantStates) { if (!labeledMdp.getInitialStates().get(relevantState)) { // Assert the constraints (1). - storm::storage::VectorSet relevantPredecessors; + boost::container::flat_set relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { if (relevantState != predecessorEntry.first && relevancyInformation.relevantStates.get(predecessorEntry.first)) { relevantPredecessors.insert(predecessorEntry.first); } } - storm::storage::VectorSet relevantSuccessors; + boost::container::flat_set relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { @@ -938,7 +938,7 @@ namespace storm { solver.add(expression); } else { // Assert the constraints (2). - storm::storage::VectorSet relevantSuccessors; + boost::container::flat_set relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { @@ -962,7 +962,7 @@ namespace storm { uint_fast64_t targetState = statePairIndexPair.first.second; // Assert constraint for (1). - storm::storage::VectorSet choicesForStatePair; + boost::container::flat_set choicesForStatePair; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (successorEntry.first == targetState) { @@ -974,7 +974,7 @@ namespace storm { for (auto choice : choicesForStatePair) { z3::expr choiceExpression = context.bool_val(true); for (auto element : choiceLabeling.at(choice)) { - if (!relevancyInformation.knownLabels.contains(element)) { + if (relevancyInformation.knownLabels.find(element) == relevancyInformation.knownLabels.end()) { choiceExpression = choiceExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(element)); } } @@ -1271,10 +1271,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, storm::storage::VectorSet const& commandSet, VariableInformation const& variableInformation) { + static void ruleOutSolution(z3::context& context, z3::solver& solver, boost::container::flat_set const& commandSet, VariableInformation const& variableInformation) { z3::expr blockSolutionExpression = context.bool_val(false); for (auto labelIndexPair : variableInformation.labelToIndexMap) { - if (commandSet.contains(labelIndexPair.first)) { + if (commandSet.find(labelIndexPair.first) != commandSet.end()) { blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second]; } } @@ -1289,8 +1289,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 storm::storage::VectorSet getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) { - storm::storage::VectorSet result; + static boost::container::flat_set getUsedLabelSet(z3::context& context, z3::model const& model, VariableInformation const& variableInformation) { + boost::container::flat_set result; for (auto const& labelIndexPair : variableInformation.labelToIndexMap) { z3::expr auxValue = model.eval(variableInformation.labelVariables.at(labelIndexPair.second)); @@ -1342,7 +1342,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 storm::storage::VectorSet findSmallestCommandSet(z3::context& context, z3::solver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { + static boost::container::flat_set 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(); @@ -1372,7 +1372,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, storm::storage::VectorSet 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, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); LOG4CPLUS_DEBUG(logger, "Analyzing solution with zero probability."); @@ -1388,10 +1388,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. - storm::storage::VectorSet reachableLabels; + boost::container::flat_set reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1428,17 +1428,17 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), 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) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!choiceLabeling[currentChoice].subsetOf(commandSet)) { + if (!std::includes(commandSet.begin(), commandSet.end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end())) { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. @@ -1449,9 +1449,9 @@ namespace storm { } if (isBorderChoice) { - storm::storage::VectorSet currentLabelSet; + boost::container::flat_set currentLabelSet; for (auto label : choiceLabeling.at(currentChoice)) { - if (!commandSet.contains(label)) { + if (commandSet.find(label) == commandSet.end()) { currentLabelSet.insert(label); } } @@ -1465,7 +1465,7 @@ namespace storm { // Given the results of the previous analysis, we construct the implications. std::vector formulae; - storm::storage::VectorSet unknownReachableLabels; + boost::container::flat_set 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))); @@ -1497,7 +1497,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, storm::storage::VectorSet 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, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { LOG4CPLUS_DEBUG(logger, "Analyzing solution with insufficient probability."); @@ -1514,10 +1514,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. - storm::storage::VectorSet reachableLabels; + boost::container::flat_set reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1548,17 +1548,17 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), 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 (!choiceLabeling[currentChoice].subsetOf(commandSet)) { - storm::storage::VectorSet currentLabelSet; + if (!std::includes(commandSet.begin(), commandSet.end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end())) { + boost::container::flat_set currentLabelSet; for (auto label : choiceLabeling[currentChoice]) { - if (!commandSet.contains(label)) { + if (commandSet.find(label) == commandSet.end()) { currentLabelSet.insert(label); } } @@ -1572,7 +1572,7 @@ namespace storm { // Given the results of the previous analysis, we construct the implications std::vector formulae; - storm::storage::VectorSet unknownReachableLabels; + boost::container::flat_set 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))); @@ -1607,7 +1607,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 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, bool includeReachabilityEncoding = false) { + static boost::container::flat_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, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1683,7 +1683,7 @@ namespace storm { // the solver. // Set up some variables for the iterations. - storm::storage::VectorSet commandSet(relevancyInformation.relevantLabels); + boost::container::flat_set commandSet(relevancyInformation.relevantLabels); bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; @@ -1699,7 +1699,7 @@ namespace storm { // Restrict the given MDP to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); - commandSet.insert(relevancyInformation.knownLabels); + commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 23ed343c8..6b67ee579 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -186,10 +186,10 @@ namespace storm { } } - void Module::restrictCommands(storm::storage::VectorSet const& indexSet) { + void Module::restrictCommands(boost::container::flat_set const& indexSet) { std::vector newCommands; for (auto const& command : commands) { - if (indexSet.contains(command.getGlobalIndex())) { + if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { newCommands.push_back(std::move(command)); } } diff --git a/src/ir/Module.h b/src/ir/Module.h index 4ee60c5f3..e6762bb8d 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -9,6 +9,7 @@ #define STORM_IR_MODULE_H_ #include "utility/OsDetection.h" +#include #ifdef LINUX #include @@ -20,7 +21,6 @@ #include #include -#include "src/storage/VectorSet.h" #include "BooleanVariable.h" #include "IntegerVariable.h" #include "Command.h" @@ -187,7 +187,7 @@ namespace storm { * * @param indexSet The set of indices for which to keep the commands. */ - void restrictCommands(storm::storage::VectorSet const& indexSet); + void restrictCommands(boost::container::flat_set const& indexSet); private: /*! diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 94006f92d..33c75c44f 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(storm::storage::VectorSet const& indexSet) { + void Program::restrictCommands(boost::container::flat_set const& indexSet) { for (auto& module : modules) { module.restrictCommands(indexSet); } diff --git a/src/ir/Program.h b/src/ir/Program.h index 6a1f1bf8b..8ce96bc87 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -12,8 +12,8 @@ #include #include #include +#include -#include "src/storage/VectorSet.h" #include "expressions/BaseExpression.h" #include "expressions/BooleanConstantExpression.h" #include "expressions/IntegerConstantExpression.h" @@ -267,7 +267,7 @@ namespace storm { * * @param indexSet The set of indices for which to keep the commands. */ - void restrictCommands(storm::storage::VectorSet const& indexSet); + void restrictCommands(boost::container::flat_set const& indexSet); private: // The type of the model. ModelType modelType; diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 4668abded..8c6a29477 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -339,13 +339,13 @@ namespace storm { for (auto const& stateChoicesPair : mec) { uint_fast64_t state = stateChoicesPair.first; - storm::storage::VectorSet const& choicesInMec = stateChoicesPair.second; + boost::container::flat_set const& choicesInMec = stateChoicesPair.second; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. - if (!choicesInMec.contains(choice)) { + if (choicesInMec.find(choice) == choicesInMec.end()) { b.push_back(storm::utility::constantZero()); typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 0d9abec5e..4ef21986e 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)) { @@ -109,7 +109,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 b11fef9d4..b9fda426d 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -3,14 +3,13 @@ #include #include - +#include #include #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" #include "src/storage/Scheduler.h" -#include "src/storage/VectorSet.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/utility/Hash.h" @@ -74,7 +73,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) { @@ -99,7 +98,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)) { @@ -167,7 +166,7 @@ class AbstractModel: public std::enable_shared_from_this> { typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex]; // Now, we determine the blocks which are reachable (in one step) from the current block. - storm::storage::VectorSet allTargetBlocks; + boost::container::flat_set allTargetBlocks; for (auto state : block) { for (auto const& transitionEntry : this->getRows(state)) { uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.first]; @@ -281,7 +280,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(); } @@ -469,7 +468,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 e474ae0b5..8de7ef8c4 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -33,7 +33,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; } @@ -52,7 +52,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)) { @@ -124,7 +124,7 @@ namespace storm { */ storm::storage::SparseMatrix getBackwardTransitions() const { uint_fast64_t numberOfStates = this->getNumberOfStates(); - uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); + uint_fast64_t numberOfTransitions = this->getTransitionMatrix().getEntryCount(); std::vector rowIndications(numberOfStates + 1); std::vector> columnsAndValues(numberOfTransitions, std::make_pair(0, storm::utility::constantZero())); @@ -266,7 +266,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 60250d461..25d128996 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)) { @@ -95,7 +95,7 @@ public: nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); - return std::shared_ptr>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + return std::shared_ptr>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } }; diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index ccf465361..f1a162a2f 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,7 +65,7 @@ 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)) { if (!this->checkValidityOfProbabilityMatrix()) { @@ -124,7 +124,7 @@ public: nondeterministicChoiceIndices[state] = state; } nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); - return std::shared_ptr>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + return std::shared_ptr>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } private: diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 0e30f8753..03f03ec7f 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -46,7 +46,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."); @@ -73,7 +73,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)) { @@ -143,7 +143,7 @@ public: storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates), boost::optional>(), boost::optional>(), - boost::optional>>()); + boost::optional>>()); } // Does the vector have the right size? @@ -266,16 +266,16 @@ public: newTransitionRewards = newTransRewardsBuilder.build(); } - boost::optional>> newChoiceLabels; + boost::optional>> newChoiceLabels; if(this->hasChoiceLabeling()) { // Get the choice label sets and move the needed values to the front. - std::vector> newChoice(this->getChoiceLabeling()); + std::vector> newChoice(this->getChoiceLabeling()); storm::utility::vector::selectVectorValues(newChoice, subSysStates, newChoice); // Throw away all values after the last state and set the choice label set for s_b as empty. newChoice.resize(newStateCount); - newChoice[newStateCount - 1] = storm::storage::VectorSet(); + newChoice[newStateCount - 1] = boost::container::flat_set(); newChoiceLabels = newChoice; } @@ -293,7 +293,7 @@ public: nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); - return std::shared_ptr>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + return std::shared_ptr>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } private: diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 8dce30e6b..f75f17560 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -26,7 +26,7 @@ namespace storm { MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, std::vector& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { @@ -46,7 +46,7 @@ namespace storm { storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { @@ -181,7 +181,7 @@ namespace storm { } nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); - return std::shared_ptr>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + return std::shared_ptr>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { diff --git a/src/models/Mdp.h b/src/models/Mdp.h index bcb9d0eac..235d4f8cf 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -12,12 +12,12 @@ #include #include #include +#include #include "AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" #include "src/settings/Settings.h" #include "src/models/AbstractNondeterministicModel.h" -#include "src/utility/set.h" #include "src/utility/matrix.h" namespace storm { @@ -50,7 +50,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."); @@ -78,7 +78,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)) { @@ -135,24 +135,24 @@ 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(storm::storage::VectorSet const& enabledChoiceLabels) const { + Mdp restrictChoiceLabels(boost::container::flat_set const& enabledChoiceLabels) const { // Only perform this operation if the given model has choice labels. if (!this->hasChoiceLabeling()) { 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::SparseMatrixBuilder transitionMatrixBuilder; 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 = choiceLabeling[choice].subsetOf(enabledChoiceLabels); + bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end()); // If the choice is valid, copy over all its elements. if (choiceValid) { @@ -179,7 +179,7 @@ public: nondeterministicChoiceIndices.push_back(currentRow); - Mdp restrictedMdp(transitionMatrixBuilder.build(), 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(transitionMatrixBuilder.build(), 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; } @@ -200,7 +200,7 @@ public: nondeterministicChoiceIndices[state] = state; } nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); - return std::shared_ptr>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + return std::shared_ptr>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } private: diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index e05e1d3dd..86e150f67 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/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 28b91b6d9..a43dcf4fd 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -19,7 +19,7 @@ namespace storm { throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata."; } - storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); + storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); return resultingAutomaton; } diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index beabf456b..f83edb50e 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/BitVector.cpp b/src/storage/BitVector.cpp index 154043fff..b4b282e0b 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -1,5 +1,6 @@ -#include "src/storage/BitVector.h" +#include +#include "src/storage/BitVector.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" @@ -496,7 +497,11 @@ namespace storm { // All necessary explicit template instantiations. template BitVector::BitVector(uint_fast64_t length, std::vector::iterator begin, std::vector::iterator end); template BitVector::BitVector(uint_fast64_t length, std::vector::const_iterator begin, std::vector::const_iterator end); + template BitVector::BitVector(uint_fast64_t length, boost::container::flat_set::iterator begin, boost::container::flat_set::iterator end); + template BitVector::BitVector(uint_fast64_t length, boost::container::flat_set::const_iterator begin, boost::container::flat_set::const_iterator end); template void BitVector::set(std::vector::iterator begin, std::vector::iterator end); template void BitVector::set(std::vector::const_iterator begin, std::vector::const_iterator end); + template void BitVector::set(boost::container::flat_set::iterator begin, boost::container::flat_set::iterator end); + template void BitVector::set(boost::container::flat_set::const_iterator begin, boost::container::flat_set::const_iterator end); } } \ No newline at end of file diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index 531f3571e..8d06c625c 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -66,16 +66,25 @@ namespace storm { return blocks[index]; } + std::ostream& operator<<(std::ostream& out, StateBlock const& block) { + out << "{"; + for (auto const& element : block) { + out << element << ", "; + } + out << "}"; + return out; + } + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition) { - out << "{"; + out << "["; if (decomposition.size() > 0) { for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) { out << decomposition.blocks[blockIndex] << ", "; } - out << decomposition.blocks[decomposition.size() - 1]; + out << decomposition.blocks.back(); } - out << "}"; + out << "]"; return out; } diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index c3711152e..707e5d0b8 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -2,12 +2,13 @@ #define STORM_STORAGE_DECOMPOSITION_H_ #include - -#include "src/storage/VectorSet.h" +#include namespace storm { namespace storage { - typedef storm::storage::VectorSet StateBlock; + typedef boost::container::flat_set StateBlock; + + std::ostream& operator<<(std::ostream& out, StateBlock const& block); /*! * This class represents the decomposition of a model into blocks which are of the template type. diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h index 923d8b9f6..58f58f68b 100644 --- a/src/storage/LabeledValues.h +++ b/src/storage/LabeledValues.h @@ -9,7 +9,7 @@ #define STORM_STORAGE_LABELEDVALUES_H #include -#include "src/storage/VectorSet.h" +#include 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. */ - storm::storage::VectorSet& addValue(ValueType value) { - valueLabelList.emplace_back(value, storm::storage::VectorSet()); + boost::container::flat_set& addValue(ValueType value) { + valueLabelList.emplace_back(value, boost::container::flat_set()); 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. */ - storm::storage::VectorSet& addValue(ValueType value, storm::storage::VectorSet const& labels) { + boost::container::flat_set& addValue(ValueType value, boost::container::flat_set 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/MaximalEndComponent.cpp b/src/storage/MaximalEndComponent.cpp index 9c01e63bb..eb61a4fa2 100644 --- a/src/storage/MaximalEndComponent.cpp +++ b/src/storage/MaximalEndComponent.cpp @@ -4,6 +4,8 @@ namespace storm { namespace storage { + std::ostream& operator<<(std::ostream& out, boost::container::flat_set const& block); + MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { // Intentionally left empty. } @@ -27,14 +29,14 @@ namespace storm { } void MaximalEndComponent::addState(uint_fast64_t state, std::vector const& choices) { - stateToChoicesMapping[state] = choices; + stateToChoicesMapping[state] = boost::container::flat_set(choices.begin(), choices.end()); } void MaximalEndComponent::addState(uint_fast64_t state, std::vector&& choices) { - stateToChoicesMapping.emplace(state, choices); + stateToChoicesMapping.emplace(state, boost::container::flat_set(choices.begin(), choices.end())); } - storm::storage::VectorSet const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { + boost::container::flat_set const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { auto stateChoicePair = stateToChoicesMapping.find(state); if (stateChoicePair == stateToChoicesMapping.end()) { @@ -80,10 +82,10 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC."; } - return stateChoicePair->second.contains(choice); + return stateChoicePair->second.find(choice) != stateChoicePair->second.end(); } - storm::storage::VectorSet MaximalEndComponent::getStateSet() const { + boost::container::flat_set MaximalEndComponent::getStateSet() const { std::vector states; states.reserve(stateToChoicesMapping.size()); @@ -91,7 +93,7 @@ namespace storm { states.push_back(stateChoicesPair.first); } - return storm::storage::VectorSet(states); + return boost::container::flat_set(states.begin(), states.end()); } std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) { diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h index c6b92540f..3efc70386 100644 --- a/src/storage/MaximalEndComponent.h +++ b/src/storage/MaximalEndComponent.h @@ -2,8 +2,7 @@ #define STORM_STORAGE_MAXIMALENDCOMPONENT_H_ #include - -#include "src/storage/VectorSet.h" +#include namespace storm { namespace storage { @@ -12,8 +11,8 @@ namespace storm { */ class MaximalEndComponent { public: - typedef std::unordered_map>::iterator iterator; - typedef std::unordered_map>::const_iterator const_iterator; + typedef std::unordered_map>::iterator iterator; + typedef std::unordered_map>::const_iterator const_iterator; /*! * Creates an empty MEC. @@ -51,7 +50,7 @@ namespace storm { * @param state The state for which to retrieve the choices. * @return A list of choices of the state in the MEC. */ - storm::storage::VectorSet const& getChoicesForState(uint_fast64_t state) const; + boost::container::flat_set const& getChoicesForState(uint_fast64_t state) const; /*! * Removes the given choice from the list of choices of the named state. @@ -90,7 +89,7 @@ namespace storm { * * @return The set of states contained in the MEC. */ - storm::storage::VectorSet getStateSet() const; + boost::container::flat_set getStateSet() const; iterator begin(); @@ -104,7 +103,7 @@ namespace storm { private: // This stores the mapping from states contained in the MEC to the choices in this MEC. - std::unordered_map> stateToChoicesMapping; + std::unordered_map> stateToChoicesMapping; }; } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index e47d6537a..7fb3a31be 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -52,7 +52,7 @@ namespace storm { // Initialize the maximal end component list to be the full state space. std::list endComponentStateSets; - endComponentStateSets.emplace_back(subsystem); + endComponentStateSets.emplace_back(subsystem.begin(), subsystem.end()); storm::storage::BitVector statesToCheck(model.getNumberOfStates()); @@ -83,7 +83,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (!scc.contains(entry.first)) { + if (scc.find(entry.first) == scc.end()) { choiceContainedInMEC = false; break; } @@ -103,13 +103,15 @@ namespace storm { // Now erase the states that have no option to stay inside the MEC with all successors. mecChanged |= !statesToRemove.empty(); - scc.erase(storm::storage::VectorSet(statesToRemove.begin(), statesToRemove.end())); + for (uint_fast64_t state : statesToRemove) { + scc.erase(state); + } // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); for (auto state : statesToRemove) { for (auto const& entry : transitionMatrix.getRow(state)) { - if (scc.contains(entry.first)) { + if (scc.find(entry.first) != scc.end()) { statesToCheck.set(entry.first); } } @@ -145,7 +147,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContained = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (!mecStateSet.contains(entry.first)) { + if (mecStateSet.find(entry.first) == mecStateSet.end()) { choiceContained = false; break; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 87f19e538..d30412c24 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -72,7 +72,7 @@ namespace storm { } else { columnsAndValues.emplace_back(column, value); if (!columnCountSet) { - columnCount = column + 1; + columnCount = std::max(columnCount, column + 1); } if (!rowCountSet) { rowCount = row + 1; @@ -661,7 +661,25 @@ namespace storm { template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB - tbb::parallel_for(tbb::blocked_range(0, result.size()), TbbMatrixRowVectorScalarProduct(*this, vector, result)); + tbb::parallel_for(tbb::blocked_range(0, result.size()), + [&] (tbb::blocked_range const& range) { + uint_fast64_t startRow = range.begin(); + uint_fast64_t endRow = range.end(); + const_iterator it = this->begin(startRow); + const_iterator ite; + typename std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; + typename std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; + typename std::vector::iterator resultIterator = result.begin() + startRow; + typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { + *resultIterator = storm::utility::constantZero(); + + for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { + *resultIterator += it->second * vector[it->first]; + } + } + }); #else const_iterator it = this->begin(); const_iterator ite; @@ -832,36 +850,6 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); -#ifdef STORM_HAVE_INTELTBB - template - TbbMatrixRowVectorScalarProduct::TbbMatrixRowVectorScalarProduct(SparseMatrix const& matrix, std::vector const& vector, std::vector& result) : result(result), vector(vector), matrix(matrix) { - // Intentionally left empty. - } - - template - void TbbMatrixRowVectorScalarProduct::operator() (tbb::blocked_range const& range) const { - uint_fast64_t startRow = range.begin(); - uint_fast64_t endRow = range.end(); - typename SparseMatrix::const_iterator it = matrix.begin(startRow); - typename SparseMatrix::const_iterator ite; - typename std::vector::const_iterator rowIterator = matrix.rowIndications.begin() + startRow; - typename std::vector::const_iterator rowIteratorEnd = matrix.rowIndications.begin() + endRow; - typename std::vector::iterator resultIterator = result.begin() + startRow; - typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; - - for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { - *resultIterator = storm::utility::constantZero(); - - for (ite = matrix.begin() + *(rowIterator + 1); it != ite; ++it) { - *resultIterator += it->second * vector[it->first]; - } - } - } - - // Explicitly instantiate the helper class. - template class TbbMatrixRowVectorScalarProduct; -#endif - } // namespace storage } // namespace storm diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 0ddcbf8e6..7f62ee16f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -34,12 +34,6 @@ namespace storm { namespace storm { namespace storage { -#ifdef STORM_HAVE_INTELTBB - // Forward declaration of the TBB Helper class. - template - class TbbMatrixRowVectorScalarProduct; -#endif - // Forward declare matrix class. template class SparseMatrix; @@ -159,12 +153,6 @@ namespace storm { friend class storm::adapters::EigenAdapter; friend class storm::adapters::StormAdapter; -#ifdef STORM_HAVE_INTELTBB - // Declare the helper class for TBB as friend. - template - friend class TbbMatrixRowVectorScalarProduct; -#endif - typedef typename std::vector>::iterator iterator; typedef typename std::vector const>::const_iterator const_iterator; @@ -619,42 +607,7 @@ namespace storm { // entry is not included anymore. std::vector rowIndications; }; - -#ifdef STORM_HAVE_INTELTBB - /*! - * This class is a helper class for parallel matrix-vector multiplication using Intel TBB. - */ - template - class TbbMatrixRowVectorScalarProduct { - public: - /*! - * Constructs a helper object with which TBB can perform parallel matrix-vector multiplication. - * - * @param matrix The matrix to use for the multiplication. - * @param vector The vector with which to multiply the matrix. - * @param result The vector that is supposed to hold the result after performing the multiplication. - */ - TbbMatrixRowVectorScalarProduct(SparseMatrix const& matrix, std::vector const& vector, std::vector& result); - - /*! - * Performs the actual multiplication of a range of rows with the given vector. - * - * @param range The range of rows to multiply with the given vector. - */ - void operator() (tbb::blocked_range const& range) const; - - private: - // The vector that is supposed to hold the result after performing the multiplication. - std::vector& result; - - // The vector with which to multiply the matrix. - std::vector const& vector; - - // The matrix to use for the multiplication. - SparseMatrix const& matrix; - }; -#endif - + } // namespace storage } // namespace storm diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 369809ea6..56a142e2f 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -1,9 +1,10 @@ #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ +#include + #include "src/storage/SparseMatrix.h" #include "src/storage/Decomposition.h" -#include "src/storage/VectorSet.h" #include "src/storage/BitVector.h" diff --git a/src/storage/VectorSet.cpp b/src/storage/VectorSet.cpp deleted file mode 100644 index bd5cc0a2e..000000000 --- a/src/storage/VectorSet.cpp +++ /dev/null @@ -1,299 +0,0 @@ -#include "src/storage/VectorSet.h" -#include "src/storage/BitVector.h" - -namespace storm { - namespace storage { - template - VectorSet::VectorSet() : data(), dirty(false) { - // Intentionally left empty. - } - - template - VectorSet::VectorSet(uint_fast64_t size) : data(), dirty(false) { - data.reserve(size); - } - - template - template - VectorSet::VectorSet(InputIterator first, InputIterator last) : dirty(true) { - this->data.insert(this->data.end(), first, last); - } - - template - VectorSet::VectorSet(std::vector const& data) : data(data), dirty(true) { - ensureSet(); - } - - template - VectorSet::VectorSet(std::set const& data) : dirty(false) { - this->data.reserve(data.size()); - for (auto const& element : data) { - this->data.push_back(element); - } - } - - template - VectorSet::VectorSet(storm::storage::BitVector const& data) : dirty(false) { - this->data.reserve(data.getNumberOfSetBits()); - for (auto element : data) { - this->data.push_back(element); - } - } - - template - VectorSet::VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { - data.reserve(to - from); - - for (uint_fast64_t element = from; element < to; ++element) { - data.push_back(element); - } - } - - template - VectorSet::VectorSet(VectorSet const& other) : dirty(false) { - other.ensureSet(); - data = other.data; - } - - template - VectorSet& VectorSet::operator=(VectorSet const& other) { - data = other.data; - dirty = other.dirty; - return *this; - } - - template - VectorSet::VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) { - // Intentionally left empty. - } - - template - VectorSet& VectorSet::operator=(VectorSet&& other) { - data = std::move(other.data); - dirty = std::move(other.dirty); - return *this; - } - - template - bool VectorSet::operator==(VectorSet const& other) const { - ensureSet(); - if (this->size() != other.size()) return false; - return std::equal(data.begin(), data.end(), other.begin()); - } - - template - bool VectorSet::operator<(VectorSet const& other) const { - ensureSet(); - 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; - } - - template - bool VectorSet::operator>(VectorSet const& other) const { - ensureSet(); - 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; - } - - template - void VectorSet::ensureSet() const { - if (dirty) { - std::sort(data.begin(), data.end()); - data.erase(std::unique(data.begin(), data.end()), data.end()); - dirty = false; - } - } - - template - bool VectorSet::contains(ValueType const& element) const { - ensureSet(); - return std::binary_search(data.begin(), data.end(), element); - } - - template - bool VectorSet::subsetOf(VectorSet const& other) const { - ensureSet(); - other.ensureSet(); - return std::includes(other.begin(), other.end(), data.begin(), data.end()); - } - - template - bool VectorSet::supersetOf(VectorSet const& other) const { - ensureSet(); - return other.subsetOf(*this); - } - - template - VectorSet 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; - } - - template - VectorSet 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; - } - - template - typename VectorSet::iterator VectorSet::begin() { - ensureSet(); - return data.begin(); - } - - template - typename VectorSet::iterator VectorSet::end() { - ensureSet(); - return data.end(); - } - - template - typename VectorSet::const_iterator VectorSet::begin() const { - ensureSet(); - return data.begin(); - } - - template - typename VectorSet::const_iterator VectorSet::end() const { - ensureSet(); - return data.end(); - } - - template - ValueType const& VectorSet::min() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.front(); - } - - template - ValueType const& VectorSet::max() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.back(); - } - - template - void VectorSet::insert(ValueType const& element) { - data.push_back(element); - dirty = true; - } - - template - typename VectorSet::iterator VectorSet::insert(typename VectorSet::iterator pos, ValueType const& element) { - dirty = true; - return data.insert(pos, element); - } - - template - void VectorSet::insert(VectorSet const& other) { - data.insert(data.end(), other.data.begin(), other.data.end()); - dirty = true; - } - - template - bool VectorSet::empty() const { - ensureSet(); - return data.empty(); - } - - template - size_t VectorSet::size() const { - ensureSet(); - return data.size(); - } - - template - void VectorSet::clear() { - data.clear(); - dirty = false; - } - - template - bool VectorSet::erase(ValueType const& element) { - ensureSet(); - uint_fast64_t lowerBound = 0; - uint_fast64_t upperBound = data.size(); - while (lowerBound != upperBound) { - uint_fast64_t currentPosition = lowerBound + (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; - } - - template - void VectorSet::erase(VectorSet const& eraseSet) { - if (eraseSet.size() > 0 && this->size() > 0) { - ensureSet(); - eraseSet.ensureSet(); - - for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { - while (setIt != eraseSet.data.rend() && *setIt > *delIt) { - ++setIt; - } - if (setIt == data.rend()) break; - - if (*setIt == *delIt) { - data.erase((setIt + 1).base()); - ++setIt; - } - } - } - } - - template - 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; - } - - template class VectorSet; - template class VectorSet>; - template VectorSet::VectorSet(storm::storage::BitVector::const_iterator, storm::storage::BitVector::const_iterator); - template std::ostream& operator<<(std::ostream& stream, VectorSet const& set); - template std::ostream& operator<<(std::ostream& stream, VectorSet> const& set); - } -} diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h deleted file mode 100644 index 389e19b54..000000000 --- a/src/storage/VectorSet.h +++ /dev/null @@ -1,116 +0,0 @@ -/* - * VectorSet.h - * - * Created on: 23.10.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_STORAGE_VECTORSET_H -#define STORM_STORAGE_VECTORSET_H - -#include -#include -#include -#include -#include -#include - -#include "src/exceptions/InvalidStateException.h" - -namespace storm { - namespace storage { - - // Forward declare bit vector class. - class BitVector; - - template - class VectorSet { - public: - typedef ValueType* difference_type; - typedef ValueType value_type; - typedef ValueType* pointer; - typedef ValueType& reference; - typedef typename std::vector::iterator iterator; - typedef typename std::vector::const_iterator const_iterator; - - VectorSet(); - - VectorSet(uint_fast64_t size); - - template - VectorSet(InputIterator first, InputIterator last); - - VectorSet(std::vector const& data); - - VectorSet(std::set const& data); - - VectorSet(BitVector const& data); - - VectorSet(uint_fast64_t from, uint_fast64_t to); - - VectorSet(VectorSet const& other); - - VectorSet& operator=(VectorSet const& other); - - VectorSet(VectorSet&& other); - - VectorSet& operator=(VectorSet&& other); - - bool operator==(VectorSet const& other) const; - - bool operator<(VectorSet const& other) const; - - bool operator>(VectorSet const& other) const; - - void ensureSet() const; - - bool contains(ValueType const& element) const; - - bool subsetOf(VectorSet const& other) const; - - bool supersetOf(VectorSet const& other) const; - - VectorSet intersect(VectorSet const& other); - - VectorSet join(VectorSet const& other); - - iterator begin(); - - iterator end(); - - const_iterator begin() const; - - const_iterator end() const; - - ValueType const& min() const; - - ValueType const& max() const; - - void insert(ValueType const& element); - - // FIXME: As soon as gcc provides an erase(const_iterator) method, change this iterator back to a const_iterator. - iterator insert(iterator pos, ValueType const& element); - - void insert(VectorSet const& other); - - bool empty() const; - - size_t size() const; - - void clear(); - - bool erase(ValueType const& element); - - void erase(VectorSet const& eraseSet); - - template - friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set); - - private: - mutable std::vector data; - mutable bool dirty; - }; - } -} - -#endif /* STORM_STORAGE_VECTORSET_H */ diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h index dda032a12..a75f1972d 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(storm::storage::VectorSet const& labelSet) { + void addChoiceLabels(boost::container::flat_set 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. */ - storm::storage::VectorSet const& getChoiceLabels() const { + boost::container::flat_set const& getChoiceLabels() const { return choiceLabels; } @@ -224,7 +224,7 @@ namespace storm { std::string actionLabel; // The labels that are associated with this choice. - storm::storage::VectorSet choiceLabels; + boost::container::flat_set 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, storm::storage::VectorSet const& labels) { + void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set 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, storm::storage::VectorSet const& labels) { + void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set const& labels) { auto& labeledEntry = choice.getOrAddEntry(state); labeledEntry.addValue(probability, labels); } diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index 12358fd85..85efce7fe 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -20,20 +20,20 @@ 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, storm::storage::VectorSet const& relevantLabels) { + std::vector> getGuaranteedLabelSets(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, boost::container::flat_set 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. for (auto state : psiStates) { - analysisInformation[state] = std::set(); + analysisInformation[state] = boost::container::flat_set(); for (auto& predecessorEntry : backwardTransitions.getRow(state)) { if (predecessorEntry.first != state) { worklist.push(std::make_pair(predecessorEntry.first, state)); @@ -53,7 +53,7 @@ namespace storm { // Iterate over the successor states for all choices and compute new analysis information. for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { - storm::storage::VectorSet tmpIntersection; + boost::container::flat_set tmpIntersection; bool choiceTargetsTargetState = false; for (auto& entry : transitionMatrix.getRow(currentChoice)) { @@ -96,13 +96,13 @@ namespace storm { * @return The set of action labels that is visited on all paths from an initial state to a target state. */ template - 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); + boost::container::flat_set getGuaranteedLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels); - storm::storage::VectorSet knownLabels(relevantLabels); - storm::storage::VectorSet tempIntersection; + boost::container::flat_set knownLabels(relevantLabels); + boost::container::flat_set tempIntersection; for (auto initialState : labeledMdp.getInitialStates()) { - tempIntersection = knownLabels.intersect(guaranteedLabels[initialState]); + std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); std::swap(knownLabels, tempIntersection); } diff --git a/src/utility/set.h b/src/utility/set.h deleted file mode 100644 index 7d5d85051..000000000 --- a/src/utility/set.h +++ /dev/null @@ -1,53 +0,0 @@ -/* - * set.h - * - * Created on: 06.12.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_UTILITY_SET_H_ -#define STORM_UTILITY_SET_H_ - -#include - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; - -namespace storm { - namespace utility { - namespace set { - - template - bool isSubsetOf(std::set const& set1, std::set const& set2) { - // First, get a comparator object. - typename std::set::key_compare comparator = set1.key_comp(); - - for (typename std::set::const_iterator it1 = set1.begin(), it2 = set2.begin(); it1 != set1.end() && it2 != set2.end(); ++it1) { - // If the value in set1 is smaller than the value in set2, set1 is not a subset of set2. - if (comparator(*it1, *it2)) { - return false; - } - - // If the value in the second set is smaller, we need to move the iterator until the comparison is false. - while(comparator(*it2, *it1) && it2 != set2.end()) { - ++it2; - } - - // If we have reached the end of set2 or the element we found is actually larger than the one in set1 - // we know that the subset property is violated. - if (it2 == set2.end() || comparator(*it1, *it2)) { - return false; - } - - // Otherwise, we have found an equivalent element and can continue with the next one. - } - return true; - } - - } // namespace set - } // namespace utility -} // namespace storm - -#endif /* STORM_UTILITY_SET_H_ */ diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 82fd9ec5c..ecde843cb 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/OutOfRangeException.h" TEST(SparseMatrixBuilder, CreationWithDimensions) { @@ -54,10 +54,10 @@ TEST(SparseMatrixBuilder, CreationWithNumberOfRows) { TEST(SparseMatrixBuilder, CreationWithoutDimensions) { storm::storage::SparseMatrixBuilder matrixBuilder; ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 3, 1.2)); ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 2, 0.2)); storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build());