Browse Source

Merge branch 'refactorMainCpp'

Former-commit-id: 21cdb65d5e
tempestpy_adaptions
sjunges 10 years ago
parent
commit
e0f9bd7865
  1. 146
      src/counterexamples/GenerateCounterexample.h
  2. 43
      src/modelchecker/prctl/CreatePrctlModelChecker.h
  3. 368
      src/storm.cpp
  4. 168
      src/utility/CLI.h
  5. 22
      src/utility/Initialize.h
  6. 38
      src/utility/InitializeLogging.h

146
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<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

43
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<double>* createPrctlModelChecker(storm::models::Dtmc<double> 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<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
} else if (linsolver == "native") {
return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::NativeLinearEquationSolver<double>());
}
// 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<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) {
// Create the appropriate model checker.
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
}
#endif

368
src/storm.cpp

@ -13,14 +13,18 @@
* Description: Central part of the application containing the main() Method * Description: Central part of the application containing the main() Method
*/ */
#include "src/utility/OsDetection.h"
#include <iostream>
#include "src/utility/Initialize.h"
#include <fstream> #include <fstream>
#include <cstdio> #include <cstdio>
#include <climits> #include <climits>
#include <sstream> #include <sstream>
#include <vector> #include <vector>
#include <chrono> #include <chrono>
#include <iostream>
#include <iomanip>
#include "storm-config.h" #include "storm-config.h"
#include "storm-version.h" #include "storm-version.h"
@ -30,12 +34,14 @@
#include "src/storage/MaximalEndComponentDecomposition.h" #include "src/storage/MaximalEndComponentDecomposition.h"
#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
#include "src/models/AtomicPropositionsLabeling.h" #include "src/models/AtomicPropositionsLabeling.h"
#include "src/modelchecker/prctl/CreatePrctlModelChecker.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/solver/GurobiLpSolver.h" #include "src/solver/GurobiLpSolver.h"
#include "src/counterexamples/GenerateCounterexample.h"
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
#include "src/counterexamples/PathBasedSubsystemGenerator.h" #include "src/counterexamples/PathBasedSubsystemGenerator.h"
@ -45,251 +51,20 @@
#include "src/utility/ErrorHandling.h" #include "src/utility/ErrorHandling.h"
#include "src/properties/Prctl.h" #include "src/properties/Prctl.h"
#include "src/utility/vector.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/PrctlFileParser.h"
#include "src/parser/LtlFileParser.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/parser/PrismParser.h"
#include "src/adapters/ExplicitModelAdapter.h" #include "src/adapters/ExplicitModelAdapter.h"
// #include "src/adapters/SymbolicModelAdapter.h" // #include "src/adapters/SymbolicModelAdapter.h"
#include "src/exceptions/InvalidSettingsException.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 <iostream>
#include <iomanip>
#include <fstream>
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
}
/*!
* 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);
}
/*!
* 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<double>* createPrctlModelChecker(storm::models::Dtmc<double> 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<double>(dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
} else if (linsolver == "native") {
return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc, new storm::solver::NativeLinearEquationSolver<double>());
}
// 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<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) {
// Create the appropriate model checker.
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
}
/*! /*!
* Checks the PRCTL formulae provided on the command line on the given model checker. * Checks the PRCTL formulae provided on the command line on the given model checker.
@ -312,131 +87,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
} }
} }
/*!
* 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++;
}
}
/*! /*!
* Main entry point. * Main entry point.
*/ */

168
src/utility/CLI.h

@ -0,0 +1,168 @@
#ifndef STORM_UTILITY_CLI_H_
#define STORM_UTILITY_CLI_H_
#include <iostream>
#include <fstream>
#include <cstdio>
#include <sstream>
#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<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

22
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

38
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<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
Loading…
Cancel
Save