@ -41,43 +41,63 @@
log4cplus : : Logger logger ;
/*!
* Initializes the logging framework .
* Initializes the logging framework and sets up logging to console .
*/
void setUpFileLogging ( ) {
log4cplus : : SharedAppenderPtr fileLogAppender ( new log4cplus : : FileAppender ( " mrmc.log " ) ) ;
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 = log4cplus : : Logger : : getInstance ( " mainLogger " ) ;
logger . addAppender ( fileLogAppender ) ;
}
void setUpConsoleLogging ( ) {
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 - > setLayout ( std : : auto_ptr < log4cplus : : Layout > ( new log4cplus : : PatternLayout ( " %-5p - %D{%H:%M:%S} (%r ms) - %b:%L : %m%n " ) ) ) ;
consoleLogAppender - > setLayout ( std : : auto_ptr < log4cplus : : Layout > ( new log4cplus : : PatternLayout ( " %-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n " ) ) ) ;
logger . addAppender ( consoleLogAppender ) ;
}
int main ( const int argc , const char * argv [ ] ) {
setUpFileLogging ( ) ;
/*!
* Sets up the logging to file .
*/
void setUpFileLogging ( ) {
mrmc : : settings : : Settings * s = mrmc : : settings : : instance ( ) ;
log4cplus : : SharedAppenderPtr fileLogAppender ( new log4cplus : : FileAppender ( s - > getString ( " logfile " ) ) ) ;
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 ) ;
}
mrmc : : settings : : Settings * s = nullptr ;
LOG4CPLUS_INFO ( logger , " This is the Markov Reward Model Checker (MRMC) by i2 of RWTH Aachen University. " ) ;
/*!
* Prints the header .
*/
void printHeader ( const int argc , const char * argv [ ] ) {
std : : cout < < " MRMC " < < std : : endl ;
std : : cout < < " ==== " < < std : : endl < < std : : endl ;
// "Compute" the command line argument string with which MRMC was invoked and log as diagnostic information.
std : : cout < < " Version: 1.0 " < < std : : endl ;
// "Compute" the command line argument string with which MRMC was invoked.
std : : stringstream commandStream ;
for ( int i = 0 ; i < argc ; + + i ) {
commandStream < < argv [ i ] < < " " ;
}
LOG4CPLUS_INFO ( logger , " MRMC command invoked " < < commandStream . str ( ) ) ;
std : : cout < < " Command line: " < < commandStream . str ( ) < < std : : endl < < std : : endl ;
}
/*!
* Prints the footer .
*/
void printFooter ( ) {
std : : cout < < " Nothing more to do, exiting. " < < std : : endl ;
}
/*!
* Function that parses the command line options .
* @ 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 [ ] ) {
mrmc : : settings : : Settings * s = nullptr ;
try {
mrmc : : settings : : Settings : : registerModule < mrmc : : modelChecker : : GmmxxDtmcPrctlModelChecker < double > > ( ) ;
mrmc : : settings : : Settings : : registerModule < mrmc : : modelChecker : : GmmxxDtmcPrctlModelChecker < double > > ( ) ;
s = mrmc : : settings : : newInstance ( argc , argv , nullptr ) ;
} catch ( mrmc : : exceptions : : InvalidSettingsException & e ) {
LOG4CPLUS_FATAL ( logger , " InvalidSettings error: " < < e . what ( ) < < " . " ) ;
LOG4CPLUS_FATAL ( logger , " Could not recover from settings error, terminating. " ) ;
std : : cout < < " Could not recover from settings error: " < < e . what ( ) < < " . " < < std : : endl ;
std : : cout < < std : : endl < < mrmc : : settings : : help ;
delete s ;
@ -87,31 +107,71 @@ int main(const int argc, const char* argv[]) {
if ( s - > isSet ( " help " ) ) {
std : : cout < < mrmc : : settings : : help ;
delete s ;
return 0 ;
return false ;
}
if ( s - > isSet ( " test-prctl " ) ) {
mrmc : : parser : : PrctlParser parser ( s - > getString ( " test-prctl " ) . c_str ( ) ) ;
delete s ;
return 0 ;
return false ;
}
if ( s - > isSet ( " verbose " ) )
{
setUpConsoleLogging ( ) ;
if ( ! s - > isSet ( " verbose " ) & & ! s - > isSet ( " logfile " ) ) {
logger . setLogLevel ( log4cplus : : FATAL_LOG_LEVEL ) ;
} else if ( ! s - > isSet ( " verbose " ) ) {
logger . removeAppender ( " mainConsoleAppender " ) ;
setUpFileLogging ( ) ;
} else if ( ! s - > isSet ( " logfile " ) ) {
LOG4CPLUS_INFO ( logger , " Enable verbose mode, log output gets printed to console. " ) ;
} else {
setUpFileLogging ( ) ;
LOG4CPLUS_INFO ( logger , " Enable verbose mode, log output gets printed to console. " ) ;
}
mrmc : : parser : : TraParser traparser ( s - > getString ( " trafile " ) . c_str ( ) ) ;
return true ;
}
/*!
* Function to perform some cleanup .
*/
void cleanUp ( ) {
if ( mrmc : : settings : : instance ( ) ! = nullptr ) {
delete mrmc : : settings : : instance ( ) ;
}
}
/*!
* Simple testing procedure .
*/
void testChecking ( ) {
mrmc : : settings : : Settings * s = mrmc : : settings : : instance ( ) ;
mrmc : : parser : : TraParser traparser ( s - > getString ( " trafile " ) . c_str ( ) ) ;
mrmc : : parser : : LabParser labparser ( traparser . getMatrix ( ) - > getRowCount ( ) , s - > getString ( " labfile " ) . c_str ( ) ) ;
mrmc : : models : : Dtmc < double > dtmc ( traparser . getMatrix ( ) , labparser . getLabeling ( ) ) ;
dtmc . printModelInformationToStream ( std : : cout ) ;
if ( s ! = nullptr ) {
delete s ;
mrmc : : formula : : Ap < double > * trueFormula = new mrmc : : formula : : Ap < double > ( " true " ) ;
mrmc : : formula : : Ap < double > * observe0Greater1Formula = new mrmc : : formula : : Ap < double > ( " observe0Greater1 " ) ;
mrmc : : formula : : Until < double > * untilFormula = new mrmc : : formula : : Until < double > ( trueFormula , observe0Greater1Formula ) ;
mrmc : : formula : : ProbabilisticNoBoundsOperator < double > * probFormula = new mrmc : : formula : : ProbabilisticNoBoundsOperator < double > ( * untilFormula ) ;
mrmc : : modelChecker : : GmmxxDtmcPrctlModelChecker < double > * mc = new mrmc : : modelChecker : : GmmxxDtmcPrctlModelChecker < double > ( dtmc ) ;
mc - > check ( * probFormula ) ;
delete mc ;
delete probFormula ;
}
/*!
* Main entry point .
*/
int main ( const int argc , const char * argv [ ] ) {
initializeLogger ( ) ;
if ( ! parseOptions ( argc , argv ) ) {
return 0 ;
}
LOG4CPLUS_INFO ( logger , " Nothing more to do, exiting. " ) ;
printHeader ( argc , argv ) ;
testChecking ( ) ;
cleanUp ( ) ;
return 0 ;
}
dehnert
12 years ago