diff --git a/src/counterexamples/GenerateCounterexample.h b/src/counterexamples/GenerateCounterexample.h new file mode 100644 index 000000000..12d0f1da5 --- /dev/null +++ b/src/counterexamples/GenerateCounterexample.h @@ -0,0 +1,146 @@ + +#ifndef STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_ +#define STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_ + + +#include "src/models/Dtmc.h" +#include "src/models/AtomicPropositionsLabeling.h" +#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "src/counterexamples/SMTMinimalCommandSetGenerator.h" +#include "src/counterexamples/PathBasedSubsystemGenerator.h" +#include "src/parser/PrctlParser.h" +#include "src/properties/Prctl.h" +#include "src/modelchecker/prctl/CreatePrctlModelChecker.h" + + +#include "src/parser/PrctlFileParser.h" + +#include "src/exceptions/InvalidSettingsException.h" + + +/*! + * Handles the counterexample generation control. + * + * @param parser An AutoParser to get the model from. + */ + void generateCounterExample(std::shared_ptr> model) { + LOG4CPLUS_INFO(logger, "Starting counterexample generation."); + LOG4CPLUS_INFO(logger, "Testing inputs..."); + + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + + // First test output directory. + std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); + if(outPath.back() != '/' && outPath.back() != '\\') { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + std::ofstream testFile(outPath + "test.dot"); + if(testFile.fail()) { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + testFile.close(); + std::remove((outPath + "test.dot").c_str()); + + // Differentiate between model types. + if(model->getType() != storm::models::DTMC) { + LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); + return; + } + + // Get the Dtmc back from the AbstractModel + // Note that the ownership of the object referenced by dtmc lies at the main function. + // Thus, it must not be deleted. + storm::models::Dtmc dtmc = *(model->as>()); + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + + // Get specified PRCTL formulas. + if(!s->isSet("prctl")) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); + std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); + + // Test for each formula if a counterexample can be generated for it. + if(formulaList.size() == 0) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula found."); + return; + } + + // Get prctl file name without the filetype + uint_fast64_t first = 0; + if(chosenPrctlFile.find('/') != std::string::npos) { + first = chosenPrctlFile.find_last_of('/') + 1; + } else if(chosenPrctlFile.find('\\') != std::string::npos) { + first = chosenPrctlFile.find_last_of('\\') + 1; + } + + uint_fast64_t length; + if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) { + length = chosenPrctlFile.find_last_of('.') - first; + } else { + length = chosenPrctlFile.length() - first; + } + + std::string outFileName = chosenPrctlFile.substr(first, length); + + // Test formulas and do generation + uint_fast64_t fIndex = 0; + for (auto formula : formulaList) { + + // First check if it is a formula type for which a counterexample can be generated. + if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { + LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); + continue; + } + + std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); + + // Do some output + std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; + LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": "); + std::cout << "\t" << formula->toString() << "\n" << std::endl; + LOG4CPLUS_INFO(logger, formula->toString()); + + // Now check if the model does not satisfy the formula. + // That is if there is at least one initial state of the model that does not. + + // Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them) + // Lower it again after the model check. + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); + storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc)); + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); + + if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) { + std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; + LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample."); + continue; + } + + // Generate counterexample + storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(dtmc, stateForm); + + LOG4CPLUS_INFO(logger, "Found counterexample."); + + // Output counterexample + // Do standard output + std::cout << "Found counterexample with following properties: " << std::endl; + counterExample.printModelInformationToStream(std::cout); + std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl; + + // Write the .dot file + std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot"); + if(outFile.good()) { + counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true); + outFile.close(); + } + + fIndex++; + } + } + +#endif \ No newline at end of file diff --git a/src/modelchecker/prctl/CreatePrctlModelChecker.h b/src/modelchecker/prctl/CreatePrctlModelChecker.h new file mode 100644 index 000000000..bd1b35c7e --- /dev/null +++ b/src/modelchecker/prctl/CreatePrctlModelChecker.h @@ -0,0 +1,43 @@ +#ifndef STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ + +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/NativeLinearEquationSolver.h" +#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GurobiLpSolver.h" +/*! + * Creates a model checker for the given DTMC that complies with the given options. + * + * @param dtmc A reference to the DTMC for which the model checker is to be created. + * @return A pointer to the resulting model checker. + */ +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc const & dtmc) { + // Create the appropriate model checker. + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString(); + if (linsolver == "gmm++") { + return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::GmmxxLinearEquationSolver()); + } else if (linsolver == "native") { + return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::NativeLinearEquationSolver()); + } + + // The control flow should never reach this point, as there is a default setting for matrixlib. + std::string message = "No matrix library suitable for DTMC model checking has been set."; + throw storm::exceptions::InvalidSettingsException() << message; + return nullptr; +} + +/*! + * Creates a model checker for the given MDP that complies with the given options. + * + * @param mdp The Dtmc that the model checker will check + * @return + */ +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const & mdp) { + // Create the appropriate model checker. + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); +} + +#endif \ No newline at end of file diff --git a/src/storm.cpp b/src/storm.cpp index a3328ae92..940e75ed8 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -13,14 +13,18 @@ * Description: Central part of the application containing the main() Method */ -#include "src/utility/OsDetection.h" -#include +#include "src/utility/Initialize.h" #include #include #include #include #include #include +#include +#include + + + #include "storm-config.h" #include "storm-version.h" @@ -30,12 +34,14 @@ #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/models/AtomicPropositionsLabeling.h" +#include "src/modelchecker/prctl/CreatePrctlModelChecker.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GurobiLpSolver.h" +#include "src/counterexamples/GenerateCounterexample.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" #include "src/counterexamples/PathBasedSubsystemGenerator.h" @@ -45,251 +51,20 @@ #include "src/utility/ErrorHandling.h" #include "src/properties/Prctl.h" #include "src/utility/vector.h" -#include "src/utility/OsDetection.h" +#include "src/utility/CLI.h" -#include "src/settings/Settings.h" -// Registers all standard options -#include "src/utility/StormOptions.h" #include "src/parser/PrctlFileParser.h" #include "src/parser/LtlFileParser.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" -log4cplus::Logger logger; - #include "src/parser/PrismParser.h" #include "src/adapters/ExplicitModelAdapter.h" // #include "src/adapters/SymbolicModelAdapter.h" #include "src/exceptions/InvalidSettingsException.h" -// Includes for the linked libraries and versions header -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif -#ifdef STORM_HAVE_GLPK -# include "glpk.h" -#endif -#ifdef STORM_HAVE_GUROBI -# include "gurobi_c.h" -#endif -#ifdef STORM_HAVE_Z3 -# include "z3.h" -#endif - -#include -#include -#include - -void printUsage() { -#ifndef WINDOWS - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - - std::cout << "===== Statistics ==============================" << std::endl; - std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; - std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; - std::cout << "===============================================" << std::endl; -#else - HANDLE hProcess = GetCurrentProcess (); - FILETIME ftCreation, ftExit, ftUser, ftKernel; - PROCESS_MEMORY_COUNTERS pmc; - if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { - std::cout << "Memory Usage: " << std::endl; - std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; - std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; - std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; - std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; - std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; - std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; - std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; - std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; - std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; - } - - GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); - - ULARGE_INTEGER uLargeInteger; - uLargeInteger.LowPart = ftKernel.dwLowDateTime; - uLargeInteger.HighPart = ftKernel.dwHighDateTime; - double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds - uLargeInteger.LowPart = ftUser.dwLowDateTime; - uLargeInteger.HighPart = ftUser.dwHighDateTime; - double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; - - std::cout << "CPU Time: " << std::endl; - std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; - std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; -#endif -} - -/*! - * Initializes the logging framework and sets up logging to console. - */ -void initializeLogger() { - logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); - log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); - consoleLogAppender->setName("mainConsoleAppender"); - consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); - consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); - logger.addAppender(consoleLogAppender); -} - -/*! - * Sets up the logging to file. - */ -void setUpFileLogging() { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString())); - fileLogAppender->setName("mainFileAppender"); - fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); - logger.addAppender(fileLogAppender); -} - -/*! -* Gives the current working directory -* -* @return std::string The path of the current working directory -*/ -std::string getCurrentWorkingDirectory() { - char temp[512]; - return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); -} - -/*! - * Prints the header. - */ -void printHeader(const int argc, const char* argv[]) { - std::cout << "StoRM" << std::endl; - std::cout << "-----" << std::endl << std::endl; - - std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; - if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { - std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; - } - std::cout << " build from revision " << STORM_CPP_VERSION_HASH; - if (STORM_CPP_VERSION_DIRTY == 1) { - std::cout << " (DIRTY)"; - } - std::cout << "." << std::endl; - -#ifdef STORM_HAVE_INTELTBB - std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; -#endif -#ifdef STORM_HAVE_GLPK - std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; -#endif -#ifdef STORM_HAVE_GUROBI - std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; -#endif -#ifdef STORM_HAVE_Z3 - unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; - Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); - std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; -#endif - - // "Compute" the command line argument string with which STORM was invoked. - std::stringstream commandStream; - for (int i = 0; i < argc; ++i) { - commandStream << argv[i] << " "; - } - std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; - std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; -} - -/*! - * Parses the given command line arguments. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return True iff the program should continue to run after parsing the options. - */ -bool parseOptions(const int argc, const char* argv[]) { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - try { - storm::settings::Settings::parse(argc, argv); - } catch (storm::exceptions::OptionParserException& e) { - std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << s->getHelpText(); - return false; - } - - if (s->isSet("help")) { - std::cout << storm::settings::Settings::getInstance()->getHelpText(); - return false; - } - - if (s->isSet("verbose")) { - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); - } - if (s->isSet("debug")) { - logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); - } - if (s->isSet("trace")) { - logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); - } - if (s->isSet("logfile")) { - setUpFileLogging(); - } - return true; -} - -/*! - * Performs some necessary initializations. - */ -void setUp() { - // Increase the precision of output. - std::cout.precision(10); -} - -/*! - * Performs some necessary clean-up. - */ -void cleanUp() { - // Intentionally left empty. -} -/*! - * Creates a model checker for the given DTMC that complies with the given options. - * - * @param dtmc A reference to the DTMC for which the model checker is to be created. - * @return A pointer to the resulting model checker. - */ -storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc const & dtmc) { - // Create the appropriate model checker. - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString(); - if (linsolver == "gmm++") { - return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::GmmxxLinearEquationSolver()); - } else if (linsolver == "native") { - return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::NativeLinearEquationSolver()); - } - - // The control flow should never reach this point, as there is a default setting for matrixlib. - std::string message = "No matrix library suitable for DTMC model checking has been set."; - throw storm::exceptions::InvalidSettingsException() << message; - return nullptr; -} -/*! - * Creates a model checker for the given MDP that complies with the given options. - * - * @param mdp The Dtmc that the model checker will check - * @return - */ -storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const & mdp) { - // Create the appropriate model checker. - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); -} /*! * Checks the PRCTL formulae provided on the command line on the given model checker. @@ -312,131 +87,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker } } -/*! - * Handles the counterexample generation control. - * - * @param parser An AutoParser to get the model from. - */ - void generateCounterExample(std::shared_ptr> model) { - LOG4CPLUS_INFO(logger, "Starting counterexample generation."); - LOG4CPLUS_INFO(logger, "Testing inputs..."); - - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - - // First test output directory. - std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); - if(outPath.back() != '/' && outPath.back() != '\\') { - LOG4CPLUS_ERROR(logger, "The output path is not valid."); - return; - } - std::ofstream testFile(outPath + "test.dot"); - if(testFile.fail()) { - LOG4CPLUS_ERROR(logger, "The output path is not valid."); - return; - } - testFile.close(); - std::remove((outPath + "test.dot").c_str()); - - // Differentiate between model types. - if(model->getType() != storm::models::DTMC) { - LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); - return; - } - - // Get the Dtmc back from the AbstractModel - // Note that the ownership of the object referenced by dtmc lies at the main function. - // Thus, it must not be deleted. - storm::models::Dtmc dtmc = *(model->as>()); - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - - // Get specified PRCTL formulas. - if(!s->isSet("prctl")) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); - return; - } - - std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); - LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); - - // Test for each formula if a counterexample can be generated for it. - if(formulaList.size() == 0) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula found."); - return; - } - - // Get prctl file name without the filetype - uint_fast64_t first = 0; - if(chosenPrctlFile.find('/') != std::string::npos) { - first = chosenPrctlFile.find_last_of('/') + 1; - } else if(chosenPrctlFile.find('\\') != std::string::npos) { - first = chosenPrctlFile.find_last_of('\\') + 1; - } - - uint_fast64_t length; - if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) { - length = chosenPrctlFile.find_last_of('.') - first; - } else { - length = chosenPrctlFile.length() - first; - } - - std::string outFileName = chosenPrctlFile.substr(first, length); - - // Test formulas and do generation - uint_fast64_t fIndex = 0; - for (auto formula : formulaList) { - - // First check if it is a formula type for which a counterexample can be generated. - if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { - LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); - continue; - } - - std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); - - // Do some output - std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; - LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": "); - std::cout << "\t" << formula->toString() << "\n" << std::endl; - LOG4CPLUS_INFO(logger, formula->toString()); - - // Now check if the model does not satisfy the formula. - // That is if there is at least one initial state of the model that does not. - - // Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them) - // Lower it again after the model check. - logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); - storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc)); - logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); - - if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) { - std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; - LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample."); - continue; - } - - // Generate counterexample - storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(dtmc, stateForm); - - LOG4CPLUS_INFO(logger, "Found counterexample."); - - // Output counterexample - // Do standard output - std::cout << "Found counterexample with following properties: " << std::endl; - counterExample.printModelInformationToStream(std::cout); - std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl; - - // Write the .dot file - std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot"); - if(outFile.good()) { - counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true); - outFile.close(); - } - - fIndex++; - } - } - /*! * Main entry point. */ diff --git a/src/utility/CLI.h b/src/utility/CLI.h new file mode 100644 index 000000000..858fdd8ff --- /dev/null +++ b/src/utility/CLI.h @@ -0,0 +1,168 @@ +#ifndef STORM_UTILITY_CLI_H_ +#define STORM_UTILITY_CLI_H_ + +#include +#include +#include +#include + + +#include "src/utility/OsDetection.h" +// Registers all standard options +#include "src/utility/StormOptions.h" + + +// Includes for the linked libraries and versions header +#ifdef STORM_HAVE_INTELTBB +# include "tbb/tbb_stddef.h" +#endif +#ifdef STORM_HAVE_GLPK +# include "glpk.h" +#endif +#ifdef STORM_HAVE_GUROBI +# include "gurobi_c.h" +#endif +#ifdef STORM_HAVE_Z3 +# include "z3.h" +#endif + +/*! +* Gives the current working directory +* +* @return std::string The path of the current working directory +*/ +std::string getCurrentWorkingDirectory() { + char temp[512]; + return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); +} + + +void printUsage() { +#ifndef WINDOWS + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + + std::cout << "===== Statistics ==============================" << std::endl; + std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; + std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "===============================================" << std::endl; +#else + HANDLE hProcess = GetCurrentProcess (); + FILETIME ftCreation, ftExit, ftUser, ftKernel; + PROCESS_MEMORY_COUNTERS pmc; + if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { + std::cout << "Memory Usage: " << std::endl; + std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; + std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; + std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; + std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; + std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; + std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; + std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; + std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; + std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; + } + + GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); + + ULARGE_INTEGER uLargeInteger; + uLargeInteger.LowPart = ftKernel.dwLowDateTime; + uLargeInteger.HighPart = ftKernel.dwHighDateTime; + double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds + uLargeInteger.LowPart = ftUser.dwLowDateTime; + uLargeInteger.HighPart = ftUser.dwHighDateTime; + double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; + + std::cout << "CPU Time: " << std::endl; + std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; + std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; +#endif +} + + + +/*! + * Prints the header. + */ +void printHeader(const int argc, const char* argv[]) { + std::cout << "StoRM" << std::endl; + std::cout << "-----" << std::endl << std::endl; + + std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; + if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { + std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; + } + std::cout << " build from revision " << STORM_CPP_VERSION_HASH; + if (STORM_CPP_VERSION_DIRTY == 1) { + std::cout << " (DIRTY)"; + } + std::cout << "." << std::endl; + +#ifdef STORM_HAVE_INTELTBB + std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; +#endif +#ifdef STORM_HAVE_GLPK + std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; +#endif +#ifdef STORM_HAVE_GUROBI + std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; +#endif +#ifdef STORM_HAVE_Z3 + unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; + Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); + std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; +#endif + + // "Compute" the command line argument string with which STORM was invoked. + std::stringstream commandStream; + for (int i = 0; i < argc; ++i) { + commandStream << argv[i] << " "; + } + std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; + std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; +} + +/*! + * Parses the given command line arguments. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(const int argc, const char* argv[]) { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + try { + storm::settings::Settings::parse(argc, argv); + } catch (storm::exceptions::OptionParserException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << s->getHelpText(); + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::Settings::getInstance()->getHelpText(); + return false; + } + + if (s->isSet("verbose")) { + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); + } + if (s->isSet("debug")) { + logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); + } + if (s->isSet("trace")) { + logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); + } + if (s->isSet("logfile")) { + setUpFileLogging(); + } + return true; +} + + +#endif \ No newline at end of file diff --git a/src/utility/Initialize.h b/src/utility/Initialize.h new file mode 100644 index 000000000..cf2facda5 --- /dev/null +++ b/src/utility/Initialize.h @@ -0,0 +1,22 @@ +#ifndef STORM_UTILITY_INITIALIZE_H_ +#define STORM_UTILITY_INITIALIZE_H_ + +#include "InitializeLogging.h" + +/*! + * Performs some necessary initializations. + */ +void setUp() { + // Increase the precision of output. + std::cout.precision(10); +} + +/*! + * Performs some necessary clean-up. + */ +void cleanUp() { + // Intentionally left empty. +} + + +#endif \ No newline at end of file diff --git a/src/utility/InitializeLogging.h b/src/utility/InitializeLogging.h new file mode 100644 index 000000000..af45f21c3 --- /dev/null +++ b/src/utility/InitializeLogging.h @@ -0,0 +1,38 @@ +#ifndef STORM_UTILITY_INITIALIZELOGGING_H_ +#define STORM_UTILITY_INITIALIZELOGGING_H_ + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" + +#include "src/settings/Settings.h" + +log4cplus::Logger logger; + +/*! + * Initializes the logging framework and sets up logging to console. + */ +void initializeLogger() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); + consoleLogAppender->setName("mainConsoleAppender"); + consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); + consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); + logger.addAppender(consoleLogAppender); +} + +/*! + * Sets up the logging to file. + */ +void setUpFileLogging() { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString())); + fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); + logger.addAppender(fileLogAppender); +} + + +#endif \ No newline at end of file