alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT

Browse source 
and SIGQUIT.
* src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise.
* src/main.cc (main): Do not intercept SIGINT in
non-interactive runs.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-29 13:06:53 +00:00
parent ea90d2f8be
commit 48c03b89b8
7 changed files with 593 additions and 561 deletions
Download patch file Download diff file Expand all files Collapse all files

10
lbtt/ChangeLog
View file

@ -1,4 +1,12 @@
2003-07-13 Alexandre Duret-Lutz <adl@gnu.org>
2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 <aduret@src.lip6.fr>
* doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo
versions are stricter on this.

596
lbtt/src/Configuration.cc
View file

@ -1,5 +1,5 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* 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,7 +426,7 @@ 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));
@ -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;
@ -664,7 +664,7 @@ void Configuration::read(int argc, char* argv[])
{
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);
@ -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<unsigned long int, less<unsigned long int>,
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
@ -1000,12 +1000,12 @@ void Configuration::read(int argc, char* argv[])
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<double>
(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,14 +1181,14 @@ 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";
@ -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<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::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 <heikki.tauriainen@hut.fi>.\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 <heikki.tauriainen@hut.fi>.\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<double>(priority)
/ static_cast<double>(total_short_unary_priority);
/ static_cast<double>(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<double>(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<double>(p1)
* operatorProbability(op, k, n - 1,
* operatorProbability(op, k, n - 1,
total_short_unary_priority,
total_long_unary_priority,
total_binary_priority,

334
lbtt/src/Configuration.h
View file

@ -1,5 +1,5 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* 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<AlgorithmInformation, /* of an algorithm and */
ALLOC(AlgorithmInformation) >::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.
@ -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<AlgorithmInformation, /* A vector containing */
ALLOC(AlgorithmInformation) > 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,9 +392,9 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class ConfigurationException : public Exception /* A class for reporting
* errors when reading
* the configuration file.
*/
* errors when reading
* the configuration file.
*/
{
public:
ConfigurationException /* Constructors. */
@ -497,12 +497,12 @@ private:
OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY};
typedef map<pair<int, int>, double, /* Type definitions for */
less<pair<int, int> >, /* the result cache used */
ALLOC(double) > /* for computing the */
less<pair<int, int> >, /* the result cache used */
ALLOC(double) > /* for computing the */
ProbabilityMapElement; /* probability */
typedef map<int, ProbabilityMapElement, /* distribution of LTL */
less<int>, /* formula operators. */
ALLOC(ProbabilityMapElement) >
less<int>, /* 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 */

4
lbtt/src/Exception.h
View file

@ -1,5 +1,5 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* This program is free software; you can redistribute it and/or
@ -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

17
lbtt/src/ExternalTranslator.cc
View file

@ -1,5 +1,5 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* This program is free software; you can redistribute it and/or
@ -22,6 +22,7 @@
#endif /* __GNUC__ */
#include <config.h>
#include <csignal>
#include <cstdio>
#include <cstdlib>
#include <sys/stat.h>
@ -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);

128
lbtt/src/TestOperations.cc
View file

@ -1,5 +1,5 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* This program is free software; you can redistribute it and/or
@ -22,6 +22,7 @@
#endif /* __GNUC__ */
#include <config.h>
#include <csignal>
#include <cstdio>
#include <cstdlib>
#include <sys/times.h>
@ -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;
@ -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;
}
@ -408,7 +409,7 @@ void generateStateSpace()
printText(" ok\n", 4);
if (configuration.statespace_generator.max_size
> configuration.statespace_generator.min_size)
> configuration.statespace_generator.min_size)
printText("number of states: "
+ toString(round_info.statespace->size())
+ '\n',
@ -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<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::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("<executing `" + command_line + "'>", 5, 10))
printText("<computing Büchi automaton>", 4, 10);
@ -838,9 +839,9 @@ void generateBuchiAutomaton
&& timing_information_end.tms_cutime != static_cast<clock_t>(-1))
automaton_stats.buchi_generation_time
= static_cast<double>(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);
@ -1040,7 +1052,7 @@ void generateBuchiAutomaton
void generateProductAutomaton
(int f,
vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::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");
@ -1173,7 +1185,7 @@ void generateProductAutomaton
void performEmptinessCheck
(int f,
vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::size_type
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id)
/* ----------------------------------------------------------------------------
*
@ -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<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::size_type
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id)
/* ----------------------------------------------------------------------------
*
@ -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<GraphEdgeContainer::size_type,
less<GraphEdgeContainer::size_type>,
ALLOC(GraphEdgeContainer::size_type) >::const_iterator
less<GraphEdgeContainer::size_type>,
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";
}
}
}

3
lbtt/src/main.cc
View file

@ -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;