diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 1ab96f9c9..f387eefba 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,4 +1,12 @@ -2003-07-13 Alexandre Duret-Lutz +2003-07-29 Alexandre Duret-Lutz + + * src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT + and SIGQUIT. + * src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise. + * src/main.cc (main): Do not intercept SIGINT in + non-interactive runs. + +2003-07-13 Alexandre Duret-Lutz * doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo versions are stricter on this. diff --git a/lbtt/src/Configuration.cc b/lbtt/src/Configuration.cc index 8392ca33f..7ea1f6f08 100644 --- a/lbtt/src/Configuration.cc +++ b/lbtt/src/Configuration.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -97,7 +97,7 @@ const struct Configuration::IntegerRange Configuration::STATESPACE_SIZE_RANGE const struct Configuration::IntegerRange Configuration::STATESPACE_MAX_SIZE_RANGE = {1, LONG_MAX, "minimum state space size exceeds the maximum state space " - "size"}; + "size"}; @@ -312,7 +312,7 @@ void Configuration::read(int argc, char* argv[]) { long int interval_length = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(interval_length, GENERATION_RANGE, false); if (opttype == OPT_FORMULACHANGEINTERVAL) @@ -426,14 +426,14 @@ void Configuration::read(int argc, char* argv[]) { long int number_of_rounds = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(number_of_rounds, ROUND_COUNT_RANGE, false); global_options.number_of_rounds = number_of_rounds; locked_options.insert(make_pair(CFG_GLOBALOPTIONS, CFG_ROUNDS)); } break; - + case OPT_SHOWCONFIG : print_config = true; break; @@ -446,7 +446,7 @@ void Configuration::read(int argc, char* argv[]) { long int rounds_to_skip = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(rounds_to_skip, ROUND_COUNT_RANGE, false); global_options.init_skip = rounds_to_skip; } @@ -465,7 +465,7 @@ void Configuration::read(int argc, char* argv[]) { long int verbosity = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(verbosity, VERBOSITY_RANGE, false); global_options.verbosity = verbosity; locked_options.insert(make_pair(CFG_GLOBALOPTIONS, CFG_VERBOSITY)); @@ -475,17 +475,17 @@ void Configuration::read(int argc, char* argv[]) case OPT_VERSION : cout << "lbtt " PACKAGE_VERSION "\n" - "lbtt is free software; you may change and " - "redistribute it under the terms of\n" - "the GNU General Public License. lbtt comes with " - "NO WARRANTY. See the file\n" - "COPYING for details.\n"; + "lbtt is free software; you may change and " + "redistribute it under the terms of\n" + "the GNU General Public License. lbtt comes with " + "NO WARRANTY. See the file\n" + "COPYING for details.\n"; exit(0); break; case OPT_ABBREVIATEDOPERATORS : case OPT_NOABBREVIATEDOPERATORS : - formula_options.allow_abbreviated_operators + formula_options.allow_abbreviated_operators = (opttype == OPT_ABBREVIATEDOPERATORS); locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_ABBREVIATEDOPERATORS)); @@ -512,7 +512,7 @@ void Configuration::read(int argc, char* argv[]) { long int priority = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(priority, PRIORITY_RANGE, false); @@ -546,7 +546,7 @@ void Configuration::read(int argc, char* argv[]) case OPT_FALSEPRIORITY : symbol = ::Ltl::LTL_FALSE; - locked_options.insert(make_pair(CFG_FORMULAOPTIONS, + locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_FALSEPRIORITY)); break; @@ -594,7 +594,7 @@ void Configuration::read(int argc, char* argv[]) case OPT_RELEASEPRIORITY : symbol = ::Ltl::LTL_V; - locked_options.insert(make_pair(CFG_FORMULAOPTIONS, + locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_RELEASEPRIORITY)); break; @@ -658,13 +658,13 @@ void Configuration::read(int argc, char* argv[]) locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_OUTPUTMODE)); break; - + case OPT_FORMULAPROPOSITIONS : case OPT_STATESPACEPROPOSITIONS : { long int num_propositions = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(num_propositions, PROPOSITION_COUNT_RANGE, false); @@ -710,7 +710,7 @@ void Configuration::read(int argc, char* argv[]) { long int size = parseCommandLineInteger - (command_line_options[option_index].name, value); + (command_line_options[option_index].name, value); checkIntegerRange(size, min_size_range, false); @@ -797,7 +797,7 @@ void Configuration::read(int argc, char* argv[]) locked_options.insert(make_pair(CFG_STATESPACEOPTIONS, CFG_GENERATEMODE)); break; - + case OPT_RANDOMCONNECTEDGRAPH : global_options.statespace_generation_mode = RANDOMCONNECTEDGRAPH; locked_options.insert(make_pair(CFG_STATESPACEOPTIONS, @@ -840,15 +840,15 @@ void Configuration::read(int argc, char* argv[]) if (error) throw ConfigurationException ("", string("unrecognized argument (`") + optarg - + "') for option `--" - + command_line_options[option_index].name + "'"); + + "') for option `--" + + command_line_options[option_index].name + "'"); } while (opttype != -1); if (optind != argc) throw ConfigurationException ("", string("unrecognized command line option `") - + argv[optind] + "'"); + + argv[optind] + "'"); /* * Read the configuration file. @@ -857,8 +857,8 @@ void Configuration::read(int argc, char* argv[]) FILE* configuration_file = fopen(global_options.cfg_filename.c_str(), "r"); if (configuration_file == NULL) throw ConfigurationException - ("", "error opening configuration file `" - + global_options.cfg_filename + "'"); + ("", "error opening configuration file `" + + global_options.cfg_filename + "'"); try { @@ -903,7 +903,7 @@ void Configuration::read(int argc, char* argv[]) } for (set, - ALLOC(unsigned long int) >::const_iterator + ALLOC(unsigned long int) >::const_iterator id = algorithm_id_set.begin(); id != algorithm_id_set.end(); ++id) @@ -933,8 +933,8 @@ void Configuration::read(int argc, char* argv[]) if (global_options.number_of_rounds <= global_options.init_skip) throw ConfigurationException - ("", "the argument for `--skip' must be less than the total " - "number of test rounds"); + ("", "the argument for `--skip' must be less than the total " + "number of test rounds"); /* * Check that there is at least one algorithm available for use. @@ -942,7 +942,7 @@ void Configuration::read(int argc, char* argv[]) if (algorithms.empty()) throw ConfigurationException - ("", "no implementations defined in the configuration file"); + ("", "no implementations defined in the configuration file"); /* * The case where the number of available variables for propositional @@ -962,7 +962,7 @@ void Configuration::read(int argc, char* argv[]) && formula_options.symbol_priority[::Ltl::LTL_TRUE] == 0 && formula_options.symbol_priority[::Ltl::LTL_FALSE] == 0) throw ConfigurationException("", "at least one atomic symbol must have " - "nonzero priority"); + "nonzero priority"); /* * If the operators ->, <->, xor, <>, [], W and M are disallowed, set their @@ -997,15 +997,15 @@ void Configuration::read(int argc, char* argv[]) it->second = formula_options.default_operator_priority; if (it->second > 0 && !unary_operator_allowed) - unary_operator_allowed = - (it->first == ::Ltl::LTL_NEGATION || it->first == ::Ltl::LTL_NEXT + unary_operator_allowed = + (it->first == ::Ltl::LTL_NEGATION || it->first == ::Ltl::LTL_NEXT || it->first == ::Ltl::LTL_FINALLY - || it->first == ::Ltl::LTL_GLOBALLY); + || it->first == ::Ltl::LTL_GLOBALLY); } if (!unary_operator_allowed) throw ConfigurationException("", "at least one unary operator must have " - "a nonzero priority"); + "a nonzero priority"); /* * Initialize the random formula generator with priorities for the LTL @@ -1024,49 +1024,49 @@ void Configuration::read(int argc, char* argv[]) { switch (it->first) { - case ::Ltl::LTL_ATOM : - case ::Ltl::LTL_TRUE : - case ::Ltl::LTL_FALSE : - formula_options.formula_generator.useSymbol(it->first, it->second); - break; + case ::Ltl::LTL_ATOM : + case ::Ltl::LTL_TRUE : + case ::Ltl::LTL_FALSE : + formula_options.formula_generator.useSymbol(it->first, it->second); + break; - case ::Ltl::LTL_NEGATION : - formula_options.formula_generator.useShortOperator + case ::Ltl::LTL_NEGATION : + formula_options.formula_generator.useShortOperator (it->first, it->second); total_short_unary_priority += it->second; - if (formula_options.generate_mode != NNF) + if (formula_options.generate_mode != NNF) { - formula_options.formula_generator.useLongOperator + formula_options.formula_generator.useLongOperator (it->first, it->second); total_long_unary_priority += it->second; } - break; + break; - case ::Ltl::LTL_NEXT : - case ::Ltl::LTL_FINALLY : - case ::Ltl::LTL_GLOBALLY : - formula_options.formula_generator.useShortOperator + case ::Ltl::LTL_NEXT : + case ::Ltl::LTL_FINALLY : + case ::Ltl::LTL_GLOBALLY : + formula_options.formula_generator.useShortOperator (it->first, it->second); total_short_unary_priority += it->second; - formula_options.formula_generator.useLongOperator + formula_options.formula_generator.useLongOperator (it->first, it->second); total_long_unary_priority += it->second; - break; + break; - case ::Ltl::LTL_CONJUNCTION : - case ::Ltl::LTL_DISJUNCTION : - case ::Ltl::LTL_IMPLICATION : - case ::Ltl::LTL_EQUIVALENCE : - case ::Ltl::LTL_XOR : - case ::Ltl::LTL_UNTIL : - case ::Ltl::LTL_V : - case ::Ltl::LTL_WEAK_UNTIL : - case ::Ltl::LTL_STRONG_RELEASE : - case ::Ltl::LTL_BEFORE : - formula_options.formula_generator.useLongOperator + case ::Ltl::LTL_CONJUNCTION : + case ::Ltl::LTL_DISJUNCTION : + case ::Ltl::LTL_IMPLICATION : + case ::Ltl::LTL_EQUIVALENCE : + case ::Ltl::LTL_XOR : + case ::Ltl::LTL_UNTIL : + case ::Ltl::LTL_V : + case ::Ltl::LTL_WEAK_UNTIL : + case ::Ltl::LTL_STRONG_RELEASE : + case ::Ltl::LTL_BEFORE : + formula_options.formula_generator.useLongOperator (it->first, it->second); total_binary_priority += it->second; - break; + break; } } } @@ -1091,9 +1091,9 @@ void Configuration::read(int argc, char* argv[]) ++op) { if (op->second > 0) - { + { switch (op->first) - { + { case ::Ltl::LTL_ATOM : case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : @@ -1106,18 +1106,18 @@ void Configuration::read(int argc, char* argv[]) = formula_options.formula_generator.size; s <= formula_options.formula_generator.max_size; s++) - { + { if (k >= s) continue; probability += operatorProbability - (op->first, k, s, + (op->first, k, s, total_short_unary_priority, total_long_unary_priority, total_binary_priority, result_cache); } probability /= static_cast - (formula_options.formula_generator.max_size + (formula_options.formula_generator.max_size - formula_options.formula_generator.size + 1); @@ -1158,18 +1158,18 @@ void Configuration::print(ostream& stream, int indent) const Exceptional_ostream estream(&stream, ios::badbit | ios::failbit); estream << string(indent, ' ') + "Program configuration:\n" - + string(indent, ' ') + string(22, '-') + "\n\n" - + string(indent + 2, ' ') - + toString(global_options.number_of_rounds) - + " test round" - + (global_options.number_of_rounds > 1 ? "s" : ""); + + string(indent, ' ') + string(22, '-') + "\n\n" + + string(indent + 2, ' ') + + toString(global_options.number_of_rounds) + + " test round" + + (global_options.number_of_rounds > 1 ? "s" : ""); if (global_options.init_skip > 0) estream << " (of which the first " - + (global_options.init_skip > 1 + + (global_options.init_skip > 1 ? toString(global_options.init_skip) + " rounds " : string("")) - + "will be skipped)"; + + "will be skipped)"; estream << ".\n" + string(indent + 2, ' '); @@ -1181,20 +1181,20 @@ void Configuration::print(ostream& stream, int indent) const estream << "Running in batch mode.\n"; estream << string(indent + 2, ' ') - + "Using " - + (global_options.product_mode == GLOBAL + + "Using " + + (global_options.product_mode == GLOBAL ? "global" : "local") - + " model checking for tests.\n"; + + " model checking for tests.\n"; if (!global_options.transcript_filename.empty()) estream << string(indent + 2, ' ') + "Writing error log to `" - + global_options.transcript_filename + "'.\n"; + + global_options.transcript_filename + "'.\n"; estream << '\n' + string(indent + 2, ' ') + "Implementations:\n"; vector::size_type algorithm_number = 0; - + for (vector ::const_iterator a = algorithms.begin(); a != algorithms.end(); @@ -1218,19 +1218,19 @@ void Configuration::print(ostream& stream, int indent) const estream << "Enabled tests:\n"; if (global_options.do_comp_test) estream << string(indent + 4, ' ') + - "Model checking result cross-comparison test\n"; + "Model checking result cross-comparison test\n"; if (global_options.do_cons_test) estream << string(indent + 4, ' ') + - "Model checking result consistency check\n"; + "Model checking result consistency check\n"; if (global_options.do_intr_test) estream << string(indent + 4, ' ') + - "Büchi automata intersection emptiness check\n"; + "Büchi automata intersection emptiness check\n"; } else estream << "All automata correctness tests disabled.\n"; estream << '\n' + string(indent + 2, ' ') + "Random state spaces:\n" - + string(indent + 4, ' '); + + string(indent + 4, ' '); switch (global_options.statespace_generation_mode) { @@ -1257,15 +1257,15 @@ void Configuration::print(ostream& stream, int indent) const estream << "..." + toString(statespace_generator.max_size); estream << string(" state") - + (statespace_generator.max_size == 1 ? "" : "s") + ", " - + toString(statespace_generator.atoms_per_state) - + " atomic proposition" - + (statespace_generator.atoms_per_state == 1 ? "" : "s") - + ")\n" + string(indent + 4, ' '); + + (statespace_generator.max_size == 1 ? "" : "s") + ", " + + toString(statespace_generator.atoms_per_state) + + " atomic proposition" + + (statespace_generator.atoms_per_state == 1 ? "" : "s") + + ")\n" + string(indent + 4, ' '); if (global_options.statespace_change_interval == 0 || global_options.statespace_change_interval - >= global_options.number_of_rounds) + >= global_options.number_of_rounds) estream << "Using a fixed state space.\n" + string(indent + 4, ' '); else { @@ -1297,16 +1297,16 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.statespace_generation_mode != ENUMERATEDPATH) { estream << "Random seed: " - + toString(global_options.statespace_random_seed) - + '\n' + string(indent + 4, ' '); + + toString(global_options.statespace_random_seed) + + '\n' + string(indent + 4, ' '); if (global_options.statespace_generation_mode & GRAPH) estream << "Random edge probability: " - + toString(statespace_generator.edge_probability) - + '\n' + string(indent + 4, ' '); + + toString(statespace_generator.edge_probability) + + '\n' + string(indent + 4, ' '); estream << "Propositional truth probability: " - + toString(statespace_generator.truth_probability) + + toString(statespace_generator.truth_probability) + "\n"; } @@ -1315,32 +1315,32 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.formula_input_filename.empty()) { estream << "Random LTL formulas:\n" + string(indent + 4, ' ') - + toString(formula_options.formula_generator.size); + + toString(formula_options.formula_generator.size); if (formula_options.formula_generator.max_size - != formula_options.formula_generator.size) + != formula_options.formula_generator.size) estream << "..." - + toString(formula_options.formula_generator.max_size); + + toString(formula_options.formula_generator.max_size); estream << string(" parse tree node") - + (formula_options.formula_generator.max_size == 1 ? "" : "s") - + ", " + + (formula_options.formula_generator.max_size == 1 ? "" : "s") + + ", " + toString(formula_options.formula_generator. number_of_available_variables) + " atomic proposition" - + (formula_options.formula_generator. + + (formula_options.formula_generator. number_of_available_variables == 1 ? "" : "s"); } else estream << "Reading LTL formulas from `" - + global_options.formula_input_filename - + "'."; + + global_options.formula_input_filename + + "'."; estream << '\n' + string(indent + 4, ' '); if (global_options.formula_change_interval == 0 || global_options.formula_change_interval - >= global_options.number_of_rounds) + >= global_options.number_of_rounds) estream << "Using a fixed LTL formula."; else { @@ -1357,7 +1357,7 @@ void Configuration::print(ostream& stream, int indent) const || global_options.formula_change_interval % 100 >= 20) { switch (global_options.formula_change_interval % 10) - { + { case 1 : estream << "st"; break; case 2 : estream << "nd"; break; case 3 : estream << "rd"; break; @@ -1378,18 +1378,18 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.formula_input_filename.empty() && formula_options.generate_mode == NNF) estream << string(indent + 4, ' ') - + "Formulas will be generated into negation normal form.\n"; + + "Formulas will be generated into negation normal form.\n"; else if (formula_options.output_mode == NNF) estream << string(indent + 4, ' ') - + "Formulas will be converted into negation normal form.\n"; + + "Formulas will be converted into negation normal form.\n"; if (global_options.formula_input_filename.empty()) { estream << string(indent + 4, ' ') + "Random seed: " - + toString(global_options.formula_random_seed) - + '\n' + string(indent + 4, ' ') - + "Atomic symbols in use (priority):\n" - + string(indent + 6, ' '); + + toString(global_options.formula_random_seed) + + '\n' + string(indent + 4, ' ') + + "Atomic symbols in use (priority):\n" + + string(indent + 6, ' '); bool first_printed = false; @@ -1410,13 +1410,13 @@ void Configuration::print(ostream& stream, int indent) const switch (op->first) { - case ::Ltl::LTL_ATOM : + case ::Ltl::LTL_ATOM : estream << "propositions"; break; - case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : + case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : estream << ::Ltl::infixSymbol(op->first); break; - default : + default : break; } @@ -1425,7 +1425,7 @@ void Configuration::print(ostream& stream, int indent) const estream << '\n' << string(indent + 4, ' ') - + "Operators used for random LTL formula generation:"; + + "Operators used for random LTL formula generation:"; string operator_name_string; string operator_priority_string; @@ -1452,7 +1452,7 @@ void Configuration::print(ostream& stream, int indent) const { operator_name_string = string(11, ' ') + operator_name_string; operator_priority_string = string(11, ' ') - + operator_priority_string; + + operator_priority_string; operator_distribution_string = string(indent + 6, ' ') + "occurrences/formula "; } @@ -1478,7 +1478,7 @@ void Configuration::print(ostream& stream, int indent) const == max_operators_per_line - 1) { estream << '\n' + operator_name_string + '\n' - + operator_priority_string + '\n'; + + operator_priority_string + '\n'; if (!formula_options.symbol_distribution.empty()) estream << operator_distribution_string + '\n'; @@ -1498,7 +1498,7 @@ void Configuration::print(ostream& stream, int indent) const if (number_of_operators_printed % max_operators_per_line != 0) { estream << '\n' + operator_name_string + '\n' + operator_priority_string - + '\n'; + + '\n'; if (!formula_options.symbol_distribution.empty()) estream << operator_distribution_string + '\n'; @@ -1512,7 +1512,7 @@ void Configuration::print(ostream& stream, int indent) const /* ========================================================================= */ string Configuration::algorithmString (vector::size_type + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) const /* ---------------------------------------------------------------------------- * @@ -1528,7 +1528,7 @@ string Configuration::algorithmString using namespace ::StringUtil; return toString(algorithm_id) + ": `" + *(algorithms[algorithm_id].name) - + '\''; + + '\''; } /* ========================================================================= */ @@ -1544,184 +1544,184 @@ void Configuration::showCommandLineHelp(const char* program_name) * ------------------------------------------------------------------------- */ { cout << string("Usage: ") + program_name - + " [OPTION]...\n\nGeneral options:\n" - " --[no]comparisontest Enable or disable the model " - "checking result\n" - " cross-comparison test\n" - " --configfile=FILE Read configuration from FILE\n" - " --[no]consistencytest Enable or disable the model " - "checking result\n" - " consistency test\n" - " --disable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]\n" - " Exclude implementation(s) from " - "tests\n" - " --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n" - " Include implementation(s) into " - "tests\n" - " --formulafile=FILE Read LTL formulas from FILE\n" - " --globalmodelcheck Use global model checking in " - "tests\n" - " (equivalent to " - "`--modelcheck=global')\n" - " -h, --help Show this help and exit\n" - " --interactive=MODE Set the interactivity mode " - "(`always', `onerror', \n" - " `never')\n" - " --[no]intersectiontest Enable or disable the Büchi " - "automata\n" - " intersection emptiness test\n" - " --localmodelcheck Use local model checking in tests" - "\n" - " (equivalent to " - "`--modelcheck=local')\n" - " --logfile=FILE Write error log to FILE\n" - " --modelcheck=MODE Set model checking mode " - "(`global' or `local')\n" - " --nopause Do not pause between test rounds " - "(equivalent to\n" - " `--interactive=never')\n" - " --pause Pause unconditionally after every " - "test round\n" - " (equivalent to " - "`--interactive=always')\n" - " --pauseonerror Pause between test rounds only in " - "case of an\n" - " error (equivalent to " - "`--interactive=onerror')\n" - " --profile Disable all automata correctness " - "tests\n" - " --quiet, --silent Run all tests silently without " - "interruption\n" - " --rounds=NUMBER-OF-ROUNDS Set number of test rounds (1-)\n" - " --showconfig Display current configuration and " - "exit\n" - " --showoperatordistribution Display probability distribution " - "for LTL formula\n" - " operators\n" - " --skip=NUMBER-OF-ROUNDS Set number of test rounds to skip " - "before\n" - " starting tests\n" - " --verbosity=INTEGER Set the verbosity of output (0-5)\n" - " --version Display program version and exit" - "\n\n" - "LTL formula generation options:\n" - " --[no]abbreviatedoperators Allow or disallow operators ->, " - "<->, xor, <>,\n" - " [], u, w in the generated " - "formulas\n" - " --andpriority=INTEGER Set priority for the /\\ operator\n" - " --beforepriority=INTEGER Set priority for the Before " - "operator\n" - " --defaultoperatorpriority=INTEGER\n" - " Set default priority for operators" - "\n" - " --equivalencepriority=INTEGER\n" - " Set priority for the <-> operator\n" - " --falsepriority=INTEGER Set priority for the constant " - "`false'\n" - " --finallypriority=INTEGER Set priority for the <> operator\n" - " --formulachangeinterval=NUMBER-OF-ROUNDS\n" - " Set formula generation interval in " - "test rounds\n" - " (0-)\n" - " --formulageneratemode=MODE Set formula generation mode " - "(`normal', `nnf')\n" - " --formulaoutputmode=MODE Set formula output mode (`normal', " - "`nnf')\n" - " --formulapropositions=NUMBER-OF-PROPOSITIONS\n" - " Set maximum number of atomic " - "propositions in\n" - " generated formulas (0-)\n" - " --formularandomseed=INTEGER Set random seed for the formula " - "generation\n" - " algorithm\n" - " --formulasize=SIZE,\n" - " --formulasize=MIN-SIZE...MAX-SIZE\n" - " Set size of random LTL formulas " - "(1-)\n" - " --[no]generatennf Force or prevent generating LTL " - "formulas in\n" - " negation normal form\n" - " --globallypriority=INTEGER Set priority for the [] operator\n" - " --implicationpriority=INTEGER\n" - " Set priority for the -> operator\n" - " --nextpriority=INTEGER Set priority for the Next operator" - "\n" - " --notpriority=INTEGER Set priority for the negation " - "operator\n" - " --orpriority=INTEGER Set priority for the \\/ operator\n" - " --[no]outputnnf Enable or disable formula " - "translation to\n" - " negation normal form before " - "invoking the\n" - " translators\n" - " --propositionpriority=INTEGER\n" - " Set priority for atomic " - "propositions\n" - " --releasepriority=INTEGER Set priority for the (Weak) Release" - " operator\n" - " --strongreleasepriority=INTEGER\n" - " Set priority for the Strong " - "Release operator\n" - " --truepriority=INTEGER Set priority for the constant " - "`true'\n" - " --untilpriority=INTEGER Set priority for the (Strong) Until" - " operator\n" - " --weakuntilpriority=INTEGER\n" - " Set priority for the Weak Until " - "operator\n" - " --xorpriority=INTEGER Set priority for the xor " - "operator\n\n" - "State space generation options:\n" - " --edgeprobability=PROBABILITY\n" - " Set random edge probability for " - "state spaces\n" - " (0.0--1.0)\n" - " --enumeratedpath Enumerate all paths of a given " - "size and a given\n" - " number of propositions per state " - "(equivalent to\n" - " `--statespacegeneratemode=" - "enumeratedpath')\n" - " --randomconnectedgraph Generate connected graphs as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randomconnectedgraph')\n" - " --randomgraph Generate random graphs as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randomgraph')\n" - " --randompath Generate random paths as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randompath')\n" - " --statespacechangeinterval=NUMBER-OF-ROUNDS\n" - " Set state space generation " - "interval in test\n" - " rounds (0-)\n" - " --statespacegeneratemode=MODE\n" - " Set state space generation mode\n" - " (`randomconnectedgraph', " - "`randomgraph',\n" - " `randompath', `enumeratedpath')\n" - " --statespacepropositions=NUMBER-OF-PROPOSITIONS\n" - " Set number of propositions per " - "state (0-)\n" - " --statespacerandomseed=INTEGER\n" - " Set random seed for the state " - "space generation\n" - " algorithm\n" - " --statespacesize=SIZE,\n" - " --statespacesize=MIN-SIZE...MAX-SIZE\n" - " Set size of generated state spaces " - "(1-)\n" - " --truthprobability=PROBABILITY\n" - " Set truth probability of " - "propositions (0.0--1.0)\n\n" - "Report bugs to .\n"; + + " [OPTION]...\n\nGeneral options:\n" + " --[no]comparisontest Enable or disable the model " + "checking result\n" + " cross-comparison test\n" + " --configfile=FILE Read configuration from FILE\n" + " --[no]consistencytest Enable or disable the model " + "checking result\n" + " consistency test\n" + " --disable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]\n" + " Exclude implementation(s) from " + "tests\n" + " --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n" + " Include implementation(s) into " + "tests\n" + " --formulafile=FILE Read LTL formulas from FILE\n" + " --globalmodelcheck Use global model checking in " + "tests\n" + " (equivalent to " + "`--modelcheck=global')\n" + " -h, --help Show this help and exit\n" + " --interactive=MODE Set the interactivity mode " + "(`always', `onerror', \n" + " `never')\n" + " --[no]intersectiontest Enable or disable the Büchi " + "automata\n" + " intersection emptiness test\n" + " --localmodelcheck Use local model checking in tests" + "\n" + " (equivalent to " + "`--modelcheck=local')\n" + " --logfile=FILE Write error log to FILE\n" + " --modelcheck=MODE Set model checking mode " + "(`global' or `local')\n" + " --nopause Do not pause between test rounds " + "(equivalent to\n" + " `--interactive=never')\n" + " --pause Pause unconditionally after every " + "test round\n" + " (equivalent to " + "`--interactive=always')\n" + " --pauseonerror Pause between test rounds only in " + "case of an\n" + " error (equivalent to " + "`--interactive=onerror')\n" + " --profile Disable all automata correctness " + "tests\n" + " --quiet, --silent Run all tests silently without " + "interruption\n" + " --rounds=NUMBER-OF-ROUNDS Set number of test rounds (1-)\n" + " --showconfig Display current configuration and " + "exit\n" + " --showoperatordistribution Display probability distribution " + "for LTL formula\n" + " operators\n" + " --skip=NUMBER-OF-ROUNDS Set number of test rounds to skip " + "before\n" + " starting tests\n" + " --verbosity=INTEGER Set the verbosity of output (0-5)\n" + " --version Display program version and exit" + "\n\n" + "LTL formula generation options:\n" + " --[no]abbreviatedoperators Allow or disallow operators ->, " + "<->, xor, <>,\n" + " [], u, w in the generated " + "formulas\n" + " --andpriority=INTEGER Set priority for the /\\ operator\n" + " --beforepriority=INTEGER Set priority for the Before " + "operator\n" + " --defaultoperatorpriority=INTEGER\n" + " Set default priority for operators" + "\n" + " --equivalencepriority=INTEGER\n" + " Set priority for the <-> operator\n" + " --falsepriority=INTEGER Set priority for the constant " + "`false'\n" + " --finallypriority=INTEGER Set priority for the <> operator\n" + " --formulachangeinterval=NUMBER-OF-ROUNDS\n" + " Set formula generation interval in " + "test rounds\n" + " (0-)\n" + " --formulageneratemode=MODE Set formula generation mode " + "(`normal', `nnf')\n" + " --formulaoutputmode=MODE Set formula output mode (`normal', " + "`nnf')\n" + " --formulapropositions=NUMBER-OF-PROPOSITIONS\n" + " Set maximum number of atomic " + "propositions in\n" + " generated formulas (0-)\n" + " --formularandomseed=INTEGER Set random seed for the formula " + "generation\n" + " algorithm\n" + " --formulasize=SIZE,\n" + " --formulasize=MIN-SIZE...MAX-SIZE\n" + " Set size of random LTL formulas " + "(1-)\n" + " --[no]generatennf Force or prevent generating LTL " + "formulas in\n" + " negation normal form\n" + " --globallypriority=INTEGER Set priority for the [] operator\n" + " --implicationpriority=INTEGER\n" + " Set priority for the -> operator\n" + " --nextpriority=INTEGER Set priority for the Next operator" + "\n" + " --notpriority=INTEGER Set priority for the negation " + "operator\n" + " --orpriority=INTEGER Set priority for the \\/ operator\n" + " --[no]outputnnf Enable or disable formula " + "translation to\n" + " negation normal form before " + "invoking the\n" + " translators\n" + " --propositionpriority=INTEGER\n" + " Set priority for atomic " + "propositions\n" + " --releasepriority=INTEGER Set priority for the (Weak) Release" + " operator\n" + " --strongreleasepriority=INTEGER\n" + " Set priority for the Strong " + "Release operator\n" + " --truepriority=INTEGER Set priority for the constant " + "`true'\n" + " --untilpriority=INTEGER Set priority for the (Strong) Until" + " operator\n" + " --weakuntilpriority=INTEGER\n" + " Set priority for the Weak Until " + "operator\n" + " --xorpriority=INTEGER Set priority for the xor " + "operator\n\n" + "State space generation options:\n" + " --edgeprobability=PROBABILITY\n" + " Set random edge probability for " + "state spaces\n" + " (0.0--1.0)\n" + " --enumeratedpath Enumerate all paths of a given " + "size and a given\n" + " number of propositions per state " + "(equivalent to\n" + " `--statespacegeneratemode=" + "enumeratedpath')\n" + " --randomconnectedgraph Generate connected graphs as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randomconnectedgraph')\n" + " --randomgraph Generate random graphs as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randomgraph')\n" + " --randompath Generate random paths as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randompath')\n" + " --statespacechangeinterval=NUMBER-OF-ROUNDS\n" + " Set state space generation " + "interval in test\n" + " rounds (0-)\n" + " --statespacegeneratemode=MODE\n" + " Set state space generation mode\n" + " (`randomconnectedgraph', " + "`randomgraph',\n" + " `randompath', `enumeratedpath')\n" + " --statespacepropositions=NUMBER-OF-PROPOSITIONS\n" + " Set number of propositions per " + "state (0-)\n" + " --statespacerandomseed=INTEGER\n" + " Set random seed for the state " + "space generation\n" + " algorithm\n" + " --statespacesize=SIZE,\n" + " --statespacesize=MIN-SIZE...MAX-SIZE\n" + " Set size of generated state spaces " + "(1-)\n" + " --truthprobability=PROBABILITY\n" + " Set truth probability of " + "propositions (0.0--1.0)\n\n" + "Report bugs to .\n"; } /* ========================================================================= */ @@ -1809,12 +1809,12 @@ long int Configuration::parseCommandLineInteger if (*endptr != '\0' || value.empty()) throw ConfigurationException - ("", "the argument for `--" + option + "' must be a nonnegative " - "integer"); + ("", "the argument for `--" + option + "' must be a nonnegative " + "integer"); if (val == LONG_MIN || val == LONG_MAX) throw ConfigurationException - ("", "the argument for `--" + option + "' is out of range"); + ("", "the argument for `--" + option + "' is out of range"); return val; } @@ -1899,7 +1899,7 @@ double Configuration::operatorProbability { if (arity == 1 && total_short_unary_priority > 0) result = static_cast(priority) - / static_cast(total_short_unary_priority); + / static_cast(total_short_unary_priority); else result = 0.0; } @@ -1931,7 +1931,7 @@ double Configuration::operatorProbability total_long_unary_priority, total_binary_priority, result_cache) - * operatorProbability(op, k - i, n - m - 1, + * operatorProbability(op, k - i, n - m - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1946,7 +1946,7 @@ double Configuration::operatorProbability if (op != ::Ltl::LTL_NEGATION || formula_options.generate_mode != NNF) result += static_cast(priority) - * operatorProbability(op, k - 1, n - 1, + * operatorProbability(op, k - 1, n - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1965,7 +1965,7 @@ double Configuration::operatorProbability total_long_unary_priority, total_binary_priority, result_cache) - * operatorProbability(op, k - 1 - i, n - m - 1, + * operatorProbability(op, k - 1 - i, n - m - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1976,7 +1976,7 @@ double Configuration::operatorProbability } result += static_cast(p1) - * operatorProbability(op, k, n - 1, + * operatorProbability(op, k, n - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, diff --git a/lbtt/src/Configuration.h b/lbtt/src/Configuration.h index 99ad8b49a..a0f4014e5 100644 --- a/lbtt/src/Configuration.h +++ b/lbtt/src/Configuration.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -55,22 +55,22 @@ public: ~Configuration(); /* Destructor. */ void read(int argc, char* argv[]); /* Reads the program - * configuration. + * configuration. */ void print /* Writes the current */ (ostream& stream = cout, int indent = 0) const; /* configuration (in a - * textual form) to a - * stream. + * textual form) to a + * stream. */ struct AlgorithmInformation; /* See below. */ string algorithmString /* Formats the the id */ (vector::size_type/* the name of the */ + ALLOC(AlgorithmInformation) >::size_type/* the name of the */ algorithm_id) const; /* algorithm into a - * string. + * string. */ static void showCommandLineHelp /* Prints the list of */ @@ -79,52 +79,52 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ enum InteractionMode {NEVER, ALWAYS, ONERROR}; /* Enumeration constants - * affecting the behaviour - * of the program as - * regards user control. + * affecting the behaviour + * of the program as + * regards user control. */ enum FormulaMode {NORMAL, NNF}; /* Enumeration constants - * affecting the generation - * and output of random - * formulae. + * affecting the generation + * and output of random + * formulae. */ enum StateSpaceMode {RANDOMGRAPH = 1, /* Enumeration constants */ - RANDOMCONNECTEDGRAPH = 2, /* affecting the */ + RANDOMCONNECTEDGRAPH = 2, /* affecting the */ GRAPH = 3, /* generation of random */ - RANDOMPATH = 4, /* state spaces. */ - ENUMERATEDPATH = 8, - PATH = 12}; + RANDOMPATH = 4, /* state spaces. */ + ENUMERATEDPATH = 8, + PATH = 12}; enum ProductMode {LOCAL, GLOBAL}; /* Enumeration constants - * for controlling the - * scope of synchronous - * products. + * for controlling the + * scope of synchronous + * products. */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ struct AlgorithmInformation /* A structure for storing - * information about a - * particular algorithm - * (name, path to - * executable, command-line - * parameters). + * information about a + * particular algorithm + * (name, path to + * executable, command-line + * parameters). */ { string* name; /* Name of the algorithm. - */ + */ string* path_to_program; /* Path to the executable - * required for running - * the algorithm. + * required for running + * the algorithm. */ string* extra_parameters; /* Additional command-line - * parameters required for - * running the executable. - */ + * parameters required for + * running the executable. + */ bool enabled; /* Determines whether the * algorithm is enabled @@ -136,42 +136,42 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ struct GlobalConfiguration /* A structure for storing - * all the information - * affecting the general - * behaviour of the - * program. + * all the information + * affecting the general + * behaviour of the + * program. */ { int verbosity; /* Determines the verbosity - * of program output (0-5, - * the bigger the value, - * the more information - * will be shown). + * of program output (0-5, + * the bigger the value, + * the more information + * will be shown). */ InteractionMode interactive; /* Controls the behaviour - * of the program as - * regards the ability of - * the user to enter - * commands between test - * rounds. Possible values - * and their meanings are: - * - * NEVER: - * Run all tests without - * interruption. - * ALWAYS: - * Pause after each test - * round to wait for - * user commands. - * ONERROR: - * Try to run the tests - * without interruption. - * However, in case of - * an error, pause and - * wait for user - * commands. - */ + * of the program as + * regards the ability of + * the user to enter + * commands between test + * rounds. Possible values + * and their meanings are: + * + * NEVER: + * Run all tests without + * interruption. + * ALWAYS: + * Pause after each test + * round to wait for + * user commands. + * ONERROR: + * Try to run the tests + * without interruption. + * However, in case of + * an error, pause and + * wait for user + * commands. + */ unsigned long int number_of_rounds; /* Number of test rounds. */ @@ -181,22 +181,22 @@ public: */ unsigned long int statespace_change_interval; /* Determines the frequency - * (in rounds) of how often - * a new state space is - * generated. + * (in rounds) of how often + * a new state space is + * generated. */ - + StateSpaceMode statespace_generation_mode; /* Random state space * generation mode. * Available options are: - * - * RANDOMGRAPH: - * Generate random - * connected graphs as - * state spaces. - * RANDOMPATH: - * Generate paths as - * state spaces, choose + * + * RANDOMGRAPH: + * Generate random + * connected graphs as + * state spaces. + * RANDOMPATH: + * Generate paths as + * state spaces, choose * the loop and the * truth assignments for * atomic propositions @@ -207,47 +207,47 @@ public: * enumerating all * possible paths of a * given length. - */ + */ unsigned long int formula_change_interval; /* Determines the frequency - * (in rounds) of how often - * a new formula is - * generated. + * (in rounds) of how often + * a new formula is + * generated. */ ProductMode product_mode; /* Determines the scope of - * the synchronous products - * computed by the program. - * Possible values and - * their meanings are: - * - * LOCAL: - * The synchronous - * products are computed - * only with respect to - * the initial state of - * the system. This will - * save memory but makes - * the algorithm cross- - * comparisons less - * powerful, possibly - * at the cost of - * chances for finding - * inconsistencies in the - * results. - * GLOBAL: - * The synchronous - * products are computed - * with respect to each - * system state (i.e. - * the formula is model - * checked in each system - * state separately). - * This will usually + * the synchronous products + * computed by the program. + * Possible values and + * their meanings are: + * + * LOCAL: + * The synchronous + * products are computed + * only with respect to + * the initial state of + * the system. This will + * save memory but makes + * the algorithm cross- + * comparisons less + * powerful, possibly + * at the cost of + * chances for finding + * inconsistencies in the + * results. + * GLOBAL: + * The synchronous + * products are computed + * with respect to each + * system state (i.e. + * the formula is model + * checked in each system + * state separately). + * This will usually * require more memory - * than the other - * alternative. - */ + * than the other + * alternative. + */ string cfg_filename; /* Name for the * configuration file. @@ -269,7 +269,7 @@ public: bool do_cons_test; /* Is the model checking * result consistency check - * enabled? + * enabled? */ bool do_intr_test; /* Is the automata @@ -285,9 +285,9 @@ public: }; struct FormulaConfiguration /* A structure for storing - * specific information - * affecting the generation - * of random formulae. + * specific information + * affecting the generation + * of random formulae. */ { int default_operator_priority; /* Default priority for all @@ -304,79 +304,79 @@ public: */ bool allow_abbreviated_operators; /* Determines whether the - * operators ->, <->, xor, + * operators ->, <->, xor, * <>, [], W and M should * be allowed when - * generating random - * formulae (these are - * `abbreviated' operators - * since they could be - * written in an equivalent - * form by using another - * operators). + * generating random + * formulae (these are + * `abbreviated' operators + * since they could be + * written in an equivalent + * form by using another + * operators). */ Configuration::FormulaMode output_mode; /* Determines whether the - * generated formulae are - * to be converted to - * negation normal form - * before passing them to - * the different - * algorithms. Possible - * values are: - * - * NORMAL: - * No conversion. - * NNF: - * Do the conversion - * (this may affect the - * size of the formulae!) - */ + * generated formulae are + * to be converted to + * negation normal form + * before passing them to + * the different + * algorithms. Possible + * values are: + * + * NORMAL: + * No conversion. + * NNF: + * Do the conversion + * (this may affect the + * size of the formulae!) + */ Configuration::FormulaMode generate_mode; /* Determines whether the - * formulae are to be - * generated in negation - * normal form (strict - * size requirement for - * formulae). Possible - * values are: - * - * NORMAL: - * Allow more flexibility - * in the generation of - * formulae. - * NNF: - * Force generation into - * negation normal form. - */ + * formulae are to be + * generated in negation + * normal form (strict + * size requirement for + * formulae). Possible + * values are: + * + * NORMAL: + * Allow more flexibility + * in the generation of + * formulae. + * NNF: + * Force generation into + * negation normal form. + */ ::Ltl::FormulaRandomizer formula_generator; /* Interface to the random - * LTL formula generation - * algorithm. - */ + * LTL formula generation + * algorithm. + */ }; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ vector algorithms; /* information about the - * algorithms used in - * the tests. + ALLOC(AlgorithmInformation) > algorithms; /* information about the + * algorithms used in + * the tests. */ GlobalConfiguration global_options; /* General configuration - * information. + * information. */ FormulaConfiguration formula_options; /* Configuration - * information for - * generating random - * formulae. + * information for + * generating random + * formulae. */ Graph::StateSpaceRandomizer /* Interface to the */ statespace_generator; /* random state space - * generation + * generation * algorithms. */ @@ -392,10 +392,10 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ class ConfigurationException : public Exception /* A class for reporting - * errors when reading - * the configuration file. - */ - { + * errors when reading + * the configuration file. + */ + { public: ConfigurationException /* Constructors. */ (const string& info = "", @@ -458,7 +458,7 @@ private: OPT_CONSISTENCYTEST, OPT_DISABLE, OPT_ENABLE, OPT_FORMULACHANGEINTERVAL, OPT_FORMULAFILE, OPT_FORMULARANDOMSEED, OPT_HELP = 'h', - OPT_GLOBALPRODUCT = 20000, OPT_INTERACTIVE, + OPT_GLOBALPRODUCT = 20000, OPT_INTERACTIVE, OPT_INTERSECTIONTEST, OPT_LOGFILE, OPT_MODELCHECK, OPT_NOCOMPARISONTEST, OPT_NOCONSISTENCYTEST, OPT_NOINTERSECTIONTEST, @@ -497,12 +497,12 @@ private: OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY}; typedef map, double, /* Type definitions for */ - less >, /* the result cache used */ - ALLOC(double) > /* for computing the */ + less >, /* the result cache used */ + ALLOC(double) > /* for computing the */ ProbabilityMapElement; /* probability */ typedef map, /* formula operators. */ - ALLOC(ProbabilityMapElement) > + less, /* formula operators. */ + ALLOC(ProbabilityMapElement) > ProbabilityMap; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ @@ -514,8 +514,8 @@ private: */ void reset(); /* Initializes the - * configuration data - * to default values. + * configuration data + * to default values. */ long int parseCommandLineInteger /* Converts an integer */ diff --git a/lbtt/src/Exception.h b/lbtt/src/Exception.h index 274ab3be6..3ac9e4dfb 100644 --- a/lbtt/src/Exception.h +++ b/lbtt/src/Exception.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -74,7 +74,7 @@ public: virtual ~UserBreakException() throw(); /* Destructor. */ UserBreakException& /* Assignment operator. */ - operator=(const UserBreakException& e); + operator=(const UserBreakException& e); /* `what' inherited from class Exception */ @@ -289,13 +289,13 @@ public: Exceptional_istream /* Constructor. */ (istream *istr, ios::iostate mask = ios::goodbit); - + /* default copy constructor */ - + ~Exceptional_istream(); /* Destructor. */ /* default assignment operator */ - + template /* Operator for reading */ Exceptional_istream &operator>>(T &t); /* from the stream. */ @@ -337,9 +337,9 @@ public: Exceptional_ostream /* Constructor. */ (ostream* ostr, ios::iostate mask = ios::goodbit); - + /* default copy constructor */ - + ~Exceptional_ostream(); /* Destructor. */ /* default assignment operator */ @@ -353,7 +353,7 @@ public: * aware output stream into * a regular output stream. */ - + private: ostream* stream; /* A pointer to the * `regular' output stream @@ -482,7 +482,7 @@ inline UserBreakException& UserBreakException::operator= (const UserBreakException& e) /* ---------------------------------------------------------------------------- * - * Descrption: Assignment operator for class UserBreakException. Assigns the + * Descrption: Assignment operator for class UserBreakException. Assigns the * value of another UserBreakException to `this' one. * * Argument: e -- A reference to a constant UserBreakException. @@ -808,7 +808,7 @@ inline FileWriteException::FileWriteException() : inline FileWriteException::FileWriteException (const string& filename, const string& details) : IOException("error writing to " + filename - + string(details.empty() ? "" : " " + details)) + + string(details.empty() ? "" : " " + details)) /* ---------------------------------------------------------------------------- * * Description: Constructor for class FileWriteException. This constructor @@ -954,7 +954,7 @@ inline Exceptional_istream::Exceptional_istream * * Arguments: istr -- A pointer to an object of type istream. * mask -- A bit mask determining when the Exceptional_istream - * should throw exceptions. The most useful constants + * should throw exceptions. The most useful constants * for the bit mask are * ios::badbit Throw an exception if the input * stream (after performing an input @@ -1060,7 +1060,7 @@ inline Exceptional_ostream::Exceptional_ostream * * Arguments: ostr -- A pointer to an object of type ostream. * mask -- A bit mask determining when the Exceptional_ostream - * should throw exceptions. The most useful constants + * should throw exceptions. The most useful constants * for the bit mask are * ios::badbit Throw an exception if the output * stream (after performing an output diff --git a/lbtt/src/ExternalTranslator.cc b/lbtt/src/ExternalTranslator.cc index d73091da7..844418944 100644 --- a/lbtt/src/ExternalTranslator.cc +++ b/lbtt/src/ExternalTranslator.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -22,6 +22,7 @@ #endif /* __GNUC__ */ #include +#include #include #include #include @@ -125,10 +126,20 @@ void ExternalTranslator::translate input_file.close(); string command_line = string(command_line_arguments[2]) - + commandLine(external_program_input_file.getName(), + + commandLine(external_program_input_file.getName(), external_program_output_file.getName()); - if (!execSuccess(system(command_line.c_str()))) + int exitcode = system(command_line.c_str()); + + /* + * system() blocks SIGINT and SIGQUIT. If the child was killed + * by such a signal, forward the signal to the current process. + */ + if (WIFSIGNALED(exitcode) && + (WTERMSIG(exitcode) == SIGINT || WTERMSIG(exitcode) == SIGQUIT)) + raise(WTERMSIG(exitcode)); + + if (!execSuccess(exitcode)) throw ExecFailedException(command_line_arguments[2]); parseAutomaton(external_program_output_file.getName(), filename); diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index 790237858..12feb4a5e 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -22,6 +22,7 @@ #endif /* __GNUC__ */ #include +#include #include #include #include @@ -207,7 +208,7 @@ void printFileContents first_line_printed = true; estream << string(indent, ' ') + message + '\n'; } - + estream << string(indent, ' ') + line_prefix + message_line + '\n'; } } @@ -245,8 +246,8 @@ void writeToTranscript(const string& message, bool show_formula_in_header) const string roundstring = "Round " + toString(round_info.current_round); round_info.transcript_file << roundstring + '\n' - + string(roundstring.length(), '-') - + "\n\n"; + + string(roundstring.length(), '-') + + "\n\n"; if (show_formula_in_header) { @@ -291,7 +292,7 @@ void generateStateSpace() using ::Graph::StateSpace; if (configuration.global_options.statespace_generation_mode - == Configuration::ENUMERATEDPATH) + == Configuration::ENUMERATEDPATH) { StateSpace::size_type current_size = configuration.statespace_generator.min_size; @@ -319,7 +320,7 @@ void generateStateSpace() 2, 6); } - else + else { current_size = configuration.statespace_generator.min_size; printText("[All state spaces have been enumerated. Staring over]\n", @@ -333,7 +334,7 @@ void generateStateSpace() { round_info.path_iterator = new Graph::PathIterator - (configuration.statespace_generator.atoms_per_state, + (configuration.statespace_generator.atoms_per_state, current_size); } @@ -367,16 +368,16 @@ void generateStateSpace() { switch (configuration.global_options.statespace_generation_mode) { - case Configuration::RANDOMGRAPH : + case Configuration::RANDOMGRAPH : statespace = configuration.statespace_generator.generateGraph(); break; - case Configuration::RANDOMCONNECTEDGRAPH : + case Configuration::RANDOMCONNECTEDGRAPH : statespace = configuration.statespace_generator. - generateConnectedGraph(); + generateConnectedGraph(); break; - default : /* Configuration::RANDOMPATH */ + default : /* Configuration::RANDOMPATH */ statespace = configuration.statespace_generator.generatePath(); break; } @@ -407,8 +408,8 @@ void generateStateSpace() printText(" ok\n", 4); - if (configuration.statespace_generator.max_size - > configuration.statespace_generator.min_size) + if (configuration.statespace_generator.max_size + > configuration.statespace_generator.min_size) printText("number of states: " + toString(round_info.statespace->size()) + '\n', @@ -572,7 +573,7 @@ void generateFormulae(istream* formula_input_stream) if (printText(" ok\n", 4)) printText("", 4, 6); - + round_info.formulae[3] = &(::Ltl::Not::construct(*round_info.formulae[2])); if (printText(" ok\n", 4)) @@ -587,7 +588,7 @@ void generateFormulae(istream* formula_input_stream) for (int f = 0; f <= 1; f++) { round_info.cout << string(6, ' ') + (f == 0 ? "" : "negated ") - + "formula:" + string(19 - 8 * f, ' '); + + "formula:" + string(19 - 8 * f, ' '); round_info.formulae[f + 2]->print(round_info.cout); round_info.cout << '\n'; @@ -742,7 +743,7 @@ void writeFormulaeToFiles() void generateBuchiAutomaton (int f, vector::size_type algorithm_id) + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) /* ---------------------------------------------------------------------------- * * Description: Constructs a BuchiAutomaton by invoking an external program @@ -811,9 +812,9 @@ void generateBuchiAutomaton command_line += *(algorithm.extra_parameters) + ' '; command_line += string(round_info.formula_file_name[f]) - + ' ' + round_info.automaton_file_name - + " 1>" + round_info.cout_capture_file - + " 2>" + round_info.cerr_capture_file; + + ' ' + round_info.automaton_file_name + + " 1>" + round_info.cout_capture_file + + " 2>" + round_info.cerr_capture_file; if (!printText("", 5, 10)) printText("", 4, 10); @@ -836,11 +837,11 @@ void generateBuchiAutomaton && timing_information_begin.tms_cutime != static_cast(-1) && timing_information_end.tms_utime != static_cast(-1) && timing_information_end.tms_cutime != static_cast(-1)) - automaton_stats.buchi_generation_time + automaton_stats.buchi_generation_time = static_cast(timing_information_end.tms_utime - + timing_information_end.tms_cutime - - timing_information_begin.tms_utime - - timing_information_begin.tms_cutime) + + timing_information_end.tms_cutime + - timing_information_begin.tms_utime + - timing_information_begin.tms_cutime) / sysconf(_SC_CLK_TCK); /* @@ -851,6 +852,17 @@ void generateBuchiAutomaton if (exitcode != 0) { + /* + * system() blocks SIGINT and SIGQUIT. If the child was killed + * by such a signal, forward the signal to the current process. + * If lbtt is interactive, SIGINT will be handled as a user + * break. If lbtt is non-interactive, SIGINT will kill lbtt. + * This is what we expect when hitting C-c while lbtt is running. + */ + if (WIFSIGNALED(exitcode) && + (WTERMSIG(exitcode) == SIGINT || WTERMSIG(exitcode) == SIGQUIT)) + raise(WTERMSIG(exitcode)); + ExecFailedException e; e.changeMessage("Execution of `" + *(algorithm.path_to_program) + "' failed" @@ -860,7 +872,7 @@ void generateBuchiAutomaton 2) + " seconds elapsed)" : string("")) - + " with exit status " + toString(exitcode)); + + " with exit status " + toString(exitcode)); throw e; } @@ -893,17 +905,17 @@ void generateBuchiAutomaton if (round_info.transcript_file.is_open()) { writeToTranscript("Büchi automaton generation failed (" - + configuration.algorithmString(algorithm_id) - + ", " - + (f == 0 ? "posi" : "nega") + + configuration.algorithmString(algorithm_id) + + ", " + + (f == 0 ? "posi" : "nega") + "tive formula)"); if (automaton_stats.buchi_generation_time >= 0.0) round_info.transcript_file << string(8, ' ') + "Elapsed time: " - + toString(automaton_stats. + + toString(automaton_stats. buchi_generation_time, 2) - + " seconds (user time)\n"; + + " seconds (user time)\n"; } try @@ -915,33 +927,33 @@ void generateBuchiAutomaton printText(string(": ") + e.what(), 2); if (round_info.transcript_file.is_open()) round_info.transcript_file << string(8, ' ') - + "Program execution failed with exit " - "status " - + toString(exitcode); + + "Program execution failed with exit " + "status " + + toString(exitcode); } catch (const BuchiAutomaton::AutomatonParseException& e) { printText(string(" parsing input: ") + e.what(), 2); if (round_info.transcript_file.is_open()) round_info.transcript_file << string(8, ' ') - + "Error reading automaton: " - + e.what(); + + "Error reading automaton: " + + e.what(); } catch (const Exception& e) { printText(string(": ") + e.what(), 2); if (round_info.transcript_file.is_open()) round_info.transcript_file << string(8, ' ') - + "lbtt internal error: " - + e.what(); + + "lbtt internal error: " + + e.what(); } catch (const bad_alloc&) { printText(": out of memory", 2); if (round_info.transcript_file.is_open()) round_info.transcript_file << string(8, ' ') - + "Out of memory while reading " - "automaton"; + + "Out of memory while reading " + "automaton"; } printText("\n", 2); @@ -1021,7 +1033,7 @@ void generateBuchiAutomaton += automaton_stats.number_of_buchi_transitions; final_statistics[algorithm_id].total_number_of_acceptance_sets[f] += automaton_stats.number_of_acceptance_sets; - + if (final_statistics[algorithm_id].total_buchi_generation_time[f] < 0.0 || automaton_stats.buchi_generation_time < 0.0) final_statistics[algorithm_id].total_buchi_generation_time[f] = -1.0; @@ -1040,7 +1052,7 @@ void generateBuchiAutomaton void generateProductAutomaton (int f, vector::size_type algorithm_id) + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) /* ---------------------------------------------------------------------------- * * Description: Computes the product of a Büchi automaton with a state @@ -1098,7 +1110,7 @@ void generateProductAutomaton if (round_info.transcript_file.is_open()) writeToTranscript("Product automaton generation aborted (" + configuration.algorithmString(algorithm_id) - + ", " + + ", " + (f == 0 ? "posi" : "nega") + "tive formula)" + ". Product may be too large.\n"); @@ -1110,7 +1122,7 @@ void generateProductAutomaton { if (!printText(" user break\n\n", 4)) printText("[User break]\n\n", 2, 10); - + if (round_info.transcript_file.is_open()) writeToTranscript("User break while generating product automaton (" + configuration.algorithmString(algorithm_id) @@ -1173,7 +1185,7 @@ void generateProductAutomaton void performEmptinessCheck (int f, vector::size_type + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) /* ---------------------------------------------------------------------------- * @@ -1211,7 +1223,7 @@ void performEmptinessCheck { round_info.product_automaton->emptinessCheck (automaton_stats.emptiness_check_result); - + automaton_stats.emptiness_check_performed = true; } catch (const UserBreakException&) @@ -1221,7 +1233,7 @@ void performEmptinessCheck if (round_info.transcript_file.is_open()) writeToTranscript("User break while searching for accepting cycles (" - + configuration.algorithmString(algorithm_id) + + configuration.algorithmString(algorithm_id) + ", " + (f == 0 ? "posi" : "nega") + "tive formula)\n"); @@ -1252,7 +1264,7 @@ void performEmptinessCheck /* ========================================================================= */ void performConsistencyCheck (vector::size_type + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) /* ---------------------------------------------------------------------------- * @@ -1322,10 +1334,10 @@ void performConsistencyCheck } printText((result ? " ok\n" : " failed\n"), 4); - + if (configuration.global_options.verbosity >= 3) printConsistencyCheckStats(cout, 8, algorithm_id); -} +} /* ========================================================================= */ void compareResults() @@ -1378,7 +1390,7 @@ void compareResults() unsigned long int dist = alg_1_stats->emptiness_check_result.hammingDistance - (alg_2_stats->emptiness_check_result); + (alg_2_stats->emptiness_check_result); alg_1_stats->cross_comparison_stats[alg_2].first = alg_2_stats->cross_comparison_stats[alg_1].first @@ -1397,9 +1409,9 @@ void compareResults() != alg_2_stats->emptiness_check_result[0]) { (final_statistics[alg_1]. - initial_cross_comparison_mismatches[alg_2])++; + initial_cross_comparison_mismatches[alg_2])++; (final_statistics[alg_2]. - initial_cross_comparison_mismatches[alg_1])++; + initial_cross_comparison_mismatches[alg_1])++; } result = false; @@ -1479,13 +1491,13 @@ void performBuchiIntersectionCheck() if (test_results[alg_1].automaton_stats[0].buchiAutomatonComputed() && test_results[alg_2].automaton_stats[1]. - buchiAutomatonComputed()) + buchiAutomatonComputed()) { automaton_intersection = 0; automaton_intersection = BuchiAutomaton::intersect - (*(test_results[alg_1].automaton_stats[0].buchi_automaton), + (*(test_results[alg_1].automaton_stats[0].buchi_automaton), *(test_results[alg_2].automaton_stats[1].buchi_automaton)); /* @@ -1519,18 +1531,18 @@ void performBuchiIntersectionCheck() unsigned long int acceptance_set_counter = 0; for (set, - ALLOC(GraphEdgeContainer::size_type) >::const_iterator + less, + ALLOC(GraphEdgeContainer::size_type) >::const_iterator state = scc->begin(); state != scc->end() && acceptance_set_counter < number_of_acceptance_sets; ++state) - { + { accept_set = acceptance_set_counter; while (accept_set < number_of_acceptance_sets) { if ((*automaton_intersection)[*state].acceptanceSets(). - test(accept_set)) + test(accept_set)) { acceptance_sets.setBit(accept_set); if (accept_set == acceptance_set_counter) @@ -1538,7 +1550,7 @@ void performBuchiIntersectionCheck() do acceptance_set_counter++; while (acceptance_set_counter - < number_of_acceptance_sets + < number_of_acceptance_sets && acceptance_sets[acceptance_set_counter]); accept_set = acceptance_set_counter; continue; @@ -1549,7 +1561,7 @@ void performBuchiIntersectionCheck() } if (acceptance_set_counter == number_of_acceptance_sets) - { + { test_results[alg_1].automaton_stats[0]. buchi_intersection_check_stats[alg_2] = 0; test_results[alg_2].automaton_stats[1]. @@ -1574,7 +1586,7 @@ void performBuchiIntersectionCheck() automaton_intersection = 0; if (test_results[alg_1].automaton_stats[0]. - buchi_intersection_check_stats[alg_2] == -1) + buchi_intersection_check_stats[alg_2] == -1) { test_results[alg_1].automaton_stats[0]. buchi_intersection_check_stats[alg_2] = 1; @@ -1606,10 +1618,10 @@ void performBuchiIntersectionCheck() writeToTranscript("User break during Büchi automata intersection " "emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " - + configuration.algorithmString(alg_1) - + ", (-) " - + configuration.algorithmString(alg_2) - + "\n\n"; + + configuration.algorithmString(alg_1) + + ", (-) " + + configuration.algorithmString(alg_2) + + "\n\n"; if (automaton_intersection != 0) { @@ -1640,10 +1652,10 @@ void performBuchiIntersectionCheck() writeToTranscript("Out of memory during Büchi automata " "intersection emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " - + configuration.algorithmString(alg_1) - + ", (-) " - + configuration.algorithmString(alg_2) - + "\n\n"; + + configuration.algorithmString(alg_1) + + ", (-) " + + configuration.algorithmString(alg_2) + + "\n\n"; } } } diff --git a/lbtt/src/main.cc b/lbtt/src/main.cc index b34619ed2..3510e176d 100644 --- a/lbtt/src/main.cc +++ b/lbtt/src/main.cc @@ -704,7 +704,8 @@ int main(int argc, char* argv[]) configuration.print(cout); user_break = false; - signal(SIGINT, breakHandler); + if (configuration.global_options.interactive != Configuration::NEVER) + signal(SIGINT, breakHandler); #ifdef HAVE_OBSTACK_H obstack_alloc_failed_handler = &ObstackAllocator::failure;