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

Update the description of the commands options (-TA,-lv,-sp,-in,-TGTA)

Browse source 
* src/tgbatest/ltl2tgba.cc: update the description of the options for
the different kinds of Testing Automata: TA, STA, GTA, SGTA and TGTA.
This commit is contained in:
Ala-Eddine Ben-Salem 2012-04-17 15:26:14 +02:00 • committed by Alexandre Duret-Lutz
parent 9319b0ca25
commit 84b1d24e8f
1 changed files with 70 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

137
src/tgbatest/ltl2tgba.cc
View file

@ -279,22 +279,23 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -v display the BDD variables used by the automaton" << " -v display the BDD variables used by the automaton"
<< std::endl << std::endl
<< std::endl
<< "Options for Testing Automata:" << "Options for Testing Automata:"
<< std::endl << std::endl
<< " -TA Translate an LTL formula into a TA (Testing automata)" << " -TA Translate an LTL formula into a GTA (Generalized"
<< " Testing automata), for Testing Automata (TA) add '-DS' option"
<< std::endl << std::endl
<< std::endl << " -lv convert into a (G)TA with an artificial livelock state,"
<< " -sp convert into a TA involving a single-pass emptiness check" << " the obtained automaton is called S(G)TA "
<< std::endl << std::endl << "(Single-pass (Generalized) Testing Automata)"
<< " -lv convert into a TA with an artificial livelock accepting" << std::endl
<< "state (single-pass emptiness check)" << " -sp convert into a (G)TA involving a single-pass emptiness "
<< "check (without adding an artificial livelock state)"
<< std::endl << std::endl
<< std::endl << std::endl
<< " -in convert into a TA without an artificial initial state" << " -in convert into a (G)TA without an artificial initial state"
<< std::endl << std::endl
<< std::endl << " -TGTA Translate an LTL formula into a TGTA "
<< " -TGTA Translate an LTL formula into a TGTA"
<< "(Transition-based Generalised Testing Automata)" << "(Transition-based Generalised Testing Automata)"
<< std::endl; << std::endl;
@ -1097,24 +1098,25 @@ main(int argc, char** argv)
break; break;
} }
//TA //TA, STA, GTA, SGTA and TGTA
spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0); if (ta_opt || tgta_opt)
bdd atomic_props_set_bdd = bdd_true();
for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i
!= aps->end(); ++i)
{ {
bdd atomic_prop = bdd_ithvar( spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0);
(a->get_dict())->var_map[*i]);
atomic_props_set_bdd &= atomic_prop; bdd atomic_props_set_bdd = bdd_true();
for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i
!= aps->end(); ++i)
{
bdd atomic_prop = bdd_ithvar((a->get_dict())->var_map[*i]);
} atomic_props_set_bdd &= atomic_prop;
delete aps;
if (ta_opt) }
{ delete aps;
spot::ta* testing_automata = 0;
if (ta_opt)
{
spot::ta* testing_automata = 0;
testing_automata testing_automata
= tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt = tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt
@ -1122,54 +1124,55 @@ main(int argc, char** argv)
opt_single_pass_emptiness_check, opt_single_pass_emptiness_check,
opt_with_artificial_livelock); opt_with_artificial_livelock);
spot::ta* testing_automata_nm = 0; spot::ta* testing_automata_nm = 0;
if (opt_minimize) if (opt_minimize)
{
testing_automata_nm = testing_automata;
testing_automata = minimize_ta(testing_automata);
}
if (output != -1)
{
tm.start("producing output");
switch (output)
{ {
case 0: testing_automata_nm = testing_automata;
spot::dotty_reachable(std::cout, testing_automata); testing_automata = minimize_ta(testing_automata);
break;
case 12:
stats_reachable(testing_automata).dump(std::cout);
break;
default:
assert(!"unknown output option");
} }
tm.stop("producing output");
if (output != -1)
{
tm.start("producing output");
switch (output)
{
case 0:
spot::dotty_reachable(std::cout, testing_automata);
break;
case 12:
stats_reachable(testing_automata).dump(std::cout);
break;
default:
assert(!"unknown output option");
}
tm.stop("producing output");
}
delete testing_automata_nm;
delete testing_automata;
a = 0;
degeneralized = 0;
if (degeneralize_opt != DegenSBA)
to_free = 0;
aut_red = 0;
output = -1;
} }
if (tgta_opt)
delete testing_automata_nm;
delete testing_automata;
a = 0;
degeneralized = 0;
if (degeneralize_opt != DegenSBA)
to_free = 0;
aut_red = 0;
output = -1;
} else if (tgta_opt)
{
spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd);
if (opt_minimize)
{ {
a = minimize_tgta(tgta); spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd);
minimized = a; if (opt_minimize)
} {
else a = minimize_tgta(tgta);
{ minimized = a;
a = tgta; }
} else
{
a = tgta;
}
to_free = tgta; to_free = tgta;
}
} }
spot::tgba* product_degeneralized = 0; spot::tgba* product_degeneralized = 0;