From 548ba8bbeb2db921732b9cbde48aff3300e46cca Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 5 Aug 2016 23:49:58 +0200 Subject: [PATCH] somehow managed my way through the policy guessing, several minor extensions to solvers Former-commit-id: c4bb6453e7ded37ae2565602eb6d94b358eb000a --- src/cli/cli.cpp | 3 +- .../region/ApproximationModel.cpp | 2 +- src/modelchecker/region/SamplingModel.cpp | 2 +- src/solver/GmmxxLinearEquationSolver.h | 2 +- src/solver/LinearEquationSolver.h | 2 +- src/solver/MinMaxLinearEquationSolver.cpp | 2 +- src/solver/MinMaxLinearEquationSolver.h | 14 +- src/solver/NativeLinearEquationSolver.cpp | 7 +- .../StandardMinMaxLinearEquationSolver.cpp | 14 +- .../StandardMinMaxLinearEquationSolver.h | 4 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 6 + .../SymbolicMinMaxLinearEquationSolver.h | 5 +- src/solver/TerminationCondition.cpp | 3 + .../TopologicalMinMaxLinearEquationSolver.cpp | 10 + .../TopologicalMinMaxLinearEquationSolver.h | 3 + src/utility/policyguessing.cpp | 81 +++---- src/utility/policyguessing.h | 16 +- src/utility/region.cpp | 25 +- src/utility/storm.h | 15 +- .../SparseDtmcRegionModelCheckerTest.cpp | 214 +++++++++--------- .../SparseMdpRegionModelCheckerTest.cpp | 24 +- 21 files changed, 250 insertions(+), 204 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index eef99ddf6..148c8d357 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -227,8 +227,7 @@ namespace storm { for (auto const& formula : formulas) { preprocessedFormulas.emplace_back(formula->substitute(constantsSubstitution)); } - std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); - + if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 53fc2c513..2c5ab2e3c 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -382,7 +382,7 @@ namespace storm { //Invoke mdp model checking std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::solver::GeneralMinMaxLinearEquationSolverFactory(), this->matrixData.matrix); solver->setTerminationCondition(std::move(terminationCondition)); - storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, + storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, this->matrixData.matrix, this->solverData.result, this->vectorData.vector, player2Goal.direction(), scheduler, diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 2452b30da..81c7aa61f 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -166,7 +166,7 @@ namespace storm { )); } } - storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, + storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver,submatrix, this->solverData.result, b, this->solverData.solveGoal->direction(), this->solverData.lastScheduler, diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index 6247723c8..7d4c09ad1 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -103,7 +103,7 @@ namespace storm { virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const override; virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const override; - + private: /*! * Solves the linear equation system A*x = b given by the parameters using the Jacobi method. diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 7586f3eeb..b52778051 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -27,7 +27,7 @@ namespace storm { virtual ~LinearEquationSolver() { // Intentionally left empty. } - + virtual void setMatrix(storm::storage::SparseMatrix const& A) = 0; virtual void setMatrix(storm::storage::SparseMatrix&& A) = 0; diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index c82514a37..9b7d65ff9 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -74,7 +74,7 @@ namespace storm { } template - std::unique_ptr MinMaxLinearEquationSolver::getScheduler() { + std::unique_ptr MinMaxLinearEquationSolver:: getScheduler() { STORM_LOG_THROW(scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve scheduler, because none was generated."); return std::move(scheduler.get()); } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 821462602..14457e778 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -96,7 +96,7 @@ namespace storm { * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently * stored scheduler (if any) is deleted. */ - void setTrackScheduler(bool trackScheduler); + void setTrackScheduler(bool trackScheduler = true); /*! * Retrieves whether this solver is set to generate schedulers. @@ -120,6 +120,18 @@ namespace storm { */ std::unique_ptr getScheduler(); + /** + * Gets the precision after which the solver takes two numbers as equal. + * + * @see getRelative() + */ + virtual ValueType getPrecision() const = 0; + + /** + * Gets whether the precision is taken to be absolute or relative + */ + virtual bool getRelative() const = 0; + // Methods related to allocating/freeing auxiliary storage. /*! diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 97d09b06d..42e861f21 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -98,7 +98,12 @@ namespace storm { localA.reset(); this->A = &A; } - + + template + void NativeLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { + localA = std::make_unique>(std::move(A)); + this->A = localA.get(); + } template diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index ba0bf43f9..8c4f01108 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -187,7 +187,19 @@ namespace storm { return false; } } - + + template + ValueType StandardMinMaxLinearEquationSolver::getPrecision() const { + return this->getSettings().getPrecision(); + } + + template + bool StandardMinMaxLinearEquationSolver::getRelative() const { + return this->getSettings().getRelativeTerminationCriterion(); + } + + + template bool StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { std::unique_ptr> solver = linearEquationSolverFactory->create(A); diff --git a/src/solver/StandardMinMaxLinearEquationSolver.h b/src/solver/StandardMinMaxLinearEquationSolver.h index 5ad43347d..d6d36b272 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/solver/StandardMinMaxLinearEquationSolver.h @@ -47,7 +47,9 @@ namespace storm { virtual bool allocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; virtual bool deallocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; virtual bool hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; - + + virtual ValueType getPrecision() const override; + virtual bool getRelative() const override; private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index ed14fff57..0c27de0cb 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -89,6 +89,12 @@ namespace storm { return xCopy; } + + template + ValueType const& SymbolicMinMaxLinearEquationSolver::getPrecision() const { + return precision; + } + template class SymbolicMinMaxLinearEquationSolver; template class SymbolicMinMaxLinearEquationSolver; diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.h b/src/solver/SymbolicMinMaxLinearEquationSolver.h index 98cb94102..3fcceabfe 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.h @@ -88,7 +88,8 @@ namespace storm { * @return The solution of the equation system. */ virtual storm::dd::Add multiply(bool minimize, storm::dd::Add const& x, storm::dd::Add const* b = nullptr, uint_fast64_t n = 1) const; - + + virtual ValueType const& getPrecision() const;// override; protected: // The matrix defining the coefficients of the linear equation system. storm::dd::Add const& A; @@ -111,7 +112,7 @@ namespace storm { // The pairs of meta variables used for renaming. std::vector> const& rowColumnMetaVariablePairs; - // The precision to achive. + // The precision to achieve. double precision; // The maximal number of iterations to perform. diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp index 04d7ff7ae..ccd1ce811 100644 --- a/src/solver/TerminationCondition.cpp +++ b/src/solver/TerminationCondition.cpp @@ -51,9 +51,12 @@ namespace storm { template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; + template class TerminateIfFilteredExtremumBelowThreshold; #ifdef STORM_HAVE_CARL template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; + template class TerminateIfFilteredExtremumBelowThreshold; + #endif } } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index 3b17ec77e..ecde49726 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -422,6 +422,16 @@ namespace storm { #endif return result; } + + template + ValueType TopologicalMinMaxLinearEquationSolver::getPrecision() const { + return this->precision; + } + + template + bool TopologicalMinMaxLinearEquationSolver::getRelative() const { + return this->relative; + } template void TopologicalMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n) const { diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h index 347675447..3a1204a01 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -36,6 +36,9 @@ namespace storm { virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n) const override; + virtual ValueType getPrecision() const override; + virtual bool getRelative() const override; + private: storm::storage::SparseMatrix const& A; double precision; diff --git a/src/utility/policyguessing.cpp b/src/utility/policyguessing.cpp index 61f9da6d6..072662c33 100644 --- a/src/utility/policyguessing.cpp +++ b/src/utility/policyguessing.cpp @@ -1,9 +1,3 @@ -/* - * File: Regions.cpp - * Author: Tim Quatmann - * - * Created on November 16, 2015, - */ #include #include "src/utility/policyguessing.h" @@ -11,6 +5,7 @@ #include "src/utility/macros.h" #include "src/utility/solver.h" #include "src/solver/LinearEquationSolver.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "graph.h" #include "ConstantsComparator.h" @@ -58,6 +53,7 @@ namespace storm { template void solveMinMaxLinearEquationSystem( storm::solver::MinMaxLinearEquationSolver& solver, + storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, OptimizationDirection goal, @@ -68,18 +64,18 @@ namespace storm { storm::storage::SparseMatrix inducedA; std::vector inducedB; storm::storage::BitVector probGreater0States; - getInducedEquationSystem(solver, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); + getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative()); solver.setTrackScheduler(); bool resultCorrect = false; while(!resultCorrect){ - solver.solveEquationSystem(goal, x, b); - scheduler = solver.getScheduler(); + solver.solveEquations(goal, x, b); + scheduler = std::move(*solver.getScheduler()); //Check if the Scheduler makes choices that lead to states from which no target state is reachable ("prob0"-states). - getInducedEquationSystem(solver, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); - resultCorrect = checkAndFixScheduler(solver, x, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); + getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); + resultCorrect = checkAndFixScheduler(A, x, b, scheduler, targetChoices, solver.getPrecision(), solver.getRelative(), inducedA, inducedB, probGreater0States); if(!resultCorrect){ //If the Scheduler could not be fixed, it indicates that our guessed values were to high. @@ -128,7 +124,7 @@ namespace storm { template - void getInducedEquationSystem(storm::solver::MinMaxLinearEquationSolver const& solver, + void getInducedEquationSystem(storm::storage::SparseMatrix const& A, std::vector const& b, storm::storage::TotalScheduler const& scheduler, storm::storage::BitVector const& targetChoices, @@ -136,19 +132,19 @@ namespace storm { std::vector& inducedB, storm::storage::BitVector& probGreater0States ){ - uint_fast64_t numberOfStates = solver.getMatrix().getRowGroupCount(); + uint_fast64_t numberOfStates = A.getRowGroupCount(); //Get the matrix A, vector b, and the targetStates induced by the Scheduler std::vector selectedRows(numberOfStates); for(uint_fast64_t stateIndex = 0; stateIndex < numberOfStates; ++stateIndex){ selectedRows[stateIndex] = (scheduler.getChoice(stateIndex)); } - inducedA = solver.getMatrix().selectRowsFromRowGroups(selectedRows, false); + inducedA = A.selectRowsFromRowGroups(selectedRows, false); inducedB = std::vector(numberOfStates); - storm::utility::vector::selectVectorValues(inducedB, selectedRows, solver.getMatrix().getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(inducedB, selectedRows, A.getRowGroupIndices(), b); storm::storage::BitVector inducedTarget(numberOfStates, false); for (uint_fast64_t state = 0; state < numberOfStates; ++state){ - if(targetChoices.get(solver.getMatrix().getRowGroupIndices()[state] + scheduler.getChoice(state))){ + if(targetChoices.get(A.getRowGroupIndices()[state] + scheduler.getChoice(state))){ inducedTarget.set(state); } } @@ -173,21 +169,24 @@ namespace storm { storm::utility::vector::selectVectorValues(subX, probGreater0States, x); std::vector subB(probGreater0States.getNumberOfSetBits()); storm::utility::vector::selectVectorValues(subB, probGreater0States, b); - std::unique_ptr> linEqSysSolver = storm::utility::solver::LinearEquationSolverFactory().create(eqSysA); - linEqSysSolver->setRelative(relative); - linEqSysSolver->setIterations(500); + + std::unique_ptr> linEqSysSolver(static_cast*>(storm::solver::GmmxxLinearEquationSolverFactory().create(eqSysA).release())); + auto& eqSettings = linEqSysSolver->getSettings(); + eqSettings.setRelativeTerminationCriterion(relative); + eqSettings.setMaximalNumberOfIterations(500); std::size_t iterations = 0; std::vector copyX(subX.size()); - ValueType newPrecision = precision; + ValueType precisionChangeFactor = storm::utility::one(); do { - linEqSysSolver->setPrecision(newPrecision); - if(!linEqSysSolver->solveEquationSystem(subX, subB)){ + eqSettings.setPrecision(eqSettings.getPrecision() * precisionChangeFactor); + if(!linEqSysSolver->solveEquations(subX, subB)){ // break; //Solver did not converge.. so we have to go on with the current solution. } subA.multiplyWithVector(subX,copyX); storm::utility::vector::addVectors(copyX, subB, copyX); // = Ax + b ++iterations; - newPrecision *= 0.5; + + precisionChangeFactor = storm::utility::convertNumber(0.5); } while(!storm::utility::vector::equalModuloPrecision(subX, copyX, precision*0.5, relative) && iterations<60); STORM_LOG_WARN_COND(iterations<60, "Solving linear equation system did not yield a precise result"); @@ -286,11 +285,12 @@ namespace storm { } template - bool checkAndFixScheduler(storm::solver::MinMaxLinearEquationSolver const& solver, + bool checkAndFixScheduler(storm::storage::SparseMatrix const& A, std::vector const& x, std::vector const& b, storm::storage::TotalScheduler& scheduler, storm::storage::BitVector const& targetChoices, + ValueType const& precision, bool relative, storm::storage::SparseMatrix& inducedA, std::vector& inducedB, storm::storage::BitVector& probGreater0States @@ -309,18 +309,18 @@ namespace storm { * We do this unil the Scheduler does not change anymore */ schedulerChanged = false; - for(uint_fast64_t state=0; state < solver.getMatrix().getRowGroupCount(); ++state){ - uint_fast64_t rowGroupIndex = solver.getMatrix().getRowGroupIndices()[state]; + for(uint_fast64_t state=0; state < A.getRowGroupCount(); ++state){ + uint_fast64_t rowGroupIndex = A.getRowGroupIndices()[state]; //Check 1.: The current choice does not lead to target if(!probGreater0States.get(state)){ //1. Is satisfied. Check 2.: There is another choice that leads to target ValueType choiceValue = x[state]; - for(uint_fast64_t otherChoice = 0; otherChoice < solver.getMatrix().getRowGroupSize(state); ++otherChoice){ + for(uint_fast64_t otherChoice = 0; otherChoice < A.getRowGroupSize(state); ++otherChoice){ if(otherChoice == scheduler.getChoice(state)) continue; - if(rowLeadsToTarget(rowGroupIndex + otherChoice, solver.getMatrix(), targetChoices, probGreater0States)){ + if(rowLeadsToTarget(rowGroupIndex + otherChoice, A, targetChoices, probGreater0States)){ //2. is satisfied. Check 3. The value of that choice is equal to the value of the choice given by the Scheduler - ValueType otherValue = solver.getMatrix().multiplyRowWithVector(rowGroupIndex + otherChoice, x) + b[rowGroupIndex + otherChoice]; - if(storm::utility::vector::equalModuloPrecision(choiceValue, otherValue, solver.getPrecision(), !solver.getRelative())){ + ValueType otherValue = A.multiplyRowWithVector(rowGroupIndex + otherChoice, x) + b[rowGroupIndex + otherChoice]; + if(storm::utility::vector::equalModuloPrecision(choiceValue, otherValue, precision, !relative)){ //3. is satisfied. scheduler.setChoice(state, otherChoice); probGreater0States.set(state); @@ -333,7 +333,7 @@ namespace storm { } //update probGreater0States and equation system - getInducedEquationSystem(solver, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); + getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States); if(probGreater0States.getNumberOfSetBits() == probGreater0States.size()){ return true; } @@ -355,12 +355,13 @@ namespace storm { ); template void solveMinMaxLinearEquationSystem( storm::solver::MinMaxLinearEquationSolver& solver, - std::vector& x, - std::vector const& b, - OptimizationDirection goal, - storm::storage::TotalScheduler& scheduler, - storm::storage::BitVector const& targetChoices, - double const& prob0Value + storm::storage::SparseMatrix const& A, + std::vector& x, + std::vector const& b, + OptimizationDirection goal, + storm::storage::TotalScheduler& Scheduler, + storm::storage::BitVector const& targetChoices, + double const& prob0Value ); template void getInducedEquationSystem(storm::solver::GameSolver const& solver, @@ -373,7 +374,7 @@ namespace storm { storm::storage::BitVector& probGreater0States ); - template void getInducedEquationSystem(storm::solver::MinMaxLinearEquationSolver const& solver, + template void getInducedEquationSystem(storm::storage::SparseMatrixconst& A, std::vector const& b, storm::storage::TotalScheduler const& scheduler, storm::storage::BitVector const& targetChoices, @@ -402,11 +403,13 @@ namespace storm { storm::storage::BitVector& probGreater0States ); - template bool checkAndFixScheduler(storm::solver::MinMaxLinearEquationSolver const& solver, + template bool checkAndFixScheduler(storm::storage::SparseMatrix const& A, std::vector const& x, std::vector const& b, storm::storage::TotalScheduler& scheduler, storm::storage::BitVector const& targetChoices, + double const& precision, + bool relative, storm::storage::SparseMatrix& inducedA, std::vector& inducedB, storm::storage::BitVector& probGreater0States diff --git a/src/utility/policyguessing.h b/src/utility/policyguessing.h index 3c4dddf7c..9fb835518 100644 --- a/src/utility/policyguessing.h +++ b/src/utility/policyguessing.h @@ -70,8 +70,8 @@ namespace storm { * To ensure a unique solution, we need to filter out the "prob0"-states. * To identify these states and set the result for them correctly, it is necessary to know whether rewards or probabilities are to be computed * - * @param solver the solver that contains the matrix + * @param A The matrix itself * @param x The initial guess of the solution. * @param b The vector to add after matrix-vector multiplication. * @param goal Sets whether we want to minimize or maximize. @@ -82,6 +82,7 @@ namespace storm { */ template void solveMinMaxLinearEquationSystem( storm::solver::MinMaxLinearEquationSolver& solver, + storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, OptimizationDirection goal, @@ -125,7 +126,7 @@ namespace storm { * Note that, depending on the schedulers, the qualitative properties of the graph defined by inducedA * might be different to the original graph. * - * @param solver the solver that contains the matrix + * @param A the matrix * @param b The vector in which to select the entries of the right hand side * @param Scheduler A Scheduler that selects rows in every rowgroup. * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state @@ -135,7 +136,7 @@ namespace storm { * @return Induced A, b and targets */ template - void getInducedEquationSystem(storm::solver::MinMaxLinearEquationSolver const& solver, + void getInducedEquationSystem(storm::storage::SparseMatrix const& A, std::vector const& b, storm::storage::TotalScheduler const& scheduler, storm::storage::BitVector const& targetChoices, @@ -210,22 +211,23 @@ namespace storm { * * If the schedulers are changed, they are updated accordingly (as well as the given inducedA, inducedB and probGreater0States) * - * @param solver the solver that contains the two player matrices + * @param A the matrix * @param x the solution vector (the result from value iteration) * @param b The vector in which to select the entries of the right hand side * @param Scheduler A Scheduler that selects rows in every rowgroup. * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state * @param inducedA the Matrix for the equation system - * @param inducedB the Vector for the equation system - * @param probGreater0States marks the states which have a positive probability to lead to a target state + * @param probGreater0States marks the states which have a positive probability to lead to a target state * @return true iff there are no more prob0-states. Also changes the given schedulers accordingly */ template - bool checkAndFixScheduler(storm::solver::MinMaxLinearEquationSolver const& solver, + bool checkAndFixScheduler(storm::storage::SparseMatrix const& A, std::vector const& x, std::vector const& b, storm::storage::TotalScheduler& Scheduler, storm::storage::BitVector const& targetChoices, + ValueType const& precision, + bool relative, storm::storage::SparseMatrix& inducedA, std::vector& inducedB, storm::storage::BitVector& probGreater0States diff --git a/src/utility/region.cpp b/src/utility/region.cpp index 94e8e4031..466be4d45 100644 --- a/src/utility/region.cpp +++ b/src/utility/region.cpp @@ -1,10 +1,3 @@ -/* - * File: Regions.cpp - * Author: Tim Quatmann - * - * Created on May 13, 2015, 12:54 PM - */ - #include #include "src/utility/region.h" @@ -72,14 +65,14 @@ namespace storm { } template<> - storm::Variable getVariableFromString(std::string variableString){ - storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString); + storm::RationalFunctionVariable getVariableFromString(std::string variableString){ + storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString); STORM_LOG_THROW(var!=carl::Variable::NO_VARIABLE, storm::exceptions::IllegalArgumentException, "Variable '" + variableString + "' could not be found."); return var; } template<> - storm::Variable getNewVariable(std::string variableName, VariableSort sort){ + storm::RationalFunctionVariable getNewVariable(std::string variableName, VariableSort sort){ carl::VariableType carlVarType; switch(sort){ case VariableSort::VS_BOOL: @@ -95,7 +88,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given variable sort is not implemented"); } - storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName); + storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName); if(var!=carl::Variable::NO_VARIABLE){ STORM_LOG_THROW(var.getType()==carlVarType, storm::exceptions::IllegalArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use for a variable of a different sort."); return var; @@ -105,7 +98,7 @@ namespace storm { } template<> - std::string getVariableName(storm::Variable variable){ + std::string getVariableName(storm::RationalFunctionVariable variable){ return carl::VariablePool::getInstance().getName(variable); } @@ -136,7 +129,7 @@ namespace storm { } template<> - void addGuardedConstraintToSmtSolver(std::shared_ptr solver,storm::Variable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){ + void addGuardedConstraintToSmtSolver(std::shared_ptr solver,storm::RationalFunctionVariable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){ STORM_LOG_THROW(guard.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver whose guard is not of type bool"); storm::CompareRelation compRel; switch (relation){ @@ -161,7 +154,7 @@ namespace storm { } template<> - void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::Variable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){ + void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){ storm::CompareRelation compRel; switch (relation){ case storm::logic::ComparisonType::Greater: @@ -185,7 +178,7 @@ namespace storm { } template<> - void addBoolVariableToSmtSolver(std::shared_ptr solver,storm::Variable const& variable, bool value){ + void addBoolVariableToSmtSolver(std::shared_ptr solver,storm::RationalFunctionVariable const& variable, bool value){ STORM_LOG_THROW(variable.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver that is a non boolean variable. Only boolean variables are allowed"); solver->add(variable, value); } @@ -197,7 +190,7 @@ namespace storm { } template<> - storm::RationalFunction getNewFunction(storm::Variable initialValue) { + storm::RationalFunction getNewFunction(storm::RationalFunctionVariable initialValue) { std::shared_ptr>> cache(new carl::Cache>()); return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache)); } diff --git a/src/utility/storm.h b/src/utility/storm.h index ed1df065a..0ffbea3f1 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -408,17 +408,12 @@ namespace storm { // Program and formula storm::prism::Program program = parseProgram(programFilePath); program.checkValidity(); - std::vector> parsedFormulas = parseFormulasForProgram(formulaString, program); - std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); + std::vector> formulas = parseFormulasForProgram(formulaString, program);; if(formulas.size()!=1){ STORM_LOG_ERROR("The given formulaString does not specify exactly one formula"); return false; } - // Parametric model - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program, constantsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> model = buildSparseModel(program, formulas); // Preprocessing and ModelChecker if(model->isOfType(storm::models::ModelType::Dtmc)){ preprocessModel>(model,formulas); @@ -447,7 +442,7 @@ namespace storm { * @return true iff the specified formula is satisfied (i.e., iff the reachability value is within the bound of the formula) */ inline bool checkSamplingPoint(std::shared_ptr> regionModelChecker, - std::map const& point){ + std::map const& point){ return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point)); } @@ -467,8 +462,8 @@ namespace storm { * proveAllSat=false, return=false ==> the approximative value IS within the bound of the formula (either the approximation is too bad or there are points in the region that satisfy the property) */ inline bool checkRegionApproximation(std::shared_ptr> regionModelChecker, - std::map const& lowerBoundaries, - std::map const& upperBoundaries, + std::map const& lowerBoundaries, + std::map const& upperBoundaries, bool proveAllSat){ storm::modelchecker::region::ParameterRegion region(lowerBoundaries, upperBoundaries); return regionModelChecker->checkRegionWithApproximation(region, proveAllSat); diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 076386154..0a5424791 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -34,24 +34,24 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint())); - EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method - storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + storm::settings::getModule().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -64,9 +64,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); @@ -96,28 +96,28 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint())); - EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -137,9 +137,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { auto exBothHardRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); @@ -152,9 +152,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { //test smt + approx auto exBothHardRegionSmtApp=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(exBothHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult()); @@ -180,18 +180,18 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); @@ -217,18 +217,18 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint())); - EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -241,9 +241,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); @@ -274,24 +274,24 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioHardRegion.getSomePoint())); - EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -311,9 +311,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); auto allVioHardRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); @@ -326,9 +326,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { //test smt + approx auto allVioHardRegionSmtApp=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allVioHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult()); @@ -354,20 +354,20 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint())); - EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegion); @@ -380,9 +380,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.01<=PF<=0.8"); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); dtmcModelchecker->checkRegion(exBothRegionSmt); @@ -409,25 +409,25 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); - EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); - ASSERT_TRUE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + ASSERT_TRUE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_FALSE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) auto allSatRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion(""); storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION); - ASSERT_FALSE(storm::settings::regionSettings().doApprox()); - ASSERT_TRUE(storm::settings::regionSettings().doSample()); - ASSERT_TRUE(storm::settings::regionSettings().doSmt()); + ASSERT_FALSE(storm::settings::getModule().doApprox()); + ASSERT_TRUE(storm::settings::getModule().doSample()); + ASSERT_TRUE(storm::settings::getModule().doSmt()); dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index fc632932a..b32743c21 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -49,12 +49,12 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { EXPECT_TRUE(storm::checkRegionApproximation(modelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), false)); //Remaining tests.. - EXPECT_NEAR(0.1666665285, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1666665529, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1716553235, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1709666953, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1826972576, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1964429282, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1666665285, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1666665529, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1716553235, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1709666953, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1826972576, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1964429282, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); @@ -89,12 +89,12 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { EXPECT_TRUE(modelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); EXPECT_FALSE(modelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint())); - EXPECT_NEAR(0.95128124239, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.26787251126, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.41880006098, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.01535089684, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.24952791523, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.01711494956, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.95128124239, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.26787251126, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.41880006098, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.01535089684, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.24952791523, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.01711494956, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF);