From d57551c1ece74af7e2b51b25eac477b35f33fa0c Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Tue, 1 Sep 2015 22:27:44 +0200
Subject: [PATCH] Fix for solver

Former-commit-id: 5fb470cdb5a7989d320d22b63b1089d815655788
---
 .../region/ApproximationModel.cpp             |  2 --
 src/solver/Smt2SmtSolver.cpp                  | 25 +++++++++++++++++--
 src/solver/Smt2SmtSolver.h                    |  5 ----
 3 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp
index 2fc8da2ce..5ef19802d 100644
--- a/src/modelchecker/region/ApproximationModel.cpp
+++ b/src/modelchecker/region/ApproximationModel.cpp
@@ -75,8 +75,6 @@ namespace storm {
             storm::storage::SparseMatrix<ConstantType> probabilityMatrix(probabilityMatrixBuilder.build());
             this->probabilityMapping.reserve(numOfNonConstProbEntries);
             
-            
-            std::cout << "2" << std::endl;
             // Now obtain transition and staterewards (if required)
             boost::optional<std::vector<ConstantType>> stateRewards;
             boost::optional<storm::storage::SparseMatrix<ConstantType>> transitionRewards;
diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp
index 33a3dc1e2..cf0e3034a 100644
--- a/src/solver/Smt2SmtSolver.cpp
+++ b/src/solver/Smt2SmtSolver.cpp
@@ -1,3 +1,12 @@
+#ifndef WINDOWS
+    #include <sys/types.h>
+    #include <unistd.h>
+    #include <sys/ioctl.h>
+    #include <signal.h>
+    #include <sys/wait.h>
+    #include <errno.h>
+#endif
+
 #include "src/solver/Smt2SmtSolver.h"
 
 #include "src/settings/SettingsManager.h"
@@ -45,10 +54,11 @@ namespace storm {
             writeCommand("( exit )", false); //do not wait for success because it does not matter at this point and may cause problems if the solver is not running properly
 #ifndef WINDOWS
             if(processIdOfSolver!=0){
-                //Since the process has been open successfully, it means that we have to close our fds   
+                //Since the process has been opened successfully, it means that we have to close our fds   
                 close(fromSolver);
                 close(toSolver);
-                //todo make sure that the process exits  waitpid kill(pid, ..);
+                kill(processIdOfSolver, SIGTERM);
+                waitpid(processIdOfSolver, nullptr, 0); //make sure the process has exited
             }
 #endif
         }
@@ -299,6 +309,17 @@ namespace storm {
                     STORM_LOG_DEBUG("Solver Output '" << solverOutput << "' did not end with newline symbol (\\n). Since we assume that this should be the case, we will wait for more output from the solver");
                     bytesReadable=1; //we expect more output!
                 }
+                if(bytesReadable>0){
+                    pid_t w=waitpid(processIdOfSolver, nullptr, WNOHANG);
+                    if(w!=0){
+                        STORM_LOG_WARN_COND(w>0, "Error when checking whether the solver is still running. Will assume that solver has terminated.");
+                        STORM_LOG_WARN("The solver exited unexpectedly when reading output: " << solverOutput);
+                        solverOutput+="terminated";
+                        this->needsRestart=true;
+                        this->processIdOfSolver=0;
+                        bytesReadable=0;
+                    }
+                }
             }
             checkForErrorMessage(solverOutput);
             std::vector<std::string> solverOutputAsVector;
diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/Smt2SmtSolver.h
index bd78f193d..3f4f8b877 100644
--- a/src/solver/Smt2SmtSolver.h
+++ b/src/solver/Smt2SmtSolver.h
@@ -3,11 +3,6 @@
 
 #include <iostream>
 #include <fstream>
-#ifndef WINDOWS
-    #include <unistd.h>
-    #include <sys/ioctl.h>
-    #include <signal.h>
-#endif
 
 #include "storm-config.h"
 #include "src/solver/SmtSolver.h"