Overhaul LaCIM's ELTL options.
* src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select this algorithm and -lo to add the default LTL operators. This replace the undocumented hack to add LTL operators when the formula with read for command-line, or the automaton was output for LBTT. * src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update call syntax. * NEWS: Mention -le, -lo, and -taa.
This commit is contained in:
Alexandre Duret-Lutz
parent
9a43a06b45
commit
369e4c419b
5 changed files with 103 additions and 67 deletions
13
ChangeLog
13
ChangeLog
|
|
@ -1,3 +1,16 @@
|
|||
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Overhaul LaCIM's ELTL options.
|
||||
|
||||
* src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select
|
||||
this algorithm and -lo to add the default LTL operators. This
|
||||
replace the undocumented hack to add LTL operators when the
|
||||
formula with read for command-line, or the automaton was output
|
||||
for LBTT.
|
||||
* src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update
|
||||
call syntax.
|
||||
* NEWS: Mention -le, -lo, and -taa.
|
||||
|
||||
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Touch up -R3b handling.
|
||||
|
|
|
|||
12
NEWS
12
NEWS
|
|
@ -8,13 +8,15 @@ New in spot 0.5 (2010-01-31):
|
|||
to Spot. You may subscribe at
|
||||
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
|
||||
* Two new LTL translations have been implemented:
|
||||
- eltl_to_tgba_lacim() is a symbolic translation for ELTL based
|
||||
on Couvreur's LaCIM'00 paper. For this translation, all operators
|
||||
are described as finite automata. A default set of operators is
|
||||
provided for LTL and user may add more automaton operators.
|
||||
- eltl_to_tgba_lacim() is a symbolic translation for ELTL based on
|
||||
Couvreur's LaCIM'00 paper. For this translation (available with
|
||||
ltl2tgba's option -le), all operators are described as finite
|
||||
automata. A default set of operators is provided for LTL
|
||||
(option -lo) and user may add more automaton operators.
|
||||
- ltl_to_taa() is a translation based on Tauriainen's PhD thesis.
|
||||
LTL is translated to "self-loop" alternating automata
|
||||
and then to Transition-based Generalized Automata.
|
||||
and then to Transition-based Generalized Automata. (ltl2tgba's
|
||||
option -taa).
|
||||
The "Couvreur/FM" translation remains the best LTL translation
|
||||
available in Spot.
|
||||
* The data structures used to represent LTL formulae have been
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ set -e
|
|||
# Check if the TGBA was corretly constructed.
|
||||
check_construct()
|
||||
{
|
||||
run 0 ../ltl2tgba -F -l -xltl -b "$1" > output
|
||||
run 0 ../ltl2tgba -F -le -b "$1" > output
|
||||
}
|
||||
|
||||
# Check if the TGBA behaves correctly by doing an emptiness check on
|
||||
|
|
|
|||
|
|
@ -83,15 +83,15 @@ syntax(char* prog)
|
|||
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
||||
prog = slash + 4;
|
||||
|
||||
std::cerr << "Usage: "<< prog << " [-f|-l|-taa] [OPTIONS...] formula"
|
||||
std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
|
||||
<< std::endl
|
||||
<< " "<< prog << " [-f|-l|-taa] -F [OPTIONS...] file"
|
||||
<< " "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
|
||||
<< std::endl
|
||||
<< " "<< prog << " -X [OPTIONS...] file" << std::endl
|
||||
<< std::endl
|
||||
|
||||
<< "Translate an LTL into an automaton, or read the automaton "
|
||||
<< "from a file." << std::endl
|
||||
<< "Translate an LTL formula into an automaton, or read the "
|
||||
<< "automaton from a file." << std::endl
|
||||
<< "Optionally multiply this automaton by another"
|
||||
<< " automaton read from a file." << std::endl
|
||||
<< "Output the result in various formats, or perform an emptiness "
|
||||
|
|
@ -109,12 +109,14 @@ syntax(char* prog)
|
|||
<< std::endl
|
||||
|
||||
<< "Translation algorithm:" << std::endl
|
||||
<< " -f use Couvreur's FM algorithm for translation"
|
||||
<< " -f use Couvreur's FM algorithm for LTL"
|
||||
<< std::endl
|
||||
<< " -l use Couvreur's LaCIM algorithm for translation "
|
||||
<< " -l use Couvreur's LaCIM algorithm for LTL "
|
||||
<< "(default)"
|
||||
<< std::endl
|
||||
<< " -taa use Tauriainen's TAA-based algorithm for translation"
|
||||
<< " -le use Couvreur's LaCIM algorithm for ELTL"
|
||||
<< std::endl
|
||||
<< " -taa use Tauriainen's TAA-based algorithm for LTL"
|
||||
<< std::endl
|
||||
<< std::endl
|
||||
|
||||
|
|
@ -140,12 +142,14 @@ syntax(char* prog)
|
|||
<< "(implies -f)" << std::endl
|
||||
<< std::endl
|
||||
|
||||
<< "Options for Couvreur's LaCIM algorithm (-l):" << std::endl
|
||||
<< "Options for Couvreur's LaCIM algorithm (-l or -le):"
|
||||
<< std::endl
|
||||
<< " -a display the acceptance_conditions BDD, not the "
|
||||
<< "reachability graph"
|
||||
<< std::endl
|
||||
<< " -A same as -a, but as a set" << std::endl
|
||||
<< " -xltl translate an extended LTL, not an LTL" << std::endl
|
||||
<< " -lo pre-define standard LTL operators as automata "
|
||||
<< "(implies -le)" << std::endl
|
||||
<< " -r display the relation BDD, not the reachability graph"
|
||||
<< std::endl
|
||||
<< " -R same as -r, but as a set" << std::endl
|
||||
|
|
@ -263,7 +267,8 @@ main(int argc, char** argv)
|
|||
bool paper_opt = false;
|
||||
enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
|
||||
enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
|
||||
enum { TransFM, TransLaCIM, TransTAA } translation = TransLaCIM;
|
||||
enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
|
||||
translation = TransLaCIM;
|
||||
int fm_red = spot::ltl::Reduce_None;
|
||||
bool fm_exprop_opt = false;
|
||||
bool fm_symb_merge_opt = true;
|
||||
|
|
@ -277,7 +282,6 @@ main(int argc, char** argv)
|
|||
bool from_file = false;
|
||||
int reduc_aut = spot::Reduce_None;
|
||||
int redopt = spot::ltl::Reduce_None;
|
||||
bool eltl = false;
|
||||
bool symbolic_scc_pruning = false;
|
||||
bool display_reduce_form = false;
|
||||
bool display_rel_sim = false;
|
||||
|
|
@ -376,14 +380,6 @@ main(int argc, char** argv)
|
|||
expect_counter_example = false;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-xltl"))
|
||||
{
|
||||
eltl = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-taa"))
|
||||
{
|
||||
translation = TransTAA;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-f"))
|
||||
{
|
||||
translation = TransFM;
|
||||
|
|
@ -457,6 +453,16 @@ main(int argc, char** argv)
|
|||
{
|
||||
translation = TransLaCIM;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-le"))
|
||||
{
|
||||
/* -lo is documented to imply -le, so do not overwrite it. */
|
||||
if (translation != TransLaCIM_ELTL_ops)
|
||||
translation = TransLaCIM_ELTL;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-lo"))
|
||||
{
|
||||
translation = TransLaCIM_ELTL_ops;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-L"))
|
||||
{
|
||||
fair_loop_approx = true;
|
||||
|
|
@ -589,6 +595,10 @@ main(int argc, char** argv)
|
|||
{
|
||||
use_timer = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-taa"))
|
||||
{
|
||||
translation = TransTAA;
|
||||
}
|
||||
else if (!strncmp(argv[formula_index], "-U", 2))
|
||||
{
|
||||
unobservables = new spot::ltl::atomic_prop_set;
|
||||
|
|
@ -665,9 +675,13 @@ main(int argc, char** argv)
|
|||
}
|
||||
|
||||
spot::ltl::formula* f = 0;
|
||||
if (!from_file)
|
||||
if (!from_file) // Reading a formula, not reading an automaton from a file.
|
||||
{
|
||||
if (!eltl)
|
||||
switch (translation)
|
||||
{
|
||||
case TransFM:
|
||||
case TransLaCIM:
|
||||
case TransTAA:
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
tm.start("parsing formula");
|
||||
|
|
@ -675,12 +689,22 @@ main(int argc, char** argv)
|
|||
tm.stop("parsing formula");
|
||||
exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
|
||||
}
|
||||
else if (!file_opt || output == 6)
|
||||
break;
|
||||
case TransLaCIM_ELTL:
|
||||
{
|
||||
// Call the LTL parser first to handle abbreviations such as
|
||||
// [] when the formula is not given in a file or when the
|
||||
// output in done in LBTT's format. The ELTL parser is then
|
||||
// called with usual LTL operators.
|
||||
spot::eltl::parse_error_list p;
|
||||
tm.start("parsing formula");
|
||||
f = spot::eltl::parse_string(input, p, env, false);
|
||||
tm.stop("parsing formula");
|
||||
exit_code = spot::eltl::format_parse_errors(std::cerr, p);
|
||||
}
|
||||
break;
|
||||
case TransLaCIM_ELTL_ops:
|
||||
{
|
||||
// Call the LTL parser first to handle operators such as
|
||||
// [] or <> and rewrite the output as a string with G or F.
|
||||
// Then prepend definitions of usual LTL operators, and parse
|
||||
// the result again as an ELTL formula.
|
||||
spot::ltl::parse_error_list pel;
|
||||
tm.start("parsing formula");
|
||||
f = spot::ltl::parse(input, pel, env, debug_opt);
|
||||
|
|
@ -693,13 +717,7 @@ main(int argc, char** argv)
|
|||
tm.stop("parsing formula");
|
||||
exit_code = spot::eltl::format_parse_errors(std::cerr, p);
|
||||
}
|
||||
else
|
||||
{
|
||||
spot::eltl::parse_error_list p;
|
||||
tm.start("parsing formula");
|
||||
f = spot::eltl::parse_string(input, p, env, false);
|
||||
tm.stop("parsing formula");
|
||||
exit_code = spot::eltl::format_parse_errors(std::cerr, p);
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (f || from_file)
|
||||
|
|
@ -752,9 +770,10 @@ main(int argc, char** argv)
|
|||
a = spot::ltl_to_taa(f, dict, containment);
|
||||
break;
|
||||
case TransLaCIM:
|
||||
if (!eltl)
|
||||
a = concrete = spot::ltl_to_tgba_lacim(f, dict);
|
||||
else
|
||||
break;
|
||||
case TransLaCIM_ELTL:
|
||||
case TransLaCIM_ELTL_ops:
|
||||
a = concrete = spot::eltl_to_tgba_lacim(f, dict);
|
||||
break;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003, 2004, 2005, 2006, 2007, 2009 Laboratoire
|
||||
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
|
||||
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
# Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
#
|
||||
|
|
@ -64,7 +66,7 @@ Algorithm
|
|||
{
|
||||
Name = "Spot (Couvreur -- LaCIM), eltl"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -l -t -xltl'"
|
||||
Parameters = "--spot '../ltl2tgba -F -lo -t'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
|
|
@ -72,7 +74,7 @@ Algorithm
|
|||
{
|
||||
Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3b'"
|
||||
Parameters = "--spot '../ltl2tgba -F -lo -t -R3b'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
|
|
@ -80,7 +82,7 @@ Algorithm
|
|||
{
|
||||
Name = "Spot (Couvreur -- LaCIM), eltl + post reduction with scc"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3'"
|
||||
Parameters = "--spot '../ltl2tgba -F -lo -t -R3'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue