From 6a4c18e4a2dee78a4c44fafbd0dcb1b584e0692e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Jun 2019 18:31:02 +0200 Subject: [PATCH] Use custom FlatSet to account for allocator changes in flat_set in Boost 1.70. Boost 1.70 changed the default allocator parameter from new_allocator to void to reduce symbol lenghts. This reverts the default to the old allocator. --- .../MILPMinimalLabelSetGenerator.h | 26 ++-- .../SMTMinimalLabelSetGenerator.h | 133 +++++++++--------- .../parser/SparseChoiceLabelingParser.cpp | 4 +- .../parser/SparseChoiceLabelingParser.h | 5 +- src/storm/generator/Choice.cpp | 7 +- src/storm/generator/JaniNextStateGenerator.h | 5 +- src/storm/generator/PrismNextStateGenerator.h | 5 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- .../exploration/ExplorationInformation.h | 4 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/storage/BitVector.cpp | 11 +- src/storm/storage/BoostTypes.h | 15 ++ src/storm/storage/Decomposition.cpp | 2 +- src/storm/storage/MaximalEndComponent.cpp | 2 +- src/storm/storage/MaximalEndComponent.h | 4 +- src/storm/storage/StateBlock.h | 4 +- src/storm/storage/jani/Automaton.cpp | 2 +- src/storm/storage/jani/Automaton.h | 4 +- src/storm/storage/jani/Edge.cpp | 2 +- src/storm/storage/jani/Edge.h | 4 +- src/storm/storage/jani/Model.cpp | 6 +- src/storm/storage/jani/Model.h | 9 +- src/storm/storage/jani/TemplateEdge.cpp | 2 +- src/storm/storage/jani/TemplateEdge.h | 8 +- src/storm/storage/prism/Module.cpp | 4 +- src/storm/storage/prism/Module.h | 6 +- src/storm/storage/prism/Program.cpp | 4 +- src/storm/storage/prism/Program.h | 4 +- src/storm/storage/prism/RewardModel.cpp | 2 +- src/storm/storage/prism/RewardModel.h | 4 +- src/storm/storage/sparse/JaniChoiceOrigins.h | 5 +- src/storm/storage/sparse/PrismChoiceOrigins.h | 4 +- src/storm/utility/counterexamples.h | 16 +-- 33 files changed, 164 insertions(+), 153 deletions(-) create mode 100644 src/storm/storage/BoostTypes.h diff --git a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h index 52ed50778..a2e6de197 100644 --- a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1,7 +1,6 @@ #pragma once #include -#include #include "storm/models/sparse/Mdp.h" #include "storm/logic/Formulas.h" @@ -26,6 +25,7 @@ #include "storm/storage/sparse/PrismChoiceOrigins.h" #include "storm/storage/sparse/JaniChoiceOrigins.h" +#include "storm/storage/BoostTypes.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -72,8 +72,8 @@ namespace storm { struct ChoiceInformation { std::unordered_map> relevantChoicesForRelevantStates; std::unordered_map> problematicChoicesForProblematicStates; - boost::container::flat_set allRelevantLabels; - boost::container::flat_set knownLabels; + storm::storage::FlatSet allRelevantLabels; + storm::storage::FlatSet knownLabels; }; /*! @@ -125,7 +125,7 @@ namespace storm { * @return A structure that stores the relevant and problematic choices in the model as well as the set * of relevant labels. */ - static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { + static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { // Create result and shortcuts to needed data for convenience. ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); @@ -180,7 +180,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, boost::container::flat_set const& relevantLabels) { + static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, storm::storage::FlatSet const& relevantLabels) { std::stringstream variableNameBuffer; std::unordered_map resultingMap; for (auto const& label : relevantLabels) { @@ -489,7 +489,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; @@ -817,7 +817,7 @@ namespace storm { * @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of * possible choices. */ - static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { + static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { // Assert that the reachability probability in the subsystem exceeds the given threshold. uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound); STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold."); @@ -865,8 +865,8 @@ namespace storm { * @param solver The MILP solver. * @param variableInformation A struct with information about the variables of the model. */ - static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { - boost::container::flat_set result; + static storm::storage::FlatSet getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + storm::storage::FlatSet result; for (auto const& labelVariablePair : variableInformation.labelToVariableMap) { bool labelTaken = solver.getBinaryValue(labelVariablePair.second); @@ -927,7 +927,7 @@ namespace storm { } public: - static boost::container::flat_set getMinimalLabelSet(Environment const& env,storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + static storm::storage::FlatSet getMinimalLabelSet(Environment const& env,storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the label sets are valid STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); @@ -962,7 +962,7 @@ namespace storm { solver->optimize(); // (4.4) Read off result from variables. - boost::container::flat_set usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); + storm::storage::FlatSet usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); // (5) Return result. @@ -1020,7 +1020,7 @@ namespace storm { } // Obtain the label sets for each choice. - std::vector> labelSets(mdp.getNumberOfChoices()); + std::vector> labelSets(mdp.getNumberOfChoices()); if (mdp.getChoiceOrigins()->isPrismChoiceOrigins()) { storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) { @@ -1037,7 +1037,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(env, mdp, labelSets, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); + storm::storage::FlatSet usedLabelSet = getMinimalLabelSet(env, mdp, labelSets, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index d1101d45a..9a66982b0 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -10,6 +10,7 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/storage/BoostTypes.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -56,18 +57,18 @@ namespace storm { storm::storage::BitVector relevantStates; // The set of relevant labels. - boost::container::flat_set relevantLabels; + storm::storage::FlatSet relevantLabels; // The set of relevant label sets. - boost::container::flat_set> relevantLabelSets; + storm::storage::FlatSet> relevantLabelSets; // The set of labels that matter in terms of minimality. - boost::container::flat_set minimalityLabels; + storm::storage::FlatSet minimalityLabels; // A set of labels that is definitely known to be taken in the final solution. - boost::container::flat_set knownLabels; + storm::storage::FlatSet knownLabels; - boost::container::flat_set dontCareLabels; + storm::storage::FlatSet dontCareLabels; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; @@ -124,7 +125,7 @@ namespace storm { * @param dontCareLabels A set of labels that are "don't care" labels wrt. minimality. * @return A structure containing the relevant labels as well as states. */ - static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& dontCareLabels) { + static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& dontCareLabels) { // Create result. RelevancyInformation relevancyInformation; @@ -166,7 +167,7 @@ namespace storm { // Compute the set of labels that are known to be taken in any case. relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); if (!relevancyInformation.knownLabels.empty()) { - boost::container::flat_set remainingLabels; + storm::storage::FlatSet remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); relevancyInformation.relevantLabels = remainingLabels; } @@ -281,7 +282,7 @@ namespace storm { return variableInformation; } - static storm::expressions::Expression getOtherSynchronizationEnabledFormula(boost::container::flat_set const& labelSet, std::map>> const& synchronizingLabels, boost::container::flat_map, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { + static storm::expressions::Expression getOtherSynchronizationEnabledFormula(storm::storage::FlatSet const& labelSet, std::map>> const& synchronizingLabels, boost::container::flat_map, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands @@ -290,7 +291,7 @@ namespace storm { storm::expressions::Expression result = variableInformation.manager->boolean(true); for (auto label : labelSet) { storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); - std::set> const& synchsForCommand = synchronizingLabels.at(label); + std::set> const& synchsForCommand = synchronizingLabels.at(label); for (auto const& synchSet : synchsForCommand) { storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true); @@ -327,7 +328,7 @@ namespace storm { * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. */ - static std::chrono::milliseconds assertCuts(storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver, bool addBackwardImplications) { + static std::chrono::milliseconds assertCuts(storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver, bool addBackwardImplications) { // Walk through the model and // * identify labels enabled in initial states // * identify labels that can directly precede a given action @@ -340,13 +341,13 @@ namespace storm { STORM_LOG_THROW(!symbolicModel.isJaniModel() || !symbolicModel.asJaniModel().usesAssignmentLevels(), storm::exceptions::NotSupportedException, "Counterexample generation with backward implications is not supported for indexed assignments"); } - boost::container::flat_set initialLabels; - std::set> initialCombinations; - boost::container::flat_set targetLabels; - boost::container::flat_set> targetCombinations; - std::map, std::set>> precedingLabels; - std::map, std::set>> followingLabels; - std::map>> synchronizingLabels; + storm::storage::FlatSet initialLabels; + std::set> initialCombinations; + storm::storage::FlatSet targetLabels; + storm::storage::FlatSet> targetCombinations; + std::map, std::set>> precedingLabels; + std::map, std::set>> followingLabels; + std::map>> synchronizingLabels; // Get some data from the model for convenient access. storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); @@ -413,7 +414,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; if (addBackwardImplications) { // Create a new solver over the same variables as the given symbolic model description to use it for // determining the symbolic cuts. @@ -671,7 +672,7 @@ namespace storm { STORM_LOG_DEBUG("Successfully gathered data for cuts."); // Compute the sets of labels such that the transitions labeled with this set possess at least one known label. - boost::container::flat_set> hasKnownSuccessor; + storm::storage::FlatSet> hasKnownSuccessor; for (auto const& labelSetFollowingSetsPair : followingLabels) { for (auto const& set : labelSetFollowingSetsPair.second) { if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { @@ -682,7 +683,7 @@ namespace storm { } // Compute the sets of labels such that the transitions labeled with this set possess at least one known predecessor. - boost::container::flat_set> hasKnownPredecessor; + storm::storage::FlatSet> hasKnownPredecessor; for (auto const& labelSetImplicationsPair : backwardImplications) { for (auto const& set : labelSetImplicationsPair.second) { if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { @@ -700,7 +701,7 @@ namespace storm { // combination that is already known. Otherwise this condition would be too strong. bool initialCombinationKnown = false; for (auto const& combination : initialCombinations) { - boost::container::flat_set tmpSet; + storm::storage::FlatSet 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; @@ -725,7 +726,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) { - boost::container::flat_set tmpSet; + storm::storage::FlatSet 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; @@ -746,12 +747,12 @@ namespace storm { if(addBackwardImplications) { STORM_LOG_DEBUG("Asserting taken labels are followed and preceeded by another label if they are not a target label or an initial label, respectively."); - boost::container::flat_map, storm::expressions::Expression> labelSetToFormula; + boost::container::flat_map, storm::expressions::Expression> labelSetToFormula; for (auto const &labelSet : relevancyInformation.relevantLabelSets) { storm::expressions::Expression labelSetFormula = variableInformation.manager->boolean(false); // Compute the set of unknown labels on the left-hand side of the implication. - boost::container::flat_set unknownLhsLabels; + storm::storage::FlatSet unknownLhsLabels; std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); for (auto label : unknownLhsLabels) { labelSetFormula = labelSetFormula || !variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); @@ -766,7 +767,7 @@ namespace storm { auto const &followingLabelSets = followingLabels.at(labelSet); for (auto const &followingSet : followingLabelSets) { - boost::container::flat_set tmpSet; + storm::storage::FlatSet 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. @@ -799,7 +800,7 @@ namespace storm { auto const &preceedingLabelSets = backwardImplications.at(labelSet); for (auto const &preceedingSet : preceedingLabelSets) { - boost::container::flat_set tmpSet; + storm::storage::FlatSet 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. @@ -868,7 +869,7 @@ namespace storm { /*! * Asserts constraints necessary to encode the reachability of at least one target state from the initial states. */ - static void assertReachabilityCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertReachabilityCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { if (!variableInformation.hasReachabilityVariables) { throw storm::exceptions::InvalidStateException() << "Impossible to assert reachability cuts without the necessary variables."; @@ -885,14 +886,14 @@ namespace storm { for (auto relevantState : relevancyInformation.relevantStates) { if (!model.getInitialStates().get(relevantState)) { // Assert the constraints (1). - boost::container::flat_set relevantPredecessors; + storm::storage::FlatSet relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { if (relevantState != predecessorEntry.getColumn() && relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) { relevantPredecessors.insert(predecessorEntry.getColumn()); } } - boost::container::flat_set relevantSuccessors; + storm::storage::FlatSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (relevantState != successorEntry.getColumn() && (relevancyInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn()))) { @@ -912,7 +913,7 @@ namespace storm { solver.add(expression); } else { // Assert the constraints (2). - boost::container::flat_set relevantSuccessors; + storm::storage::FlatSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (relevantState != successorEntry.getColumn() && (relevancyInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn()))) { @@ -936,7 +937,7 @@ namespace storm { uint_fast64_t targetState = statePairIndexPair.first.second; // Assert constraint for (1). - boost::container::flat_set choicesForStatePair; + storm::storage::FlatSet choicesForStatePair; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { if (successorEntry.getColumn() == targetState) { @@ -1163,8 +1164,8 @@ namespace storm { * @param model The model from which to extract the information. * @param variableInformation A structure with information about the variables of the solver. */ - static boost::container::flat_set getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { - boost::container::flat_set result; + static storm::storage::FlatSet getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { + storm::storage::FlatSet result; for (auto const& labelIndexPair : variableInformation.labelToIndexMap) { bool commandIncluded = model.getBooleanValue(variableInformation.labelVariables.at(labelIndexPair.second)); @@ -1213,7 +1214,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 boost::optional> findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { + static boost::optional> findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { // Check if we can find a solution with the current bound. storm::expressions::Expression assumption = !variableInformation.auxiliaryVariables.back(); @@ -1239,10 +1240,10 @@ namespace storm { return getUsedLabelSet(*solver.getModel(), variableInformation); } - static void ruleOutSingleSolution(storm::solver::SmtSolver& solver, boost::container::flat_set const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void ruleOutSingleSolution(storm::solver::SmtSolver& solver, storm::storage::FlatSet const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { std::vector formulae; - boost::container::flat_set unknownLabels; + storm::storage::FlatSet unknownLabels; std::set_intersection(labelSet.begin(), labelSet.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); //std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); @@ -1250,7 +1251,7 @@ namespace storm { formulae.emplace_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - boost::container::flat_set remainingLabels; + storm::storage::FlatSet remainingLabels; //std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); std::set_difference(relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); @@ -1262,10 +1263,10 @@ namespace storm { assertDisjunction(solver, formulae, *variableInformation.manager); } - static void ruleOutBiggerSolutions(storm::solver::SmtSolver& solver, boost::container::flat_set const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void ruleOutBiggerSolutions(storm::solver::SmtSolver& solver, storm::storage::FlatSet const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { std::vector formulae; - boost::container::flat_set unknownLabels; + storm::storage::FlatSet unknownLabels; std::set_intersection(labelSet.begin(), labelSet.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); //std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); @@ -1289,7 +1290,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(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { storm::storage::BitVector reachableStates(subModel.getNumberOfStates()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); @@ -1307,7 +1308,7 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. - boost::container::flat_set reachableLabels; + storm::storage::FlatSet reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1345,15 +1346,15 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantLabels; + storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); STORM_LOG_DEBUG("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::set> cutLabels; + std::set> cutLabels; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) { @@ -1367,7 +1368,7 @@ namespace storm { } if (isBorderChoice) { - boost::container::flat_set currentLabelSet; + storm::storage::FlatSet currentLabelSet; std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin())); std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); @@ -1379,9 +1380,9 @@ namespace storm { // Given the results of the previous analysis, we construct the implications. std::vector formulae; - boost::container::flat_set unknownReachableLabels; + storm::storage::FlatSet unknownReachableLabels; std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - boost::container::flat_set unknownReachableMinimalityLabels; + storm::storage::FlatSet unknownReachableMinimalityLabels; std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end())); for (auto label : unknownReachableMinimalityLabels) { @@ -1412,7 +1413,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(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { STORM_LOG_DEBUG("Analyzing solution with insufficient probability."); @@ -1430,7 +1431,7 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. - boost::container::flat_set reachableLabels; + storm::storage::FlatSet reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1462,17 +1463,17 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantLabels; + storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. - std::set> cutLabels; + std::set> cutLabels; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) { - boost::container::flat_set currentLabelSet; + storm::storage::FlatSet currentLabelSet; std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin())); std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); @@ -1483,9 +1484,9 @@ namespace storm { // Given the results of the previous analysis, we construct the implications std::vector formulae; - boost::container::flat_set unknownReachableLabels; + storm::storage::FlatSet unknownReachableLabels; std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - boost::container::flat_set unknownReachableMinimalityLabels; + storm::storage::FlatSet unknownReachableMinimalityLabels; std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end())); for (auto label : unknownReachableMinimalityLabels) { @@ -1510,11 +1511,11 @@ namespace storm { * Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet. * Also returns the Labelsets of the sub-model. */ - static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet, boost::optional absorbState = boost::none) { + static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, storm::storage::FlatSet const& filterLabelSet, boost::optional absorbState = boost::none) { bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp); - std::vector> resultLabelSet; + std::vector> resultLabelSet; storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, customRowGrouping, model.getTransitionMatrix().getRowGroupCount()); // Check for each choice of each state, whether the choice commands are fully contained in the given command set. @@ -1643,11 +1644,11 @@ namespace storm { * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). * @param options A set of options for customization. */ - static std::vector> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector propertyThreshold, boost::optional> const& rewardName, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { + static std::vector> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector propertyThreshold, boost::optional> const& rewardName, bool strictBound, storm::storage::FlatSet const& dontCareLabels = storm::storage::FlatSet(), Options const& options = Options()) { #ifdef STORM_HAVE_Z3 STORM_LOG_THROW(propertyThreshold.size() > 0, storm::exceptions::InvalidArgumentException, "At least one threshold has to be specified."); STORM_LOG_THROW(propertyThreshold.size() == 1 || (rewardName && rewardName.get().size() == propertyThreshold.size()), storm::exceptions::InvalidArgumentException, "Multiple thresholds is only supported for multiple reward structures"); - std::vector> result; + std::vector> result; // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); @@ -1670,7 +1671,7 @@ namespace storm { STORM_LOG_THROW(model.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origins."); STORM_LOG_THROW(model.getChoiceOrigins()->isPrismChoiceOrigins() || model.getChoiceOrigins()->isJaniChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for model without PRISM or JANI choice origins."); - std::vector> labelSets(model.getNumberOfChoices()); + std::vector> labelSets(model.getNumberOfChoices()); if (model.getChoiceOrigins()->isPrismChoiceOrigins()) { storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = model.getChoiceOrigins()->asPrismChoiceOrigins(); for (uint_fast64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { @@ -1730,7 +1731,7 @@ namespace storm { // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from // the solver. - boost::container::flat_set commandSet(relevancyInformation.knownLabels); + storm::storage::FlatSet commandSet(relevancyInformation.knownLabels); // If there are no relevant labels, return directly. if (relevancyInformation.relevantLabels.empty()) { @@ -1758,7 +1759,7 @@ namespace storm { } STORM_LOG_DEBUG("Computing minimal command set."); solverClock = std::chrono::high_resolution_clock::now(); - boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound); + boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound); totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; if(smallest == boost::none) { STORM_LOG_DEBUG("No further counterexamples."); @@ -1784,7 +1785,7 @@ namespace storm { auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0)); std::shared_ptr> const& subModel = subChoiceOrigins.first; - std::vector> const& subLabelSets = subChoiceOrigins.second; + std::vector> const& subLabelSets = subChoiceOrigins.second; // Now determine the maximal reachability probability in the sub-model. maximalPropertyValue = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates, rewardName); @@ -1864,7 +1865,7 @@ namespace storm { stats.iterations = iterations; if (storm::settings::getModule().isShowStatisticsSet()) { - boost::container::flat_set allLabels; + storm::storage::FlatSet allLabels; for (auto const& e : labelSets) { allLabels.insert(e.begin(), e.end()); } @@ -1894,7 +1895,7 @@ namespace storm { #endif } - static void extendLabelSetLowerBound(storm::models::sparse::Model const& model, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) { + static void extendLabelSetLowerBound(storm::models::sparse::Model const& model, storm::storage::FlatSet& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) { auto startTime = std::chrono::high_resolution_clock::now(); // Create sub-model that only contains the choices allowed by the given command set. @@ -2080,7 +2081,7 @@ namespace storm { } - static std::vector> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, CexInput const& counterexInput, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options(true)) { + static std::vector> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, CexInput const& counterexInput, storm::storage::FlatSet const& dontCareLabels = storm::storage::FlatSet(), Options const& options = Options(true)) { STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models."); // Delegate the actual computation work to the function of equal name. diff --git a/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp index 452045319..8a741aaa5 100644 --- a/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp @@ -12,7 +12,7 @@ namespace storm { using namespace storm::utility::cstring; - std::vector> SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { + std::vector> SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); @@ -20,7 +20,7 @@ namespace storm { uint_fast64_t totalNumberOfChoices = nondeterministicChoiceIndices.back(); // Create choice labeling vector with given choice count. - std::vector> result(totalNumberOfChoices); + std::vector> result(totalNumberOfChoices); // Now parse state reward assignments. uint_fast64_t state = 0; diff --git a/src/storm-parsers/parser/SparseChoiceLabelingParser.h b/src/storm-parsers/parser/SparseChoiceLabelingParser.h index a0b509b69..873ad6e04 100644 --- a/src/storm-parsers/parser/SparseChoiceLabelingParser.h +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.h @@ -1,10 +1,11 @@ #ifndef STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ #define STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ -#include #include #include +#include "storm/storage/BoostTypes.h" + namespace storm { namespace parser { /*! @@ -20,7 +21,7 @@ namespace storm { * @param filename The name of the file to parse. * @return The resulting choice labeling. */ - static std::vector> parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename); + static std::vector> parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename); }; } } diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index be5f597da..43189e623 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -1,7 +1,5 @@ #include "storm/generator/Choice.h" -#include - #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" @@ -10,6 +8,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace generator { @@ -101,9 +100,9 @@ namespace storm { if (!data.empty()) { // Reaching this point means that the both the existing and the given data are non-empty - auto existingDataAsIndexSet = boost::any_cast>(&this->originData.get()); + auto existingDataAsIndexSet = boost::any_cast>(&this->originData.get()); if (existingDataAsIndexSet != nullptr) { - auto givenDataAsIndexSet = boost::any_cast>(&data); + auto givenDataAsIndexSet = boost::any_cast>(&data); STORM_LOG_THROW(givenDataAsIndexSet != nullptr, storm::exceptions::InvalidOperationException, "Types of existing and given choice origin data do not match."); existingDataAsIndexSet->insert(givenDataAsIndexSet->begin(), givenDataAsIndexSet->end()); } else { diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index a5bcb0450..1979acf05 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -1,13 +1,12 @@ #pragma once -#include - #include "storm/generator/NextStateGenerator.h" #include "storm/generator/TransientVariableInformation.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/ArrayEliminator.h" #include "storm/storage/jani/OrderedAssignments.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace builder { @@ -28,7 +27,7 @@ namespace storm { class JaniNextStateGenerator : public NextStateGenerator { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - typedef boost::container::flat_set EdgeIndexSet; + typedef storm::storage::FlatSet EdgeIndexSet; enum class EdgeFilter {All, WithRate, WithoutRate}; JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 41be2912d..4b643e48b 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -1,11 +1,10 @@ #ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ #define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ -#include - #include "storm/generator/NextStateGenerator.h" #include "storm/storage/prism/Program.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace builder { @@ -21,7 +20,7 @@ namespace storm { class PrismNextStateGenerator : public NextStateGenerator { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - typedef boost::container::flat_set CommandSet; + typedef storm::storage::FlatSet CommandSet; enum class CommandFilter {All, Markovian, Probabilistic}; PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index b1d8ffea9..ef5518668 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -777,7 +777,7 @@ namespace storm { for (auto const& stateChoicesPair : mec) { uint64_t state = stateChoicesPair.first; - boost::container::flat_set const& choicesInMec = stateChoicesPair.second; + storm::storage::FlatSet const& choicesInMec = stateChoicesPair.second; for (uint64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { diff --git a/src/storm/modelchecker/exploration/ExplorationInformation.h b/src/storm/modelchecker/exploration/ExplorationInformation.h index 648d325af..0e20f9980 100644 --- a/src/storm/modelchecker/exploration/ExplorationInformation.h +++ b/src/storm/modelchecker/exploration/ExplorationInformation.h @@ -6,13 +6,13 @@ #include #include -#include #include "storm/solver/OptimizationDirection.h" #include "storm/generator/CompressedState.h" #include "storm/storage/SparseMatrix.h" +#include "storm/storage/BoostTypes.h" #include "storm/settings/modules/ExplorationSettings.h" @@ -23,7 +23,7 @@ namespace storm { class ExplorationInformation { public: typedef StateType ActionType; - typedef boost::container::flat_set StateSet; + typedef storm::storage::FlatSet StateSet; typedef std::unordered_map IdToStateMap; typedef typename IdToStateMap::const_iterator const_iterator; typedef std::vector>> MatrixType; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index dcadd10f8..85817db72 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1320,7 +1320,7 @@ namespace storm { for (auto const& stateChoicesPair : mec) { uint_fast64_t state = stateChoicesPair.first; - boost::container::flat_set const& choicesInMec = stateChoicesPair.second; + storm::storage::FlatSet const& choicesInMec = stateChoicesPair.second; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 616d2b424..d66af49b0 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1,4 +1,3 @@ -#include #include #include @@ -6,6 +5,8 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/OutOfRangeException.h" +#include "storm/storage/BoostTypes.h" + #include "storm/utility/OsDetection.h" #include "storm/utility/Hash.h" #include "storm/utility/macros.h" @@ -1216,12 +1217,12 @@ 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 BitVector::BitVector(uint_fast64_t length, storm::storage::FlatSet::iterator begin, storm::storage::FlatSet::iterator end); + template BitVector::BitVector(uint_fast64_t length, storm::storage::FlatSet::const_iterator begin, storm::storage::FlatSet::const_iterator end); template void BitVector::set(std::vector::iterator begin, std::vector::iterator end, bool value); template void BitVector::set(std::vector::const_iterator begin, std::vector::const_iterator end, bool value); - template void BitVector::set(boost::container::flat_set::iterator begin, boost::container::flat_set::iterator end, bool value); - template void BitVector::set(boost::container::flat_set::const_iterator begin, boost::container::flat_set::const_iterator end, bool value); + template void BitVector::set(storm::storage::FlatSet::iterator begin, storm::storage::FlatSet::iterator end, bool value); + template void BitVector::set(storm::storage::FlatSet::const_iterator begin, storm::storage::FlatSet::const_iterator end, bool value); template struct Murmur3BitVectorHash; template struct Murmur3BitVectorHash; diff --git a/src/storm/storage/BoostTypes.h b/src/storm/storage/BoostTypes.h new file mode 100644 index 000000000..3808f634b --- /dev/null +++ b/src/storm/storage/BoostTypes.h @@ -0,0 +1,15 @@ +#pragma once + +#include + +namespace storm { + namespace storage { + + /*! + * Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void. + */ + template + using FlatSet = boost::container::flat_set, boost::container::new_allocator>; + + } +} diff --git a/src/storm/storage/Decomposition.cpp b/src/storm/storage/Decomposition.cpp index 494cd01f5..efe850083 100644 --- a/src/storm/storage/Decomposition.cpp +++ b/src/storm/storage/Decomposition.cpp @@ -106,7 +106,7 @@ namespace storm { block_type const& block = this->getBlock(currentBlockIndex); // Now, we determine the blocks which are reachable (in one step) from the current block. - boost::container::flat_set allTargetBlocks; + storm::storage::FlatSet allTargetBlocks; for (auto state : block) { for (auto const& transitionEntry : matrix.getRowGroup(state)) { uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()]; diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp index a704eea46..d6e080583 100644 --- a/src/storm/storage/MaximalEndComponent.cpp +++ b/src/storm/storage/MaximalEndComponent.cpp @@ -4,7 +4,7 @@ namespace storm { namespace storage { - std::ostream& operator<<(std::ostream& out, boost::container::flat_set const& block); + std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet const& block); MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { // Intentionally left empty. diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index 7f7100c4a..c46a4c0d6 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -2,9 +2,9 @@ #define STORM_STORAGE_MAXIMALENDCOMPONENT_H_ #include -#include #include "storm/storage/sparse/StateType.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace storage { @@ -14,7 +14,7 @@ namespace storm { */ class MaximalEndComponent { public: - typedef boost::container::flat_set set_type; + typedef storm::storage::FlatSet set_type; typedef std::unordered_map map_type; typedef map_type::iterator iterator; typedef map_type::const_iterator const_iterator; diff --git a/src/storm/storage/StateBlock.h b/src/storm/storage/StateBlock.h index 40f834825..9098c5338 100644 --- a/src/storm/storage/StateBlock.h +++ b/src/storm/storage/StateBlock.h @@ -3,17 +3,17 @@ #include -#include #include #include "storm/utility/OsDetection.h" #include "storm/storage/sparse/StateType.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace storage { // Typedef the most common state container. - typedef boost::container::flat_set FlatSetStateContainer; + typedef storm::storage::FlatSet FlatSetStateContainer; std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block); diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index bc3d68efa..844393c08 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -565,7 +565,7 @@ namespace storm { return result; } - void Automaton::restrictToEdges(boost::container::flat_set const& edgeIndices) { + void Automaton::restrictToEdges(storm::storage::FlatSet const& edgeIndices) { std::vector oldEdges = this->edges.getConcreteEdges(); this->edges.clearConcreteEdges(); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 809ddb1cc..f9c6d857f 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -4,12 +4,12 @@ #include #include #include -#include #include "storm/storage/jani/VariableSet.h" #include "storm/storage/jani/TemplateEdgeContainer.h" #include "storm/storage/jani/EdgeContainer.h" #include "storm/storage/jani/FunctionDefinition.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace jani { @@ -375,7 +375,7 @@ namespace storm { /*! * Restricts the automaton to the edges given by the indices. All other edges are deleted. */ - void restrictToEdges(boost::container::flat_set const& edgeIndices); + void restrictToEdges(storm::storage::FlatSet const& edgeIndices); private: /// The name of the automaton. diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 55f21e027..bb5826ccd 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -100,7 +100,7 @@ namespace storm { this->color = newColor; } - boost::container::flat_set const& Edge::getWrittenGlobalVariables() const { + storm::storage::FlatSet const& Edge::getWrittenGlobalVariables() const { return templateEdge->getWrittenGlobalVariables(); } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index e45bf7f93..6a3c08d75 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -3,11 +3,11 @@ #include #include -#include #include #include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/OrderedAssignments.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace jani { @@ -89,7 +89,7 @@ namespace storm { /*! * Retrieves a set of (global) variables that are written by at least one of the edge's destinations. */ - boost::container::flat_set const& getWrittenGlobalVariables() const; + storm::storage::FlatSet const& getWrittenGlobalVariables() const; /*! * Retrieves the assignments of this edge. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 9d61a10cc..0db4a183f 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -622,7 +622,7 @@ namespace storm { return actions; } - boost::container::flat_set const& Model::getNonsilentActionIndices() const { + storm::storage::FlatSet const& Model::getNonsilentActionIndices() const { return nonsilentActionIndices; } @@ -1491,14 +1491,14 @@ namespace storm { return std::make_pair(index >> 32, index & ((1ull << 32) - 1)); } - Model Model::restrictEdges(boost::container::flat_set const& automataAndEdgeIndices) const { + Model Model::restrictEdges(storm::storage::FlatSet const& automataAndEdgeIndices) const { Model result(*this); // Restrict all automata. for (uint64_t automatonIndex = 0; automatonIndex < result.automata.size(); ++automatonIndex) { // Compute the set of edges that is to be kept for this automaton. - boost::container::flat_set automatonEdgeIndices; + storm::storage::FlatSet automatonEdgeIndices; for (auto const& e : automataAndEdgeIndices) { auto automatonAndEdgeIndex = decodeAutomatonAndEdgeIndices(e); if (automatonAndEdgeIndex.first == automatonIndex) { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index c96611940..e70762ebe 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -3,8 +3,6 @@ #include -#include - #include "storm/storage/jani/VariableSet.h" #include "storm/storage/jani/Action.h" #include "storm/storage/jani/ModelType.h" @@ -17,6 +15,7 @@ #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/ModelFeatures.h" +#include "storm/storage/BoostTypes.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -158,7 +157,7 @@ namespace storm { /*! * Retrieves all non-silent action indices of the model. */ - boost::container::flat_set const& getNonsilentActionIndices() const; + storm::storage::FlatSet const& getNonsilentActionIndices() const; /*! * Adds the given constant to the model. @@ -630,7 +629,7 @@ namespace storm { * Creates a new model that only contains the selected edges. The edge indices encode the automata and * (local) indices of the edges within the automata. */ - Model restrictEdges(boost::container::flat_set const& automataAndEdgeIndices) const; + Model restrictEdges(storm::storage::FlatSet const& automataAndEdgeIndices) const; void writeDotToStream(std::ostream& outStream = std::cout) const; @@ -672,7 +671,7 @@ namespace storm { std::unordered_map nonTrivialRewardModels; /// The set of non-silent action indices. - boost::container::flat_set nonsilentActionIndices; + storm::storage::FlatSet nonsilentActionIndices; /// The constants defined by the model. std::vector constants; diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 50f5b4d8b..bd8bcb1c1 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -43,7 +43,7 @@ namespace storm { } } - boost::container::flat_set const& TemplateEdge::getWrittenGlobalVariables() const { + storm::storage::FlatSet const& TemplateEdge::getWrittenGlobalVariables() const { return writtenGlobalVariables; } diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index 9e8c0e761..c112aa9b1 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/src/storm/storage/jani/TemplateEdge.h @@ -3,11 +3,9 @@ #include #include -#include - #include "storm/storage/expressions/Expression.h" - #include "storm/storage/jani/TemplateEdgeDestination.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace jani { @@ -52,7 +50,7 @@ namespace storm { /*! * Retrieves a set of (global) variables that are written by at least one of the edge's destinations. */ - boost::container::flat_set const& getWrittenGlobalVariables() const; + storm::storage::FlatSet const& getWrittenGlobalVariables() const; /*! * Substitutes all variables in all expressions according to the given substitution. @@ -129,7 +127,7 @@ namespace storm { /// A set of global variables that is written by at least one of the edge's destinations. This set is /// initialized by the call to finalize. - boost::container::flat_set writtenGlobalVariables; + storm::storage::FlatSet writtenGlobalVariables; }; } diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index a47021959..265fa27ec 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -180,7 +180,7 @@ namespace storm { } } - Module Module::restrictCommands(boost::container::flat_set const& indexSet) const { + Module Module::restrictCommands(storm::storage::FlatSet const& indexSet) const { // First construct the new vector of commands. std::vector newCommands; for (auto const& command : commands) { @@ -192,7 +192,7 @@ namespace storm { return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands); } - Module Module::restrictActionIndices(boost::container::flat_set const& actionIndices) const { + Module Module::restrictActionIndices(storm::storage::FlatSet const& actionIndices) const { // First construct the new vector of commands. std::vector newCommands; for (auto const& command : commands) { diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 970304ab5..27d9551ac 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -6,12 +6,12 @@ #include #include #include -#include #include "storm/storage/prism/BooleanVariable.h" #include "storm/storage/prism/IntegerVariable.h" #include "storm/storage/prism/ClockVariable.h" #include "storm/storage/prism/Command.h" +#include "storm/storage/BoostTypes.h" #include "storm/utility/OsDetection.h" namespace storm { @@ -232,7 +232,7 @@ namespace storm { * @param indexSet The set of indices for which to keep the commands. * @return The module resulting from erasing all commands whose indices are not in the given set. */ - Module restrictCommands(boost::container::flat_set const& indexSet) const; + Module restrictCommands(storm::storage::FlatSet const& indexSet) const; /*! * Creates a new module that drops all commands whose action indices are not in the given set. @@ -240,7 +240,7 @@ namespace storm { * @param indexSet The set of action indices for which to keep the commands. * @return The module resulting from erasing all commands whose action indices are not in the given set. */ - Module restrictActionIndices(boost::container::flat_set const& actionIndices) const; + Module restrictActionIndices(storm::storage::FlatSet const& actionIndices) const; /*! * Substitutes all variables in the module according to the given map. diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 1a22f87dc..54620f5ad 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -749,7 +749,7 @@ namespace storm { this->labels = std::move(newLabels); } - Program Program::restrictCommands(boost::container::flat_set const& indexSet) const { + Program Program::restrictCommands(storm::storage::FlatSet const& indexSet) const { std::vector newModules; newModules.reserve(this->getNumberOfModules()); @@ -1447,7 +1447,7 @@ namespace storm { std::map newActionToIndexMap; std::vector newRewardModels; if (!actionIndicesToDelete.empty()) { - boost::container::flat_set actionsToKeep; + storm::storage::FlatSet actionsToKeep; std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin())); // Insert the silent action as this is not contained in the synchronizing action indices. diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 8b6cb1eb1..be7244262 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -5,7 +5,6 @@ #include #include #include -#include #include #include "storm/storage/prism/Constant.h" @@ -16,6 +15,7 @@ #include "storm/storage/prism/SystemCompositionConstruct.h" #include "storm/storage/prism/InitialConstruct.h" #include "storm/storage/prism/Composition.h" +#include "storm/storage/BoostTypes.h" #include "storm/utility/solver.h" #include "storm/utility/OsDetection.h" @@ -580,7 +580,7 @@ namespace storm { * * @param indexSet The set of indices for which to keep the commands. */ - Program restrictCommands(boost::container::flat_set const& indexSet) const; + Program restrictCommands(storm::storage::FlatSet const& indexSet) const; /*! * Defines the undefined constants according to the given map and returns the resulting program. diff --git a/src/storm/storage/prism/RewardModel.cpp b/src/storm/storage/prism/RewardModel.cpp index 53576f53b..96767a17d 100644 --- a/src/storm/storage/prism/RewardModel.cpp +++ b/src/storm/storage/prism/RewardModel.cpp @@ -81,7 +81,7 @@ namespace storm { return true; } - RewardModel RewardModel::restrictActionRelatedRewards(boost::container::flat_set const& actionIndicesToKeep) const { + RewardModel RewardModel::restrictActionRelatedRewards(storm::storage::FlatSet const& actionIndicesToKeep) const { std::vector newStateActionRewards; for (auto const& stateActionReward : this->getStateActionRewards()) { if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) { diff --git a/src/storm/storage/prism/RewardModel.h b/src/storm/storage/prism/RewardModel.h index cda14bdc4..c47b310c5 100644 --- a/src/storm/storage/prism/RewardModel.h +++ b/src/storm/storage/prism/RewardModel.h @@ -4,11 +4,11 @@ #include #include #include -#include #include "storm/storage/prism/StateReward.h" #include "storm/storage/prism/StateActionReward.h" #include "storm/storage/prism/TransitionReward.h" +#include "storm/storage/BoostTypes.h" #include "storm/utility/OsDetection.h" namespace storm { @@ -113,7 +113,7 @@ namespace storm { * @param actionIndicesToKeep The set of action indices to keep. * @return The resulting reward model. */ - RewardModel restrictActionRelatedRewards(boost::container::flat_set const& actionIndicesToKeep) const; + RewardModel restrictActionRelatedRewards(storm::storage::FlatSet const& actionIndicesToKeep) const; friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel); diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 9e4de090b..93698a0f0 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/src/storm/storage/sparse/JaniChoiceOrigins.h @@ -3,9 +3,8 @@ #include #include -#include - #include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/BoostTypes.h" namespace storm { namespace jani { @@ -21,7 +20,7 @@ namespace storm { */ class JaniChoiceOrigins : public ChoiceOrigins { public: - typedef boost::container::flat_set EdgeIndexSet; + typedef storm::storage::FlatSet EdgeIndexSet; /*! * Creates a new representation of the choice indices to their origin in the Jani specification diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index f2a6af716..06ff3c584 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/src/storm/storage/sparse/PrismChoiceOrigins.h @@ -2,10 +2,10 @@ #include #include -#include #include "storm/storage/sparse/ChoiceOrigins.h" #include "storm/storage/prism/Program.h" +#include "storm/storage/BoostTypes.h" namespace storm { @@ -19,7 +19,7 @@ namespace storm { class PrismChoiceOrigins : public ChoiceOrigins { public: - typedef boost::container::flat_set CommandSet; + typedef storm::storage::FlatSet CommandSet; /*! * Creates a new representation of the choice indices to their origin in the prism program diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index 1ff429a5d..6705e40f7 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -18,7 +18,7 @@ namespace storm { * @return The set of labels that is visited on all paths from any state to a target state. */ template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); // Get some data from the model for convenient access. @@ -27,7 +27,7 @@ namespace storm { storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); + std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); std::queue worklist; storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); @@ -35,7 +35,7 @@ namespace storm { // Initially, put all predecessors of target states in the worklist and empty the analysis information them. for (auto state : psiStates) { - analysisInformation[state] = boost::container::flat_set(); + analysisInformation[state] = storm::storage::FlatSet(); for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { worklist.push(predecessorEntry.getColumn()); @@ -69,7 +69,7 @@ namespace storm { if (modifiedChoice) { for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (markedStates.get(entry.getColumn())) { - boost::container::flat_set tmpIntersection; + storm::storage::FlatSet tmpIntersection; std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); analysisInformation[currentState] = std::move(tmpIntersection); @@ -108,11 +108,11 @@ namespace storm { * @return The set of labels that is executed on all paths from an initial state to a target state. */ template - boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); + storm::storage::FlatSet getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); - boost::container::flat_set knownLabels(relevantLabels); - boost::container::flat_set tempIntersection; + storm::storage::FlatSet knownLabels(relevantLabels); + storm::storage::FlatSet tempIntersection; for (auto initialState : model.getInitialStates()) { std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); std::swap(knownLabels, tempIntersection);