diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h index 2626ce7ab..bb0e9f111 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.h +++ b/src/storm/modelchecker/parametric/ParameterLifting.h @@ -27,7 +27,8 @@ namespace storm { typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; ParameterLifting(SparseModelType const& parametricModel); - + virtual ~ParameterLifting() = default; + ParameterLiftingSettings const& getSettings() const; void setSettings(ParameterLiftingSettings const& newSettings); diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h index d654e76f9..d51f87f38 100644 --- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h @@ -17,6 +17,7 @@ namespace storm { class SparseInstantiationModelChecker { public: SparseInstantiationModelChecker(SparseModelType const& parametricModel); + virtual ~SparseInstantiationModelChecker() = default; void specifyFormula(CheckTask const& checkTask); diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h index 3eaa520ec..c71d0d25d 100644 --- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h @@ -21,6 +21,7 @@ namespace storm { class SparseParameterLiftingModelChecker { public: SparseParameterLiftingModelChecker(SparseModelType const& parametricModel); + virtual ~SparseParameterLiftingModelChecker() = default; virtual bool canHandle(CheckTask const& checkTask) const = 0; diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index f0c0e3417..c08db00e6 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -9,6 +9,11 @@ namespace storm { namespace solver { + template + GameSolver::GameSolver() : trackSchedulers(false), cachingEnabled(false) { + // Intentionally left empty + } + template void GameSolver::setTrackSchedulers(bool value) { trackSchedulers = value; diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index e4756c24f..0940ac75b 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -25,6 +25,8 @@ namespace storm { template class GameSolver : public AbstractEquationSolver { public: + + virtual ~GameSolver() = default; /*! * Solves the equation system defined by the game matrices. Note that the game matrices have to be given upon @@ -137,6 +139,9 @@ namespace storm { void setBounds(ValueType const& lower, ValueType const& upper); protected: + + GameSolver(); + /// Whether we generate schedulers during solving. bool trackSchedulers; diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index dc3627d88..16f10587b 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -187,15 +187,15 @@ namespace storm { linEqSolverPlayer2Matrix->setCachingEnabled(true); } - if (!auxiliaryP2RowVector.get()) { + if (!auxiliaryP2RowVector) { auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); } - if (!auxiliaryP2RowGroupVector.get()) { + if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); } - if (!auxiliaryP1RowGroupVector.get()) { + if (!auxiliaryP1RowGroupVector) { auxiliaryP1RowGroupVector = std::make_unique>(player1Matrix.getRowGroupCount()); } @@ -266,11 +266,11 @@ namespace storm { linEqSolverPlayer2Matrix->setCachingEnabled(true); } - if (!auxiliaryP2RowVector.get()) { + if (!auxiliaryP2RowVector) { auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); } - if (!auxiliaryP2RowGroupVector.get()) { + if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); } std::vector& multiplyResult = *auxiliaryP2RowVector; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 2a5abf3e3..4d68f00c1 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -216,12 +216,12 @@ namespace storm { linEqSolverA->setCachingEnabled(true); } - if (!auxiliaryRowVector.get()) { + if (!auxiliaryRowVector) { auxiliaryRowVector = std::make_unique>(A.getRowCount()); } std::vector& multiplyResult = *auxiliaryRowVector; - if (!auxiliaryRowGroupVector.get()) { + if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(A.getRowGroupCount()); } @@ -301,7 +301,7 @@ namespace storm { linEqSolverA->setCachingEnabled(true); } - if (!auxiliaryRowVector.get()) { + if (!auxiliaryRowVector) { auxiliaryRowVector = std::make_unique>(A.getRowCount()); } std::vector& multiplyResult = *auxiliaryRowVector; diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm/transformer/SparseParametricModelSimplifier.h index 2f7cedd9d..bf1d95214 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.h +++ b/src/storm/transformer/SparseParametricModelSimplifier.h @@ -19,6 +19,7 @@ namespace storm { class SparseParametricModelSimplifier { public: SparseParametricModelSimplifier(SparseModelType const& model); + virtual ~SparseParametricModelSimplifier() = default; /* * Invokes the simplification of the model w.r.t. the given formula. diff --git a/src/test/solver/GameSolverTest.cpp b/src/test/solver/GameSolverTest.cpp index 18f75b8dd..adac18443 100644 --- a/src/test/solver/GameSolverTest.cpp +++ b/src/test/solver/GameSolverTest.cpp @@ -3,13 +3,12 @@ #include "storm/storage/SparseMatrix.h" -#include "storm/utility/solver.h" #include "storm/settings/SettingsManager.h" -#include "storm/solver/GameSolver.h" +#include "storm/solver/StandardGameSolver.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" -TEST(GameSolverTest, Solve) { +TEST(GameSolverTest, Solve_vi) { // Construct simple game. Start with player 2 matrix. storm::storage::SparseMatrixBuilder player2MatrixBuilder(0, 0, 0, false, true); player2MatrixBuilder.newRowGroup(0); @@ -39,8 +38,9 @@ TEST(GameSolverTest, Solve) { player1MatrixBuilder.addNextValue(4, 4, 1); storm::storage::SparseMatrix player1Matrix = player1MatrixBuilder.build(); - std::unique_ptr> solverFactory(new storm::utility::solver::GameSolverFactory()); - std::unique_ptr> solver = solverFactory->create(player1Matrix, player2Matrix); + storm::solver::StandardGameSolverSettings settings; + settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::ValueIteration); + auto solver = std::make_unique>(player1Matrix, player2Matrix, std::make_unique>(), settings); // Create solution and target state vector. std::vector result(4); @@ -67,3 +67,65 @@ TEST(GameSolverTest, Solve) { solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b); EXPECT_NEAR(0.99999892625817599, result[0], storm::settings::getModule().getPrecision()); } + +TEST(GameSolverTest, Solve_pi) { + // Construct simple game. Start with player 2 matrix. + // Note: policy iteration is not sound if there are non-trivial end components. + storm::storage::SparseMatrixBuilder player2MatrixBuilder(0, 0, 0, false, true); + player2MatrixBuilder.newRowGroup(0); + player2MatrixBuilder.addNextValue(0, 0, 0.4); + player2MatrixBuilder.addNextValue(0, 1, 0.6); + player2MatrixBuilder.addNextValue(1, 1, 0.2); + player2MatrixBuilder.addNextValue(1, 2, 0.8); + player2MatrixBuilder.newRowGroup(2); + player2MatrixBuilder.addNextValue(2, 2, 0.5); + player2MatrixBuilder.addNextValue(2, 3, 0.5); + player2MatrixBuilder.newRowGroup(4); + player2MatrixBuilder.newRowGroup(5); + player2MatrixBuilder.newRowGroup(6); + storm::storage::SparseMatrix player2Matrix = player2MatrixBuilder.build(); + + // Now build player 1 matrix. + storm::storage::SparseMatrixBuilder player1MatrixBuilder(0, 0, 0, false, true); + player1MatrixBuilder.newRowGroup(0); + player1MatrixBuilder.addNextValue(0, 0, 1); + player1MatrixBuilder.addNextValue(1, 1, 1); + player1MatrixBuilder.newRowGroup(2); + player1MatrixBuilder.addNextValue(2, 2, 1); + player1MatrixBuilder.newRowGroup(3); + player1MatrixBuilder.addNextValue(3, 3, 1); + player1MatrixBuilder.newRowGroup(4); + player1MatrixBuilder.addNextValue(4, 4, 1); + storm::storage::SparseMatrix player1Matrix = player1MatrixBuilder.build(); + + storm::solver::StandardGameSolverSettings settings; + settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::PolicyIteration); + auto solver = std::make_unique>(player1Matrix, player2Matrix, std::make_unique>(), settings); + + + // Create solution and target state vector. + std::vector result(4); + std::vector b(7); + b[4] = 1; + b[6] = 1; + + // Now solve the game with different strategies for the players. + solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, result, b); + EXPECT_NEAR(0, result[0], storm::settings::getModule().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b); + EXPECT_NEAR(0.5, result[0], storm::settings::getModule().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b); + EXPECT_NEAR(0.2, result[0], storm::settings::getModule().getPrecision()); + + result = std::vector(4); + + solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b); + EXPECT_NEAR(1, result[0], storm::settings::getModule().getPrecision()); +} +