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

* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add

Browse source 
the reduce_ltl argument.
* src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4.
* src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4.
* bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled
algorithms.
This commit is contained in:
Alexandre Duret-Lutz 2005-05-04 13:47:38 +00:00
parent 7ef117e3dc
commit 9063c5abb4
7 changed files with 127 additions and 201 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2005-05-04 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add
the reduce_ltl argument.
* src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4.
* src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4.
* bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled
algorithms.
2005-04-19 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-04-19 Alexandre Duret-Lutz <adl@src.lip6.fr>
* bench/ltl2tgba/README: More instructions. * bench/ltl2tgba/README: More instructions.

31
bench/ltl2tgba/algorithms
View file

@ -63,6 +63,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "FM, degen, +symb_merge, +exprop, +INpre, +post, +flapprox"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -D -F'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch" Name = "FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch"
@ -71,6 +79,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "FM, degen, +symb_merge, +exprop, +INpre, +post, +flapprox, +post_branch"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -D -p -F'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "FM, degen, +symb_merge, +exprop, +post_branch, LTLopt" Name = "FM, degen, +symb_merge, +exprop, +post_branch, LTLopt"
@ -208,6 +224,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "FM, gen, +symb_merge, +exprop, +INpre, +post, +flapprox"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -F'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch" Name = "FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch"
@ -216,6 +240,13 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "FM, gen, +symb_merge, +exprop, +INpre, +post, +flapprox, +post_branch"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -p -F'"
Enabled = yes
}
Algorithm Algorithm
{ {

2
bench/ltl2tgba/parseout.pl
View file

@ -52,7 +52,7 @@ while (<>)
if (/Pos\. formulae \|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/) if (/Pos\. formulae \|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/)
{ {
$acc = $1; $acc = $1;
$time = $2; $time = $2 || 0;
} }
next unless /Pos\. formulae \|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/; next unless /Pos\. formulae \|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/;
if ($line % 2) if ($line % 2)

28
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -637,7 +637,8 @@ namespace spot
tgba_explicit* tgba_explicit*
ltl_to_tgba_fm(const formula* f, bdd_dict* dict, ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
bool exprop, bool symb_merge, bool branching_postponement, bool exprop, bool symb_merge, bool branching_postponement,
bool fair_loop_approx, const ltl::atomic_prop_set* unobs) bool fair_loop_approx, const atomic_prop_set* unobs,
int reduce_ltl)
{ {
possible_fair_loop_checker pflc; possible_fair_loop_checker pflc;
@ -649,6 +650,14 @@ namespace spot
formula* f2 = negative_normal_form(f1); formula* f2 = negative_normal_form(f1);
destroy(f1); destroy(f1);
// Simplify the formula, if requested.
if (reduce_ltl)
{
formula* tmp = reduce(f2, reduce_ltl);
destroy(f2);
f2 = tmp;
}
typedef std::set<const formula*, formula_ptr_less_than> set_type; typedef std::set<const formula*, formula_ptr_less_than> set_type;
set_type formulae_seen; set_type formulae_seen;
set_type formulae_to_translate; set_type formulae_to_translate;
@ -675,8 +684,8 @@ namespace spot
if (unobs) if (unobs)
{ {
bdd neg_events = bddtrue; bdd neg_events = bddtrue;
std::auto_ptr<ltl::atomic_prop_set> aps(ltl::atomic_prop_collect(f)); std::auto_ptr<atomic_prop_set> aps(atomic_prop_collect(f));
for (ltl::atomic_prop_set::const_iterator i = aps->begin(); for (atomic_prop_set::const_iterator i = aps->begin();
i != aps->end(); ++i) i != aps->end(); ++i)
{ {
int p = d.register_proposition(*i); int p = d.register_proposition(*i);
@ -685,7 +694,7 @@ namespace spot
observable_events = (observable_events & neg) | (neg_events & pos); observable_events = (observable_events & neg) | (neg_events & pos);
neg_events &= neg; neg_events &= neg;
} }
for (ltl::atomic_prop_set::const_iterator i = unobs->begin(); for (atomic_prop_set::const_iterator i = unobs->begin();
i != unobs->end(); ++i) i != unobs->end(); ++i)
{ {
int p = d.register_proposition(*i); int p = d.register_proposition(*i);
@ -790,6 +799,17 @@ namespace spot
bdd dest_bdd = bdd_existcomp(cube, d.next_set); bdd dest_bdd = bdd_existcomp(cube, d.next_set);
const formula* dest = d.conj_bdd_to_formula(dest_bdd); const formula* dest = d.conj_bdd_to_formula(dest_bdd);
// Simplify the formula, if requested.
if (reduce_ltl)
{
formula* tmp = reduce(dest, reduce_ltl);
destroy(dest);
dest = tmp;
// Ignore the arc if the destination reduces to false.
if (dest == constant::false_instance())
continue;
}
// If we already know a state with the same // If we already know a state with the same
// successors, use it in lieu of the current one. // successors, use it in lieu of the current one.
if (symb_merge) if (symb_merge)

27
src/tgbaalgos/ltl2tgba_fm.hh
View file

@ -25,6 +25,7 @@
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbaexplicit.hh"
#include "ltlvisit/apcollect.hh" #include "ltlvisit/apcollect.hh"
#include "ltlvisit/reduce.hh"
namespace spot namespace spot
{ {
@ -95,12 +96,36 @@ namespace spot
/// are interpreted as events that exclude each other. The events in the /// are interpreted as events that exclude each other. The events in the
/// formula are observable events, and \c unobs can be filled with /// formula are observable events, and \c unobs can be filled with
/// additional unobservable events. /// additional unobservable events.
///
/// \param reduce_ltl If this parameter is set, the LTL formulae representing
/// each state of the automaton will be simplified using spot::ltl::reduce()
/// before computing the successor. \a reduce_ltl should specify the type
/// of reduction to apply as documented for spot::ltl::reduce().
/// This idea is taken from the following paper.
/// \verbatim
/// @InProceedings{ thirioux.02.fmics,
/// author = {Xavier Thirioux},
/// title = {Simple and Efficient Translation from {LTL} Formulas to
/// {B\"u}chi Automata},
/// booktitle = {Proceedings of the 7th International ERCIM Workshop in
/// Formal Methods for Industrial Critical Systems (FMICS'02)},
/// series = {Electronic Notes in Theoretical Computer Science},
/// volume = {66(2)},
/// publisher = {Elsevier},
/// editor = {Rance Cleaveland and Hubert Garavel},
/// year = {2002},
/// month = jul,
/// address = {M{\'a}laga, Spain}
/// }
/// \endverbatim
///
/// \return A spot::tgba_explicit that recognizes the language of \a f. /// \return A spot::tgba_explicit that recognizes the language of \a f.
tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
bool exprop = false, bool symb_merge = true, bool exprop = false, bool symb_merge = true,
bool branching_postponement = false, bool branching_postponement = false,
bool fair_loop_approx = false, bool fair_loop_approx = false,
const ltl::atomic_prop_set* unobs = 0); const ltl::atomic_prop_set* unobs = 0,
int reduce_ltl = ltl::Reduce_None);
} }
#endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH

28
src/tgbatest/ltl2tgba.cc
View file

@ -74,6 +74,10 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -f use Couvreur's FM algorithm for translation" << " -f use Couvreur's FM algorithm for translation"
<< std::endl << std::endl
<< " -fr1 use -r1 (see below) at each step of FM" << std::endl
<< " -fr2 use -r2 (see below) at each step of FM" << std::endl
<< " -fr3 use -r3 (see below) at each step of FM" << std::endl
<< " -fr4 use -r4 (see below) at each step of FM" << std::endl
<< " -F read the formula from the file" << std::endl << " -F read the formula from the file" << std::endl
<< " -g graph the accepting run on the automaton (requires -e)" << " -g graph the accepting run on the automaton (requires -e)"
<< std::endl << std::endl
@ -144,6 +148,7 @@ main(int argc, char** argv)
bool paper_opt = false; bool paper_opt = false;
enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
bool fm_opt = false; bool fm_opt = false;
int fm_red = spot::ltl::Reduce_None;
bool fm_exprop_opt = false; bool fm_exprop_opt = false;
bool fm_symb_merge_opt = true; bool fm_symb_merge_opt = true;
bool file_opt = false; bool file_opt = false;
@ -246,6 +251,26 @@ main(int argc, char** argv)
{ {
fm_opt = true; fm_opt = true;
} }
else if (!strcmp(argv[formula_index], "-fr1"))
{
fm_opt = true;
fm_red |= spot::ltl::Reduce_Basics;
}
else if (!strcmp(argv[formula_index], "-fr2"))
{
fm_opt = true;
fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
}
else if (!strcmp(argv[formula_index], "-fr3"))
{
fm_opt = true;
fm_red |= spot::ltl::Reduce_Syntactic_Implications;
}
else if (!strcmp(argv[formula_index], "-fr4"))
{
fm_opt = true;
fm_red |= spot::ltl::Reduce_All;
}
else if (!strcmp(argv[formula_index], "-F")) else if (!strcmp(argv[formula_index], "-F"))
{ {
file_opt = true; file_opt = true;
@ -472,7 +497,8 @@ main(int argc, char** argv)
to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
fm_symb_merge_opt, fm_symb_merge_opt,
post_branching, post_branching,
fair_loop_approx, unobservables); fair_loop_approx, unobservables,
fm_red);
else else
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
} }

203
src/tgbatest/spotlbtt.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
@ -100,6 +100,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM), reduction of formula in FM"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -fr4 -F -f -t'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), post reduction with direct simulation" Name = "Spot (Couvreur -- FM), post reduction with direct simulation"
@ -156,38 +164,6 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM), fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM), reduction of formula, fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -r4 -F -f -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM), without symb_merge, fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -y -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM), fake, LTL simplifications by ltl2ba"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '${srcdir}/ltl2baw.pl --spot=\"-f -T\" -F'"
Enabled = no
}
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM exprop)" Name = "Spot (Couvreur -- FM exprop)"
@ -244,167 +220,6 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM exprop + post_branch), fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -x -p -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM exprop + flapprox), fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -x -L -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM exprop + post_branch + flapprox), fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -x -p -L -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM exprop), fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -x -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM exprop), without symb_merge, fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -F -f -x -y -T'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'"
Enabled = no
}
Algorithm
{
Name = "Spin"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spin spin"
Enabled = no
}
Algorithm
{
Name = "LBT"
Path = "${LBTT_TRANSLATE}"
Parameters = "--lbt lbt"
Enabled = no
}
Algorithm
{
Name = "LTL2BA"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spin ltl2ba"
Enabled = no
}
Algorithm
{
Name = "LTL2BA, generalized fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '${srcdir}/ltl2baw.pl -F'"
Enabled = no
}
Algorithm
{
Name = "LTL2BA without LTL and SCC simplifications"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spin 'ltl2ba -l -c'"
Enabled = no
}
Algorithm
{
Name = "LTL2BA without LTL and SCC simplifications, generalized fake"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '${srcdir}/ltl2baw.pl -l -c -F'"
Enabled = no
}
Algorithm
{
Name = "Wring (GPVW)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --0'"
Enabled = no
}
Algorithm
{
Name = "Wring (GPVW+)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --1'"
Enabled = no
}
Algorithm
{
Name = "Wring (LTL2AUT)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --2'"
Enabled = no
}
Algorithm
{
Name = "Wring (Wring RewRule)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --3'"
Enabled = no
}
Algorithm
{
Name = "Wring (Wring RewRule+BoolOpt)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --4'"
Enabled = no
}
Algorithm
{
Name = "Wring (Wring RewRule+BoolOpt+AutSempl)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --5'"
Enabled = no
}
Algorithm
{
Name = "Wring (Wring BoolOpt)"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --6'"
Enabled = no
}
Algorithm
{
Name = "Wring (Wring RewRule+BoolOpt), degeneralized"
Path = "sh"
Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt -d --4'"
Enabled = no
}
GlobalOptions GlobalOptions
{ {
Rounds = 100 Rounds = 100