/* Copyright (c) 2012-2014 Artur Meski */ #include "reactics.hh" int main(int argc, char **argv) { rsin_driver driver; Options *opts = new Options; driver.setOptions(opts); bool show_reactions = false; bool rstl_model_checking = false; bool reach_states = false; bool reach_states_succ = false; bool export_to_ispl = false; bool export_to_xml = false; bool bmc = true; bool benchmarking = false; bool dump_help_message = false; bool print_parsed_sys = false; std::string property_name = "default"; static struct option long_options[] = { {"trace-parsing", no_argument, 0, 0 }, {"trace-scanning", no_argument, 0, 0 }, {0, 0, 0, 0 } }; int c; int option_index = 0; while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheyEG", long_options, &option_index)) != -1) { switch (c) { case 0: printf("option %s", long_options[option_index].name); if (optarg) { printf(" with arg %s", optarg); } printf("\n"); if (strcmp(long_options[option_index].name, "trace-parsing")) { driver.trace_parsing = true; } else if (strcmp(long_options[option_index].name, "trace-scanning")) { driver.trace_scanning = true; } break; case 'e': export_to_ispl = true; break; case 'y': export_to_xml = true; break; //case 'b': // printf("-b with %s\n", optarg); // break; case 'b': bmc = false; break; case 'p': opts->show_progress = true; break; case 'P': print_parsed_sys = true; break; case 'r': show_reactions = true; break; case 'c': rstl_model_checking = true; property_name = optarg; break; case 'm': opts->measure = true; break; case 'B': benchmarking = true; opts->measure = true; break; case 's': reach_states = true; break; case 't': reach_states_succ = true; break; case 'v': opts->verbose++; break; case 'E': opts->reorder_reach = false; opts->reorder_trans = false; break; case 'G': opts->part_tr_rel = false; break; case 'X': opts->backend_mode = true; break; case 'h': dump_help_message = true; break; default: dump_help_message = true; break; } } std::string inputfile; if (optind < argc) { inputfile = argv[optind]; } else if (!dump_help_message) { cout << "Missing input file" << endl; dump_help_message = true; } if (dump_help_message) { print_help(std::string(argv[0])); return 100; } if (!(reach_states || reach_states_succ || rstl_model_checking || show_reactions || print_parsed_sys || export_to_ispl || export_to_xml)) { FERROR("No task specified: -c, -P, -r, -s, or -e needs to be used"); } if (opts->verbose > 0) { cout << "Verbose level: " << opts->verbose << endl; } VERB("Parsing " << inputfile); if (driver.parse(inputfile)) { FERROR("Parse error"); } // // Here we retrieve the reaction system from the parser // // We decide which RS will be used at the parser level. // This decision depends on whether we use concentrations, // context automaton, etc. // auto rs = *driver.getReactionSystem(); bool result = true; rs.setOptions(opts); // these need to be passed to the driver if (show_reactions) { rs.showReactions(); } if (print_parsed_sys) { rs.printSystem(); } if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl || export_to_xml) { SymRS srs(&rs, opts); ModelChecker mc(&srs, opts); if (reach_states) { mc.printReach(); } if (reach_states_succ) { mc.printReachWithSucc(); } if (export_to_ispl) { RSExporter exp(&rs, &driver); exp.exportToISPL(); } if (export_to_xml) { RSExporter exp(&rs, &driver); exp.exportToXML(); } if (rstl_model_checking) { if (bmc) { cout << "Using BDD-based Bounded Model Checking" << endl; result = mc.checkRSCTLK(driver.getFormRSCTLK(property_name)); } else { result = mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name)); } } } if (opts->measure) { cout << endl << std::setprecision(4) << "Encoding time: " << opts->enc_time << " sec" << endl << "Verification time: " << opts->ver_time << " sec" << endl << "Encoding memory: " << opts->enc_mem << " MB" << endl << "Memory (total): " << opts->ver_mem << " MB" << endl << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl; if (benchmarking) { cout << std::setprecision(4) << "STAT; " << opts->enc_time << " ; " << opts->ver_time << " ; " << opts->enc_mem << " ; " << opts->ver_mem << " ; " << opts->enc_time + opts->ver_time << endl; } } delete opts; int ret_val; if (result) { ret_val = 0; } else { ret_val = 1; } return ret_val; } void print_help(std::string path_str) { cout << endl << " ------------------------------------------------" << endl << " -- ReactICS -- Reaction Systems Model Checker --" << endl << " ------------------------------------------------" << endl << endl << " Version: " << VERSION << endl << " Contact: " << AUTHOR << endl << endl #ifndef PUBLIC_RELEASE << " ###################################" << endl << " THIS IS A PRIVATE VERSION OF RSMC " << endl << " PLEASE, DO NOT DISTRIBUTE " << endl << " ###################################" << endl << endl #endif << " Usage: " << path_str << " [options] " << endl << endl << " TASKS:" << endl << " -c form -- perform RSCTLK model checking (form: formula identifier)" << endl //<< " -f K -- generate SMT input for the depth K" << endl << " -P -- print parsed system" << endl << " -r -- print reactions" << endl << " -s -- print all the reachable states" << endl << " -t -- print all the reachable states with their successors" << endl << endl << " OTHER:" << endl << " -b -- disable bounded model checking (BMC) heuristic" << endl << " -v -- verbose (use more than once to increase verbosity)" << endl << " -p -- show progress (where possible)" << endl << " -X -- backend mode (makes output parsing easier)" << endl << " -y -- export to XML (for GUI tool)" << endl << endl << " Optimisations:" << endl << " -E -- disable auto-reordering optimisation of BDDs" << endl << " -G -- disable partitioned transition relation optimisation" << endl << endl << " Benchmarking options:" << endl << " -m -- measure and display time and memory usage" << endl << " -B -- display an easy to parse summary (enables -m)" << endl << " -e -- exports to ISPL (MCMAS input format)" << endl << endl; } /** EOF **/