diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index c7fed339c..023607f44 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -261,7 +261,13 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now(); this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState); std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now(); - // std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl; + + //std::string funcStr = " (/ " + + // this->reachProbFunction.nominator().toString(false, true) + " " + + // this->reachProbFunction.denominator().toString(false, true) + + // " )"; + // std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl; + std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now(); initializeSMTSolver(this->smtSolver, this->reachProbFunction,*this->probabilityOperatorFormula); @@ -386,7 +392,6 @@ namespace storm { solver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); ParametricType bound= storm::utility::regions::convertNumber(this->probabilityOperatorFormula->getBound()); - std::cout << "bound is " << bound << std::endl; // To prove that the property is satisfied in the initial state for all parameters, // we ask the solver whether the negation of the property is satisfiable and invert the answer. @@ -529,7 +534,6 @@ namespace storm { template bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool viaReachProbFunction) { - // check whether the property is satisfied or not at the given point bool valueInBoundOfFormula; if(viaReachProbFunction){ @@ -865,7 +869,10 @@ namespace storm { return true; case storm::solver::SmtSolver::CheckResult::Unknown: default: - STORM_LOG_WARN("The SMT solver was not able to compute a result for this region"); + STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); + if(this->smtSolver->isNeedsRestart()){ + initializeSMTSolver(this->smtSolver,this->reachProbFunction, *this->probabilityOperatorFormula); + } return false; } } diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp index 6f06f3a3a..941fe7a3e 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/Smt2SmtSolver.cpp @@ -41,7 +41,7 @@ namespace storm { } Smt2SmtSolver::~Smt2SmtSolver() { - writeCommand("( exit )", true); + 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 @@ -150,6 +150,9 @@ namespace storm { if(solverOutput[0]=="sat") return SmtSolver::CheckResult::Sat; if(solverOutput[0]=="unsat") return SmtSolver::CheckResult::Unsat; if(solverOutput[0]=="unknown") return SmtSolver::CheckResult::Unknown; + //if we reach this point, something unexpected happened. Lets return unknown and print some debug output + STORM_LOG_DEBUG("unexpected solver output: " << solverOutput[0] << ". Returning result 'unknown'"); + return SmtSolver::CheckResult::Unknown; } else{ STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\""); @@ -174,6 +177,9 @@ namespace storm { #ifdef WINDOWS STORM_LOG_WARN("opening a thread for the smt solver is not implemented on Windows. Hence, no actual solving will be done") #else + signal(SIGPIPE, SIG_IGN); + this->needsRestart=false; + //for executing the solver we will need the path to the executable file as well as the arguments as a char* array //where the first argument is the path to the executable file and the last is NULL const std::string cmdString = storm::settings::smt2SmtSolverSettings().getSolverCommand(); @@ -201,6 +207,7 @@ namespace storm { // duplicate the fd so that standard input and output will be send to our pipes dup2(pipeIn[READ], STDIN_FILENO); dup2(pipeOut[WRITE], STDOUT_FILENO); + dup2(pipeOut[WRITE], STDERR_FILENO); // we can now close everything since our child process will use std in and out to address the pipes close(pipeIn[READ]); close(pipeIn[WRITE]); @@ -217,6 +224,8 @@ namespace storm { close(pipeOut[WRITE]); close(pipeIn[READ]); processIdOfSolver=pid; + + #endif } else{ @@ -236,6 +245,10 @@ namespace storm { //writeCommand("( get-info :name )"); } + bool Smt2SmtSolver::isNeedsRestart() const { + return this->needsRestart; + } + void Smt2SmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) { if (isCommandFileOpen) { commandFile << smt2Command << std::endl; @@ -243,7 +256,9 @@ namespace storm { #ifndef WINDOWS if (processIdOfSolver!=0){ - write(toSolver, (smt2Command+"\n").c_str(), smt2Command.length()+1); + if(write(toSolver, (smt2Command+"\n").c_str(), smt2Command.length()+1) < 0){ + STORM_LOG_DEBUG("Was not able to write " << smt2Command << "to the solver."); + } if(expectSuccess){ auto output=readSolverOutput(); STORM_LOG_THROW(output.size()==1, storm::exceptions::UnexpectedException, "expected a single success response after smt2 command " + smt2Command + ". Got " + std::to_string(output.size()) + " lines of output instead."); @@ -280,7 +295,7 @@ namespace storm { return std::vector(); } if(bytesReadable==0 && solverOutput.back()!='\n'){ - STORM_LOG_DEBUG("Solver Output did not end with newline symbol (\\n). Since we assume that this should case, we will wait for more output from the solver"); + 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! } } @@ -298,22 +313,33 @@ namespace storm { void Smt2SmtSolver::checkForErrorMessage(const std::string message){ size_t errorOccurrance = message.find("error"); if (errorOccurrance!=std::string::npos){ - std::string errorMsg = "An error was detected while checking the solver output. "; - STORM_LOG_DEBUG("Detected an error message in the solver response:\n" + message); - size_t firstQuoteSign = message.find('\"',errorOccurrance); - if(firstQuoteSign!=std::string::npos && message.find("\\\"", firstQuoteSign-1)!=firstQuoteSign-1){ - size_t secondQuoteSign = message.find('\"', firstQuoteSign+1); - while(secondQuoteSign!=std::string::npos && message.find("\\\"", secondQuoteSign-1)==secondQuoteSign-1){ - secondQuoteSign = message.find('\"',secondQuoteSign+1); - } - if(secondQuoteSign!=std::string::npos){ - errorMsg += "The error message was:\n" + message.substr(errorOccurrance,secondQuoteSign-errorOccurrance+1) + "."; - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg); - return; + this->needsRestart=true; + //do not throw an exception for timeout or memout errors + if(message.find("timeout")!=std::string::npos){ + STORM_LOG_INFO("SMT solver answered: '" << message << "' and I am interpreting this as timeout "); + } + else if(message.find("memory")!=std::string::npos){ + STORM_LOG_INFO("SMT solver answered: '" << message << "' and I am interpreting this as out of memory "); + this->processIdOfSolver=0; + } + else{ + std::string errorMsg = "An error was detected while checking the solver output. "; + STORM_LOG_DEBUG("Detected an error message in the solver response:\n" + message); + size_t firstQuoteSign = message.find('\"',errorOccurrance); + if(firstQuoteSign!=std::string::npos && message.find("\\\"", firstQuoteSign-1)!=firstQuoteSign-1){ + size_t secondQuoteSign = message.find('\"', firstQuoteSign+1); + while(secondQuoteSign!=std::string::npos && message.find("\\\"", secondQuoteSign-1)==secondQuoteSign-1){ + secondQuoteSign = message.find('\"',secondQuoteSign+1); + } + if(secondQuoteSign!=std::string::npos){ + errorMsg += "The error message was: <<" + message.substr(errorOccurrance,secondQuoteSign-errorOccurrance+1) + ">>."; + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg); + return; + } } + errorMsg += "The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance,200); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg); } - errorMsg += "The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance,200); - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg); } } } diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/Smt2SmtSolver.h index 40710d562..a1bcf03d5 100644 --- a/src/solver/Smt2SmtSolver.h +++ b/src/solver/Smt2SmtSolver.h @@ -6,6 +6,7 @@ #ifndef WINDOWS #include #include + #include #endif #include "storm-config.h" @@ -73,10 +74,12 @@ namespace storm { virtual CheckResult check() override; virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; - #ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; #endif + + bool isNeedsRestart() const; + //Todo: some of these might be added in the future //virtual storm::expressions::SimpleValuation getModelAsValuation() override; @@ -154,6 +157,9 @@ namespace storm { // A flag that states whether to use readable variable names bool useReadableVarNames=true; + // A flag that states whether some error has occured + bool needsRestart=false; + }; } } diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index ed3f34c27..fd1717014 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -146,9 +146,6 @@ namespace storm { template<> storm::Variable getNewVariable(std::string variableName, VariableSort sort){ - storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName); - STORM_LOG_THROW(var==carl::Variable::NO_VARIABLE, storm::exceptions::InvalidArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use."); - carl::VariableType carlVarType; switch(sort){ case VariableSort::VS_BOOL: @@ -163,6 +160,14 @@ namespace storm { default: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given variable sort is not implemented"); } + + storm::Variable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName); + //STORM_LOG_THROW(var==carl::Variable::NO_VARIABLE, storm::exceptions::InvalidArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use."); + if(var!=carl::Variable::NO_VARIABLE){ + STORM_LOG_THROW(var.getType()==carlVarType, storm::exceptions::InvalidArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use for a variable of a different sort."); + return var; + } + return carl::VariablePool::getInstance().getFreshVariable(variableName, carlVarType); } diff --git a/src/utility/regions.h b/src/utility/regions.h index 02975761a..bc1a76307 100644 --- a/src/utility/regions.h +++ b/src/utility/regions.h @@ -102,7 +102,8 @@ namespace storm { /* * Creates a new variable with the given name and the given sort - * Throws an exception if there is already a variable with that name. + * If there is already a variable with that name, that variable is returned. + * An exception is thrown if there already is a variable with the given name, but with a different sort. */ template VariableType getNewVariable(std::string variableName, VariableSort sort);