From b8120ed73a6cfe35a8c36eb2849fb60bc57e6e5f Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 20 Oct 2017 15:46:36 +0200 Subject: [PATCH 01/33] Markov automaton model checker now clearing basic requirements --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 4c49a6325..612456a0d 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -90,9 +90,11 @@ namespace storm { // Check for requirements of the solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -377,9 +379,11 @@ namespace storm { // Check for requirements of the solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); + requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->setLowerBound(storm::utility::zero<ValueType>()); solver->setRequirementsChecked(); solver->solveEquations(dir, x, b); From 4e4526182f548eb044498f307baec4d323d5877f Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 23 Oct 2017 14:21:20 +0200 Subject: [PATCH 02/33] adding information about which technique is used to symbolic native linear equation solver --- src/storm/solver/SymbolicNativeLinearEquationSolver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 21d06a678..9ad5e90af 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -119,7 +119,9 @@ namespace storm { template<storm::dd::DdType DdType, typename ValueType> storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsJacobi(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const { storm::dd::DdManager<DdType>& manager = this->getDdManager(); - + + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (jacobi)"); + // Start by computing the Jacobi decomposition of the matrix A. storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); diagonal &= this->allRows; @@ -185,6 +187,7 @@ namespace storm { template<storm::dd::DdType DdType, typename ValueType> storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsPower(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const { + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (power)"); PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations()); if (result.status == SolverStatus::Converged) { @@ -311,6 +314,7 @@ namespace storm { template<storm::dd::DdType DdType, typename ValueType> storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearch(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const { + STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (rational search)"); return solveEquationsRationalSearchHelper<double>(x, b); } From 33585c811fe49d29f43a525e2a8a1dfef9e183e1 Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Wed, 25 Oct 2017 17:51:36 +0200 Subject: [PATCH 03/33] MinMax Solver requirements now respect whether the solution is known to be unique or not. --- ...SparseDtmcParameterLiftingModelChecker.cpp | 9 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 16 +- .../prctl/helper/HybridMdpPrctlHelper.cpp | 15 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 55 ++++--- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 30 +++- .../IterativeMinMaxLinearEquationSolver.cpp | 152 +++--------------- .../IterativeMinMaxLinearEquationSolver.h | 2 +- .../solver/LpMinMaxLinearEquationSolver.cpp | 6 +- .../solver/LpMinMaxLinearEquationSolver.h | 2 +- .../solver/MinMaxLinearEquationSolver.cpp | 19 ++- src/storm/solver/MinMaxLinearEquationSolver.h | 18 ++- .../SymbolicMinMaxLinearEquationSolver.cpp | 46 +++--- .../SymbolicMinMaxLinearEquationSolver.h | 17 +- 13 files changed, 187 insertions(+), 200 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 8ac2bdea8..27960daac 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -146,9 +146,9 @@ namespace storm { lowerResultBound = storm::utility::zero<ConstantType>(); upperResultBound = storm::utility::one<ConstantType>(); - auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). + auto req = solverFactory->getRequirements(true); req.clearBounds(); - req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); solverFactory->setRequirementsChecked(true); } @@ -185,8 +185,8 @@ namespace storm { // We only know a lower bound for the result lowerResultBound = storm::utility::zero<ConstantType>(); - auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards); - req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations). + // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). + auto req = solverFactory->getRequirements(true); req.clearLowerBounds(); if (req.requiresUpperBounds()) { solvingRequiresUpperRewardBounds = true; @@ -253,6 +253,7 @@ namespace storm { solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration); } auto solver = solverFactory->create(parameterLifter->getMatrix()); + solver->setHasUniqueSolution(); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) { solver->setUpperBound(upperResultBound.get()); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 612456a0d..0bdc633f7 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -89,11 +89,13 @@ namespace storm { } // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities); + // The solution is unique as we assume non-zeno MAs. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setHasUniqueSolution(); solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); @@ -378,12 +380,14 @@ namespace storm { std::vector<ValueType> x(numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); - requirements.clearLowerBounds(); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->setHasUniqueSolution(); solver->setLowerBound(storm::utility::zero<ValueType>()); + solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); solver->setRequirementsChecked(); solver->solveEquations(dir, x, b); @@ -588,10 +592,14 @@ namespace storm { std::vector<ValueType> b = probabilisticChoiceRewards; // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards); + // The solution is unique as we assume non-zeno MAs. + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir); + requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); + solver->setLowerBound(storm::utility::zero<ValueType>()); + solver->setHasUniqueSolution(true); solver->setRequirementsChecked(true); solver->setCachingEnabled(true); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 1d6864fa3..232bb91da 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -135,8 +135,10 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { + // If we minimize, we know that the solution to the equation system is unique. + bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize; // Check for requirements of the solver early so we can adjust the maybe state computation accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; SolverRequirementsData<ValueType> solverRequirementsData; bool extendMaybeStates = false; @@ -212,6 +214,10 @@ namespace storm { std::vector<ValueType> x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero<ValueType>()); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); + + // Set whether the equation system will have a unique solution + solver->setHasUniqueSolution(uniqueSolution); + if (solverRequirementsData.initialScheduler) { solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get())); } @@ -487,8 +493,10 @@ namespace storm { } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { + // If we maximize, we know that the solution to the equation system is unique. + bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize; // Check for requirements of the solver this early so we can adapt the maybe states accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; bool extendMaybeStates = false; if (!clearedRequirements.empty()) { @@ -568,6 +576,9 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(); + // Set whether the equation system will have a unique solution + solver->setHasUniqueSolution(uniqueSolution); + // If the solver requires upper bounds, compute them now. if (requirements.requiresUpperBounds()) { setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get()); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 4a5688f5c..73115ac64 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -22,7 +22,7 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" - + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MinMaxEquationSolverSettings.h" @@ -38,6 +38,11 @@ namespace storm { namespace modelchecker { namespace helper { + enum class EquationSystemType { + UntilProbabilities, + ExpectedRewards + }; + template<typename ValueType> std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); @@ -91,12 +96,12 @@ namespace storm { } template<typename ValueType> - std::vector<uint_fast64_t> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) { + std::vector<uint_fast64_t> computeValidSchedulerHint(EquationSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) { storm::storage::Scheduler<ValueType> validScheduler(maybeStates.size()); - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler, boost::none); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler); } else { STORM_LOG_ASSERT(false, "Unexpected equation system type."); @@ -114,7 +119,7 @@ namespace storm { template<typename ValueType> struct SparseMdpHintType { - SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false) { + SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) { // Intentionally left empty. } @@ -169,6 +174,10 @@ namespace storm { bool getComputeUpperBounds() { return computeUpperBounds; } + + bool hasUniqueSolution() const { + return uniqueSolution; + } boost::optional<std::vector<uint64_t>> schedulerHint; boost::optional<std::vector<ValueType>> valueHint; @@ -177,6 +186,7 @@ namespace storm { boost::optional<std::vector<ValueType>> upperResultBounds; bool eliminateEndComponents; bool computeUpperBounds; + bool uniqueSolution; }; template<typename ValueType> @@ -230,19 +240,22 @@ namespace storm { } template<typename ValueType> - SparseMdpHintType<ValueType> computeHints(storm::solver::EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) { + SparseMdpHintType<ValueType> computeHints(EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) { SparseMdpHintType<ValueType> result; + // The solution to the min-max equation system is unique if we minimize until probabilities or + // maximize reachability rewards or if the hint tells us that there are no end-compontnes. + result.uniqueSolution = (dir == storm::solver::OptimizationDirection::Minimize && type == EquationSystemType::UntilProbabilities) + || (dir == storm::solver::OptimizationDirection::Maximize && type == EquationSystemType::ExpectedRewards) + || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()); + // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(result.uniqueSolution, dir); if (!requirements.empty()) { - // If the hint tells us that there are no end-components, we can clear that requirement. - if (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()) { - requirements.clearNoEndComponents(); - } // If the solver still requires no end-components, we have to eliminate them later. if (requirements.requiresNoEndComponents()) { + STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); result.eliminateEndComponents = true; requirements.clearNoEndComponents(); @@ -256,9 +269,9 @@ namespace storm { } // Finally, we have information on the bounds depending on the problem type. - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { requirements.clearBounds(); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { requirements.clearLowerBounds(); } if (requirements.requiresUpperBounds()) { @@ -273,8 +286,7 @@ namespace storm { // Only if there is no end component decomposition that we will need to do later, we use value and scheduler // hints from the provided hint. if (!result.eliminateEndComponents) { - bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()); - extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); + extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution); } else { STORM_LOG_WARN_COND(hint.isEmpty(), "A non-empty hint was provided, but its information will be disregarded."); } @@ -283,7 +295,7 @@ namespace storm { if (!result.hasLowerResultBound()) { result.lowerResultBound = storm::utility::zero<ValueType>(); } - if (!result.hasUpperResultBound() && type == storm::solver::EquationSystemType::UntilProbabilities) { + if (!result.hasUpperResultBound() && type == EquationSystemType::UntilProbabilities) { result.upperResultBound = storm::utility::one<ValueType>(); } @@ -326,6 +338,7 @@ namespace storm { // Set up the solver. std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); + solver->setHasUniqueSolution(hint.hasUniqueSolution()); if (hint.hasLowerResultBound()) { solver->setLowerBound(hint.getLowerResultBound()); } @@ -526,7 +539,7 @@ namespace storm { // In this case we have have to compute the remaining probabilities. // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory); + SparseMdpHintType<ValueType> hintInformation = computeHints(EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix<ValueType> submatrix; @@ -882,7 +895,7 @@ namespace storm { } // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices); + SparseMdpHintType<ValueType> hintInformation = computeHints(EquationSystemType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix<ValueType> submatrix; @@ -1089,14 +1102,16 @@ namespace storm { storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath); - requirements.clearLowerBounds(); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, goal.direction()); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::vector<ValueType> sspResult(numberOfSspStates); goal.restrictRelevantValues(statesNotContainedInAnyMec); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix); solver->setLowerBound(storm::utility::zero<ValueType>()); + solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end())); + solver->setHasUniqueSolution(); solver->setRequirementsChecked(); solver->solveEquations(sspResult, b); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 518f50acc..cc1d3bcf9 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -21,15 +21,21 @@ namespace storm { namespace modelchecker { namespace helper { + + enum class EquationSystemType { + UntilProbabilities, + ExpectedRewards + }; + template<storm::dd::DdType DdType, typename ValueType> - storm::dd::Bdd<DdType> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) { + storm::dd::Bdd<DdType> computeValidSchedulerHint(EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) { storm::dd::Bdd<DdType> result; - if (type == storm::solver::EquationSystemType::UntilProbabilities) { + if (type == EquationSystemType::UntilProbabilities) { result = storm::utility::graph::computeSchedulerProbGreater0E(model, transitionMatrix.notZero(), maybeStates, targetStates); - } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) { + } else if (type == EquationSystemType::ExpectedRewards) { result = storm::utility::graph::computeSchedulerProb1E(model, transitionMatrix.notZero(), maybeStates, targetStates, maybeStates || targetStates); } @@ -78,13 +84,18 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + // If we minimize, we know that the solution is unique + if (dir == storm::solver::OptimizationDirection::Minimize) { + solver->setHasUniqueSolution(); + } + // Check requirements of solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir); boost::optional<storm::dd::Bdd<DdType>> initialScheduler; if (!requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); - initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second); + initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second); requirements.clearValidInitialScheduler(); } requirements.clearBounds(); @@ -237,13 +248,18 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); + // If we maximize, we know that the solution is unique + if (dir == storm::solver::OptimizationDirection::Maximize) { + solver->setHasUniqueSolution(); + } + // Check requirements of solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir); boost::optional<storm::dd::Bdd<DdType>> initialScheduler; if (!requirements.empty()) { if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); - initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates); + initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates); requirements.clearValidInitialScheduler(); } requirements.clearLowerBounds(); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index b706ab585..eb6a970b9 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -45,7 +45,6 @@ namespace storm { switch (solutionMethod) { case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; - case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break; case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver."); @@ -136,9 +135,6 @@ namespace storm { case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: result = solveEquationsPolicyIteration(dir, x, b); break; - case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::Acyclic: - result = solveEquationsAcyclic(dir, x, b); - break; case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch: result = solveEquationsRationalSearch(dir, x, b); break; @@ -268,67 +264,44 @@ namespace storm { } template<typename ValueType> - MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const { // Start by copying the requirements of the linear equation solver. MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements()); - // General requirements. if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) { - requirements.requireLowerBounds(); - } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) { - // As rational search needs to approach the solution from below, we cannot start with a valid scheduler hint as we would otherwise do. - // Instead, we need to require no end components. - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { + if (this->getSettings().getForceSoundness()) { + // Interval iteration requires a unique solution and lower+upper bounds + if (!this->hasUniqueSolution()) { requirements.requireNoEndComponents(); } - } - } - - // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) { - requirements.requireNoEndComponents(); - } - - // Guide requirements by whether or not we force soundness. - if (this->getSettings().getForceSoundness()) { - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) { - // Require both bounds now. requirements.requireBounds(); - - // If we need to also converge from above, we cannot deal with end components in the notorious cases. - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireNoEndComponents(); - } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireNoEndComponents(); - } - } - } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) { - if (equationSystemType == EquationSystemType::UntilProbabilities) { + } else if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique. + // Computing a scheduler is only possible if the solution is unique + if (this->isTrackSchedulerSet()) { + requirements.requireNoEndComponents(); + } else { + // As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above). if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); + requirements.requireLowerBounds(); } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); + requirements.requireUpperBounds(); } } } - } else { - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); - } - } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); - } + } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) { + // Rational search needs to approach the solution from below. + requirements.requireLowerBounds(); + // The solution needs to be unique in case of minimizing or in cases where we want a scheduler. + if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) { + requirements.requireNoEndComponents(); + } + } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) { + if (!this->hasUniqueSolution()) { + requirements.requireValidInitialScheduler(); } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver."); } return requirements; @@ -934,83 +907,6 @@ namespace storm { return solveEquationsRationalSearchHelper<double>(dir, x, b); } - template<typename ValueType> - bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsAcyclic(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const { - uint64_t numGroups = this->A->getRowGroupCount(); - - // Allocate memory for the scheduler (if required) - if (this->isTrackSchedulerSet()) { - if (this->schedulerChoices) { - this->schedulerChoices->resize(numGroups); - } else { - this->schedulerChoices = std::vector<uint_fast64_t>(numGroups); - } - } - - // We now compute a topological sort of the row groups. - // If caching is enabled, it might be possible to obtain this sort from the cache. - if (this->isCachingEnabled()) { - if (rowGroupOrdering) { - for (auto const& group : *rowGroupOrdering) { - computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr); - } - return true; - } else { - rowGroupOrdering = std::make_unique<std::vector<uint64_t>>(); - rowGroupOrdering->reserve(numGroups); - } - } - - auto transposedMatrix = this->A->transpose(true); - - // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. - storm::storage::BitVector processedGroups(numGroups, false); - // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now. - // A group can be processed if all successors have already been processed. - // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true. - // This is due to the observation that groups with higher indices usually need to be processed earlier. - storm::storage::BitVector candidates(numGroups, true); - uint64_t candidate = numGroups - 1; - for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) { - candidates.set(numGroups - candidate - 1, false); - - // Check if the candidate row group has an unprocessed successor - bool hasUnprocessedSuccessor = false; - for (auto const& entry : this->A->getRowGroup(candidate)) { - if (!processedGroups.get(entry.getColumn())) { - hasUnprocessedSuccessor = true; - break; - } - } - - uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1; - - if (!hasUnprocessedSuccessor) { - // This candidate can be processed. - processedGroups.set(candidate); - computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr); - if (this->isCachingEnabled()) { - rowGroupOrdering->push_back(candidate); - } - - // Add new candidates - for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) { - uint64_t predecessor = predecessorEntry.getColumn(); - if (!candidates.get(numGroups - predecessor - 1)) { - candidates.set(numGroups - predecessor - 1, true); - nextCandidate = std::max(nextCandidate, predecessor); - ++numCandidates; - } - } - } - candidate = nextCandidate; - } - - assert(candidates.empty()); - STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic."); - return true; - } - template<typename ValueType> void IterativeMinMaxLinearEquationSolver<ValueType>::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, uint_fast64_t* choice) const { uint64_t row = this->A->getRowGroupIndices()[group]; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index f4aa7e7a3..cfce17ddb 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -62,7 +62,7 @@ namespace storm { ValueType getPrecision() const; bool getRelative() const; - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override; private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const; diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 024bcf260..fce0aeae9 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -110,12 +110,12 @@ namespace storm { template<typename ValueType> - MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const { MinMaxLinearEquationSolverRequirements requirements; - // In case we need to retrieve a scheduler, end components are forbidden - if (this->isTrackSchedulerSet()) { + // In case we need to retrieve a scheduler, the solution has to be unique + if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) { requirements.requireNoEndComponents(); } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index 3e5af458f..d7bcc0c72 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -18,7 +18,7 @@ namespace storm { virtual void clearCache() const override; - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override; private: std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index c41455e16..e4dce9084 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -19,7 +19,7 @@ namespace storm { namespace solver { template<typename ValueType> - MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) { + MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) { // Intentionally left empty. } @@ -56,6 +56,16 @@ namespace storm { direction = OptimizationDirectionSetting::Unset; } + template<typename ValueType> + void MinMaxLinearEquationSolver<ValueType>::setHasUniqueSolution(bool value) { + uniqueSolution = value; + } + + template<typename ValueType> + bool MinMaxLinearEquationSolver<ValueType>::hasUniqueSolution() const { + return uniqueSolution; + } + template<typename ValueType> void MinMaxLinearEquationSolver<ValueType>::setTrackScheduler(bool trackScheduler) { this->trackScheduler = trackScheduler; @@ -127,7 +137,7 @@ namespace storm { } template<typename ValueType> - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const { return MinMaxLinearEquationSolverRequirements(); } @@ -199,10 +209,11 @@ namespace storm { } template<typename ValueType> - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const { // Create dummy solver and ask it for requirements. std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create(); - return solver->getRequirements(equationSystemType, direction); + solver->setHasUniqueSolution(hasUniqueSolution); + return solver->getRequirements(direction); } template<typename ValueType> diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 61742d326..5f095f5c8 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -12,7 +12,6 @@ #include "storm/storage/sparse/StateType.h" #include "storm/storage/Scheduler.h" #include "storm/solver/OptimizationDirection.h" -#include "storm/solver/EquationSystemType.h" #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -94,6 +93,16 @@ namespace storm { */ void unsetOptimizationDirection(); + /*! + * Sets whether the solution to the min max equation system is known to be unique. + */ + void setHasUniqueSolution(bool value = true); + + /*! + * Retrieves whether the solution to the min max equation system is assumed to be unique + */ + bool hasUniqueSolution() const; + /*! * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently * stored scheduler (if any) is deleted. @@ -155,7 +164,7 @@ namespace storm { * Retrieves the requirements of this solver for solving equations with the current settings. The requirements * are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -184,6 +193,9 @@ namespace storm { boost::optional<std::vector<uint_fast64_t>> initialScheduler; private: + // Whether the solver can assume that the min-max equation system has a unique solution + bool uniqueSolution; + /// Whether some of the generated data during solver calls should be cached. bool cachingEnabled; @@ -212,7 +224,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; + MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index c6c6ec261..a5845d556 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -86,12 +86,12 @@ namespace storm { } template<storm::dd::DdType DdType, typename ValueType> - SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), requirementsChecked(false) { + SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), uniqueSolution(false), requirementsChecked(false) { // Intentionally left empty. } template<storm::dd::DdType DdType, typename ValueType> - SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) { + SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), uniqueSolution(false), requirementsChecked(false) { // Intentionally left empty. } @@ -419,39 +419,42 @@ namespace storm { } template<storm::dd::DdType DdType, typename ValueType> - MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const { MinMaxLinearEquationSolverRequirements requirements; if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) { - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (!direction || direction.get() == OptimizationDirection::Maximize) { - requirements.requireValidInitialScheduler(); - } - } - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); - } + if (!this->hasUniqueSolution()) { + requirements.requireValidInitialScheduler(); } } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) { - requirements.requireLowerBounds(); - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { + if (!this->hasUniqueSolution()) { + if (!direction || direction.get() == storm::solver::OptimizationDirection::Maximize) { + requirements.requireLowerBounds(); + } + if (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize) { requirements.requireValidInitialScheduler(); } } } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) { requirements.requireLowerBounds(); - if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireNoEndComponents(); - } + if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) { + requirements.requireNoEndComponents(); } } return requirements; } + template<storm::dd::DdType DdType, typename ValueType> + void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setHasUniqueSolution(bool value) { + this->uniqueSolution = value; + } + + template<storm::dd::DdType DdType, typename ValueType> + bool SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::hasUniqueSolution() const { + return this->uniqueSolution; + } + template<storm::dd::DdType DdType, typename ValueType> void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setRequirementsChecked(bool value) { this->requirementsChecked = value; @@ -484,9 +487,10 @@ namespace storm { } template<storm::dd::DdType DdType, typename ValueType> - MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const { + MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const { std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = this->create(); - return solver->getRequirements(equationSystemType, direction); + solver->setHasUniqueSolution(hasUniqueSolution); + return solver->getRequirements(direction); } template<storm::dd::DdType DdType, typename ValueType> diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 6853582f1..a58552b01 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -127,7 +127,17 @@ namespace storm { /*! * Retrieves the requirements of the solver. */ - virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; + + /*! + * Sets whether the solution to the min max equation system is known to be unique. + */ + void setHasUniqueSolution(bool value = true); + + /*! + * Retrieves whether the solution to the min max equation system is assumed to be unique + */ + bool hasUniqueSolution() const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -208,6 +218,9 @@ namespace storm { // The settings to use. SymbolicMinMaxLinearEquationSolverSettings<ValueType> settings; + // Whether the solver can assume that the min-max equation system has a unique solution + bool uniqueSolution; + // A flag indicating whether the requirements were checked. bool requirementsChecked; @@ -230,7 +243,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; + MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const; private: virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create() const = 0; From 3571f0ddcada672ef3bab7ed264f4ec9775059b4 Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Wed, 25 Oct 2017 19:48:17 +0200 Subject: [PATCH 04/33] Respected that the solution is unique when doing value iteration --- src/storm/solver/AbstractEquationSolver.cpp | 22 ++++++++--------- src/storm/solver/AbstractEquationSolver.h | 1 + .../IterativeMinMaxLinearEquationSolver.cpp | 24 ++++++++++++------- .../SymbolicMinMaxLinearEquationSolver.cpp | 12 ++++++---- 4 files changed, 35 insertions(+), 24 deletions(-) diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index afbec8ac7..c7fe0bd01 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -168,6 +168,16 @@ namespace storm { } } + template<typename ValueType> + void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const { + STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); + if (this->hasUpperBound(BoundType::Global)) { + upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound()); + } else { + upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end()); + } + } + template<typename ValueType> void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const { STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s)."); @@ -179,17 +189,7 @@ namespace storm { upperBoundsVector = std::make_unique<std::vector<ValueType>>(length, this->getUpperBound()); } } else { - if (this->hasUpperBound(BoundType::Global)) { - for (auto& e : *upperBoundsVector) { - e = this->getUpperBound(); - } - } else { - auto upperBoundsIt = this->getUpperBounds().begin(); - for (auto& e : *upperBoundsVector) { - e = *upperBoundsIt; - ++upperBoundsIt; - } - } + createUpperBoundsVector(*upperBoundsVector); } } diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 22e9d0f56..98f6895f4 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -160,6 +160,7 @@ namespace storm { TerminationCondition<ValueType> const& getTerminationCondition() const; std::unique_ptr<TerminationCondition<ValueType>> const& getTerminationConditionPointer() const; + void createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const; void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const; void createLowerBoundsVector(std::vector<ValueType>& lowerBoundsVector) const; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index eb6a970b9..1aa038ebd 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -367,9 +367,8 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount()); } - // By default, the guarantee that we can provide is that our solution is always less-or-equal than the - // actual solution. - SolverGuarantee guarantee = SolverGuarantee::LessOrEqual; + // By default, we can not provide any guarantee + SolverGuarantee guarantee = SolverGuarantee::None; if (this->hasInitialScheduler()) { // Resolve the nondeterminism according to the initial scheduler. @@ -391,14 +390,21 @@ namespace storm { } submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); - // If we were given an initial scheduler and are in fact minimizing, our current solution becomes - // always greater-or-equal than the actual solution. - if (dir == storm::OptimizationDirection::Minimize) { + // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes + // always less-or-equal (greater-or-equal) than the actual solution. + if (dir == storm::OptimizationDirection::Maximize) { + guarantee = SolverGuarantee::LessOrEqual; + } else { + guarantee = SolverGuarantee::GreaterOrEqual; + } + } else if (!this->hasUniqueSolution()) { + if (dir == storm::OptimizationDirection::Maximize) { + this->createLowerBoundsVector(x); + guarantee = SolverGuarantee::LessOrEqual; + } else { + this->createUpperBoundsVector(x); guarantee = SolverGuarantee::GreaterOrEqual; } - } else { - // If no initial scheduler is given, we start from the lower bound. - this->createLowerBoundsVector(x); } std::vector<ValueType>* newX = auxiliaryRowGroupVector.get(); diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index a5845d556..5036ce5ea 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -280,11 +280,15 @@ namespace storm { // Set up the environment. storm::dd::Add<DdType, ValueType> localX; - // If we were given an initial scheduler, we take its solution as the starting point. - if (this->hasInitialScheduler()) { - localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + if (this->hasUniqueSolution()) { + localX = x; } else { - localX = this->getLowerBoundsVector(); + // If we were given an initial scheduler, we take its solution as the starting point. + if (this->hasInitialScheduler()) { + localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + } else { + localX = this->getLowerBoundsVector(); + } } ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations()); From f44ce8801c2aa359d7d24ec9356257321e4b25ac Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Wed, 25 Oct 2017 20:14:06 +0200 Subject: [PATCH 05/33] "fixed" the tests that failed because of unsound value iteration --- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 ++++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 ++-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 16 ++++++++-------- .../NativeMdpPrctlModelCheckerTest.cpp | 8 ++++---- 4 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 60e6834e0..a10f772fc 100644 --- a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 1fe94cde7..50ba06a78 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index fce5f55bb..a981a0929 100644 --- a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); @@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index f4c2f7913..4a58e62bc 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) { result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); From 9859f60db0af7f9d56ca642545fc2ab4539b0365 Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Wed, 25 Oct 2017 20:27:14 +0200 Subject: [PATCH 06/33] Fixed solver tests --- .../storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp | 4 ++++ .../storm/solver/NativeMinMaxLinearEquationSolverTest.cpp | 5 ++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index da68456fe..db72b1087 100644 --- a/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -19,6 +19,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>(); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); @@ -42,6 +43,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>(); auto solver = factory.create(A); + solver->setLowerBound(0.0); + solver->setUpperBound(1.0); solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true)); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); @@ -111,6 +114,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); diff --git a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp index bfd1defcc..bdebc139e 100644 --- a/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -20,6 +20,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>(); auto solver = factory.create(A); + solver->setHasUniqueSolution(); ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); @@ -83,7 +84,9 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration); auto solver = factory.create(A); - + solver->setLowerBound(0.0); + solver->setUpperBound(1.0); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); From e6f61fb441a1ac1f266866be91d69c24640a429a Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 26 Oct 2017 09:32:42 +0200 Subject: [PATCH 07/33] fixed bug in hybrid engine when using interval iteration --- src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 232bb91da..2b45011a7 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -108,8 +108,8 @@ namespace storm { oneStepProbabilities = std::move(subvector); } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); - eliminateExtendedStatesFromExplicitRepresentation(explicitRepresentation, solverRequirementsData.initialScheduler, solverRequirementsData.properMaybeStates); oneStepProbabilities = explicitRepresentation.first.getConstrainedRowGroupSumVector(solverRequirementsData.properMaybeStates, targetStates); + eliminateExtendedStatesFromExplicitRepresentation(explicitRepresentation, solverRequirementsData.initialScheduler, solverRequirementsData.properMaybeStates); } } From 518773f18f27c315e6678ae6dd57b0c65bd78a91 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 26 Oct 2017 09:53:14 +0200 Subject: [PATCH 08/33] commit missing version file --- version.cmake | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 version.cmake diff --git a/version.cmake b/version.cmake new file mode 100644 index 000000000..21ee2f621 --- /dev/null +++ b/version.cmake @@ -0,0 +1,4 @@ +set(STORM_VERSION_MAJOR 1) +set(STORM_VERSION_MINOR 1) +set(STORM_VERSION_PATCH 0) + From c4c6c9cbce44442e241231cfbe7e0a6373e54d69 Mon Sep 17 00:00:00 2001 From: Matthias Volk <matthias.volk@cs.rwth-aachen.de> Date: Thu, 26 Oct 2017 22:22:08 +0200 Subject: [PATCH 09/33] Test compiler configurations within cmake --- CMakeLists.txt | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index b6c56e03c..c0d958476 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,7 +14,8 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmak include(ExternalProject) include(RegisterSourceGroup) include(imported) - +include(CheckCXXSourceCompiles) +include(CheckCSourceCompiles) ############################################################# ## @@ -292,6 +293,31 @@ else() set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fomit-frame-pointer") endif() +# Test compiler by compiling small program. +CHECK_C_SOURCE_COMPILES(" + #include <stdio.h> + int main() { + const char* text = \"A Storm is coming.\"; + return 0; + }" + COMPILER_C_WORKS +) +CHECK_CXX_SOURCE_COMPILES(" + #include <string> + int main() { + const std::string text = \"A Storm is coming.\"; + return 0; + }" + COMPILER_CXX_WORKS +) +if ((NOT COMPILER_CXX_WORKS) OR (NOT COMPILER_C_WORKS)) + if (MACOSX) + message(FATAL_ERROR "The C/C++ compiler is not configured correctly.\nTry running 'xcode-select --install'.") + else() + message(FATAL_ERROR "The C/C++ compiler is not configured correctly.") + endif() +endif() + ############################################################# ## ## RPATH settings From 419fcd1b437dde46d1dd08fe85c4aeb7f91f1abf Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Fri, 27 Oct 2017 16:01:52 +0200 Subject: [PATCH 10/33] Fixed test --- src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 4a58e62bc..e700f347e 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); From 2682100cfd045f9d9f7c477559c4d66fcb0d4854 Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Sun, 29 Oct 2017 20:17:50 +0100 Subject: [PATCH 11/33] fixed more tests --- src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 50ba06a78..64ca71caf 100644 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); - EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); From 374f7e1fbb121a7a69e63a9d7b842450844e1625 Mon Sep 17 00:00:00 2001 From: Tom Janson <tom.janson@rwth-aachen.de> Date: Mon, 30 Oct 2017 17:02:37 +0100 Subject: [PATCH 12/33] kSP: disallow access to index 0 (1-based indices!) --- src/storm/utility/shortestPaths.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index c2f6a97b9..8432ce1a5 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -11,7 +11,6 @@ #include "storm/utility/shortestPaths.h" // FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! -// Accessing zero should trigger a warning! // (Also, did I document this? I think so, somewhere. I went with k>=1 because // that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...) @@ -336,6 +335,10 @@ namespace storm { template <typename T> void ShortestPathsGenerator<T>::computeKSP(unsigned long k) { + if (k == 0) { + throw std::invalid_argument("Index 0 is invalid, since we use 1-based indices (sorry)!"); + } + unsigned long alreadyComputedK = kShortestPaths[metaTarget].size(); for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { From 41bc2c0de44393fbe7708ac6fc4a24fe8c665c79 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Tue, 31 Oct 2017 12:46:02 +0100 Subject: [PATCH 13/33] explicit instantiations to make gcc hapy --- src/storm/utility/KwekMehlhorn.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/utility/KwekMehlhorn.cpp b/src/storm/utility/KwekMehlhorn.cpp index 985f12789..ec81a3357 100644 --- a/src/storm/utility/KwekMehlhorn.cpp +++ b/src/storm/utility/KwekMehlhorn.cpp @@ -73,6 +73,9 @@ namespace storm { } } + template storm::RationalNumber sharpen(uint64_t precision, double const& input); + template storm::RationalNumber sharpen(uint64_t precision, storm::RationalNumber const& input); + template void sharpen(uint64_t precision, std::vector<double> const& input, std::vector<storm::RationalNumber>& output); template void sharpen(uint64_t precision, std::vector<storm::RationalNumber> const& input, std::vector<storm::RationalNumber>& output); From b99bc59215b6d2541bec7ad6f53e255b0eded44e Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Tue, 31 Oct 2017 14:05:01 +0100 Subject: [PATCH 14/33] adding some primes --- src/storm/storage/BitVectorHashMap.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index dd3e3dbb0..e6b769a67 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -9,7 +9,7 @@ namespace storm { namespace storage { template<class ValueType, class Hash1, class Hash2> - const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003}; + const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003, 205726009, 411452021, 822904099, 1645808237, 3291616481, 6583232969, 13166465941, 26332931887, 52665863819, 105331727639}; template<class ValueType, class Hash1, class Hash2> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { From db7d05880027ba1e69006230258b720390951a18 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 1 Nov 2017 19:22:40 +0100 Subject: [PATCH 15/33] converted some assertions into exceptions in bit vector hash map --- src/storm/exceptions/InternalException.h | 12 ++++++++++++ src/storm/storage/BitVectorHashMap.cpp | 7 ++++--- 2 files changed, 16 insertions(+), 3 deletions(-) create mode 100644 src/storm/exceptions/InternalException.h diff --git a/src/storm/exceptions/InternalException.h b/src/storm/exceptions/InternalException.h new file mode 100644 index 000000000..e28f8f4fd --- /dev/null +++ b/src/storm/exceptions/InternalException.h @@ -0,0 +1,12 @@ +#pragma once + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(InternalException) + + } +} diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index e6b769a67..641fc07aa 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -5,6 +5,7 @@ #include <algorithm> #include "storm/utility/macros.h" +#include "storm/exceptions/InternalException.h" namespace storm { namespace storage { @@ -72,7 +73,7 @@ namespace storm { template<class ValueType, class Hash1, class Hash2> void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() { ++currentSizeIterator; - STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big."); // Create new containers and swap them with the old ones. numberOfElements = 0; @@ -97,10 +98,10 @@ namespace storm { uint_fast64_t failCount = 0; while (fail) { ++failCount; - STORM_LOG_ASSERT(failCount < 2, "Increasing size failed too often."); + STORM_LOG_THROW(failCount < 2, storm::exceptions::InternalException, "Increasing size failed too often."); ++currentSizeIterator; - STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big."); numberOfElements = 0; buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); From f772af624125c235a3269092c6ac33d2ac18c129 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 2 Nov 2017 14:12:46 +0100 Subject: [PATCH 16/33] fixed bug in bit vector hash map --- src/storm/storage/BitVectorHashMap.cpp | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index 641fc07aa..a522a5863 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -10,11 +10,15 @@ namespace storm { namespace storage { template<class ValueType, class Hash1, class Hash2> - const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003, 205726009, 411452021, 822904099, 1645808237, 3291616481, 6583232969, 13166465941, 26332931887, 52665863819, 105331727639}; + const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223}; template<class ValueType, class Hash1, class Hash2> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { - // Intentionally left empty. +#ifndef NDEBUG + for (uint64_t i = 0; i < sizes.size() - 1; ++i) { + STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes."); + } +#endif } template<class ValueType, class Hash1, class Hash2> @@ -73,7 +77,8 @@ namespace storm { template<class ValueType, class Hash1, class Hash2> void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() { ++currentSizeIterator; - STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big."); + STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << "."); // Create new containers and swap them with the old ones. numberOfElements = 0; @@ -113,7 +118,7 @@ namespace storm { // If we failed to insert just one element, we have to redo the procedure with a larger container size. if (fail) { - continue; + break; } } } @@ -213,6 +218,7 @@ namespace storm { template<class ValueType, class Hash1, class Hash2> std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucket(storm::storage::BitVector const& key) const { uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; + uint_fast64_t stride = hasher2(key); uint_fast64_t bucket = initialHash; uint_fast64_t counter = 0; @@ -221,7 +227,7 @@ namespace storm { if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } - bucket += hasher2(key); + bucket += stride; bucket %= *currentSizeIterator; if (bucket == initialHash) { @@ -236,15 +242,16 @@ namespace storm { template<bool increaseStorage> std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucketToInsert(storm::storage::BitVector const& key) { uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; + uint_fast64_t stride = hasher2(key); uint_fast64_t bucket = initialHash; - + uint_fast64_t counter = 0; while (isBucketOccupied(bucket)) { ++counter; if (buckets.matches(bucket * bucketSize, key)) { return std::make_tuple(true, bucket, false); } - bucket += hasher2(key); + bucket += stride; bucket %= *currentSizeIterator; if (bucket == initialHash) { @@ -256,7 +263,7 @@ namespace storm { } } } - + return std::make_tuple(false, bucket, false); } From 3a11914da0631ac565271564c7d1b68b68b29ed6 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 2 Nov 2017 16:32:40 +0100 Subject: [PATCH 17/33] commit to switch workplace --- src/storm/builder/ExplicitModelBuilder.cpp | 4 +- src/storm/storage/BitVector.cpp | 17 --- src/storm/storage/BitVector.h | 6 - src/storm/storage/BitVectorHashMap.cpp | 159 ++++++++++++--------- src/storm/storage/BitVectorHashMap.h | 18 ++- 5 files changed, 109 insertions(+), 95 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 7a552e9bd..48d5b2a75 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -149,7 +149,9 @@ namespace storm { stateRemapping.get()[currentIndex] = currentRowGroup; } - STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); + if (currentIndex % 100000 == 0) { + STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); + } generator->load(currentState); storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback); diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 469fb8441..e5498b82c 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -999,22 +999,6 @@ namespace storm { out << std::endl; } - std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const { - STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size."); - std::size_t result = 0; - - for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) { - result ^= result << 3; - result ^= result >> bitvector.getAsInt(index << 6, 5); - } - - // Erase the last bit and add one to definitely make this hash value non-zero. - result &= ~1ull; - result += 1; - - return result; - } - // All necessary explicit template instantiations. template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end); template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::const_iterator begin, std::vector<uint_fast64_t>::const_iterator end); @@ -1028,7 +1012,6 @@ namespace storm { } namespace std { - std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const { return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount()); } diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index bcb56ae0d..0b5a7670b 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -501,7 +501,6 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); friend struct std::hash<storm::storage::BitVector>; - friend struct NonZeroBitVectorHash; private: /*! @@ -571,11 +570,6 @@ namespace storm { static const uint_fast64_t mod64mask = (1 << 6) - 1; }; - // A hashing functor that guarantees that the result of the hash is never going to be -1. - struct NonZeroBitVectorHash { - std::size_t operator()(storm::storage::BitVector const& bv) const; - }; - } // namespace storage } // namespace storm diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index a522a5863..c1d9d46d1 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -9,47 +9,43 @@ namespace storm { namespace storage { - template<class ValueType, class Hash1, class Hash2> - const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223}; + template<class ValueType, class Hash> + const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223}; - template<class ValueType, class Hash1, class Hash2> - BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { -#ifndef NDEBUG - for (uint64_t i = 0; i < sizes.size() - 1; ++i) { - STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes."); - } -#endif + template<class ValueType, class Hash> + BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { + // Intentionally left empty. } - template<class ValueType, class Hash1, class Hash2> - bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) { + template<class ValueType, class Hash> + bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) { return &map == &other.map && *indexIt == *other.indexIt; } - template<class ValueType, class Hash1, class Hash2> - bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) { + template<class ValueType, class Hash> + bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) { return !(*this == other); } - template<class ValueType, class Hash1, class Hash2> - typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++(int) { + template<class ValueType, class Hash> + typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++(int) { ++indexIt; return *this; } - template<class ValueType, class Hash1, class Hash2> - typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++() { + template<class ValueType, class Hash> + typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++() { ++indexIt; return *this; } - template<class ValueType, class Hash1, class Hash2> - std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const { + template<class ValueType, class Hash> + std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator*() const { return map.getBucketAndValue(*indexIt); } - template<class ValueType, class Hash1, class Hash2> - BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { + template<class ValueType, class Hash> + BitVectorHashMap<ValueType, Hash>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64."); currentSizeIterator = std::find_if(sizes.begin(), sizes.end(), [=] (uint64_t value) { return value > initialSize; } ); @@ -57,28 +53,42 @@ namespace storm { buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); occupied = storm::storage::BitVector(*currentSizeIterator); values = std::vector<ValueType>(*currentSizeIterator); + +#ifndef NDEBUG + for (uint64_t i = 0; i < sizes.size() - 1; ++i) { + STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes."); + } + numberOfInsertions = 0; + numberOfInsertionProbingSteps = 0; + numberOfFinds = 0; + numberOfFindProbingSteps = 0; +#endif } - template<class ValueType, class Hash1, class Hash2> - bool BitVectorHashMap<ValueType, Hash1, Hash2>::isBucketOccupied(uint_fast64_t bucket) const { + template<class ValueType, class Hash> + bool BitVectorHashMap<ValueType, Hash>::isBucketOccupied(uint_fast64_t bucket) const { return occupied.get(bucket); } - template<class ValueType, class Hash1, class Hash2> - std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::size() const { + template<class ValueType, class Hash> + std::size_t BitVectorHashMap<ValueType, Hash>::size() const { return numberOfElements; } - template<class ValueType, class Hash1, class Hash2> - std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::capacity() const { + template<class ValueType, class Hash> + std::size_t BitVectorHashMap<ValueType, Hash>::capacity() const { return *currentSizeIterator; } - template<class ValueType, class Hash1, class Hash2> - void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() { + template<class ValueType, class Hash> + void BitVectorHashMap<ValueType, Hash>::increaseSize() { ++currentSizeIterator; STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); +#ifndef NDEBUG + STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast<double>(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast<double>(numberOfInsertions)) << " probing steps)."); +#else STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << "."); +#endif // Create new containers and swap them with the old ones. numberOfElements = 0; @@ -124,8 +134,8 @@ namespace storm { } } - template<class ValueType, class Hash1, class Hash2> - bool BitVectorHashMap<ValueType, Hash1, Hash2>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) { + template<class ValueType, class Hash> + bool BitVectorHashMap<ValueType, Hash>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) { std::tuple<bool, std::size_t, bool> flagBucketTuple = this->findBucketToInsert<false>(key); if (std::get<2>(flagBucketTuple)) { return false; @@ -143,18 +153,18 @@ namespace storm { } } - template<class ValueType, class Hash1, class Hash2> - ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) { + template<class ValueType, class Hash> + ValueType BitVectorHashMap<ValueType, Hash>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) { return findOrAddAndGetBucket(key, value).first; } - template<class ValueType, class Hash1, class Hash2> - void BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) { + template<class ValueType, class Hash> + void BitVectorHashMap<ValueType, Hash>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) { setOrAddAndGetBucket(key, value); } - template<class ValueType, class Hash1, class Hash2> - std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { + template<class ValueType, class Hash> + std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. if (numberOfElements >= loadFactor * *currentSizeIterator) { this->increaseSize(); @@ -174,8 +184,8 @@ namespace storm { } } - template<class ValueType, class Hash1, class Hash2> - std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { + template<class ValueType, class Hash> + std::size_t BitVectorHashMap<ValueType, Hash>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. if (numberOfElements >= loadFactor * *currentSizeIterator) { this->increaseSize(); @@ -193,42 +203,51 @@ namespace storm { return std::get<1>(flagBucketTuple); } - template<class ValueType, class Hash1, class Hash2> - ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const { + template<class ValueType, class Hash> + ValueType BitVectorHashMap<ValueType, Hash>::getValue(storm::storage::BitVector const& key) const { std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key); STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); return values[flagBucketPair.second]; } - template<class ValueType, class Hash1, class Hash2> - bool BitVectorHashMap<ValueType, Hash1, Hash2>::contains(storm::storage::BitVector const& key) const { + template<class ValueType, class Hash> + bool BitVectorHashMap<ValueType, Hash>::contains(storm::storage::BitVector const& key) const { return findBucket(key).first; } - template<class ValueType, class Hash1, class Hash2> - typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::begin() const { + template<class ValueType, class Hash> + typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::begin() const { return const_iterator(*this, occupied.begin()); } - template<class ValueType, class Hash1, class Hash2> - typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::end() const { + template<class ValueType, class Hash> + typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::end() const { return const_iterator(*this, occupied.end()); } - template<class ValueType, class Hash1, class Hash2> - std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucket(storm::storage::BitVector const& key) const { - uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; - uint_fast64_t stride = hasher2(key); + template<class ValueType, class Hash> + uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const { + return (currentValue + step + step*step) % *currentSizeIterator; + } + + template<class ValueType, class Hash> + std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash>::findBucket(storm::storage::BitVector const& key) const { +#ifndef NDEBUG + ++numberOfFinds; +#endif + uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - uint_fast64_t counter = 0; + uint_fast64_t i = 0; while (isBucketOccupied(bucket)) { - ++counter; + ++i; +#ifndef NDEBUG + ++numberOfFindProbingSteps; +#endif if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } - bucket += stride; - bucket %= *currentSizeIterator; + bucket = getNextBucketInProbingSequence(bucket, i); if (bucket == initialHash) { return std::make_pair(false, bucket); @@ -238,26 +257,30 @@ namespace storm { return std::make_pair(false, bucket); } - template<class ValueType, class Hash1, class Hash2> + template<class ValueType, class Hash> template<bool increaseStorage> - std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucketToInsert(storm::storage::BitVector const& key) { - uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; - uint_fast64_t stride = hasher2(key); + std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash>::findBucketToInsert(storm::storage::BitVector const& key) { +#ifndef NDEBUG + ++numberOfInsertions; +#endif + uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - uint_fast64_t counter = 0; + uint64_t i = 0; while (isBucketOccupied(bucket)) { - ++counter; + ++i; +#ifndef NDEBUG + ++numberOfInsertionProbingSteps; +#endif if (buckets.matches(bucket * bucketSize, key)) { return std::make_tuple(true, bucket, false); } - bucket += stride; - bucket %= *currentSizeIterator; + bucket = getNextBucketInProbingSequence(bucket, i); if (bucket == initialHash) { if (increaseStorage) { this->increaseSize(); - bucket = initialHash = hasher1(key) % *currentSizeIterator; + bucket = initialHash = hasher(key) % *currentSizeIterator; } else { return std::make_tuple(false, bucket, true); } @@ -267,13 +290,13 @@ namespace storm { return std::make_tuple(false, bucket, false); } - template<class ValueType, class Hash1, class Hash2> - std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::getBucketAndValue(std::size_t bucket) const { + template<class ValueType, class Hash> + std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::getBucketAndValue(std::size_t bucket) const { return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]); } - template<class ValueType, class Hash1, class Hash2> - void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) { + template<class ValueType, class Hash> + void BitVectorHashMap<ValueType, Hash>::remap(std::function<ValueType(ValueType const&)> const& remapping) { for (auto pos : occupied) { values[pos] = remapping(values[pos]); } diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h index a5941e2f8..ab9e6c4be 100644 --- a/src/storm/storage/BitVectorHashMap.h +++ b/src/storm/storage/BitVectorHashMap.h @@ -14,7 +14,7 @@ namespace storm { * queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of * 64. */ - template<typename ValueType, typename Hash1 = std::hash<storm::storage::BitVector>, class Hash2 = storm::storage::NonZeroBitVectorHash> + template<typename ValueType, typename Hash = std::hash<storm::storage::BitVector>> class BitVectorHashMap { public: class BitVectorHashMapIterator { @@ -204,6 +204,11 @@ namespace storm { */ void increaseSize(); + /*! + * Computes the next bucket in the probing sequence. + */ + uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const; + // The load factor determining when the size of the map is increased. double loadFactor; @@ -229,11 +234,18 @@ namespace storm { std::vector<std::size_t>::const_iterator currentSizeIterator; // Functor object that are used to perform the actual hashing. - Hash1 hasher1; - Hash2 hasher2; + Hash hasher; // A static table that produces the next possible size of the hash table. static const std::vector<std::size_t> sizes; + +#ifndef NDEBUG + // Some performance metrics. + mutable uint64_t numberOfInsertions; + mutable uint64_t numberOfInsertionProbingSteps; + mutable uint64_t numberOfFinds; + mutable uint64_t numberOfFindProbingSteps; +#endif }; } From 8116b360ba3813135e740e44ea960db899553da3 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 2 Nov 2017 18:30:22 +0100 Subject: [PATCH 18/33] changed hash function of bit vector hash map --- src/storm/storage/BitVectorHashMap.cpp | 8 ++++---- src/storm/storage/BitVectorHashMap.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index c1d9d46d1..9cec1aa20 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -226,7 +226,7 @@ namespace storm { } template<class ValueType, class Hash> - uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const { + uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t, uint_fast64_t currentValue, uint_fast64_t step) const { return (currentValue + step + step*step) % *currentSizeIterator; } @@ -237,7 +237,7 @@ namespace storm { #endif uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - + uint_fast64_t i = 0; while (isBucketOccupied(bucket)) { ++i; @@ -247,7 +247,7 @@ namespace storm { if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } - bucket = getNextBucketInProbingSequence(bucket, i); + bucket = getNextBucketInProbingSequence(initialHash, bucket, i); if (bucket == initialHash) { return std::make_pair(false, bucket); @@ -275,7 +275,7 @@ namespace storm { if (buckets.matches(bucket * bucketSize, key)) { return std::make_tuple(true, bucket, false); } - bucket = getNextBucketInProbingSequence(bucket, i); + bucket = getNextBucketInProbingSequence(initialHash, bucket, i); if (bucket == initialHash) { if (increaseStorage) { diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h index ab9e6c4be..e2ca51a5e 100644 --- a/src/storm/storage/BitVectorHashMap.h +++ b/src/storm/storage/BitVectorHashMap.h @@ -207,7 +207,7 @@ namespace storm { /*! * Computes the next bucket in the probing sequence. */ - uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const; + uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t initialValue, uint_fast64_t currentValue, uint_fast64_t step) const; // The load factor determining when the size of the map is increased. double loadFactor; From 12dda40919add16ce911f78bd39a76249741439b Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@gmail.com> Date: Fri, 3 Nov 2017 00:20:18 +0100 Subject: [PATCH 19/33] split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs --- src/storm-cli-utilities/model-handling.h | 37 ++++--- .../settings/modules/GSPNExportSettings.cpp | 4 +- .../settings/modules/GSPNExportSettings.h | 0 .../settings/modules/GSPNSettings.cpp | 2 +- .../settings/modules/GSPNSettings.h | 0 src/storm-pars-cli/storm-pars.cpp | 34 +----- src/storm-pgcl-cli/storm-pgcl.cpp | 2 +- .../settings/modules/PGCLSettings.cpp | 2 +- .../settings/modules/PGCLSettings.h | 0 src/storm/api/model_descriptions.cpp | 8 +- src/storm/api/model_descriptions.h | 2 +- src/storm/builder/BuilderOptions.cpp | 6 +- src/storm/builder/ExplicitModelBuilder.cpp | 4 +- .../parser/ImcaMarkovAutomatonParser.cpp | 4 +- src/storm/parser/PrismParser.cpp | 14 +-- src/storm/parser/PrismParser.h | 8 +- src/storm/settings/SettingsManager.cpp | 3 +- src/storm/settings/modules/BuildSettings.cpp | 95 ++++++++++++++++ src/storm/settings/modules/BuildSettings.h | 84 ++++++++++++++ src/storm/settings/modules/CoreSettings.h | 4 +- src/storm/settings/modules/IOSettings.cpp | 104 ++++-------------- src/storm/settings/modules/IOSettings.h | 81 +------------- src/storm/solver/AbstractEquationSolver.cpp | 1 - src/storm/storage/prism/Program.cpp | 20 ++-- src/storm/storage/prism/Program.h | 4 +- .../storm/builder/DdJaniModelBuilderTest.cpp | 26 ++--- .../storm/builder/DdPrismModelBuilderTest.cpp | 28 ++--- .../builder/ExplicitJaniModelBuilderTest.cpp | 14 +-- .../ExplicitJitJaniModelBuilderTest.cpp | 15 +-- .../builder/ExplicitPrismModelBuilderTest.cpp | 14 +-- .../GmmxxCtmcCslModelCheckerTest.cpp | 25 +---- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 45 ++------ .../NativeCtmcCslModelCheckerTest.cpp | 25 +---- .../NativeHybridCtmcCslModelCheckerTest.cpp | 42 ++----- 34 files changed, 340 insertions(+), 417 deletions(-) rename src/{storm => storm-gspn}/settings/modules/GSPNExportSettings.cpp (97%) rename src/{storm => storm-gspn}/settings/modules/GSPNExportSettings.h (100%) rename src/{storm => storm-gspn}/settings/modules/GSPNSettings.cpp (98%) rename src/{storm => storm-gspn}/settings/modules/GSPNSettings.h (100%) rename src/{storm => storm-pgcl}/settings/modules/PGCLSettings.cpp (98%) rename src/{storm => storm-pgcl}/settings/modules/PGCLSettings.h (100%) create mode 100644 src/storm/settings/modules/BuildSettings.cpp create mode 100644 src/storm/settings/modules/BuildSettings.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d91d84479..35a8a0196 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -27,6 +27,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -50,7 +51,7 @@ namespace storm { void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { if (ioSettings.isPrismOrJaniInputSet()) { if (ioSettings.isPrismInputSet()) { - input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename()); + input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled()); } else { auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); input.model = janiInput.first; @@ -95,6 +96,7 @@ namespace storm { SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); + auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>(); SymbolicInput output = input; @@ -113,7 +115,7 @@ namespace storm { // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { bool transformToJani = ioSettings.isPrismToJaniSet(); - bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); + bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && buildSettings.isJitSet(); STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); transformToJani |= transformToJaniForJit; @@ -171,22 +173,22 @@ namespace storm { template <storm::dd::DdType DdType, typename ValueType> std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()); + return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildFullModelSet()); } template <typename ValueType> - std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>(); storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); - options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); - options.setBuildStateValuations(ioSettings.isBuildStateValuationsSet()); + options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); + options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); - options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); - options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); - if (ioSettings.isBuildFullModelSet()) { + options.setBuildAllLabels(buildSettings.isBuildFullModelSet()); + options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet()); + if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); } - return storm::api::buildSparseModel<ValueType>(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet()); + return storm::api::buildSparseModel<ValueType>(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet()); } template <typename ValueType> @@ -206,13 +208,14 @@ namespace storm { template <storm::dd::DdType DdType, typename ValueType> std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { storm::utility::Stopwatch modelBuildingWatch(true); + auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); std::shared_ptr<storm::models::ModelBase> result; if (input.model) { if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { result = buildModelDd<DdType, ValueType>(input); } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { - result = buildModelSparse<ValueType>(input, ioSettings); + result = buildModelSparse<ValueType>(input, buildSettings); } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); @@ -254,18 +257,17 @@ namespace storm { std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>(); auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>(); - auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false); if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()); - result.second = true; + result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()); + result.second = true; } if (generalSettings.isBisimulationSet()) { - result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); - result.second = true; + result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); + result.second = true; } return result; @@ -597,8 +599,9 @@ namespace storm { template <storm::dd::DdType DdType, typename ValueType> std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); + auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); std::shared_ptr<storm::models::ModelBase> model; - if (!ioSettings.isNoBuildModelSet()) { + if (!buildSettings.isNoBuildModelSet()) { model = buildModel<DdType, ValueType>(engine, input, ioSettings); } diff --git a/src/storm/settings/modules/GSPNExportSettings.cpp b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp similarity index 97% rename from src/storm/settings/modules/GSPNExportSettings.cpp rename to src/storm-gspn/settings/modules/GSPNExportSettings.cpp index 8a5c315dc..a3c46f250 100644 --- a/src/storm/settings/modules/GSPNExportSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp @@ -1,5 +1,5 @@ -#include "GSPNExportSettings.h" -#include "JaniExportSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm-gspn/settings/modules/GSPNExportSettings.h similarity index 100% rename from src/storm/settings/modules/GSPNExportSettings.h rename to src/storm-gspn/settings/modules/GSPNExportSettings.h diff --git a/src/storm/settings/modules/GSPNSettings.cpp b/src/storm-gspn/settings/modules/GSPNSettings.cpp similarity index 98% rename from src/storm/settings/modules/GSPNSettings.cpp rename to src/storm-gspn/settings/modules/GSPNSettings.cpp index 9184f9137..2a0588b3d 100644 --- a/src/storm/settings/modules/GSPNSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNSettings.cpp @@ -1,4 +1,4 @@ -#include "GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/GSPNSettings.h b/src/storm-gspn/settings/modules/GSPNSettings.h similarity index 100% rename from src/storm/settings/modules/GSPNSettings.h rename to src/storm-gspn/settings/modules/GSPNSettings.h diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 907688ef4..8a8c9fa6a 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -29,34 +29,6 @@ namespace storm { typedef typename storm::cli::SymbolicInput SymbolicInput; - template <typename ValueType> - std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - return storm::api::buildSparseModel<ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet()); - } - - template <storm::dd::DdType DdType, typename ValueType> - std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - storm::utility::Stopwatch modelBuildingWatch(true); - - std::shared_ptr<storm::models::ModelBase> result; - if (input.model) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { - result = storm::cli::buildModelDd<DdType, ValueType>(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { - result = storm::pars::buildModelSparse<ValueType>(input, ioSettings); - } - } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); - result = storm::cli::buildModelExplicit<ValueType>(ioSettings); - } - - modelBuildingWatch.stop(); - if (result) { - STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); - } - - return result; - } template <typename ValueType> @@ -271,14 +243,16 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>(); auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); + + auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>(); auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); std::shared_ptr<storm::models::ModelBase> model; - if (!ioSettings.isNoBuildModelSet()) { - model = storm::pars::buildModel<DdType, ValueType>(engine, input, ioSettings); + if (!buildSettings.isNoBuildModelSet()) { + model = storm::cli::buildModel<DdType, ValueType>(engine, input, ioSettings); } if (model) { diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index ce579938f..bfbb6cad4 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -15,7 +15,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/PGCLSettings.h" +#include "storm-pgcl/settings/modules/PGCLSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" diff --git a/src/storm/settings/modules/PGCLSettings.cpp b/src/storm-pgcl/settings/modules/PGCLSettings.cpp similarity index 98% rename from src/storm/settings/modules/PGCLSettings.cpp rename to src/storm-pgcl/settings/modules/PGCLSettings.cpp index 5035f3632..a70b87f6f 100644 --- a/src/storm/settings/modules/PGCLSettings.cpp +++ b/src/storm-pgcl/settings/modules/PGCLSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/settings/modules/PGCLSettings.h" +#include "PGCLSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/PGCLSettings.h b/src/storm-pgcl/settings/modules/PGCLSettings.h similarity index 100% rename from src/storm/settings/modules/PGCLSettings.h rename to src/storm-pgcl/settings/modules/PGCLSettings.h diff --git a/src/storm/api/model_descriptions.cpp b/src/storm/api/model_descriptions.cpp index bd1e399f3..76ce24116 100644 --- a/src/storm/api/model_descriptions.cpp +++ b/src/storm/api/model_descriptions.cpp @@ -6,11 +6,15 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/BuildSettings.h" + namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename) { - storm::prism::Program program = storm::parser::PrismParser::parse(filename).simplify().simplify(); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility) { + storm::prism::Program program = storm::parser::PrismParser::parse(filename, prismCompatibility).simplify().simplify(); program.checkValidity(); return program; } diff --git a/src/storm/api/model_descriptions.h b/src/storm/api/model_descriptions.h index 99ab5d24d..533c5e8d1 100644 --- a/src/storm/api/model_descriptions.h +++ b/src/storm/api/model_descriptions.h @@ -14,7 +14,7 @@ namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false); std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename); diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 2ee5bf37c..00718e3f1 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -3,7 +3,7 @@ #include "storm/logic/Formulas.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/macros.h" @@ -55,9 +55,9 @@ namespace storm { } } - auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); + auto const& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>(); auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>(); - explorationChecks = ioSettings.isExplorationChecksSet(); + explorationChecks = buildSettings.isExplorationChecksSet(); showProgress = generalSettings.isVerboseSet(); showProgressDelay = generalSettings.getShowProgressDelay(); } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 48d5b2a75..d4aa08590 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -11,7 +11,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/builder/RewardModelBuilder.h" #include "storm/builder/ChoiceInformationBuilder.h" @@ -43,7 +43,7 @@ namespace storm { namespace builder { template <typename ValueType, typename RewardModelType, typename StateType> - ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::IOSettings>().getExplorationOrder()) { + ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) { // Intentionally left empty. } diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm/parser/ImcaMarkovAutomatonParser.cpp index c00b44497..01cb93671 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm/parser/ImcaMarkovAutomatonParser.cpp @@ -1,7 +1,7 @@ #include "storm/parser/ImcaMarkovAutomatonParser.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/utility/file.h" #include "storm/utility/builder.h" @@ -11,7 +11,7 @@ namespace storm { template <typename ValueType, typename StateType> ImcaParserGrammar<ValueType, StateType>::ImcaParserGrammar() : ImcaParserGrammar<ValueType, StateType>::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) { - buildChoiceLabels = storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildChoiceLabelsSet(); + buildChoiceLabels = storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildChoiceLabelsSet(); initialize(); } diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 38ed0cb12..18f42d39c 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -2,7 +2,6 @@ #include "storm/storage/prism/Compositions.h" -#include "storm/settings/SettingsManager.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" @@ -16,7 +15,7 @@ namespace storm { namespace parser { - storm::prism::Program PrismParser::parse(std::string const& filename) { + storm::prism::Program PrismParser::parse(std::string const& filename, bool prismCompatibility) { // Open file and initialize result. std::ifstream inputFileStream; storm::utility::openFile(filename, inputFileStream); @@ -25,7 +24,7 @@ namespace storm { // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>())); - result = parseFromString(fileContent, filename); + result = parseFromString(fileContent, filename, prismCompatibility); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. storm::utility::closeFile(inputFileStream); @@ -37,7 +36,7 @@ namespace storm { return result; } - storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) { + storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); @@ -47,7 +46,7 @@ namespace storm { storm::prism::Program result; // Create grammar. - storm::parser::PrismParser grammar(filename, first); + storm::parser::PrismParser grammar(filename, first, prismCompatibility); try { // Start first run. bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); @@ -74,7 +73,7 @@ namespace storm { return result; } - PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { + PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { ExpressionParser& expression_ = *expressionParser; // Parse simple identifier. @@ -671,8 +670,9 @@ namespace storm { STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'."); finalModelType = storm::prism::Program::ModelType::MDP; } + - return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); } void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index 129cd7b43..fe7f0bc83 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -77,7 +77,7 @@ namespace storm { * @param filename the name of the file to parse. * @return The resulting PRISM program. */ - static storm::prism::Program parse(std::string const& filename); + static storm::prism::Program parse(std::string const& filename, bool prismCompatability = false); /*! * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. @@ -86,7 +86,7 @@ namespace storm { * @param filename The name of the file from which the input was read. * @return The resulting PRISM program. */ - static storm::prism::Program parseFromString(std::string const& input, std::string const& filename); + static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool prismCompatability = false); private: struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> { @@ -150,7 +150,7 @@ namespace storm { * @param filename The filename that is to be read. This is used for proper error reporting. * @param first The iterator to the beginning of the input. */ - PrismParser(std::string const& filename, Iterator first); + PrismParser(std::string const& filename, Iterator first, bool prismCompatibility); /*! * Sets an internal flag that indicates the second run is now taking place. @@ -159,6 +159,8 @@ namespace storm { // A flag that stores whether the grammar is currently doing the second run. bool secondRun; + + bool prismCompatibility; /*! * Sets whether doubles literals are allowed in the parsed expression. diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index b271ca581..188d1cba2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -1,7 +1,6 @@ #include "storm/settings/SettingsManager.h" #include <cstring> -#include <cctype> #include <mutex> #include <iomanip> #include <fstream> @@ -19,6 +18,7 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/CounterexampleGeneratorSettings.h" #include "storm/settings/modules/CuddSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/SylvanSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" @@ -511,6 +511,7 @@ namespace storm { // Register all known settings modules. storm::settings::addModule<storm::settings::modules::GeneralSettings>(); storm::settings::addModule<storm::settings::modules::IOSettings>(); + storm::settings::addModule<storm::settings::modules::BuildSettings>(); storm::settings::addModule<storm::settings::modules::CoreSettings>(); storm::settings::addModule<storm::settings::modules::DebugSettings>(); storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp new file mode 100644 index 000000000..a813b08fa --- /dev/null +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -0,0 +1,95 @@ +#include "storm/settings/modules/BuildSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/parser/CSVParser.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string BuildSettings::moduleName = "build"; + + const std::string jitOptionName = "jit"; + const std::string explorationOrderOptionName = "explorder"; + const std::string explorationOrderOptionShortName = "eo"; + const std::string explorationChecksOptionName = "explchecks"; + const std::string explorationChecksOptionShortName = "ec"; + const std::string prismCompatibilityOptionName = "prismcompat"; + const std::string prismCompatibilityOptionShortName = "pc"; + const std::string noBuildOptionName = "nobuild"; + const std::string fullModelBuildOptionName = "buildfull"; + const std::string buildChoiceLabelOptionName = "buildchoicelab"; + const std::string buildStateValuationsOptionName = "buildstateval"; + BuildSettings::BuildSettings() : ModuleSettings(moduleName) { + + std::vector<std::string> explorationOrders = {"dfs", "bfs"}; + this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); + + } + + + bool BuildSettings::isJitSet() const { + return this->getOption(jitOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isExplorationOrderSet() const { + return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isPrismCompatibilityEnabled() const { + return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildFullModelSet() const { + return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isNoBuildModelSet() const { + return this->getOption(noBuildOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildChoiceLabelsSet() const { + return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildStateValuationsSet() const { + return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); + } + + + storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const { + std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); + if (explorationOrderAsString == "dfs") { + return storm::builder::ExplorationOrder::Dfs; + } else if (explorationOrderAsString == "bfs") { + return storm::builder::ExplorationOrder::Bfs; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); + } + + bool BuildSettings::isExplorationChecksSet() const { + return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); + } + } + + + } +} diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h new file mode 100644 index 000000000..4ef0f5193 --- /dev/null +++ b/src/storm/settings/modules/BuildSettings.h @@ -0,0 +1,84 @@ +#pragma once + + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" +#include "storm/builder/ExplorationOrder.h" + +namespace storm { + namespace settings { + namespace modules { + class BuildSettings : public ModuleSettings { + + public: + + /*! + * Creates a new set of core settings. + */ + BuildSettings(); + /*! + * Retrieves whether the option to use the JIT builder is set. + * + * @return True iff the JIT builder is to be used. + */ + bool isJitSet() const; + + /*! + * Retrieves whether the model exploration order was set. + * + * @return True if the model exploration option was set. + */ + bool isExplorationOrderSet() const; + + /*! + * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). + * + * @return True if additional checks are to be performed. + */ + bool isExplorationChecksSet() const; + + /*! + * Retrieves the exploration order if it was set. + * + * @return The chosen exploration order. + */ + storm::builder::ExplorationOrder getExplorationOrder() const; + + /*! + * Retrieves whether the PRISM compatibility mode was enabled. + * + * @return True iff the PRISM compatibility mode was enabled. + */ + bool isPrismCompatibilityEnabled() const; + + /** + * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. + */ + bool isNoBuildModelSet() const; + + /*! + * Retrieves whether the full model should be build, that is, the model including all labels and rewards. + * + * @return true iff the full model should be build. + */ + bool isBuildFullModelSet() const; + + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildChoiceLabelsSet() const; + + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildStateValuationsSet() const; + + + // The name of the module. + static const std::string moduleName; + }; + } + } +} \ No newline at end of file diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index e0359bf62..afd16cd78 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -117,9 +117,9 @@ namespace storm { bool isDdLibraryTypeSetFromDefaultValue() const; /*! - * Retrieves whether statistics are to be shown for counterexample generation. + * Retrieves whether statistics are to be shown * - * @return True iff statistics are to be shown for counterexample generation. + * @return True iff statistics are to be shown */ bool isShowStatisticsSet() const; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 44f94296d..ec36ef9d8 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -29,22 +29,13 @@ namespace storm { const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; - const std::string IOSettings::jitOptionName = "jit"; - const std::string IOSettings::explorationOrderOptionName = "explorder"; - const std::string IOSettings::explorationOrderOptionShortName = "eo"; - const std::string IOSettings::explorationChecksOptionName = "explchecks"; - const std::string IOSettings::explorationChecksOptionShortName = "ec"; + const std::string IOSettings::transitionRewardsOptionName = "transrew"; const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::choiceLabelingOptionName = "choicelab"; const std::string IOSettings::constantsOptionName = "constants"; const std::string IOSettings::constantsOptionShortName = "const"; - const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; - const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; - const std::string IOSettings::noBuildOptionName = "nobuild"; - const std::string IOSettings::fullModelBuildOptionName = "buildfull"; - const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab"; - const std::string IOSettings::buildStateValuationsOptionName = "buildstateval"; + const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; @@ -52,7 +43,6 @@ namespace storm { IOSettings::IOSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.") @@ -73,19 +63,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build()) .build()); - std::vector<std::string> explorationOrders = {"dfs", "bfs"}; - this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); @@ -102,7 +83,7 @@ namespace storm { bool IOSettings::isExportDotSet() const { return this->getOption(exportDotOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } @@ -114,11 +95,11 @@ namespace storm { std::string IOSettings::getExportJaniDotFilename() const { return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isExportExplicitSet() const { return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getExportExplicitFilename() const { return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); } @@ -126,11 +107,11 @@ namespace storm { bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getTransitionFilename() const { return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); } - + std::string IOSettings::getLabelingFilename() const { return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); } @@ -154,15 +135,15 @@ namespace storm { bool IOSettings::isPrismInputSet() const { return this->getOption(prismInputOptionName).getHasOptionBeenSet(); } - + bool IOSettings::isPrismOrJaniInputSet() const { return isJaniInputSet() || isPrismInputSet(); } - + bool IOSettings::isPrismToJaniSet() const { return this->getOption(prismToJaniOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getPrismInputFilename() const { return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString(); } @@ -174,93 +155,48 @@ namespace storm { std::string IOSettings::getJaniInputFilename() const { return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString(); } - - bool IOSettings::isJitSet() const { - return this->getOption(jitOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isExplorationOrderSet() const { - return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); - } - - storm::builder::ExplorationOrder IOSettings::getExplorationOrder() const { - std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); - if (explorationOrderAsString == "dfs") { - return storm::builder::ExplorationOrder::Dfs; - } else if (explorationOrderAsString == "bfs") { - return storm::builder::ExplorationOrder::Bfs; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); - } - - bool IOSettings::isExplorationChecksSet() const { - return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); - } - + bool IOSettings::isTransitionRewardsSet() const { return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getTransitionRewardsFilename() const { return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isStateRewardsSet() const { return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getStateRewardsFilename() const { return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isChoiceLabelingSet() const { return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getChoiceLabelingFilename() const { return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); } - - std::unique_ptr<storm::settings::SettingMemento> IOSettings::overridePrismCompatibilityMode(bool stateToSet) { - return this->overrideOption(prismCompatibilityOptionName, stateToSet); - } - + bool IOSettings::isConstantsSet() const { return this->getOption(constantsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getConstantDefinitionString() const { return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); } - + bool IOSettings::isJaniPropertiesSet() const { return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); } - + std::vector<std::string> IOSettings::getJaniProperties() const { return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); } - bool IOSettings::isPrismCompatibilityEnabled() const { - return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildFullModelSet() const { - return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isNoBuildModelSet() const { - return this->getOption(noBuildOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildChoiceLabelsSet() const { - return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildStateValuationsSet() const { - return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 53216e240..f0a90ad27 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -158,34 +158,6 @@ namespace storm { */ std::string getJaniInputFilename() const; - /*! - * Retrieves whether the option to use the JIT builder is set. - * - * @return True iff the JIT builder is to be used. - */ - bool isJitSet() const; - - /*! - * Retrieves whether the model exploration order was set. - * - * @return True if the model exploration option was set. - */ - bool isExplorationOrderSet() const; - - /*! - * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). - * - * @return True if additional checks are to be performed. - */ - bool isExplorationChecksSet() const; - - /*! - * Retrieves the exploration order if it was set. - * - * @return The chosen exploration order. - */ - storm::builder::ExplorationOrder getExplorationOrder() const; - /*! * Retrieves whether the transition reward option was set. * @@ -218,7 +190,7 @@ namespace storm { /*! * Retrieves whether the choice labeling option was set. - * + * * @return True iff the choice labeling option was set. */ bool isChoiceLabelingSet() const; @@ -231,15 +203,7 @@ namespace storm { */ std::string getChoiceLabelingFilename() const; - /*! - * Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As - * soon as the returned memento goes out of scope, the original value is restored. - * - * @param stateToSet The value that is to be set for the option. - * @return The memento that will eventually restore the original value. - */ - std::unique_ptr<storm::settings::SettingMemento> overridePrismCompatibilityMode(bool stateToSet); - + /*! * Retrieves whether the export-to-dot option was set. * @@ -286,36 +250,6 @@ namespace storm { */ std::string getPropertyFilter() const; - /*! - * Retrieves whether the PRISM compatibility mode was enabled. - * - * @return True iff the PRISM compatibility mode was enabled. - */ - bool isPrismCompatibilityEnabled() const; - - /** - * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. - */ - bool isNoBuildModelSet() const; - - /*! - * Retrieves whether the full model should be build, that is, the model including all labels and rewards. - * - * @return true iff the full model should be build. - */ - bool isBuildFullModelSet() const; - - /*! - * Retrieves whether the choice labels should be build - * @return - */ - bool isBuildChoiceLabelsSet() const; - - /*! - * Retrieves whether the choice labels should be build - * @return - */ - bool isBuildStateValuationsSet() const; bool check() const override; void finalize() override; @@ -337,22 +271,11 @@ namespace storm { static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; - static const std::string jitOptionName; - static const std::string explorationChecksOptionName; - static const std::string explorationChecksOptionShortName; - static const std::string explorationOrderOptionName; - static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; static const std::string choiceLabelingOptionName; static const std::string constantsOptionName; static const std::string constantsOptionShortName; - static const std::string prismCompatibilityOptionName; - static const std::string prismCompatibilityOptionShortName; - static const std::string fullModelBuildOptionName; - static const std::string noBuildOptionName; - static const std::string buildChoiceLabelOptionName; - static const std::string buildStateValuationsOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index c7fe0bd01..1a32c610b 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -4,7 +4,6 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/constants.h" diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 387423066..9a4132420 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -8,8 +8,6 @@ #include "storm/storage/jani/Property.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -138,7 +136,7 @@ namespace storm { std::set<std::string> appearingModules; }; - Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename, uint_fast64_t lineNumber, bool finalModel) + Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename, uint_fast64_t lineNumber, bool finalModel) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), @@ -146,7 +144,7 @@ namespace storm { formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct), labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), - synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() + synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility) { // Start by creating the necessary mappings from the given ones. @@ -166,7 +164,7 @@ namespace storm { if (finalModel) { // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian // commands and issue a warning. - if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismCompatibilityEnabled()) { + if (modelType == storm::prism::Program::ModelType::CTMC && prismCompatibility) { bool hasProbabilisticCommands = false; for (auto& module : this->modules) { for (auto& command : module.getCommands()) { @@ -689,7 +687,7 @@ namespace storm { newModules.push_back(module.restrictCommands(indexSet)); } - return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility); } void Program::createMappings() { @@ -783,7 +781,7 @@ namespace storm { } } - return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility); } Program Program::substituteConstants() const { @@ -846,7 +844,7 @@ namespace storm { newLabels.emplace_back(label.substitute(constantSubstitution)); } - return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility); } void Program::checkValidity(Program::ValidityCheckLevel lvl) const { @@ -1122,7 +1120,7 @@ namespace storm { } if (hasLabeledMarkovianCommand) { - if (storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismCompatibilityEnabled()) { + if (prismCompatibility) { STORM_LOG_WARN_COND(false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics."); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics."); @@ -1362,7 +1360,7 @@ namespace storm { } } - return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility); } Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const { @@ -1558,7 +1556,7 @@ namespace storm { // Finally, we can create the module and the program and return it. storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); - return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), this->getFilename(), 0, true); + return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index a92fdcbb6..46d704803 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -57,7 +57,7 @@ namespace storm { * @param lineNumber The line number in which the program is defined. * @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing. */ - Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true); + Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true); // Provide default implementations for constructors and assignments. Program() = default; @@ -697,6 +697,8 @@ namespace storm { // A mapping from variable names to the modules in which they were declared. std::map<std::string, uint_fast64_t> variableToModuleIndexMap; + + bool prismCompatibility; }; std::ostream& operator<<(std::ostream& out, Program::ModelType const& type); diff --git a/src/test/storm/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp index 0bc5940e0..fa657a96f 100644 --- a/src/test/storm/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/DdJaniModelBuilderTest.cpp @@ -15,7 +15,6 @@ #include "storm/settings/SettingMemento.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -89,35 +88,32 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { } TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder; std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(66ul, model->getNumberOfStates()); @@ -125,35 +121,33 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) { } TEST(DdJaniModelBuilderTest_Cudd, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder; std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); model = builder.build(janiModel); EXPECT_EQ(66ul, model->getNumberOfStates()); diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index 04a4a391b..1ff4a79fe 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/settings/SettingMemento.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" @@ -78,35 +78,33 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { } TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); @@ -114,35 +112,33 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { } TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index 4a0584ea9..4f21c3a64 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -8,7 +8,6 @@ #include "storm/generator/JaniNextStateGenerator.h" #include "storm/storage/jani/Model.h" -#include "storm/settings/modules/IOSettings.h" TEST(ExplicitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); @@ -44,35 +43,32 @@ TEST(ExplicitJaniModelBuilderTest, Dtmc) { } TEST(ExplicitJaniModelBuilderTest, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::jani::Model janiModel = program.toJani(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); janiModel = program.toJani(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); janiModel = program.toJani(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); janiModel = program.toJani(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); janiModel = program.toJani(); model = storm::builder::ExplicitModelBuilder<double>(janiModel).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); diff --git a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp index efb10e00f..334735b02 100644 --- a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -8,7 +8,6 @@ #include "storm/storage/jani/Model.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); @@ -44,35 +43,33 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { } TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::jani::Model janiModel = program.toJani(); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); janiModel = program.toJani(); model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); janiModel = program.toJani(); model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); janiModel = program.toJani(); model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); janiModel = program.toJani(); model = storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();; EXPECT_EQ(66ul, model->getNumberOfStates()); diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index 4da7e5039..8e5929618 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -2,11 +2,9 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/settings/SettingMemento.h" #include "storm/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" -#include "storm/settings/modules/IOSettings.h" TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); @@ -37,31 +35,29 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) { } TEST(ExplicitPrismModelBuilderTest, Ctmc) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); model = storm::builder::ExplicitModelBuilder<double>(program).build(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); model = storm::builder::ExplicitModelBuilder<double>(program).build(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true); model = storm::builder::ExplicitModelBuilder<double>(program).build(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); model = storm::builder::ExplicitModelBuilder<double>(program).build(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); diff --git a/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 56a1a498f..62f77d023 100644 --- a/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -13,7 +13,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" @@ -21,11 +20,8 @@ #include "storm/storage/expressions/ExpressionManager.h" TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -98,11 +94,8 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { } TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -160,11 +153,8 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { } TEST(GmmxxCtmcCslModelCheckerTest, Polling) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -194,18 +184,13 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { } TEST(GmmxxCtmcCslModelCheckerTest, Fms) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // No properties to check at this point. } TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); diff --git a/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index e6a167fc9..821bf9297 100644 --- a/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -17,18 +17,15 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/storage/expressions/ExpressionManager.h" TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -122,11 +119,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -220,11 +214,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -300,11 +291,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -380,11 +368,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -417,11 +402,9 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -454,18 +437,13 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // No properties to check at this point. } TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -550,11 +528,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { } TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr<storm::logic::Formula const> formula(nullptr); diff --git a/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp index ed79b2db8..246ac41ca 100644 --- a/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -14,14 +14,10 @@ #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/IOSettings.h" TEST(NativeCtmcCslModelCheckerTest, Cluster) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -86,11 +82,9 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { } TEST(NativeCtmcCslModelCheckerTest, Embedded) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -143,11 +137,8 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { } TEST(NativeCtmcCslModelCheckerTest, Polling) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -170,18 +161,14 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { } TEST(NativeCtmcCslModelCheckerTest, Fms) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // No properties to check at this point. } TEST(NativeCtmcCslModelCheckerTest, Tandem) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); diff --git a/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 6daa4a818..f8aa35701 100644 --- a/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -17,16 +17,12 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -120,11 +116,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { } TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -218,11 +211,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { } TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -298,11 +288,9 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { } TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - + // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -378,11 +366,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { } TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -415,11 +400,9 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { } TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -452,18 +435,14 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { } TEST(NativeHybridCtmcCslModelCheckerTest, Fms) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // No properties to check at this point. } TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); @@ -550,11 +529,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { } TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { - // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - // Parse the model description. - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program); std::shared_ptr<storm::logic::Formula const> formula(nullptr); From 6501fffac33245b76cc87e47147fccbc679fbd73 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 11:14:05 +0100 Subject: [PATCH 20/33] several optimizations related to explicit model building --- src/storm/builder/ExplicitModelBuilder.cpp | 8 ++-- src/storm/builder/ExplicitModelBuilder.h | 2 +- .../CounterexampleGeneratorSettings.cpp | 1 - src/storm/storage/BitVectorHashMap.cpp | 5 +++ src/storm/storage/BitVectorHashMap.h | 7 +++ .../expressions/CompiledExpression.cpp | 21 +++++++++ .../storage/expressions/CompiledExpression.h | 20 +++++++++ src/storm/storage/expressions/Expression.cpp | 20 ++++++++- src/storm/storage/expressions/Expression.h | 20 +++++++++ .../expressions/ExprtkCompiledExpression.cpp | 19 ++++++++ .../expressions/ExprtkCompiledExpression.h | 25 +++++++++++ .../expressions/ExprtkExpressionEvaluator.cpp | 43 +++++++------------ .../expressions/ExprtkExpressionEvaluator.h | 22 +++------- .../SyntacticalEqualityCheckVisitor.cpp | 2 +- .../SyntacticalEqualityCheckVisitor.h | 2 +- src/storm/utility/exprtk.h | 11 +++++ 16 files changed, 175 insertions(+), 53 deletions(-) create mode 100644 src/storm/storage/expressions/CompiledExpression.cpp create mode 100644 src/storm/storage/expressions/CompiledExpression.h create mode 100644 src/storm/storage/expressions/ExprtkCompiledExpression.cpp create mode 100644 src/storm/storage/expressions/ExprtkCompiledExpression.h create mode 100644 src/storm/utility/exprtk.h diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index d4aa08590..d6096e750 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -91,12 +91,12 @@ namespace storm { if (actualIndexBucketPair.first == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { - statesToExplore.push_front(state); + statesToExplore.emplace_front(state, actualIndexBucketPair.first); // Reserve one slot for the new state in the remapping. stateRemapping.get().push_back(storm::utility::zero<StateType>()); } else if (options.explorationOrder == ExplorationOrder::Bfs) { - statesToExplore.push_back(state); + statesToExplore.emplace_back(state, actualIndexBucketPair.first); } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } @@ -139,8 +139,8 @@ namespace storm { // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. - CompressedState currentState = statesToExplore.front(); - StateType currentIndex = stateStorage.stateToId.getValue(currentState); + CompressedState currentState = statesToExplore.front().first; + StateType currentIndex = statesToExplore.front().second; statesToExplore.pop_front(); // If the exploration order differs from breadth-first, we remember that this row group was actually diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index ef5da691b..9440b7e08 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -136,7 +136,7 @@ namespace storm { storm::storage::sparse::StateStorage<StateType> stateStorage; /// A set of states that still need to be explored. - std::deque<CompressedState> statesToExplore; + std::deque<std::pair<CompressedState, StateType>> statesToExplore; /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be /// built in case the exploration order is not BFS. diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp index f2c4a483d..b33a332df 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp @@ -29,7 +29,6 @@ namespace storm { return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); } - bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; } diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index 9cec1aa20..434ab6906 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -210,6 +210,11 @@ namespace storm { return values[flagBucketPair.second]; } + template<class ValueType, class Hash> + ValueType BitVectorHashMap<ValueType, Hash>::getValue(std::size_t bucket) const { + return values[bucket]; + } + template<class ValueType, class Hash> bool BitVectorHashMap<ValueType, Hash>::contains(storm::storage::BitVector const& key) const { return findBucket(key).first; diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h index e2ca51a5e..7c400c1cd 100644 --- a/src/storm/storage/BitVectorHashMap.h +++ b/src/storm/storage/BitVectorHashMap.h @@ -113,6 +113,13 @@ namespace storm { * @return The value associated with the given key (if any). */ ValueType getValue(storm::storage::BitVector const& key) const; + + /*! + * Retrieves the value associated with the given bucket. + * + * @return The value associated with the given bucket (if any). + */ + ValueType getValue(std::size_t bucket) const; /*! * Checks if the given key is already contained in the map. diff --git a/src/storm/storage/expressions/CompiledExpression.cpp b/src/storm/storage/expressions/CompiledExpression.cpp new file mode 100644 index 000000000..759ea899c --- /dev/null +++ b/src/storm/storage/expressions/CompiledExpression.cpp @@ -0,0 +1,21 @@ +#include "storm/storage/expressions/CompiledExpression.h" + +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + +namespace storm { + namespace expressions { + + bool CompiledExpression::isExprtkCompiledExpression() const { + return false; + } + + ExprtkCompiledExpression& CompiledExpression::asExprtkCompiledExpression() { + return static_cast<ExprtkCompiledExpression&>(*this); + } + + ExprtkCompiledExpression const& CompiledExpression::asExprtkCompiledExpression() const { + return static_cast<ExprtkCompiledExpression const&>(*this); + } + + } +} diff --git a/src/storm/storage/expressions/CompiledExpression.h b/src/storm/storage/expressions/CompiledExpression.h new file mode 100644 index 000000000..786408c94 --- /dev/null +++ b/src/storm/storage/expressions/CompiledExpression.h @@ -0,0 +1,20 @@ +#pragma once + +namespace storm { + namespace expressions { + + class ExprtkCompiledExpression; + + class CompiledExpression { + public: + + virtual bool isExprtkCompiledExpression() const; + ExprtkCompiledExpression& asExprtkCompiledExpression(); + ExprtkCompiledExpression const& asExprtkCompiledExpression() const; + + private: + // Currently empty. + }; + + } +} diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 95c4f69e0..ed00728f0 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -9,6 +9,7 @@ #include "storm/storage/expressions/ChangeManagerVisitor.h" #include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h" #include "storm/storage/expressions/Expressions.h" +#include "storm/storage/expressions/CompiledExpression.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/macros.h" @@ -26,6 +27,11 @@ namespace storm { STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager."); } + // Spell out destructor explicitly so we can use forward declarations in the header. + Expression::~Expression() { + // Intentionally left empty. + } + Expression::Expression(std::shared_ptr<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) { // Intentionally left empty. } @@ -196,7 +202,19 @@ namespace storm { return true; } SyntacticalEqualityCheckVisitor checker; - return checker.isSyntaticallyEqual(*this, other); + return checker.isSyntacticallyEqual(*this, other); + } + + bool Expression::hasCompiledExpression() const { + return static_cast<bool>(compiledExpression); + } + + void Expression::setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const { + this->compiledExpression = compiledExpression; + } + + CompiledExpression const& Expression::getCompiledExpression() const { + return *compiledExpression; } std::string Expression::toString() const { diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 26d6033c6..98a2e6417 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -15,6 +15,7 @@ namespace storm { class ExpressionManager; class Variable; class ExpressionVisitor; + class CompiledExpression; class Expression { public: @@ -58,6 +59,7 @@ namespace storm { friend Expression maximum(Expression const& first, Expression const& second); Expression() = default; + ~Expression(); /*! * Creates an expression representing the given variable. @@ -358,11 +360,29 @@ namespace storm { */ bool isSyntacticallyEqual(storm::expressions::Expression const& other) const; + /*! + * Retrieves whether this expression object has an associated compiled expression. + */ + bool hasCompiledExpression() const; + + /*! + * Associates the given compiled expression with this expression object. + */ + void setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const; + + /*! + * Retrieves the associated compiled expression object (if there is any). + */ + CompiledExpression const& getCompiledExpression() const; + friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: // A pointer to the underlying base expression. std::shared_ptr<BaseExpression const> expressionPtr; + + // A pointer to an associated compiled expression object (if any). + mutable std::shared_ptr<CompiledExpression> compiledExpression; }; // Provide operator overloads to conveniently construct new expressions from other expressions. diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.cpp b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp new file mode 100644 index 000000000..2dda7945d --- /dev/null +++ b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp @@ -0,0 +1,19 @@ +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + +namespace storm { + namespace expressions { + + ExprtkCompiledExpression::ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression) : exprtkCompiledExpression(exprtkCompiledExpression) { + // Intentionally left empty. + } + + ExprtkCompiledExpression::CompiledExpressionType const& ExprtkCompiledExpression::getCompiledExpression() const { + return exprtkCompiledExpression; + } + + bool ExprtkCompiledExpression::isExprtkCompiledExpression() const { + return true; + } + + } +} diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.h b/src/storm/storage/expressions/ExprtkCompiledExpression.h new file mode 100644 index 000000000..b2c98fc2b --- /dev/null +++ b/src/storm/storage/expressions/ExprtkCompiledExpression.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/storage/expressions/CompiledExpression.h" + +#include "storm/utility/exprtk.h" + +namespace storm { + namespace expressions { + + class ExprtkCompiledExpression : public CompiledExpression { + public: + typedef exprtk::expression<double> CompiledExpressionType; + + ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression); + + CompiledExpressionType const& getCompiledExpression() const; + + virtual bool isExprtkCompiledExpression() const override; + + private: + CompiledExpressionType exprtkCompiledExpression; + }; + + } +} diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp index 70cd6e162..3b8b3ea70 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -26,34 +26,26 @@ namespace storm { template<typename RationalType> bool ExprtkExpressionEvaluatorBase<RationalType>::asBool(Expression const& expression) const { - std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return compiledExpression.value() == ValueType(1); - } - return expressionPair->second.value() == ValueType(1); + auto const& compiledExpression = getCompiledExpression(expression); + return compiledExpression.value() == ValueType(1); } template<typename RationalType> int_fast64_t ExprtkExpressionEvaluatorBase<RationalType>::asInt(Expression const& expression) const { - std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return static_cast<int_fast64_t>(compiledExpression.value()); - } - return static_cast<int_fast64_t>(expressionPair->second.value()); + auto const& compiledExpression = getCompiledExpression(expression); + return static_cast<int_fast64_t>(compiledExpression.value()); } template<typename RationalType> - typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const { - std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType()); - CompiledExpressionType& compiledExpression = result.first->second; - compiledExpression.register_symbol_table(*symbolTable); - bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression); - STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")"); - return compiledExpression; + typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType const& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const { + if (!expression.hasCompiledExpression() || !expression.getCompiledExpression().isExprtkCompiledExpression()) { + CompiledExpressionType compiledExpression; + compiledExpression.register_symbol_table(*symbolTable); + bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression); + STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")"); + expression.setCompiledExpression(std::make_shared<ExprtkCompiledExpression>(compiledExpression)); + } + return expression.getCompiledExpression().asExprtkCompiledExpression().getCompiledExpression(); } template<typename RationalType> @@ -76,13 +68,8 @@ namespace storm { } double ExprtkExpressionEvaluator::asRational(Expression const& expression) const { - std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return static_cast<double>(compiledExpression.value()); - } - return static_cast<double>(expressionPair->second.value()); + auto const& compiledExpression = getCompiledExpression(expression); + return static_cast<double>(compiledExpression.value()); } template class ExprtkExpressionEvaluatorBase<double>; diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h index 1eefe163b..e6a7c6fb4 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h @@ -6,18 +6,12 @@ #include "storm/storage/expressions/ExpressionEvaluatorBase.h" -#pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wunused-variable" - -#pragma GCC diagnostic push - -#include "exprtk.hpp" - -#pragma GCC diagnostic pop -#pragma clang diagnostic pop +#include "storm/utility/exprtk.h" #include "storm/storage/expressions/ToExprtkStringVisitor.h" +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + namespace storm { namespace expressions { template <typename RationalType> @@ -34,15 +28,14 @@ namespace storm { protected: typedef double ValueType; - typedef exprtk::expression<ValueType> CompiledExpressionType; - typedef std::unordered_map<std::shared_ptr<BaseExpression const>, CompiledExpressionType> CacheType; + typedef ExprtkCompiledExpression::CompiledExpressionType CompiledExpressionType; /*! - * Adds a compiled version of the given expression to the internal storage. + * Retrieves a compiled version of the given expression. * * @param expression The expression that is to be compiled. */ - CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const; + CompiledExpressionType const& getCompiledExpression(storm::expressions::Expression const& expression) const; // The parser used. mutable std::unique_ptr<exprtk::parser<ValueType>> parser; @@ -54,9 +47,6 @@ namespace storm { std::vector<ValueType> booleanValues; std::vector<ValueType> integerValues; std::vector<ValueType> rationalValues; - - // A mapping of expressions to their compiled counterpart. - mutable CacheType compiledExpressions; }; class ExprtkExpressionEvaluator : public ExprtkExpressionEvaluatorBase<double> { diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp index c1133c9db..7f45240d7 100644 --- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp +++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - bool SyntacticalEqualityCheckVisitor::isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) { + bool SyntacticalEqualityCheckVisitor::isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) { return boost::any_cast<bool>(expression1.accept(*this, std::ref(expression2.getBaseExpression()))); } diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h index ef556d827..2c255b5c2 100644 --- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h +++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h @@ -9,7 +9,7 @@ namespace storm { class SyntacticalEqualityCheckVisitor : public ExpressionVisitor { public: - bool isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2); + bool isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2); virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; diff --git a/src/storm/utility/exprtk.h b/src/storm/utility/exprtk.h new file mode 100644 index 000000000..3aba1b8db --- /dev/null +++ b/src/storm/utility/exprtk.h @@ -0,0 +1,11 @@ +#pragma once + +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wunused-variable" + +#pragma GCC diagnostic push + +#include "exprtk.hpp" + +#pragma GCC diagnostic pop +#pragma clang diagnostic pop From ac759d267190d87566031375aedcead5826b857c Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 14:06:39 +0100 Subject: [PATCH 21/33] minor performance improvements to model building --- src/storm/builder/ExplicitModelBuilder.cpp | 16 +++++++++------- src/storm/generator/JaniNextStateGenerator.cpp | 4 ++-- src/storm/generator/JaniNextStateGenerator.h | 2 +- src/storm/generator/NextStateGenerator.cpp | 6 ++++-- src/storm/generator/NextStateGenerator.h | 6 +++--- src/storm/generator/PrismNextStateGenerator.cpp | 4 ++-- src/storm/generator/PrismNextStateGenerator.h | 2 +- src/storm/storage/sparse/StateStorage.h | 2 +- 8 files changed, 23 insertions(+), 19 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index d6096e750..ac4b554d5 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -89,20 +89,22 @@ namespace storm { // Check, if the state was already registered. std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - if (actualIndexBucketPair.first == newIndex) { + StateType actualIndex = actualIndexBucketPair.first; + + if (actualIndex == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { - statesToExplore.emplace_front(state, actualIndexBucketPair.first); + statesToExplore.emplace_front(state, actualIndex); // Reserve one slot for the new state in the remapping. stateRemapping.get().push_back(storm::utility::zero<StateType>()); } else if (options.explorationOrder == ExplorationOrder::Bfs) { - statesToExplore.emplace_back(state, actualIndexBucketPair.first); + statesToExplore.emplace_back(state, actualIndex); } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } } - return actualIndexBucketPair.first; + return actualIndex; } template <typename ValueType, typename RewardModelType, typename StateType> @@ -306,7 +308,7 @@ namespace storm { buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); - // initialize the model components with the obtained information. + // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); // Now finalize all reward models. @@ -316,7 +318,7 @@ namespace storm { // Build the choice labeling modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); - // if requested, build the state valuations and choice origins + // If requested, build the state valuations and choice origins if (generator->getOptions().isBuildStateValuationsSet()) { std::vector<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { @@ -334,7 +336,7 @@ namespace storm { template <typename ValueType, typename RewardModelType, typename StateType> storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() { - return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); + return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } // Explicitly instantiate the class. diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f7d86e914..40481fd83 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -608,7 +608,7 @@ namespace storm { } template<typename ValueType, typename StateType> - storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) { + storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap; @@ -625,7 +625,7 @@ namespace storm { transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second)); } - return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions); + return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } template<typename ValueType, typename StateType> diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 3fcfc2777..594efc91c 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -30,7 +30,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override; private: /*! diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 15c6048c3..f69014364 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -53,7 +53,7 @@ namespace storm { } template<typename ValueType, typename StateType> - storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) { + storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) { for (auto const& expression : this->options.getExpressionLabels()) { std::stringstream stream; @@ -67,12 +67,14 @@ namespace storm { labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it)); // Prepare result. - storm::models::sparse::StateLabeling result(states.size()); + storm::models::sparse::StateLabeling result(stateStorage.getNumberOfStates()); // Initialize labeling. for (auto const& label : labelsAndExpressions) { result.addLabel(label.first); } + + storm::storage::BitVectorHashMap<StateType> const& states = stateStorage.stateToId; for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 25335dbfc..54f7f1024 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -7,7 +7,7 @@ #include <boost/variant.hpp> #include "storm/storage/expressions/Expression.h" -#include "storm/storage/BitVectorHashMap.h" +#include "storm/storage/sparse/StateStorage.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/sparse/ChoiceOrigins.h" @@ -61,7 +61,7 @@ namespace storm { storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -71,7 +71,7 @@ namespace storm { /*! * Creates the state labeling for the given states using the provided labels and expressions. */ - storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions); + storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions); void postprocess(StateBehavior<ValueType, StateType>& result); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index bf9d73876..db74175c0 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -575,7 +575,7 @@ namespace storm { } template<typename ValueType, typename StateType> - storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) { + storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) { // Gather a vector of labels and their expressions. std::vector<std::pair<std::string, storm::expressions::Expression>> labels; if (this->options.isBuildAllLabelsSet()) { @@ -592,7 +592,7 @@ namespace storm { } } - return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, labels); + return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); } template<typename ValueType, typename StateType> diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 0097e7055..5cc8ce9ba 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -28,7 +28,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override; virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override; diff --git a/src/storm/storage/sparse/StateStorage.h b/src/storm/storage/sparse/StateStorage.h index 789e16c88..65b592cb5 100644 --- a/src/storm/storage/sparse/StateStorage.h +++ b/src/storm/storage/sparse/StateStorage.h @@ -27,7 +27,7 @@ namespace storm { // The number of bits of each state. uint64_t bitsPerState; - // The number of states that were found in the exploration so far. + // Get the number of states that were found in the exploration so far. uint_fast64_t getNumberOfStates() const; }; From 8ba365fee9474a27244a943c15f982a16566b912 Mon Sep 17 00:00:00 2001 From: Matthias Volk <matthias.volk@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 15:58:04 +0100 Subject: [PATCH 22/33] Fixed includes after moving files --- src/storm-dft/settings/DftSettings.cpp | 4 ++-- src/storm-gspn-cli/storm-gspn.cpp | 4 ++-- src/storm-gspn/storm-gspn.h | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index ce48c6fd9..b80afa2ce 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -16,8 +16,8 @@ #include "storm/settings/modules/BisimulationSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/JaniExportSettings.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" namespace storm { diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index fc493391a..d6a493981 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -28,8 +28,8 @@ #include "storm/exceptions/FileIoException.h" #include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h index d043ce53d..e0d6dd3a6 100644 --- a/src/storm-gspn/storm-gspn.h +++ b/src/storm-gspn/storm-gspn.h @@ -6,7 +6,7 @@ #include "storm-gspn/storage/gspn/GSPN.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm/utility/file.h" From a072ef5310434381171b2b0ac71cf15991e057be Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 16:06:24 +0100 Subject: [PATCH 23/33] some fixes to handle large parameters --- src/storm/adapters/Z3ExpressionAdapter.cpp | 2 +- src/storm/utility/cli.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index d715f4599..74e2d219c 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -237,7 +237,7 @@ namespace storm { } boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { - return context.int_val(static_cast<int>(expression.getValue())); + return context.int_val(expression.getValue()); } boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp index ded3f9a6a..ddc46fae2 100644 --- a/src/storm/utility/cli.cpp +++ b/src/storm/utility/cli.cpp @@ -55,7 +55,7 @@ namespace storm { throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << "."; } } else if (variable.hasIntegerType()) { - int_fast64_t integerValue = std::stoi(value); + int_fast64_t integerValue = std::stoll(value); constantDefinitions[variable] = manager.integer(integerValue); } else if (variable.hasRationalType()) { try { From ce5c740c511f8acb8f32a664ecef3143e08e33cf Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 16:31:06 +0100 Subject: [PATCH 24/33] resolved ambiguity to make gcc happy --- src/storm/adapters/Z3ExpressionAdapter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index 74e2d219c..e55f5fe3c 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -237,7 +237,7 @@ namespace storm { } boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { - return context.int_val(expression.getValue()); + return context.int_val(static_cast<long long>(expression.getValue())); } boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { From b110172b0da1201dcf78c7f22f67aeef27624c44 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 3 Nov 2017 20:11:32 +0100 Subject: [PATCH 25/33] fixed bug in MaxSMT-based counterexample generation pointed out by Milan Ceska --- src/storm/counterexamples/SMTMinimalLabelSetGenerator.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index e2373b567..fe313ab51 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -451,7 +451,7 @@ namespace storm { // 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 // of the current choice have enabled synchronization options. - storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); + storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(true); for (auto label : labelSetFollowingSetsPair.first) { storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); std::set<boost::container::flat_set<uint_fast64_t>> const& synchsForCommand = synchronizingLabels.at(label); From 456523b6ecf87d9dc047098adf21601b7dd25c47 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@gmail.com> Date: Sun, 5 Nov 2017 22:53:01 +0100 Subject: [PATCH 26/33] fix missing initialisations --- src/storm-pars/settings/ParsSettings.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index 53907dc1c..e36793b04 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -1,3 +1,4 @@ +#include <storm/settings/modules/CounterexampleGeneratorSettings.h> #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" @@ -7,6 +8,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/SylvanSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" @@ -33,7 +35,10 @@ namespace storm { storm::settings::addModule<storm::settings::modules::CoreSettings>(); storm::settings::addModule<storm::settings::modules::ParametricSettings>(); storm::settings::addModule<storm::settings::modules::RegionSettings>(); - + storm::settings::addModule<storm::settings::modules::BuildSettings>(); + storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); + + storm::settings::addModule<storm::settings::modules::DebugSettings>(); storm::settings::addModule<storm::settings::modules::SylvanSettings>(); storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>(); From 8e3e99c4cebbf4ff6f7b1cb4b5363648018f75c4 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 6 Nov 2017 21:32:06 +0100 Subject: [PATCH 27/33] fixed bug in submatrix computation pointed out by Timo Gros --- src/storm/storage/SparseMatrix.cpp | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index bf1b15d14..d4c9ba5ad 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -897,12 +897,11 @@ namespace storm { // Start by creating a temporary vector that stores for each index whose bit is set to true the number of // bits that were set before that particular index. std::vector<index_type> columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices(); - std::vector<index_type>* rowBitsSetBeforeIndex; - if (&rowGroupConstraint == &columnConstraint) { - rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex; - } else { - rowBitsSetBeforeIndex = new std::vector<index_type>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); + std::unique_ptr<std::vector<index_type>> tmp; + if (rowGroupConstraint != columnConstraint) { + tmp = std::make_unique<std::vector<index_type>>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); } + std::vector<index_type> const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex; // Then, we need to determine the number of entries and the number of rows of the submatrix. index_type subEntries = 0; @@ -917,7 +916,7 @@ namespace storm { if (columnConstraint.get(it->getColumn())) { ++subEntries; - if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { + if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { foundDiagonalElement = true; } } @@ -946,9 +945,9 @@ namespace storm { for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { if (columnConstraint.get(it->getColumn())) { - if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { + if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { insertedDiagonalElement = true; - } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > (*rowBitsSetBeforeIndex)[index]) { + } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > rowBitsSetBeforeIndex[index]) { matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>()); insertedDiagonalElement = true; } @@ -956,18 +955,13 @@ namespace storm { } } if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) { - matrixBuilder.addNextValue(rowGroupCount, rowGroupCount, storm::utility::zero<ValueType>()); + matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>()); } ++rowCount; } ++rowGroupCount; } - // If the constraints were not the same, we have allocated some additional memory we need to free now. - if (&rowGroupConstraint != &columnConstraint) { - delete rowBitsSetBeforeIndex; - } - return matrixBuilder.build(); } From ace351bd71746c939725cec87f7fe5a30e253381 Mon Sep 17 00:00:00 2001 From: Sebastian Junges <sebastian.junges@rwth-aachen.de> Date: Wed, 8 Nov 2017 15:35:03 +0100 Subject: [PATCH 28/33] Constants wrongfully marked as not graphpresreving. Bugfix for bug reported by Nils Jansen. --- src/storm/storage/prism/Program.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 9a4132420..edd17c3d0 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -247,13 +247,7 @@ namespace storm { } } - // Then check the formulas. - for (auto const& formula : this->getFormulas()) { - if (formula.getExpression().containsVariable(undefinedConstantVariables)) { - return false; - } - } - + // Proceed by checking each of the modules. for (auto const& module : this->getModules()) { if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) { From 1f9e2967c837d812f57b57dcc1a4a62bc5f9231d Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 13 Nov 2017 16:56:57 +0100 Subject: [PATCH 29/33] some optimizations in explicit model building --- src/storm/builder/jit/Distribution.cpp | 54 ++++++++++- src/storm/builder/jit/Distribution.h | 10 ++ src/storm/builder/jit/DistributionEntry.cpp | 33 ++++--- src/storm/builder/jit/DistributionEntry.h | 8 +- .../builder/jit/ModelComponentsBuilder.cpp | 2 +- src/storm/generator/NextStateGenerator.cpp | 2 +- .../generator/PrismNextStateGenerator.cpp | 47 ++++----- src/storm/storage/BitVector.cpp | 14 +++ src/storm/storage/BitVector.h | 5 + src/storm/storage/BitVectorHashMap.cpp | 95 +++++++------------ src/storm/storage/BitVectorHashMap.h | 23 ++--- 11 files changed, 166 insertions(+), 127 deletions(-) diff --git a/src/storm/builder/jit/Distribution.cpp b/src/storm/builder/jit/Distribution.cpp index 29a0a1075..2e3c0c5aa 100644 --- a/src/storm/builder/jit/Distribution.cpp +++ b/src/storm/builder/jit/Distribution.cpp @@ -2,6 +2,8 @@ #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/storage/BitVector.h" + namespace storm { namespace builder { namespace jit { @@ -11,16 +13,48 @@ namespace storm { // Intentionally left empty. } + template <typename IndexType, typename ValueType> + Distribution<IndexType, ValueType>::Distribution(Distribution<IndexType, ValueType> const& other) { + this->storage = other.storage; + this->compressed = other.compressed; + } + + template <typename IndexType, typename ValueType> + Distribution<IndexType, ValueType>::Distribution(Distribution<IndexType, ValueType>&& other) { + this->storage = std::move(other.storage); + this->compressed = other.compressed; + other.compressed = true; + } + + template <typename IndexType, typename ValueType> + Distribution<IndexType, ValueType>& Distribution<IndexType, ValueType>::operator=(Distribution<IndexType, ValueType> const& other) { + if (this != &other) { + this->storage = other.storage; + this->compressed = other.compressed; + } + return *this; + } + + template <typename IndexType, typename ValueType> + Distribution<IndexType, ValueType>& Distribution<IndexType, ValueType>::operator=(Distribution<IndexType, ValueType>&& other) { + if (this != &other) { + this->storage = std::move(other.storage); + this->compressed = other.compressed; + other.compressed = true; + } + return *this; + } + template <typename IndexType, typename ValueType> void Distribution<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) { storage.push_back(entry); - compressed &= storage.back().getIndex() < entry.getIndex(); + compressed &= storage.back().getState() < entry.getState(); } template <typename IndexType, typename ValueType> void Distribution<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) { storage.emplace_back(index, value); - compressed &= storage.back().getIndex() < index; + compressed &= storage.back().getState() < index; } template <typename IndexType, typename ValueType> @@ -34,7 +68,7 @@ namespace storm { if (!compressed) { std::sort(storage.begin(), storage.end(), [] (DistributionEntry<IndexType, ValueType> const& a, DistributionEntry<IndexType, ValueType> const& b) { - return a.getIndex() < b.getIndex(); + return a.getState() < b.getState(); } ); @@ -45,7 +79,7 @@ namespace storm { if (first != last) { auto result = first; while (++first != last) { - if (!(result->getIndex() == first->getIndex())) { + if (!(result->getState() == first->getState())) { if (++result != first) { *result = std::move(*first); } @@ -68,6 +102,12 @@ namespace storm { } } + template <typename IndexType, typename ValueType> + void Distribution<IndexType, ValueType>::clear() { + this->storage.clear(); + this->compressed = true; + } + template <typename IndexType, typename ValueType> typename Distribution<IndexType, ValueType>::ContainerType::iterator Distribution<IndexType, ValueType>::begin() { return storage.begin(); @@ -91,7 +131,11 @@ namespace storm { template class Distribution<uint32_t, double>; template class Distribution<uint32_t, storm::RationalNumber>; template class Distribution<uint32_t, storm::RationalFunction>; - + + template class Distribution<storm::storage::BitVector, double>; + template class Distribution<storm::storage::BitVector, storm::RationalNumber>; + template class Distribution<storm::storage::BitVector, storm::RationalFunction>; + } } } diff --git a/src/storm/builder/jit/Distribution.h b/src/storm/builder/jit/Distribution.h index 670b30a2c..f0e933d91 100644 --- a/src/storm/builder/jit/Distribution.h +++ b/src/storm/builder/jit/Distribution.h @@ -15,6 +15,11 @@ namespace storm { Distribution(); + Distribution(Distribution const&); + Distribution(Distribution&&); + Distribution& operator=(Distribution const&); + Distribution& operator=(Distribution&&); + /*! * Adds the given entry to the distribution. */ @@ -41,6 +46,11 @@ namespace storm { */ void divide(ValueType const& value); + /*! + * Clears this distribution. + */ + void clear(); + /*! * Access to iterators over the entries of the distribution. Note that there may be multiple entries for * the same index. Also, no order is guaranteed. After a call to compress, the order is guaranteed to be diff --git a/src/storm/builder/jit/DistributionEntry.cpp b/src/storm/builder/jit/DistributionEntry.cpp index 352908d4e..1fd7448bc 100644 --- a/src/storm/builder/jit/DistributionEntry.cpp +++ b/src/storm/builder/jit/DistributionEntry.cpp @@ -2,37 +2,39 @@ #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/storage/BitVector.h" + namespace storm { namespace builder { namespace jit { - template <typename IndexType, typename ValueType> - DistributionEntry<IndexType, ValueType>::DistributionEntry() : index(0), value(0) { + template <typename StateType, typename ValueType> + DistributionEntry<StateType, ValueType>::DistributionEntry() : state(0), value(0) { // Intentionally left empty. } - template <typename IndexType, typename ValueType> - DistributionEntry<IndexType, ValueType>::DistributionEntry(IndexType const& index, ValueType const& value) : index(index), value(value) { + template <typename StateType, typename ValueType> + DistributionEntry<StateType, ValueType>::DistributionEntry(StateType const& state, ValueType const& value) : state(state), value(value) { // Intentionally left empty. } - template <typename IndexType, typename ValueType> - IndexType const& DistributionEntry<IndexType, ValueType>::getIndex() const { - return index; + template <typename StateType, typename ValueType> + StateType const& DistributionEntry<StateType, ValueType>::getState() const { + return state; } - template <typename IndexType, typename ValueType> - ValueType const& DistributionEntry<IndexType, ValueType>::getValue() const { + template <typename StateType, typename ValueType> + ValueType const& DistributionEntry<StateType, ValueType>::getValue() const { return value; } - template <typename IndexType, typename ValueType> - void DistributionEntry<IndexType, ValueType>::addToValue(ValueType const& value) { + template <typename StateType, typename ValueType> + void DistributionEntry<StateType, ValueType>::addToValue(ValueType const& value) { this->value += value; } - template <typename IndexType, typename ValueType> - void DistributionEntry<IndexType, ValueType>::divide(ValueType const& value) { + template <typename StateType, typename ValueType> + void DistributionEntry<StateType, ValueType>::divide(ValueType const& value) { this->value /= value; } @@ -40,6 +42,11 @@ namespace storm { template class DistributionEntry<uint32_t, storm::RationalNumber>; template class DistributionEntry<uint32_t, storm::RationalFunction>; + template class DistributionEntry<storm::storage::BitVector, double>; + template class DistributionEntry<storm::storage::BitVector, storm::RationalNumber>; + template class DistributionEntry<storm::storage::BitVector, storm::RationalFunction>; + + } } } diff --git a/src/storm/builder/jit/DistributionEntry.h b/src/storm/builder/jit/DistributionEntry.h index fa0abc3fb..329273f81 100644 --- a/src/storm/builder/jit/DistributionEntry.h +++ b/src/storm/builder/jit/DistributionEntry.h @@ -4,20 +4,20 @@ namespace storm { namespace builder { namespace jit { - template <typename IndexType, typename ValueType> + template <typename StateType, typename ValueType> class DistributionEntry { public: DistributionEntry(); - DistributionEntry(IndexType const& index, ValueType const& value); + DistributionEntry(StateType const& state, ValueType const& value); - IndexType const& getIndex() const; + StateType const& getState() const; ValueType const& getValue() const; void addToValue(ValueType const& value); void divide(ValueType const& value); private: - IndexType index; + StateType state; ValueType value; }; diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp index ec07e80f7..208d4490f 100644 --- a/src/storm/builder/jit/ModelComponentsBuilder.cpp +++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp @@ -58,7 +58,7 @@ namespace storm { for (auto const& choice : behaviour.getChoices()) { // Add the elements to the transition matrix. for (auto const& element : choice.getDistribution()) { - transitionMatrixBuilder->addNextValue(currentRow, element.getIndex(), element.getValue()); + transitionMatrixBuilder->addNextValue(currentRow, element.getState(), element.getValue()); } // Add state-action reward entries. diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index f69014364..2be706715 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -74,7 +74,7 @@ namespace storm { result.addLabel(label.first); } - storm::storage::BitVectorHashMap<StateType> const& states = stateStorage.stateToId; + auto const& states = stateStorage.stateToId; for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index db74175c0..f9cb0a102 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -8,6 +8,8 @@ #include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/builder/jit/Distribution.h" + #include "storm/solver/SmtSolver.h" #include "storm/utility/constants.h" @@ -449,6 +451,9 @@ namespace storm { std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector<Choice<ValueType>> result; + storm::builder::jit::Distribution<CompressedState, ValueType> currentDistribution; + storm::builder::jit::Distribution<CompressedState, ValueType> nextDistribution; + for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex); @@ -465,40 +470,32 @@ namespace storm { // As long as there is one feasible combination of commands, keep on expanding it. bool done = false; while (!done) { - boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); - boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); - - currentTargetStates->emplace(state, storm::utility::one<ValueType>()); + currentDistribution.clear(); + nextDistribution.clear(); + + currentDistribution.add(state, storm::utility::one<ValueType>()); for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::prism::Command const& command = *iteratorList[i]; for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { storm::prism::Update const& update = command.getUpdate(j); - for (auto const& stateProbabilityPair : *currentTargetStates) { - ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()); + for (auto const& stateProbability : currentDistribution) { + ValueType probability = stateProbability.getValue() * this->evaluator->asRational(update.getLikelihoodExpression()); if (!storm::utility::isZero<ValueType>(probability)) { // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update); - - // If the new state was already found as a successor state, update the probability - // and otherwise insert it. - auto targetStateIt = newTargetStates->find(newTargetState); - if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += probability; - } else { - newTargetStates->emplace(newTargetState, probability); - } + CompressedState newTargetState = applyUpdate(stateProbability.getState(), update); + nextDistribution.add(newTargetState, probability); } } } + nextDistribution.compress(); + // If there is one more command to come, shift the target states one time step back. if (i < iteratorList.size() - 1) { - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); + currentDistribution = std::move(nextDistribution); } } @@ -524,11 +521,11 @@ namespace storm { // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero<ValueType>(); - for (auto const& stateProbabilityPair : *newTargetStates) { - StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); - choice.addProbability(actualIndex, stateProbabilityPair.second); + for (auto const& stateProbability : nextDistribution) { + StateType actualIndex = stateToIdCallback(stateProbability.getState()); + choice.addProbability(actualIndex, stateProbability.getValue()); if (this->options.isExplorationChecksSet()) { - probabilitySum += stateProbabilityPair.second; + probabilitySum += stateProbability.getValue(); } } @@ -550,10 +547,6 @@ namespace storm { choice.addReward(stateActionRewardValue); } - // Dispose of the temporary maps. - delete currentTargetStates; - delete newTargetStates; - // Now, check whether there is one more command combination to consider. bool movedIterator = false; for (int_fast64_t j = iteratorList.size() - 1; !movedIterator && j >= 0; --j) { diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index e5498b82c..97b1945e6 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -999,6 +999,20 @@ namespace storm { out << std::endl; } + std::size_t FNV1aBitVectorHash::operator()(storm::storage::BitVector const& bv) const { + std::size_t seed = 14695981039346656037ull; + uint64_t prime = 1099511628211ull; + + unsigned char const* it = reinterpret_cast<unsigned char const*>(bv.buckets); + unsigned char const* ite = it + 8 * bv.bucketCount(); + + for (; it != ite; ++it) { + seed = (*it ^ seed) * prime; + } + + return seed; + } + // All necessary explicit template instantiations. template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end); template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::const_iterator begin, std::vector<uint_fast64_t>::const_iterator end); diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 0b5a7670b..17d470eab 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -501,6 +501,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); friend struct std::hash<storm::storage::BitVector>; + friend struct FNV1aBitVectorHash; private: /*! @@ -570,6 +571,10 @@ namespace storm { static const uint_fast64_t mod64mask = (1 << 6) - 1; }; + struct FNV1aBitVectorHash { + std::size_t operator()(storm::storage::BitVector const& bv) const; + }; + } // namespace storage } // namespace storm diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index 434ab6906..5409e2cef 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -9,9 +9,6 @@ namespace storm { namespace storage { - template<class ValueType, class Hash> - const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223}; - template<class ValueType, class Hash> BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { // Intentionally left empty. @@ -45,19 +42,20 @@ namespace storm { } template<class ValueType, class Hash> - BitVectorHashMap<ValueType, Hash>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { + BitVectorHashMap<ValueType, Hash>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), currentSize(1), numberOfElements(0) { STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64."); - currentSizeIterator = std::find_if(sizes.begin(), sizes.end(), [=] (uint64_t value) { return value > initialSize; } ); + + while (initialSize > 0) { + ++currentSize; + initialSize >>= 1; + } // Create the underlying containers. - buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); - occupied = storm::storage::BitVector(*currentSizeIterator); - values = std::vector<ValueType>(*currentSizeIterator); - + buckets = storm::storage::BitVector(bucketSize * (1ull << currentSize)); + occupied = storm::storage::BitVector(1ull << currentSize); + values = std::vector<ValueType>(1ull << currentSize); + #ifndef NDEBUG - for (uint64_t i = 0; i < sizes.size() - 1; ++i) { - STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes."); - } numberOfInsertions = 0; numberOfInsertionProbingSteps = 0; numberOfFinds = 0; @@ -77,60 +75,32 @@ namespace storm { template<class ValueType, class Hash> std::size_t BitVectorHashMap<ValueType, Hash>::capacity() const { - return *currentSizeIterator; + return 1ull << currentSize; } template<class ValueType, class Hash> void BitVectorHashMap<ValueType, Hash>::increaseSize() { - ++currentSizeIterator; - STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + ++currentSize; #ifndef NDEBUG - STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast<double>(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast<double>(numberOfInsertions)) << " probing steps)."); + STORM_LOG_TRACE("Increasing size of hash map from " << (1ull << (currentSize - 1)) << " to " << (1ull << currentSize) << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast<double>(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast<double>(numberOfInsertions)) << " probing steps)."); #else - STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << "."); + STORM_LOG_TRACE("Increasing size of hash map from " << (1ull << (currentSize - 1)) << " to " << (1ull << currentSize) << "."); #endif // Create new containers and swap them with the old ones. numberOfElements = 0; - storm::storage::BitVector oldBuckets(bucketSize * *currentSizeIterator); + storm::storage::BitVector oldBuckets(bucketSize * (1ull << currentSize)); std::swap(oldBuckets, buckets); - storm::storage::BitVector oldOccupied = storm::storage::BitVector(*currentSizeIterator); + storm::storage::BitVector oldOccupied = storm::storage::BitVector(1ull << currentSize); std::swap(oldOccupied, occupied); - std::vector<ValueType> oldValues = std::vector<ValueType>(*currentSizeIterator); + std::vector<ValueType> oldValues = std::vector<ValueType>(1ull << currentSize); std::swap(oldValues, values); // Now iterate through the elements and reinsert them in the new storage. bool fail = false; for (auto bucketIndex : oldOccupied) { fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); - - // If we failed to insert just one element, we have to redo the procedure with a larger container size. - if (fail) { - break; - } - } - - uint_fast64_t failCount = 0; - while (fail) { - ++failCount; - STORM_LOG_THROW(failCount < 2, storm::exceptions::InternalException, "Increasing size failed too often."); - - ++currentSizeIterator; - STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big."); - - numberOfElements = 0; - buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); - occupied = storm::storage::BitVector(*currentSizeIterator); - values = std::vector<ValueType>(*currentSizeIterator); - - for (auto bucketIndex : oldOccupied) { - fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); - - // If we failed to insert just one element, we have to redo the procedure with a larger container size. - if (fail) { - break; - } - } + STORM_LOG_ASSERT(!fail, "Expected to be able to insert all elements."); } } @@ -166,7 +136,7 @@ namespace storm { template<class ValueType, class Hash> std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. - if (numberOfElements >= loadFactor * *currentSizeIterator) { + if (numberOfElements >= loadFactor * (1ull << currentSize)) { this->increaseSize(); } @@ -187,7 +157,7 @@ namespace storm { template<class ValueType, class Hash> std::size_t BitVectorHashMap<ValueType, Hash>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. - if (numberOfElements >= loadFactor * *currentSizeIterator) { + if (numberOfElements >= loadFactor * (1ull << currentSize)) { this->increaseSize(); } @@ -230,17 +200,12 @@ namespace storm { return const_iterator(*this, occupied.end()); } - template<class ValueType, class Hash> - uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t, uint_fast64_t currentValue, uint_fast64_t step) const { - return (currentValue + step + step*step) % *currentSizeIterator; - } - template<class ValueType, class Hash> std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash>::findBucket(storm::storage::BitVector const& key) const { #ifndef NDEBUG ++numberOfFinds; #endif - uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; + uint_fast64_t initialHash = hasher(key) % (1ull << currentSize); uint_fast64_t bucket = initialHash; uint_fast64_t i = 0; @@ -252,8 +217,11 @@ namespace storm { if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } - bucket = getNextBucketInProbingSequence(initialHash, bucket, i); - + bucket += 1; + if (bucket == (1ull << currentSize)) { + bucket = 0; + } + if (bucket == initialHash) { return std::make_pair(false, bucket); } @@ -268,7 +236,7 @@ namespace storm { #ifndef NDEBUG ++numberOfInsertions; #endif - uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; + uint_fast64_t initialHash = hasher(key) % (1ull << currentSize); uint_fast64_t bucket = initialHash; uint64_t i = 0; @@ -280,12 +248,15 @@ namespace storm { if (buckets.matches(bucket * bucketSize, key)) { return std::make_tuple(true, bucket, false); } - bucket = getNextBucketInProbingSequence(initialHash, bucket, i); - + bucket += 1; + if (bucket == (1ull << currentSize)) { + bucket = 0; + } + if (bucket == initialHash) { if (increaseStorage) { this->increaseSize(); - bucket = initialHash = hasher(key) % *currentSizeIterator; + bucket = initialHash = hasher(key) % (1ull << currentSize); } else { return std::make_tuple(false, bucket, true); } diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h index 7c400c1cd..28eb6c187 100644 --- a/src/storm/storage/BitVectorHashMap.h +++ b/src/storm/storage/BitVectorHashMap.h @@ -14,7 +14,8 @@ namespace storm { * queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of * 64. */ - template<typename ValueType, typename Hash = std::hash<storm::storage::BitVector>> +// template<typename ValueType, typename Hash = std::hash<storm::storage::BitVector>> + template<typename ValueType, typename Hash = FNV1aBitVectorHash> class BitVectorHashMap { public: class BitVectorHashMapIterator { @@ -57,6 +58,11 @@ namespace storm { */ BitVectorHashMap(uint64_t bucketSize = 64, uint64_t initialSize = 1000, double loadFactor = 0.75); + BitVectorHashMap(BitVectorHashMap const&) = default; + BitVectorHashMap(BitVectorHashMap&&) = default; + BitVectorHashMap& operator=(BitVectorHashMap const&) = default; + BitVectorHashMap& operator=(BitVectorHashMap&&) = default; + /*! * Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the * key is inserted with the given value. @@ -211,19 +217,14 @@ namespace storm { */ void increaseSize(); - /*! - * Computes the next bucket in the probing sequence. - */ - uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t initialValue, uint_fast64_t currentValue, uint_fast64_t step) const; - // The load factor determining when the size of the map is increased. double loadFactor; // The size of one bucket. uint64_t bucketSize; - // The number of buckets. - std::size_t numberOfBuckets; + // The number of buckets is 2^currentSize. + uint64_t currentSize; // The buckets that hold the elements of the map. storm::storage::BitVector buckets; @@ -237,15 +238,9 @@ namespace storm { // The number of elements in this map. std::size_t numberOfElements; - // An iterator to a value in the static sizes table. - std::vector<std::size_t>::const_iterator currentSizeIterator; - // Functor object that are used to perform the actual hashing. Hash hasher; - // A static table that produces the next possible size of the hash table. - static const std::vector<std::size_t> sizes; - #ifndef NDEBUG // Some performance metrics. mutable uint64_t numberOfInsertions; From e8dc6ee05de4bf10cd43b1bcc0214e6c656f3a01 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 13 Nov 2017 19:24:10 +0100 Subject: [PATCH 30/33] applying the same performance improvements for explicit JANI model building --- .../generator/JaniNextStateGenerator.cpp | 41 ++++++++----------- 1 file changed, 17 insertions(+), 24 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 40481fd83..7e49b0771 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -6,7 +6,6 @@ #include "storm/solver/SmtSolver.h" - #include "storm/storage/jani/Edge.h" #include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/Model.h" @@ -16,6 +15,8 @@ #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" +#include "storm/builder/jit/Distribution.h" + #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" @@ -414,36 +415,32 @@ namespace storm { iteratorList[i] = edgeCombination[i].second.cbegin(); } + storm::builder::jit::Distribution<CompressedState, ValueType> currentDistribution; + storm::builder::jit::Distribution<CompressedState, ValueType> nextDistribution; + // As long as there is one feasible combination of commands, keep on expanding it. bool done = false; while (!done) { - boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); - boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>()); - currentTargetStates->emplace(state, storm::utility::one<ValueType>()); + currentDistribution.add(state, storm::utility::one<ValueType>()); for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::jani::Edge const& edge = **iteratorList[i]; for (auto const& destination : edge.getDestinations()) { - for (auto const& stateProbabilityPair : *currentTargetStates) { + for (auto const& stateProbability : currentDistribution) { // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, this->variableInformation.locationVariables[edgeCombination[i].first]); + CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first]); // If the new state was already found as a successor state, update the probability // and otherwise insert it. - ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); + ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability()); if (edge.hasRate()) { probability *= this->evaluator->asRational(edge.getRate()); } if (probability != storm::utility::zero<ValueType>()) { - auto targetStateIt = newTargetStates->find(newTargetState); - if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += probability; - } else { - newTargetStates->emplace(newTargetState, probability); - } + nextDistribution.add(newTargetState, probability); } } @@ -452,11 +449,11 @@ namespace storm { performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } + nextDistribution.compress(); + // If there is one more command to come, shift the target states one time step back. if (i < iteratorList.size() - 1) { - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); + currentDistribution = std::move(nextDistribution); } } @@ -473,12 +470,12 @@ namespace storm { // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero<ValueType>(); - for (auto const& stateProbabilityPair : *newTargetStates) { - StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); - choice.addProbability(actualIndex, stateProbabilityPair.second); + for (auto const& stateProbability : nextDistribution) { + StateType actualIndex = stateToIdCallback(stateProbability.getState()); + choice.addProbability(actualIndex, stateProbability.getValue()); if (this->options.isExplorationChecksSet()) { - probabilitySum += stateProbabilityPair.second; + probabilitySum += stateProbability.getValue(); } } @@ -487,10 +484,6 @@ namespace storm { STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); } - // Dispose of the temporary maps. - delete currentTargetStates; - delete newTargetStates; - // Now, check whether there is one more command combination to consider. bool movedIterator = false; for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) { From 03489be59ffb3078503a253205c8054bfde74a04 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 13 Nov 2017 20:19:28 +0100 Subject: [PATCH 31/33] sligh FNV1a hash improvement --- src/storm/storage/BitVector.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 97b1945e6..60fdf166b 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1001,13 +1001,15 @@ namespace storm { std::size_t FNV1aBitVectorHash::operator()(storm::storage::BitVector const& bv) const { std::size_t seed = 14695981039346656037ull; - uint64_t prime = 1099511628211ull; unsigned char const* it = reinterpret_cast<unsigned char const*>(bv.buckets); unsigned char const* ite = it + 8 * bv.bucketCount(); - for (; it != ite; ++it) { - seed = (*it ^ seed) * prime; + while (it < ite) { + seed ^= *it++; + + // Multiplication with magic prime. + seed += (seed << 1) + (seed << 4) + (seed << 5) + (seed << 7) + (seed << 8) + (seed << 40); } return seed; From ef7b25d65c7cc51f75bda932e540970dcf21f89b Mon Sep 17 00:00:00 2001 From: Matthias Volk <matthias.volk@cs.rwth-aachen.de> Date: Mon, 13 Nov 2017 21:45:49 +0100 Subject: [PATCH 32/33] Fixed cli settings for storm-dft --- src/storm-dft-cli/storm-dft.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 3e69fb217..e68c853c3 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -85,7 +85,7 @@ void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - storm::cli::processOptions(); + // storm::cli::processOptions(); storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>(); storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>(); From d6c5367e85577a8d476ac1b0abace4e39eea928a Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Tue, 14 Nov 2017 09:00:56 +0100 Subject: [PATCH 33/33] fix possible memory leak in bitvector --- src/storm/storage/BitVector.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 60fdf166b..924657b44 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -116,7 +116,10 @@ namespace storm { // Only perform the assignment if the source and target are not identical. if (this != &other) { bitCount = other.bitCount; - buckets = new uint64_t[other.bucketCount()]; + if (buckets && bucketCount() != other.bucketCount()) { + delete[] buckets; + buckets = new uint64_t[other.bucketCount()]; + } std::copy_n(other.buckets, other.bucketCount(), buckets); } return *this;