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

Touch up -R3b handling.

Browse source 
* src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other
LaCIM options.
(main): Speak of "symbolic SCC pruning" instead of "deleting
unaccepting SCC", and do that right after the translation, before
degeneralization.  Also error out when -R3b is used on non
symbolic automata.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-30 09:46:46 +01:00
parent c00a80a2fc
commit 9a43a06b45
2 changed files with 39 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Touch up -R3b handling.
* src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other
LaCIM options.
(main): Speak of "symbolic SCC pruning" instead of "deleting
unaccepting SCC", and do that right after the translation, before
degeneralization. Also error out when -R3b is used on non
symbolic automata.
2010-01-29 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-01-29 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Update some text files for upcoming 0.5. Update some text files for upcoming 0.5.

42
src/tgbatest/ltl2tgba.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2007, 2008, 2009 Laboratoire de Recherche et Développement // Copyright (C) 2007, 2008, 2009, 2010 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis // Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie. // Coopératifs (SRC), Université Pierre et Marie Curie.
@ -149,6 +149,8 @@ syntax(char* prog)
<< " -r display the relation BDD, not the reachability graph" << " -r display the relation BDD, not the reachability graph"
<< std::endl << std::endl
<< " -R same as -r, but as a set" << std::endl << " -R same as -r, but as a set" << std::endl
<< " -R3b symbolically prune unaccepting SCC from BDD relation"
<< std::endl
<< std::endl << std::endl
<< "Options for Tauriainen's TAA-based algorithm (-taa):" << "Options for Tauriainen's TAA-based algorithm (-taa):"
@ -191,7 +193,6 @@ syntax(char* prog)
<< " -R2t remove transitions using delayed simulation" << " -R2t remove transitions using delayed simulation"
<< std::endl << std::endl
<< " -R3 use SCC to reduce the automata" << std::endl << " -R3 use SCC to reduce the automata" << std::endl
<< " -R3b delete unaccepting SCC directly on the BDD" << std::endl
<< " -Rd display the simulation relation" << std::endl << " -Rd display the simulation relation" << std::endl
<< " -RD display the parity game (dot format)" << std::endl << " -RD display the parity game (dot format)" << std::endl
<< std::endl << std::endl
@ -277,7 +278,7 @@ main(int argc, char** argv)
int reduc_aut = spot::Reduce_None; int reduc_aut = spot::Reduce_None;
int redopt = spot::ltl::Reduce_None; int redopt = spot::ltl::Reduce_None;
bool eltl = false; bool eltl = false;
bool delete_unaccepting_scc = false; bool symbolic_scc_pruning = false;
bool display_reduce_form = false; bool display_reduce_form = false;
bool display_rel_sim = false; bool display_rel_sim = false;
bool display_parity_game = false; bool display_parity_game = false;
@ -558,7 +559,7 @@ main(int argc, char** argv)
} }
else if (!strcmp(argv[formula_index], "-R3b")) else if (!strcmp(argv[formula_index], "-R3b"))
{ {
delete_unaccepting_scc = true; symbolic_scc_pruning = true;
} }
else if (!strcmp(argv[formula_index], "-rd")) else if (!strcmp(argv[formula_index], "-rd"))
{ {
@ -761,6 +762,28 @@ main(int argc, char** argv)
to_free = a; to_free = a;
} }
if (symbolic_scc_pruning)
{
spot::tgba_bdd_concrete* bc =
dynamic_cast<spot::tgba_bdd_concrete*>(a);
if (!bc)
{
std::cerr << ("Error: Automaton is not symbolic: cannot "
"prune SCCs symbolically.\n"
" Try -R3 instead of -R3b, or use "
"another translation.")
<< std::endl;
exit(2);
}
else
{
tm.start("reducing A_f w/ symbolic SCC pruning");
if (bc)
bc->delete_unaccepting_scc();
tm.stop("reducing A_f w/ symbolic SCC pruning");
}
}
spot::tgba_tba_proxy* degeneralized = 0; spot::tgba_tba_proxy* degeneralized = 0;
spot::tgba_sgba_proxy* state_labeled = 0; spot::tgba_sgba_proxy* state_labeled = 0;
@ -779,15 +802,6 @@ main(int argc, char** argv)
a = state_labeled = new spot::tgba_sgba_proxy(a); a = state_labeled = new spot::tgba_sgba_proxy(a);
} }
if (delete_unaccepting_scc)
{
tm.start("reducing A_f w/ SCC on BDD");
if (spot::tgba_bdd_concrete* bc =
dynamic_cast<spot::tgba_bdd_concrete*>(a))
bc->delete_unaccepting_scc();
tm.stop("reducing A_f w/ SCC on BDD");
}
spot::tgba_reduc* aut_red = 0; spot::tgba_reduc* aut_red = 0;
spot::tgba* aut_scc = 0; spot::tgba* aut_scc = 0;
if (reduc_aut != spot::Reduce_None) if (reduc_aut != spot::Reduce_None)