Fixed game solver test and potential memory leaks

src/storm/modelchecker/parametric/ParameterLifting.h

@@ -27,7 +27,8 @@ namespace storm {
                 typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
 
                 ParameterLifting(SparseModelType const& parametricModel);
-
+                virtual ~ParameterLifting() = default;
+                
                 ParameterLiftingSettings const& getSettings() const;
                 void setSettings(ParameterLiftingSettings const& newSettings);
                 

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<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
                 

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<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
                 

src/storm/solver/GameSolver.cpp

@@ -9,6 +9,11 @@
 namespace storm {
     namespace solver {
         
+        template<typename ValueType>
+        GameSolver<ValueType>::GameSolver() : trackSchedulers(false), cachingEnabled(false) {
+            // Intentionally left empty
+        }
+        
         template<typename ValueType>
         void GameSolver<ValueType>::setTrackSchedulers(bool value) {
             trackSchedulers = value;

src/storm/solver/GameSolver.h

@@ -25,6 +25,8 @@ namespace storm {
         template<class ValueType>
         class GameSolver : public AbstractEquationSolver<ValueType> {
         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;
 

src/storm/solver/StandardGameSolver.cpp

@@ -187,15 +187,15 @@ namespace storm {
                 linEqSolverPlayer2Matrix->setCachingEnabled(true);
             }
             
-            if (!auxiliaryP2RowVector.get()) {
+            if (!auxiliaryP2RowVector) {
                 auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
             }
                
-            if (!auxiliaryP2RowGroupVector.get()) {
+            if (!auxiliaryP2RowGroupVector) {
                 auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
             }
              
-            if (!auxiliaryP1RowGroupVector.get()) {
+            if (!auxiliaryP1RowGroupVector) {
                 auxiliaryP1RowGroupVector = std::make_unique<std::vector<ValueType>>(player1Matrix.getRowGroupCount());
             }
              
@@ -266,11 +266,11 @@ namespace storm {
                 linEqSolverPlayer2Matrix->setCachingEnabled(true);
             }
             
-            if (!auxiliaryP2RowVector.get()) {
+            if (!auxiliaryP2RowVector) {
                 auxiliaryP2RowVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowCount());
             }
                
-            if (!auxiliaryP2RowGroupVector.get()) {
+            if (!auxiliaryP2RowGroupVector) {
                 auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(player2Matrix.getRowGroupCount());
             }
             std::vector<ValueType>& multiplyResult = *auxiliaryP2RowVector;

src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@@ -216,12 +216,12 @@ namespace storm {
                 linEqSolverA->setCachingEnabled(true);
             }
             
-            if (!auxiliaryRowVector.get()) {
+            if (!auxiliaryRowVector) {
                 auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
             }
             std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;
             
-            if (!auxiliaryRowGroupVector.get()) {
+            if (!auxiliaryRowGroupVector) {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(A.getRowGroupCount());
             }
             
@@ -301,7 +301,7 @@ namespace storm {
                 linEqSolverA->setCachingEnabled(true);
             }
             
-            if (!auxiliaryRowVector.get()) {
+            if (!auxiliaryRowVector) {
                 auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
             }
             std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;

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.

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<double> player2MatrixBuilder(0, 0, 0, false, true);
     player2MatrixBuilder.newRowGroup(0);
@@ -39,8 +38,9 @@ TEST(GameSolverTest, Solve) {
     player1MatrixBuilder.addNextValue(4, 4, 1);
     storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix = player1MatrixBuilder.build();
 
-    std::unique_ptr<storm::utility::solver::GameSolverFactory<double>> solverFactory(new storm::utility::solver::GameSolverFactory<double>());
-    std::unique_ptr<storm::solver::GameSolver<double>> solver = solverFactory->create(player1Matrix, player2Matrix);
+	storm::solver::StandardGameSolverSettings<double> settings;
+	settings.setSolutionMethod(storm::solver::StandardGameSolverSettings<double>::SolutionMethod::ValueIteration);
+    auto solver = std::make_unique<storm::solver::StandardGameSolver<double>>(player1Matrix, player2Matrix, std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<double>>(), settings);
 
     // Create solution and target state vector.
     std::vector<double> 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<storm::settings::modules::NativeEquationSolverSettings>().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<double> 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<double> player2Matrix = player2MatrixBuilder.build();
+
+    // Now build player 1 matrix.
+    storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> 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<storm::storage::sparse::state_type> player1Matrix = player1MatrixBuilder.build();
+
+	storm::solver::StandardGameSolverSettings<double> settings;
+	settings.setSolutionMethod(storm::solver::StandardGameSolverSettings<double>::SolutionMethod::PolicyIteration);
+    auto solver = std::make_unique<storm::solver::StandardGameSolver<double>>(player1Matrix, player2Matrix, std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<double>>(), settings);
+
+
+    // Create solution and target state vector.
+    std::vector<double> result(4);
+    std::vector<double> 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<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, result, b);
+    EXPECT_NEAR(0.5, result[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, result, b);
+    EXPECT_NEAR(0.2, result[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+
+    result = std::vector<double>(4);
+
+    solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, result, b);
+    EXPECT_NEAR(1, result[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+}
+