* tests/core/ikwiad.cc: Rewrite the help text without std::endl.
This commit is contained in:
Alexandre Duret-Lutz
parent
546fa92a5d
commit
8bc10dea82
1 changed files with 145 additions and 203 deletions
|
|
@ -77,197 +77,139 @@ syntax(char* prog)
|
||||||
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
||||||
prog = slash + 4;
|
prog = slash + 4;
|
||||||
|
|
||||||
std::cerr << "Usage: "<< prog << " [-f|-l|-taa] [OPTIONS...] formula"
|
std::cerr <<
|
||||||
<< std::endl
|
"Usage: " << prog << " [-f|-l|-taa] [OPTIONS...] formula\n"
|
||||||
<< " "<< prog << " [-f|-l|-taa] -F [OPTIONS...] file"
|
" " << prog << " [-f|-l|-taa] -F [OPTIONS...] file\n"
|
||||||
<< std::endl
|
" " << prog << " -XH [OPTIONS...] file\n"
|
||||||
<< " "<< prog << " -XH [OPTIONS...] file" << std::endl
|
"\n"
|
||||||
<< std::endl
|
"Translate an LTL formula into an automaton, or read the automaton from "
|
||||||
|
"a file.\n"
|
||||||
<< "Translate an LTL formula into an automaton, or read the "
|
"Optionally multiply this automaton by another automaton read "
|
||||||
<< "automaton from a file." << std::endl
|
"from a file.\n"
|
||||||
<< "Optionally multiply this automaton by another"
|
"Output the result in various formats, or perform an emptiness check."
|
||||||
<< " automaton read from a file." << std::endl
|
"\n\n"
|
||||||
<< "Output the result in various formats, or perform an emptiness "
|
"Input options:\n"
|
||||||
<< "check." << std::endl
|
" -F read the formula from a file, not from the command line\n"
|
||||||
<< std::endl
|
" -XD do not compute an automaton, read it from an ltl2dstar file\n"
|
||||||
|
" -XDB like -XD, and convert it to TGBA\n"
|
||||||
<< "Input options:" << std::endl
|
" -XH do not compute an automaton, read it from a HOA file\n"
|
||||||
<< " -F read the formula from a file, not from the command line"
|
" -XL do not compute an automaton, read it from an LBTT file\n"
|
||||||
<< std::endl
|
" -XN do not compute an automaton, read it from a neverclaim file\n"
|
||||||
<< " -XD do not compute an automaton, read it from an"
|
" -Pfile multiply the formula automaton with the TGBA read"
|
||||||
<< " ltl2dstar file" << std::endl
|
" from `file'\n"
|
||||||
<< " -XDB like -XD, and convert it to TGBA\n"
|
" -KPfile multiply the formula automaton with the Kripke"
|
||||||
<< " -XH do not compute an automaton, read it from a"
|
" structure from `file'\n"
|
||||||
<< " HOA file\n"
|
"\n"
|
||||||
<< " -XL do not compute an automaton, read it from an"
|
"Translation algorithm:\n"
|
||||||
<< " LBTT file" << std::endl
|
" -f use Couvreur's FM algorithm for LTL (default)\n"
|
||||||
<< " -XN do not compute an automaton, read it from a"
|
" -taa use Tauriainen's TAA-based algorithm for LTL\n"
|
||||||
<< " neverclaim file" << std::endl
|
" -u use Compositional translation\n"
|
||||||
<< " -Pfile multiply the formula automaton with the TGBA read"
|
"\n"
|
||||||
<< " from `file'\n"
|
"Options for Couvreur's FM algorithm (-f):\n"
|
||||||
<< " -KPfile multiply the formula automaton with the Kripke"
|
" -fr reduce formula at each step of FM\n"
|
||||||
<< " structure from `file'\n"
|
" as specified with the -r{1..7} options\n"
|
||||||
<< std::endl
|
" -fu build unambiguous automata\n"
|
||||||
|
" -L fair-loop approximation (implies -f)\n"
|
||||||
<< "Translation algorithm:" << std::endl
|
" -p branching postponement (implies -f)\n"
|
||||||
<< " -f use Couvreur's FM algorithm for LTL"
|
" -U[PROPS] consider atomic properties of the formula as "
|
||||||
<< " (default)" << std::endl
|
"exclusive events, and\n"
|
||||||
<< " -taa use Tauriainen's TAA-based algorithm for LTL"
|
" PROPS as unobservables events (implies -f)\n"
|
||||||
<< std::endl
|
" -x try to produce a more deterministic automaton "
|
||||||
<< " -u use Compositional translation"
|
"(implies -f)\n"
|
||||||
<< std::endl
|
" -y do not merge states with same symbolic representation "
|
||||||
<< std::endl
|
"(implies -f)\n"
|
||||||
|
"\n"
|
||||||
<< "Options for Couvreur's FM algorithm (-f):" << std::endl
|
"Options for Tauriainen's TAA-based algorithm (-taa):\n"
|
||||||
<< " -fr reduce formula at each step of FM" << std::endl
|
" -c enable language containment checks (implies -taa)\n"
|
||||||
<< " as specified with the -r{1..7} options" << std::endl
|
"\n"
|
||||||
<< " -fu build unambiguous automata" << std::endl
|
"Formula simplification (before translation):\n"
|
||||||
<< " -L fair-loop approximation (implies -f)" << std::endl
|
" -r1 reduce formula using basic rewriting\n"
|
||||||
<< " -p branching postponement (implies -f)" << std::endl
|
" -r2 reduce formula using class of eventuality and universality\n"
|
||||||
<< " -U[PROPS] consider atomic properties of the formula as "
|
" -r3 reduce formula using implication between sub-formulae\n"
|
||||||
<< "exclusive events, and" << std::endl
|
" -r4 reduce formula using all above rules\n"
|
||||||
<< " PROPS as unobservables events (implies -f)"
|
" -r5 reduce formula using tau03\n"
|
||||||
<< std::endl
|
" -r6 reduce formula using tau03+\n"
|
||||||
<< " -x try to produce a more deterministic automaton "
|
" -r7 reduce formula using tau03+ and -r4\n"
|
||||||
<< "(implies -f)" << std::endl
|
" -rd display the reduced formula\n"
|
||||||
<< " -y do not merge states with same symbolic representation "
|
" -rD dump statistics about the simplifier cache\n"
|
||||||
<< "(implies -f)" << std::endl
|
" -rL disable basic rewritings producing larger formulas\n"
|
||||||
<< std::endl
|
" -ru lift formulae that are eventual and universal\n"
|
||||||
|
"\n"
|
||||||
<< "Options for Tauriainen's TAA-based algorithm (-taa):"
|
"Automaton degeneralization (after translation):\n"
|
||||||
<< std::endl
|
" -DT degeneralize the automaton as a TBA\n"
|
||||||
<< " -c enable language containment checks (implies -taa)"
|
" -DS degeneralize the automaton as an SBA\n"
|
||||||
<< std::endl
|
" (append z/Z, o/O, l/L: to turn on/off options "
|
||||||
<< std::endl
|
"(default: zol)\n "
|
||||||
|
" z: level resetting, o: adaptive order, "
|
||||||
<< "Formula simplification (before translation):"
|
"l: level cache)\n"
|
||||||
<< std::endl
|
"\n"
|
||||||
<< " -r1 reduce formula using basic rewriting" << std::endl
|
"Automaton simplifications (after translation):\n"
|
||||||
<< " -r2 reduce formula using class of eventuality and "
|
" -R3 use SCCs to remove useless states and acceptance sets\n"
|
||||||
<< "universality" << std::endl
|
" -R3f clean more acceptance sets than -R3\n"
|
||||||
<< " -r3 reduce formula using implication between "
|
" "
|
||||||
<< "sub-formulae" << std::endl
|
"(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)\n"
|
||||||
<< " -r4 reduce formula using all above rules" << std::endl
|
" -RDS reduce the automaton with direct simulation\n"
|
||||||
<< " -r5 reduce formula using tau03" << std::endl
|
" -RRS reduce the automaton with reverse simulation\n"
|
||||||
<< " -r6 reduce formula using tau03+" << std::endl
|
" -RIS iterate both direct and reverse simulations\n"
|
||||||
<< " -r7 reduce formula using tau03+ and -r4" << std::endl
|
" -Rm attempt to WDBA-minimize the automaton\n"
|
||||||
<< " -rd display the reduced formula" << std::endl
|
" -RM attempt to WDBA-minimize the automaton unless the "
|
||||||
<< " -rD dump statistics about the simplifier cache" << std::endl
|
"result is bigger\n"
|
||||||
<< " -rL disable basic rewritings producing larger formulas"
|
" -RQ determinize a TGBA (assuming it's legal!)\n"
|
||||||
<< std::endl
|
"\n"
|
||||||
<< " -ru lift formulae that are eventual and universal"
|
"Automaton conversion:\n"
|
||||||
<< std::endl << std::endl
|
" -M convert into a det. minimal monitor (implies -R3 or R3b)\n"
|
||||||
|
" -s convert to explicit automaton, and number states in DFS order\n"
|
||||||
<< "Automaton degeneralization (after translation):"
|
" -S convert to explicit automaton, and number states in BFS order\n"
|
||||||
<< std::endl
|
"\n"
|
||||||
<< " -DT degeneralize the automaton as a TBA" << std::endl
|
"Conversion to Testing Automaton:\n"
|
||||||
<< " -DS degeneralize the automaton as an SBA" << std::endl
|
" -TA output a Generalized Testing Automaton (GTA),\n"
|
||||||
<< " (append z/Z, o/O, l/L: to turn on/off options "
|
" or a Testing Automaton (TA) with -DS\n"
|
||||||
<< "(default: zol)\n "
|
" -lv add an artificial livelock state to obtain a Single-pass (G)TA\n"
|
||||||
<< " z: level resetting, o: adaptive order, "
|
" -sp convert into a single-pass (G)TA without artificial "
|
||||||
<< "l: level cache)\n"
|
"livelock state\n"
|
||||||
<< std::endl
|
" -in do not use an artificial initial state\n"
|
||||||
|
" -TGTA output a Transition-based Generalized TA\n"
|
||||||
<< "Automaton simplifications (after translation):"
|
" -RT reduce the (G)TA/TGTA using bisimulation.\n"
|
||||||
<< std::endl
|
"\n"
|
||||||
<< " -R3 use SCC to reduce the automaton" << std::endl
|
"Options for performing emptiness checks (on TGBA):\n"
|
||||||
<< " -R3f clean more acceptance conditions than -R3" << std::endl
|
" -e[ALGO] run emptiness check, expect and compute an "
|
||||||
<< " "
|
"accepting run\n"
|
||||||
<< "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
|
" -E[ALGO] run emptiness check, expect no accepting run\n"
|
||||||
<< std::endl
|
" -C compute an accepting run (Counterexample) if it exists\n"
|
||||||
<< " -RDS reduce the automaton with direct simulation"
|
" -CR compute and replay an accepting run (implies -C)\n"
|
||||||
<< std::endl
|
" -G graph the accepting run seen as an automaton (requires -e)\n"
|
||||||
<< " -RRS reduce the automaton with reverse simulation"
|
" -m try to reduce accepting runs, in a second pass\n"
|
||||||
<< std::endl
|
"Where ALGO should be one of:\n"
|
||||||
<< " -RIS iterate both direct and reverse simulations"
|
" Cou99(OPTIONS) (the default)\n"
|
||||||
<< std::endl
|
" CVWY90(OPTIONS)\n"
|
||||||
<< " -Rm attempt to WDBA-minimize the automaton" << std::endl
|
" GV04(OPTIONS)\n"
|
||||||
<< std::endl
|
" SE05(OPTIONS)\n"
|
||||||
<< " -RM attempt to WDBA-minimize the automaton unless the "
|
" Tau03(OPTIONS)\n"
|
||||||
<< "result is bigger" << std::endl
|
" Tau03_opt(OPTIONS)\n"
|
||||||
<< " -RQ determinize a TGBA (assuming it's legal!)" << std::endl
|
"\n"
|
||||||
<< std::endl
|
"If no emptiness check is run, the automaton will be output "
|
||||||
|
"in dot format\nby default. This can be "
|
||||||
<< "Automaton conversion:" << std::endl
|
"changed with the following options.\n"
|
||||||
<< " -M convert into a deterministic minimal monitor "
|
"\n"
|
||||||
<< "(implies -R3 or R3b)" << std::endl
|
"Output options (if no emptiness check):\n"
|
||||||
<< " -s convert to explicit automaton, and number states "
|
" -ks display statistics on the automaton (size only)\n"
|
||||||
<< "in DFS order" << std::endl
|
" -kt display statistics on the automaton (size + subtransitions)\n"
|
||||||
<< " -S convert to explicit automaton, and number states "
|
" -K dump the graph of SCCs in dot format\n"
|
||||||
<< "in BFS order" << std::endl
|
" -KC list cycles in automaton\n"
|
||||||
<< std::endl
|
" -KW list weak SCCs\n"
|
||||||
|
" -N output the never clain for Spin (implies -DS)\n"
|
||||||
<< "Conversion to Testing Automaton:" << std::endl
|
" -NN output the never clain for Spin, with commented states"
|
||||||
<< " -TA output a Generalized Testing Automaton (GTA),\n"
|
" (implies -DS)\n"
|
||||||
<< " or a Testing Automaton (TA) with -DS\n"
|
" -O tell if a formula represents a safety, guarantee, "
|
||||||
<< " -lv add an artificial livelock state to obtain a "
|
"or obligation property\n"
|
||||||
<< "Single-pass (G)TA\n"
|
" -t output automaton in LBTT's format\n"
|
||||||
<< " -sp convert into a single-pass (G)TA without artificial "
|
"\n"
|
||||||
<< "livelock state\n"
|
"Miscellaneous options:\n"
|
||||||
<< " -in do not use an artificial initial state\n"
|
" -0 produce minimal output dedicated to the paper\n"
|
||||||
<< " -TGTA output a Transition-based Generalized TA"
|
" -8 output UTF-8 formulae\n"
|
||||||
<< std::endl
|
" -d turn on traces during parsing\n"
|
||||||
<< " -RT reduce the (G)TA/TGTA using bisimulation.\n"
|
" -T time the different phases of the translation\n"
|
||||||
<< std::endl
|
" -v display the BDD variables used by the automaton\n";
|
||||||
|
|
||||||
<< "Options for performing emptiness checks (on TGBA):" << std::endl
|
|
||||||
<< " -e[ALGO] run emptiness check, expect and compute an "
|
|
||||||
<< "accepting run" << std::endl
|
|
||||||
<< " -E[ALGO] run emptiness check, expect no accepting run"
|
|
||||||
<< std::endl
|
|
||||||
<< " -C compute an accepting run (Counterexample) if it exists"
|
|
||||||
<< std::endl
|
|
||||||
<< " -CR compute and replay an accepting run (implies -C)"
|
|
||||||
<< std::endl
|
|
||||||
<< " -G graph the accepting run seen as an automaton "
|
|
||||||
<< " (requires -e)" << std::endl
|
|
||||||
<< " -m try to reduce accepting runs, in a second pass"
|
|
||||||
<< std::endl
|
|
||||||
<< "Where ALGO should be one of:" << std::endl
|
|
||||||
<< " Cou99(OPTIONS) (the default)" << std::endl
|
|
||||||
<< " CVWY90(OPTIONS)" << std::endl
|
|
||||||
<< " GV04(OPTIONS)" << std::endl
|
|
||||||
<< " SE05(OPTIONS)" << std::endl
|
|
||||||
<< " Tau03(OPTIONS)" << std::endl
|
|
||||||
<< " Tau03_opt(OPTIONS)" << std::endl
|
|
||||||
<< std::endl
|
|
||||||
|
|
||||||
<< "If no emptiness check is run, the automaton will be output "
|
|
||||||
<< "in dot format" << std::endl << "by default. This can be "
|
|
||||||
<< "changed with the following options." << std::endl
|
|
||||||
<< std::endl
|
|
||||||
|
|
||||||
<< "Output options (if no emptiness check):" << std::endl
|
|
||||||
<< " -ks display statistics on the automaton (size only)"
|
|
||||||
<< std::endl
|
|
||||||
<< " -kt display statistics on the automaton (size + "
|
|
||||||
<< "subtransitions)"
|
|
||||||
<< std::endl
|
|
||||||
<< " -K dump the graph of SCCs in dot format" << std::endl
|
|
||||||
<< " -KC list cycles in automaton" << std::endl
|
|
||||||
<< " -KW list weak SCCs" << std::endl
|
|
||||||
<< " -N output the never clain for Spin (implies -DS)"
|
|
||||||
<< std::endl
|
|
||||||
<< " -NN output the never clain for Spin, with commented states"
|
|
||||||
<< " (implies -DS)" << std::endl
|
|
||||||
<< " -O tell if a formula represents a safety, guarantee, "
|
|
||||||
<< "or obligation property"
|
|
||||||
<< std::endl
|
|
||||||
<< " -t output automaton in LBTT's format" << std::endl
|
|
||||||
<< std::endl
|
|
||||||
|
|
||||||
<< "Miscellaneous options:" << std::endl
|
|
||||||
<< " -0 produce minimal output dedicated to the paper"
|
|
||||||
<< std::endl
|
|
||||||
<< " -8 output UTF-8 formulae" << std::endl
|
|
||||||
<< " -d turn on traces during parsing" << std::endl
|
|
||||||
<< " -T time the different phases of the translation"
|
|
||||||
<< std::endl
|
|
||||||
<< " -v display the BDD variables used by the automaton"
|
|
||||||
<< std::endl
|
|
||||||
<< std::endl;
|
|
||||||
|
|
||||||
exit(2);
|
exit(2);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -278,7 +220,7 @@ to_int(const char* s)
|
||||||
int res = strtol(s, &endptr, 10);
|
int res = strtol(s, &endptr, 10);
|
||||||
if (*endptr)
|
if (*endptr)
|
||||||
{
|
{
|
||||||
std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
|
std::cerr << "Failed to parse `" << s << "' as an integer.\n";
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
return res;
|
return res;
|
||||||
|
|
@ -815,7 +757,7 @@ checked_main(int argc, char** argv)
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
std::cerr << "Unknown suboption `" << *c
|
std::cerr << "Unknown suboption `" << *c
|
||||||
<< "' for option -u" << std::endl;
|
<< "' for option -u\n";
|
||||||
}
|
}
|
||||||
++c;
|
++c;
|
||||||
}
|
}
|
||||||
|
|
@ -864,7 +806,7 @@ checked_main(int argc, char** argv)
|
||||||
if ((graph_run_tgba_opt)
|
if ((graph_run_tgba_opt)
|
||||||
&& (!echeck_inst || !expect_counter_example))
|
&& (!echeck_inst || !expect_counter_example))
|
||||||
{
|
{
|
||||||
std::cerr << argv[0] << ": error: -G requires -e." << std::endl;
|
std::cerr << argv[0] << ": error: -G requires -e.\n";
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -968,7 +910,7 @@ checked_main(int argc, char** argv)
|
||||||
&& (translation != TransFM && translation != TransCompo))
|
&& (translation != TransFM && translation != TransCompo))
|
||||||
{
|
{
|
||||||
std::cerr << "Only the FM algorithm can translate PSL formulae;"
|
std::cerr << "Only the FM algorithm can translate PSL formulae;"
|
||||||
<< " I'm using it for this formula." << std::endl;
|
<< " I'm using it for this formula.\n";
|
||||||
translation = TransFM;
|
translation = TransFM;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1047,7 +989,7 @@ checked_main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
std::cerr << "Error: Without a formula I cannot make "
|
std::cerr << "Error: Without a formula I cannot make "
|
||||||
<< "sure that the automaton built with -Rm\n"
|
<< "sure that the automaton built with -Rm\n"
|
||||||
<< " is correct." << std::endl;
|
<< " is correct.\n";
|
||||||
exit(2);
|
exit(2);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -1280,7 +1222,7 @@ checked_main(int argc, char** argv)
|
||||||
stats_reachable(testing_automaton).dump(std::cout);
|
stats_reachable(testing_automaton).dump(std::cout);
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
std::cerr << "unsupported output option" << std::endl;
|
std::cerr << "unsupported output option\n";
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
tm.stop("producing output");
|
tm.stop("producing output");
|
||||||
|
|
@ -1315,7 +1257,7 @@ checked_main(int argc, char** argv)
|
||||||
stats_reachable(a).dump(std::cout);
|
stats_reachable(a).dump(std::cout);
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
std::cerr << "unsupported output option" << std::endl;
|
std::cerr << "unsupported output option\n";
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
tm.stop("producing output");
|
tm.stop("producing output");
|
||||||
|
|
@ -1365,7 +1307,7 @@ checked_main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
std::cerr << echeck_algo << " requires at least "
|
std::cerr << echeck_algo << " requires at least "
|
||||||
<< echeck_inst->min_sets()
|
<< echeck_inst->min_sets()
|
||||||
<< " acceptance sets." << std::endl;
|
<< " acceptance sets.\n";
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -1547,9 +1489,9 @@ checked_main(int argc, char** argv)
|
||||||
std::cout << "no accepting run found";
|
std::cout << "no accepting run found";
|
||||||
if (!ec->safe() && expect_counter_example)
|
if (!ec->safe() && expect_counter_example)
|
||||||
{
|
{
|
||||||
std::cout << " even if expected" << std::endl;
|
std::cout << " even if expected\n";
|
||||||
std::cout << "this may be due to the use of the bit"
|
std::cout << "this may be due to the use of the bit"
|
||||||
<< " state hashing technique" << std::endl;
|
<< " state hashing technique\n";
|
||||||
std::cout << "you can try to increase the heap size "
|
std::cout << "you can try to increase the heap size "
|
||||||
<< "or use an explicit storage"
|
<< "or use an explicit storage"
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
@ -1566,7 +1508,7 @@ checked_main(int argc, char** argv)
|
||||||
|
|
||||||
if (!run)
|
if (!run)
|
||||||
{
|
{
|
||||||
std::cout << "an accepting run exists" << std::endl;
|
std::cout << "an accepting run exists\n";
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1597,7 +1539,7 @@ checked_main(int argc, char** argv)
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
std::cout << "an accepting run exists "
|
std::cout << "an accepting run exists "
|
||||||
<< "(use -C to print it)" << std::endl;
|
<< "(use -C to print it)\n";
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue