From 2b807dd72eb621757bc005e18b8c7553c435d2b8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 11 Apr 2015 17:09:17 +0200 Subject: [PATCH] implemented communication with solver Former-commit-id: 8e34e1772200f84defc070593ba2cfe80f9b6ff8 --- .../SparseDtmcEliminationModelChecker.cpp | 20 +- .../modules/Smt2SmtSolverSettings.cpp | 10 +- src/settings/modules/Smt2SmtSolverSettings.h | 2 +- src/solver/Smt2SmtSolver.cpp | 187 +++++++++++++++--- src/solver/Smt2SmtSolver.h | 51 ++++- 5 files changed, 227 insertions(+), 43 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 1e0cdd9ba..60a56f07b 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/solver/SmtSolver.h" #include "src/solver/Smt2SmtSolver.h" #include "src/utility/graph.h" @@ -1072,7 +1073,6 @@ namespace storm { // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; - std::cout << "states with prob 0" << statesWithProbability0 << std::endl; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); @@ -1142,9 +1142,6 @@ namespace storm { //now lets add the actual transitions for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){ storm::RationalFunction reachProbability(oneStepProbabilities[state]); - if(!reachProbability.isZero()){ - std::cout << "non zero " << state << ": " << reachProbability << std::endl; - } for(auto const& transition : flexibleMatrix.getRow(state)){ reachProbability += transition.getValue() * stateProbVars[transition.getColumn()]; } @@ -1187,8 +1184,17 @@ namespace storm { solver.add(carl::Constraint(uB,storm::CompareRelation::LEQ)); } - flexibleMatrix.print(); - + switch (solver.check()){ + case storm::solver::SmtSolver::CheckResult::Sat: + std::cout << "sat!" << std::endl; + break; + case storm::solver::SmtSolver::CheckResult::Unsat: + std::cout << "unsat!" << std::endl; + break; + case storm::solver::SmtSolver::CheckResult::Unknown: + std::cout << "unknown!" << std::endl; + break; + } /* //testing stuff... @@ -1290,7 +1296,7 @@ namespace storm { flexibleMatrix.getRow(*initialStates.begin()).clear(); } } - */ + std::cout << std::endl << "-----------------------" << std::endl << "testing stuff..." << std::endl; std::map testmap; diff --git a/src/settings/modules/Smt2SmtSolverSettings.cpp b/src/settings/modules/Smt2SmtSolverSettings.cpp index 8d63f7bb2..3f6738c50 100644 --- a/src/settings/modules/Smt2SmtSolverSettings.cpp +++ b/src/settings/modules/Smt2SmtSolverSettings.cpp @@ -6,14 +6,14 @@ namespace storm { namespace settings { namespace modules { - const std::string Smt2SmtSolverSettings::moduleName = "smt2smtsolver"; + const std::string Smt2SmtSolverSettings::moduleName = "smt2"; const std::string Smt2SmtSolverSettings::solverCommandOption = "solvercommand"; - const std::string Smt2SmtSolverSettings::exportSmtLibScriptOption = "exportSmtLibScript"; + const std::string Smt2SmtSolverSettings::exportScriptOption = "exportscript"; Smt2SmtSolverSettings::Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, solverCommandOption, true, "If set, this command is used to call the solver and to let the solver know that it should read SMT-LIBv2 commands from standard input. If not set, only a SMT-LIB script file might be exported.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("command", "path to the solver + command line arguments.").setDefaultValueString("").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportSmtLibScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build()); } bool Smt2SmtSolverSettings::isSolverCommandSet() const{ @@ -26,12 +26,12 @@ namespace storm { bool Smt2SmtSolverSettings::isExportSmtLibScriptSet() const{ - return this->getOption(exportSmtLibScriptOption).getHasOptionBeenSet(); + return this->getOption(exportScriptOption).getHasOptionBeenSet(); } std::string Smt2SmtSolverSettings::getExportSmtLibScriptPath() const{ - return this->getOption(solverCommandOption).getArgumentByName("path").getValueAsString(); + return this->getOption(exportScriptOption).getArgumentByName("path").getValueAsString(); } diff --git a/src/settings/modules/Smt2SmtSolverSettings.h b/src/settings/modules/Smt2SmtSolverSettings.h index 07702affd..c199a99cb 100644 --- a/src/settings/modules/Smt2SmtSolverSettings.h +++ b/src/settings/modules/Smt2SmtSolverSettings.h @@ -55,7 +55,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string solverCommandOption; - static const std::string exportSmtLibScriptOption; + static const std::string exportScriptOption; }; } // namespace modules diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp index 2ca8ec5e8..577163d82 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/Smt2SmtSolver.cpp @@ -8,6 +8,7 @@ #include "src/exceptions/IllegalFunctionCallException.h" #include "utility/macros.h" #include "adapters/CarlAdapter.h" +#include "exceptions/UnexpectedException.h" namespace storm { namespace solver { @@ -28,32 +29,42 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) { + Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) { #ifndef STORM_HAVE_CARL STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL"); +#endif +#ifndef WINDOWS + processIdOfSolver=0; #endif expressionAdapter = std::unique_ptr(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true)); init(); } Smt2SmtSolver::~Smt2SmtSolver() { - writeCommand("( exit )"); - //todo make sure that the process exits + writeCommand("( exit )", true); +#ifndef WINDOWS + if(processIdOfSolver!=0){ + //Since the process has been open successfully, it means that we have to close our fds + close(fromSolver); + close(toSolver); + //todo make sure that the process exits waitpid kill(pid, ..); + } +#endif } void Smt2SmtSolver::push() { expressionAdapter->increaseScope(); - writeCommand("( push 1 ) "); + writeCommand("( push 1 ) ", true); } void Smt2SmtSolver::pop() { expressionAdapter->decreaseScope(); - writeCommand("( pop 1 ) "); + writeCommand("( pop 1 ) ", true); } void Smt2SmtSolver::pop(uint_fast64_t n) { expressionAdapter->decreaseScope(n); - writeCommand("( pop " + std::to_string(n) + " ) "); + writeCommand("( pop " + std::to_string(n) + " ) ", true); } void Smt2SmtSolver::reset() { @@ -74,9 +85,9 @@ namespace storm { rightHandSide.gatherVariables(variables); std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); for (auto declaration : varDeclarations){ - writeCommand(declaration); + writeCommand(declaration, true); } - writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )"); + writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true); } template<> @@ -90,24 +101,34 @@ namespace storm { std::set variables = constraint.lhs().gatherVariables(); std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); for (auto declaration : varDeclarations){ - writeCommand(declaration); + writeCommand(declaration, true); } - writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )"); + writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); } #endif SmtSolver::CheckResult Smt2SmtSolver::check() { - writeCommand("( check-sat )"); - if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){ - // todo get the result - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + writeCommand("( check-sat )", false); +#ifdef WINDOWS + STORM_LOG_WARN("SMT-LIBv2 Solver can not be started on Windows as this is not yet implemented. Assume that the check-result is \"unknown\""); + return SmtSolver::CheckResult::Unknown; +#else + + if (processIdOfSolver!=0){ + auto solverOutput = readSolverOutput(); + STORM_LOG_THROW(solverOutput.size()==1, storm::exceptions::UnexpectedException, "expected a single line of output after smt2 command ( check-sat ). Got " + std::to_string(solverOutput.size()) + " lines of output instead."); + solverOutput[0].erase(std::remove_if(solverOutput[0].begin(), solverOutput[0].end(), isspace), solverOutput[0].end()); //remove spaces + if(solverOutput[0]=="sat") return SmtSolver::CheckResult::Sat; + if(solverOutput[0]=="unsat") return SmtSolver::CheckResult::Unsat; + if(solverOutput[0]=="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\""); return SmtSolver::CheckResult::Unknown; } +#endif } SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set const& assumptions) { @@ -123,8 +144,53 @@ namespace storm { void Smt2SmtSolver::init() { if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){ - //todo call the solver! - std::string cmd = storm::settings::smt2SmtSolverSettings().getSolverCommand(); +#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 + //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(); + std::vector solverCommandVec; + boost::split(solverCommandVec, cmdString, boost::is_any_of("\t ")); + char** solverArgs = new char* [solverCommandVec.size()+1]; + solverArgs[0] = const_cast(solverCommandVec[0].substr(0, cmdString.rfind('/')+1).c_str()); + for(uint_fast64_t argumentIndex = 1; argumentIndex(solverCommandVec[argumentIndex].c_str()); + } + solverArgs[solverCommandVec.size()] = NULL; + + //get the pipes started + int pipeIn[2]; + int pipeOut[2]; + const int READ=0; + const int WRITE=1; + STORM_LOG_THROW(pipe(pipeIn) == 0 && pipe(pipeOut)==0, storm::exceptions::UnexpectedException, "Could not open pipe to new process"); + + //now start the child process, i.e., the solver + pid_t pid = fork(); + STORM_LOG_THROW(pid>=0, storm::exceptions::UnexpectedException, "Could not start new process for the smt solver"); + if (pid == 0){ + // Child process + // 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); + // 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]); + close(pipeOut[READ]); + close(pipeOut[WRITE]); + + execv(solverCommandVec[0].c_str(), solverArgs); //"-smt2 -in" + // if we reach this point, execl was not successful + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not execute the solver correctly"); + } + // Parent Process + toSolver=pipeIn[WRITE]; + fromSolver=pipeOut[READ]; + close(pipeOut[WRITE]); + close(pipeIn[READ]); + processIdOfSolver=pid; +#endif } else{ STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done"); @@ -133,22 +199,95 @@ namespace storm { if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){ STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file"); commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc); - STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + isCommandFileOpen=commandFile.is_open(); + STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); } //some initial commands - writeCommand("( set-logic QF_NRA )"); - + writeCommand("( set-option :print-success true )", true); + writeCommand("( set-logic QF_NRA )", true); + //writeCommand("( get-info :name )"); } - void Smt2SmtSolver::writeCommand(std::string smt2Command) { - if (commandFile.is_open()) { + void Smt2SmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) { + if (isCommandFileOpen) { commandFile << smt2Command << std::endl; - } else{ - std::cout << "COMMAND FILE IS CLOSED" <> response after smt2 command " + smt2Command + ". Got <<" + output[0] + ">> instead"); + } + } +#endif + } + + std::vector Smt2SmtSolver::readSolverOutput(bool waitForOutput){ +#ifndef WINDOWS + if (processIdOfSolver==0){ + STORM_LOG_DEBUG("failed to read solver output as the solver is not running"); + return std::vector(); + } + int bytesReadable; + if(waitForOutput){ + bytesReadable=1;//just assume that there are bytes readable + } + else if(ioctl(fromSolver, FIONREAD, &bytesReadable)< 0){ //actually obtain the readable bytes + STORM_LOG_ERROR("Could not check if the solver has output"); + return std::vector(); + } + std::string solverOutput=""; + const ssize_t MAX_CHUNK_SIZE=256; + char chunk[MAX_CHUNK_SIZE]; + while(bytesReadable>0){ + ssize_t chunkSize = read(fromSolver, chunk, MAX_CHUNK_SIZE); + STORM_LOG_THROW(chunkSize>=0, storm::exceptions::UnexpectedException, "failed to read solver output"); + solverOutput += std::string(chunk, chunkSize); + if(ioctl(fromSolver, FIONREAD, &bytesReadable)< 0){//obtain the new amount of readable bytes + STORM_LOG_ERROR("Could not check if the solver has output"); + 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"); + bytesReadable=1; //we expect more output! + } + } + checkForErrorMessage(solverOutput); + std::vector solverOutputAsVector; + if(solverOutput.length()>0){ + solverOutput=solverOutput.substr(0,solverOutput.length()-1); + boost::split(solverOutputAsVector, solverOutput, boost::is_any_of("\n")); + //note: this is a little bit unsafe as \n can be contained within a solver response + } + return solverOutputAsVector; +#endif + } + + 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; + } + } + errorMsg += "The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance,200); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg); + } } } } \ No newline at end of file diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/Smt2SmtSolver.h index 5571660ad..3ba191349 100644 --- a/src/solver/Smt2SmtSolver.h +++ b/src/solver/Smt2SmtSolver.h @@ -3,6 +3,10 @@ #include #include +#ifndef WINDOWS + #include + #include +#endif #include "storm-config.h" #include "src/solver/SmtSolver.h" @@ -11,7 +15,12 @@ namespace storm { namespace solver { - + /*! + * This class represents an SMT-LIBv2 conforming solver. + * Any SMT-LIBv2 conforming solver can be called and will be opened as a child process. + * It is also possible to export the SMT2 script for later use. + * @note The parsing of the solver responses is a little bit crude and might cause bugs (e.g., if a variable name has the infix "error") + */ class Smt2SmtSolver : public SmtSolver { public: @@ -31,7 +40,7 @@ namespace storm { public: /*! * Creates a new solver with the given manager. - * In addition to storm expressions, this solver also allows carl expressions (but not both). + * In addition to storm expressions, this solver also allows carl expressions (but not both to not confuse variables). * Hence, there is a flag to chose between the two */ Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false); @@ -79,21 +88,51 @@ namespace storm { /*! - * Initializes the solver + * Initializes the solver, i.e. opens a new process for it and creates a file stream for the script file (if demanded) + * Moreover, some initial commands are send to the solver */ void init(); - /*! Writes the given command to the solver + /*! + * Writes the given command to the solver * @param smt2Command the command that the solver will receive + * @param expectSuccess set this flag to true whenever a success response from the solver is expected. */ - void writeCommand(std::string smt2Command); - + void writeCommand(std::string smt2Command, bool expectSuccess); + + /*! + * Reads from the solver. The output is checked for an error message and an exception is thrown in that case. + * @param waitForOutput if this is true and there is currently no output, we will wait until there is output. + * @return the output of the solver. Every entry of the vector corresponds to one output line + */ + std::vector readSolverOutput(bool waitForOutput=true); + + /*! + * Checks if the given message contains an error message and throws an exception. + * More precisely, an exception is thrown whenever the word "error" is contained in the message. + * This function is directly called when reading the solver output via readSolverOutput() + * We will try to parse the message in the SMT-LIBv2 format, i.e., + * ( error "this is the error message from the solver" ) to give some debug information + * However, the whole message is always written to the debug log (providing there is an error) + * @param message the considered message which should be an output of the solver. + */ + void checkForErrorMessage(const std::string message); +#ifndef WINDOWS + // descriptors for the pipe from and to the solver + int toSolver; + int fromSolver; + // A flag storing the Process ID of the solver. If this is zero, then the solver is not running + pid_t processIdOfSolver; +#endif + // a filestream where the commands that we send to the solver will be stored (can be used for debugging purposes) std::ofstream commandFile; + bool isCommandFileOpen; + // An expression adapter that is used for translating the expression into Smt2's format. std::unique_ptr expressionAdapter;