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

* src/tgbatest/ltl2tgba.cc (main): Fix handing of -R1q -R1t -R2q -R2t.

Browse source 
Add support for -r8/-fr8.
This commit is contained in:
Alexandre Duret-Lutz 2007-04-30 08:12:00 +00:00
parent 5d8727258d
commit eb6bde4dd4
3 changed files with 34 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2007-04-30 Alexandre Duret-Lutz <adl@gnu.org>
* src/tgbatest/ltl2tgba.cc (main): Fix handing of -R1q -R1t -R2q -R2t.
Add support for -r8/-fr8.
* src/tgbatest/spotlbtt.test: Also check -R1q -R1t -R2q -R2t.
2007-04-29 Alexandre Duret-Lutz <adl@gnu.org> 2007-04-29 Alexandre Duret-Lutz <adl@gnu.org>
* src/ltlvisit/reduce.cc (reduce): Repeat the reduction as * src/ltlvisit/reduce.cc (reduce): Repeat the reduction as

30
src/tgbatest/ltl2tgba.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
@ -83,6 +83,7 @@ syntax(char* prog)
<< " -fr5 use -r5 (see below) at each step of FM" << std::endl << " -fr5 use -r5 (see below) at each step of FM" << std::endl
<< " -fr6 use -r6 (see below) at each step of FM" << std::endl << " -fr6 use -r6 (see below) at each step of FM" << std::endl
<< " -fr7 use -r7 (see below) at each step of FM" << std::endl << " -fr7 use -r7 (see below) at each step of FM" << std::endl
<< " -fr8 use -r8 (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
@ -106,7 +107,8 @@ syntax(char* prog)
<< " -r4 reduce formula using all above rules" << std::endl << " -r4 reduce formula using all above rules" << std::endl
<< " -r5 reduce formula using tau03" << std::endl << " -r5 reduce formula using tau03" << std::endl
<< " -r6 reduce formula using tau03+" << std::endl << " -r6 reduce formula using tau03+" << std::endl
<< " -r7 reduce formula using tau03+ and -r4" << std::endl << " -r7 reduce formula using tau03+ and -r1" << std::endl
<< " -r8 reduce formula using tau03+ and -r4" << std::endl
<< " -rd display the reduce formula" << std::endl << " -rd display the reduce formula" << std::endl
<< " -R same as -r, but as a set" << std::endl << " -R same as -r, but as a set" << std::endl
<< " -R1q merge states using direct simulation " << " -R1q merge states using direct simulation "
@ -580,16 +582,22 @@ main(int argc, char** argv)
if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim)) spot::Reduce_transition_Dir_Sim))
rel_dir = {
spot::get_direct_relation_simulation(a, rel_dir =
std::cout, spot::get_direct_relation_simulation(a,
display_parity_game); std::cout,
else if (reduc_aut & (spot::Reduce_quotient_Del_Sim | display_parity_game);
assert(rel_dir);
}
if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim)) spot::Reduce_transition_Del_Sim))
rel_del = {
spot::get_delayed_relation_simulation(a, rel_del =
std::cout, spot::get_delayed_relation_simulation(a,
display_parity_game); std::cout,
display_parity_game);
assert(rel_del);
}
if (display_rel_sim) if (display_rel_sim)
{ {

8
src/tgbatest/spotlbtt.test
View file

@ -158,6 +158,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM), pre + allpost reduction"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot './ltl2tgba -r4 -R1q -R1t -R2q -R2t -R3 -F -f -t'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), without symb_merge" Name = "Spot (Couvreur -- FM), without symb_merge"