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

* src/ltltest/formules.ltl: A pattern of 2000 formulas.

Browse source 
* src/ltltest/inf.test: Test some case of implies.
* src/ltltest/inf.cc: Test some case of implies.
* src/ltltest/reduc.test: Test reduction of a file of formula.
* src/ltltest/reduc.cc: Test reduction of a formula.

* src/ltlvisit/formlength.cc: Gives the lenght of a formula.
* src/ltlvisit/forminf.cc: To know if a formula implies an other.
* src/ltlvisit/basereduc.cc: Implement only basic reduction.
* src/ltlvisit/reducform.cc: Implement reduction.
* src/ltlvisit/reducform.hh: To reduce a formula.
This commit is contained in:
martinez 2004-05-10 16:40:34 +00:00
parent bafc92d0b8
commit 61e7d4e21f
2 changed files with 31 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

14
ChangeLog
View file

@ -1,3 +1,17 @@
2004-05-10 Thomas MARTINEZ <martinez@abacus.lip6.fr>
* src/ltltest/formules.ltl: A pattern of 2000 formulas.
* src/ltltest/inf.test: Test some case of implies.
* src/ltltest/inf.cc: Test some case of implies.
* src/ltltest/reduc.test: Test reduction of a file of formula.
* src/ltltest/reduc.cc: Test reduction of a formula.
* src/ltlvisit/formlength.cc: Gives the lenght of a formula.
* src/ltlvisit/forminf.cc: To know if a formula implies an other.
* src/ltlvisit/basereduc.cc: Implement only basic reduction.
* src/ltlvisit/reducform.cc: Implement reduction.
* src/ltlvisit/reducform.hh: To reduce a formula.
2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine

18
src/tgbatest/ltl2tgba.cc
View file

@ -24,6 +24,7 @@
#include <fstream> #include <fstream>
#include <string> #include <string>
#include "ltlvisit/destroy.hh" #include "ltlvisit/destroy.hh"
#include "ltlvisit/reducform.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlparse/public.hh" #include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_lacim.hh"
@ -91,7 +92,9 @@ syntax(char* prog)
<< " -X do not compute an automaton, read it from a file" << " -X do not compute an automaton, read it from a file"
<< std::endl << std::endl
<< " -y do not merge states with same symbolic representation " << " -y do not merge states with same symbolic representation "
<< "(implies -f)" << std::endl; << "(implies -f)" << std::endl
<< " -z to reduce formula "
<< std::endl;
exit(2); exit(2);
} }
@ -113,6 +116,7 @@ main(int argc, char** argv)
bool magic_many = false; bool magic_many = false;
bool expect_counter_example = false; bool expect_counter_example = false;
bool from_file = false; bool from_file = false;
bool reduc = false;
bool post_branching = false; bool post_branching = false;
bool fair_loop_approx = false; bool fair_loop_approx = false;
@ -250,6 +254,10 @@ main(int argc, char** argv)
fm_opt = true; fm_opt = true;
fm_symb_merge_opt = false; fm_symb_merge_opt = false;
} }
else if (!strcmp(argv[formula_index], "-z"))
{
reduc = true;
}
else else
{ {
break; break;
@ -312,6 +320,9 @@ main(int argc, char** argv)
} }
else else
{ {
spot::ltl::formula* ftmp = f;
if (reduc)
f = spot::ltl::reduce(f);
if (fm_opt) if (fm_opt)
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,
@ -319,6 +330,11 @@ main(int argc, char** argv)
fair_loop_approx); fair_loop_approx);
else else
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
if (reduc)
spot::ltl::destroy(ftmp);
spot::ltl::destroy(f);
} }
spot::tgba_tba_proxy* degeneralized = 0; spot::tgba_tba_proxy* degeneralized = 0;