From 1e3686480a63b1fa2baa601c31732d66e13765f9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Jun 2019 17:10:34 +0200 Subject: [PATCH 01/12] is_equal_to_one() is not used in Boost 1.70 --- src/storm-parsers/parser/ExpressionParser.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-parsers/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp index 0596b1b4e..481274b13 100644 --- a/src/storm-parsers/parser/ExpressionParser.cpp +++ b/src/storm-parsers/parser/ExpressionParser.cpp @@ -21,10 +21,12 @@ namespace boost { return true; } +#if BOOST_VERSION < 107000 template<> bool is_equal_to_one(storm::RationalNumber const& value) { return storm::utility::isOne(value); } +#endif template<> storm::RationalNumber negate(bool neg, storm::RationalNumber const& number) { From 6a4c18e4a2dee78a4c44fafbd0dcb1b584e0692e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Jun 2019 18:31:02 +0200 Subject: [PATCH 02/12] 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); From 47344f9080e7e2123c75cb42833a5758e1099972 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Jun 2019 18:47:17 +0200 Subject: [PATCH 03/12] Removed unused flat_set includes --- src/storm-dft/builder/ExplicitDFTModelBuilder.h | 1 - src/storm-dft/storage/dft/DFT.cpp | 1 - src/storm/builder/ExplicitModelBuilder.h | 1 - 3 files changed, 3 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index 46ac973b8..a8090a83f 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -1,6 +1,5 @@ #pragma once -#include #include #include #include diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 927343ebc..0475d898f 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -1,6 +1,5 @@ #include "DFT.h" -#include #include #include "storm/exceptions/InvalidArgumentException.h" diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 9440b7e08..58be400ab 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -7,7 +7,6 @@ #include #include #include -#include #include #include #include "storm/models/sparse/StandardRewardModel.h" From 9780ffeb1e3f2f955c5bc9e1efc109913f08774c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 27 Jun 2019 10:31:45 +0200 Subject: [PATCH 04/12] Git ignore for any dir with infix 'build' --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 13689e55f..ee2a4f77b 100644 --- a/.gitignore +++ b/.gitignore @@ -36,7 +36,7 @@ obj/ CMakeFiles/ CPackConfig.cmake # The build Dir -build/ +*build*/ build//CMakeLists.txt /*.vcxproj /*.filters From b357868a3224a6956baf831b07c930bae7a6ea89 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 6 Jun 2019 21:16:08 +0200 Subject: [PATCH 05/12] GurobiLpSolver: Fixed rounding of integral results. --- src/storm/solver/GurobiLpSolver.cpp | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index cd556c936..7056b5093 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -86,6 +86,9 @@ namespace storm { // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option. error = GRBsetdblparam(env, "IntFeasTol", storm::settings::getModule().getIntegerTolerance()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + // error = GRBsetintparam(env, "NumericFocus", 3); + // STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter NumericFocus (" << GRBgeterrormsg(env) << ", error code " << error << ")."); } template @@ -342,9 +345,9 @@ namespace storm { double value = 0; int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - STORM_LOG_THROW(std::abs(static_cast(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(std::round(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); - return static_cast(value); + return static_cast(std::round(value)); } template @@ -363,12 +366,12 @@ namespace storm { STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); if (value > 0.5) { - STORM_LOG_THROW(std::abs(static_cast(value) - 1) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(value - 1.0) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + return true; } else { - STORM_LOG_THROW(value <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + return false; } - - return static_cast(value); } template @@ -496,9 +499,9 @@ namespace storm { STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - STORM_LOG_THROW(std::abs(static_cast(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(std::round(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); - return static_cast(value); + return static_cast(std::round(value)); } template @@ -520,12 +523,12 @@ namespace storm { STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); if (value > 0.5) { - STORM_LOG_THROW(std::abs(static_cast(value) - 1) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(value - 1) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + return true; } else { - STORM_LOG_THROW(value <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + STORM_LOG_THROW(std::abs(value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + return false; } - - return static_cast(value); } template From fedac853df973e8cd277837724faf6c334c4382a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 27 Jun 2019 12:18:03 +0200 Subject: [PATCH 06/12] Fixed gitignore to only exclude build dirs in the root folder. Otherwise, e.g. src/storm/builder/ would also be excluded. --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index ee2a4f77b..98a24b25d 100644 --- a/.gitignore +++ b/.gitignore @@ -36,7 +36,7 @@ obj/ CMakeFiles/ CPackConfig.cmake # The build Dir -*build*/ +/*build*/ build//CMakeLists.txt /*.vcxproj /*.filters From d0596ecf0cf7eb6155ac77d65a0ad92a1c7eb076 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 4 Jul 2019 11:57:20 +0200 Subject: [PATCH 07/12] Changed cmake policy for finding packages: Now path specified via -D_ROOT=/path/to/package/ are automatically considered when searching for packages. --- CMakeLists.txt | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index b2fe1b814..6b67feefb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,6 +1,13 @@ cmake_minimum_required (VERSION 3.2) + cmake_policy(VERSION 3.2) +# When searching for packages, we would like to first search in prefixes specified by _ROOT. +# However, this behavior is only supported since CMake 3.12. +if(POLICY CMP0074) + cmake_policy(SET CMP0074 NEW) +endif() + # Set project name project (storm CXX C) From 230a2c86d34888a123cdf6273051158c736d7423 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 8 Jul 2019 09:23:02 +0200 Subject: [PATCH 08/12] Mentioning QVBS as Benchmark source in README --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 6dcf702a0..c8d4dbb38 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,8 @@ Benchmarks Example input files for Storm can be obtained from https://github.com/moves-rwth/storm-examples. +Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Suite (QVBS)](http://qcomp.org/benchmarks). + Further examples and benchmarks can be found in the following repositories: * **Prism files** (DTMC, MDP, CTMC): From adfe82d0d678fe7b36b69c5701fa6dba31b8099f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 10:18:12 +0200 Subject: [PATCH 09/12] Fixed typo to void --- src/storm/builder/DdJaniModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 27e1e586e..a9b4f62b9 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -733,7 +733,7 @@ namespace storm { // Intentionally left empty. } - bool setMarkovian(bool markovian) { + void setMarkovian(bool markovian) { this->markovian = markovian; } From 685b5c6b27499f4a21413d9022fc660ad2902337 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 11:19:24 +0200 Subject: [PATCH 10/12] Throw exceptions after switch/case to silence compiler warnings about not returning anything --- src/storm-pomdp/storage/PomdpMemory.cpp | 4 +++- src/storm/logic/Bound.h | 4 +++- src/storm/logic/ComparisonType.h | 5 +++++ src/storm/modelchecker/results/FilterType.cpp | 3 +++ src/storm/solver/LinearEquationSolverRequirements.cpp | 4 ++++ .../solver/MinMaxLinearEquationSolverRequirements.cpp | 4 ++++ src/storm/solver/Multiplier.cpp | 2 ++ src/storm/storage/dd/bisimulation/SignatureComputer.cpp | 2 ++ src/storm/storage/jani/JSONExporter.cpp | 8 +++----- src/storm/utility/builder.cpp | 5 ++++- 10 files changed, 33 insertions(+), 8 deletions(-) diff --git a/src/storm-pomdp/storage/PomdpMemory.cpp b/src/storm-pomdp/storage/PomdpMemory.cpp index 1c5f74cf4..161f89f8c 100644 --- a/src/storm-pomdp/storage/PomdpMemory.cpp +++ b/src/storm-pomdp/storage/PomdpMemory.cpp @@ -2,6 +2,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace storage { @@ -110,6 +111,7 @@ namespace storm { case PomdpMemoryPattern::Full: return buildFullyConnectedMemory(numStates); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown PomdpMemoryPattern"); } PomdpMemory PomdpMemoryBuilder::buildTrivialMemory() const { @@ -177,4 +179,4 @@ namespace storm { return PomdpMemory(transitions, 0); } } -} \ No newline at end of file +} diff --git a/src/storm/logic/Bound.h b/src/storm/logic/Bound.h index 0b152ea06..e429dbc6e 100644 --- a/src/storm/logic/Bound.h +++ b/src/storm/logic/Bound.h @@ -1,10 +1,11 @@ #ifndef STORM_LOGIC_BOUND_H_ #define STORM_LOGIC_BOUND_H_ +#include "storm/exceptions/IllegalArgumentException.h" #include "storm/logic/ComparisonType.h" #include "storm/storage/expressions/Expression.h" #include "storm/utility/constants.h" - +#include "storm/utility/macros.h" namespace storm { namespace logic { @@ -29,6 +30,7 @@ namespace storm { case ComparisonType::LessEqual: return compareValue <= thresholdAsValueType; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } friend std::ostream& operator<<(std::ostream& out, Bound const& bound); diff --git a/src/storm/logic/ComparisonType.h b/src/storm/logic/ComparisonType.h index 19475960f..c47fb2786 100644 --- a/src/storm/logic/ComparisonType.h +++ b/src/storm/logic/ComparisonType.h @@ -3,6 +3,9 @@ #include +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace logic { enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; @@ -26,6 +29,7 @@ namespace storm { case ComparisonType::GreaterEqual: return ComparisonType::Less; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } inline ComparisonType invertPreserveStrictness(ComparisonType t) { @@ -39,6 +43,7 @@ namespace storm { case ComparisonType::GreaterEqual: return ComparisonType::LessEqual; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); diff --git a/src/storm/modelchecker/results/FilterType.cpp b/src/storm/modelchecker/results/FilterType.cpp index 17a69063e..e7eac999b 100644 --- a/src/storm/modelchecker/results/FilterType.cpp +++ b/src/storm/modelchecker/results/FilterType.cpp @@ -1,5 +1,7 @@ #include "FilterType.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { @@ -27,6 +29,7 @@ namespace storm { case FilterType::VALUES: return "the values"; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); } } } diff --git a/src/storm/solver/LinearEquationSolverRequirements.cpp b/src/storm/solver/LinearEquationSolverRequirements.cpp index 445e776d7..e4075b1e1 100644 --- a/src/storm/solver/LinearEquationSolverRequirements.cpp +++ b/src/storm/solver/LinearEquationSolverRequirements.cpp @@ -1,5 +1,8 @@ #include "storm/solver/LinearEquationSolverRequirements.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace solver { @@ -36,6 +39,7 @@ namespace storm { case Element::LowerBounds: return lowerBounds(); break; case Element::UpperBounds: return upperBounds(); break; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType"); } void LinearEquationSolverRequirements::clearLowerBounds() { diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp index 3e5e867ab..3d7cdc607 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp @@ -1,5 +1,8 @@ #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" + namespace storm { namespace solver { @@ -56,6 +59,7 @@ namespace storm { case Element::LowerBounds: return lowerBounds(); break; case Element::UpperBounds: return upperBounds(); break; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType"); } void MinMaxLinearEquationSolverRequirements::clearUniqueSolution() { diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 3347ef2dc..abcb53f3d 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -12,6 +12,7 @@ #include "storm/solver/NativeMultiplier.h" #include "storm/solver/GmmxxMultiplier.h" #include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace solver { @@ -79,6 +80,7 @@ namespace storm { case MultiplierType::Native: return std::make_unique>(matrix); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType"); } template class Multiplier; diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index 89345ee9d..407ed33b9 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -6,6 +6,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/OutOfRangeException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace dd { @@ -23,6 +24,7 @@ namespace storm { case SignatureMode::Eager: return position < 1; case SignatureMode::Lazy: return position < 2; } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown SignatureMode"); } template diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index be2c98e9f..b0b315e8a 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -12,6 +12,7 @@ #include "storm/exceptions/InvalidJaniException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/IllegalArgumentException.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" @@ -120,9 +121,8 @@ namespace storm { return ">"; case storm::logic::ComparisonType::GreaterEqual: return "≥"; - default: - assert(false); } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } modernjson::json numberToJson(storm::RationalNumber rn) { @@ -1104,10 +1104,8 @@ namespace storm { return "argmax"; case storm::modelchecker::FilterType::VALUES: return "values"; - default: - assert(false); - } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); } modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp index a6b85e9b1..481ed8020 100644 --- a/src/storm/utility/builder.cpp +++ b/src/storm/utility/builder.cpp @@ -7,6 +7,8 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/exceptions/InvalidModelException.h" + namespace storm { namespace utility { namespace builder { @@ -27,6 +29,7 @@ namespace storm { case storm::models::ModelType::S2pg: return std::make_shared>(std::move(components)); } + STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type"); } template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); @@ -35,4 +38,4 @@ namespace storm { template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); } } -} \ No newline at end of file +} From 7fb660227f4906be2cd304b50c47fb5d7855aa61 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 4 Jul 2019 11:20:04 +0200 Subject: [PATCH 11/12] Replaced assert(false) by throwing an exception --- src/storm-gspn/adapters/XercesAdapter.h | 15 ++++++--------- .../builder/JaniProgramGraphBuilder.cpp | 7 +++---- src/storm/analysis/GraphConditions.cpp | 7 ++++--- src/storm/storage/jani/JSONExporter.cpp | 2 +- src/storm/utility/shortestPaths.cpp | 4 ++-- 5 files changed, 16 insertions(+), 19 deletions(-) diff --git a/src/storm-gspn/adapters/XercesAdapter.h b/src/storm-gspn/adapters/XercesAdapter.h index 0a39c8f2e..c7f22846f 100644 --- a/src/storm-gspn/adapters/XercesAdapter.h +++ b/src/storm-gspn/adapters/XercesAdapter.h @@ -10,7 +10,8 @@ #include #include - +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace adapters { @@ -27,16 +28,12 @@ namespace storm { auto elementNode = (xercesc::DOMElement *) node; return XMLtoString(elementNode->getTagName()); } - case xercesc::DOMNode::NodeType::TEXT_NODE: { + case xercesc::DOMNode::NodeType::TEXT_NODE: return XMLtoString(node->getNodeValue()); - } - case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { + case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: return XMLtoString(node->getNodeName()); - } - default: { - assert(false); - return ""; - } + default: + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown DOMNode type"); } } } diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp index bcb569917..361a4ce25 100644 --- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp +++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp @@ -1,6 +1,7 @@ #include "JaniProgramGraphBuilder.h" #include "storm/storage/jani/EdgeDestination.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace builder { @@ -23,12 +24,10 @@ namespace storm { variables.emplace(v.first, janiVar); automaton.addVariable(*janiVar); } else { - // Not yet supported. - assert(false); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded right bound is not supported yet"); } } else { - // Not yet supported. - assert(false); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded left bound is not supported yet"); } } else { storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first)); diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 2152adfe7..246f256be 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -4,6 +4,7 @@ #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/UnexpectedException.h" #include "storm/models/sparse/StandardRewardModel.h" namespace storm { @@ -44,7 +45,7 @@ namespace storm { } else if (entry.denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); @@ -111,7 +112,7 @@ namespace storm { } else if (transition.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); @@ -147,7 +148,7 @@ namespace storm { } else if (entry.getValue().denominator().constantPart() < 0) { wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); } else { - assert(false); // Should fail before. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before."); } } else { wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index b0b315e8a..2975f9ff3 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -796,7 +796,7 @@ namespace storm { typeDescr["kind"] = "array"; typeDescr["base"] = buildTypeDescription(type.getElementType()); } else { - assert(false); + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown expression type."); } return typeDescr; } diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index b18e309d4..dccfa43f4 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -9,6 +9,7 @@ #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/shortestPaths.h" +#include "storm/exceptions/UnexpectedException.h" // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! // (Also, did I document this? I think so, somewhere. I went with k>=1 because @@ -247,8 +248,7 @@ namespace storm { // there is no such edge // let's disallow that for now, because I'm not expecting it to happen - assert(false); - return zero(); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should not happen."); } else { // edge must be "virtual edge" to meta-target assert(isMetaTargetPredecessor(tailNode)); From 9c52d0d2ab1ad9b0326fbc4af3946e18e9b1892a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Jul 2019 10:24:07 +0200 Subject: [PATCH 12/12] Workaround for IntelTBB linker issue by CMake/Regex magic. IntelTBB does not use symlinks (as commonly used) to reference its libraries but instead uses linker scripts. These linker scripts do not work with GCC and linking fails. As a workaround we manually set the correct library in CMake after extracting the path from the linker script with regex magic. This workaround is highly hackish and might break in the future. --- resources/3rdparty/CMakeLists.txt | 32 ++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 5fc6d8275..4e46c4c3b 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -562,9 +562,35 @@ if (STORM_USE_INTELTBB) message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") set(STORM_HAVE_INTELTBB ON) - link_directories(${TBB_LIBRARY_DIRS}) - include_directories(${TBB_INCLUDE_DIRS}) - list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) + # Under Linux libtbb.so contains a linker script to libtbb.so.2 instead of a symlink. + # This breaks CMake. + # As a workaround we manually try to add the necessary suffix ".2" to the so file and hope for the best. + if (LINUX) + # Check if the library is a linker script which only links to the correct library + # Read first bytes of file + file(READ "${TBB_LIBRARY}" TMPTXT LIMIT 128) + # Check if file starts with "INPUT (libtbb.so.2)" + if("${TMPTXT}" MATCHES "INPUT \\(libtbb\\.so\\.(.*)\\)") + # Manually set library by adding the suffix from the linker script. + # CMAKE_MATCH_1 contains the parsed suffix. + set(TBB_LIB_LINUX "${TBB_LIBRARY}.${CMAKE_MATCH_1}") + set(TBB_MALLOC_LIB_LINUX "${TBB_MALLOC_LIBRARY}.${CMAKE_MATCH_1}") + if (EXISTS "${TBB_LIB_LINUX}") + set(TBB_LIBRARY ${TBB_LIB_LINUX}) + message(STATUS "Storm - Using Intel TBB library in manually set path ${TBB_LIBRARY}.") + endif() + if (EXISTS "${TBB_MALLOC_LIB_LINUX}") + set(TBB_MALLOC_LIBRARY ${TBB_MALLOC_LIB_LINUX}) + message(STATUS "Storm - Using Intel TBB malloc library in manually set path ${TBB_MALLOC_LIBRARY}.") + endif() + endif() + endif() + + add_imported_library(tbb SHARED ${TBB_LIBRARY} ${TBB_INCLUDE_DIRS}) + list(APPEND STORM_DEP_TARGETS tbb_SHARED) + add_imported_library(tbb_malloc SHARED ${TBB_MALLOC_LIBRARY} ${TBB_INCLUDE_DIRS}) + list(APPEND STORM_DEP_TARGETS tbb_malloc_SHARED) + else(TBB_FOUND) message(FATAL_ERROR "Storm - TBB was requested, but not found.") endif(TBB_FOUND)