factored out code parts from storm.cpp

Former-commit-id: 91cd8e52ad
10 years ago · b3810dc75b
4 changed files with 342 additions and 0 deletions
--- a/src/counterexamples/GenerateCounterexample.h
+++ b/src/counterexamples/GenerateCounterexample.h
@ -0,0 +1,132 @@
+
+#ifndef STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_
+#define STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_
+
+
+
+/*!
+ * Handles the counterexample generation control.
+ *
+ * @param parser An AutoParser to get the model from.
+ */
+ void generateCounterExample(std::shared_ptr<storm::models::AbstractModel<double>> 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<double> dtmc = *(model->as<storm::models::Dtmc<double>>());
+	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<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> 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<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild()).get() == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula.");
+			continue;
+		}
+
+		std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> stateForm = std::static_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(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<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::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
--- a/src/utility/CLI.h
+++ b/src/utility/CLI.h
@ -0,0 +1,151 @@
+#ifndef STORM_UTILITY_CLI_H_
+#define STORM_UTILITY_CLI_H_
+
+#include <iostream>
+#include <fstream>
+#include <cstdio>
+#include <sstream>
+
+
+#include "src/utility/OsDetection.h"
+
+/*!
+* 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<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
+	uLargeInteger.LowPart = ftUser.dwLowDateTime;
+	uLargeInteger.HighPart = ftUser.dwHighDateTime;
+	double userTime = static_cast<double>(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
--- a/src/utility/Initialize.h
+++ 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
--- a/src/utility/InitializeLogging.h
+++ b/src/utility/InitializeLogging.h
@ -0,0 +1,37 @@
+#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"
+
+
+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<log4cplus::Layout>(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<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
+	logger.addAppender(fileLogAppender);
+}
+
+
+#endif