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

* src/bin/ltl2tgta.cc: Simplify using spot::translator().

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-10-22 17:55:29 +02:00
parent 9dd59f1974
commit d415a23804
1 changed files with 10 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/bin/ltl2tgta.cc
View file

@ -36,7 +36,7 @@
#include "ltlvisit/simplify.hh" #include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/postproc.hh" #include "tgbaalgos/translate.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "taalgos/tgba2ta.hh" #include "taalgos/tgba2ta.hh"
@ -159,12 +159,10 @@ namespace
class trans_processor: public job_processor class trans_processor: public job_processor
{ {
public: public:
spot::ltl::ltl_simplifier& simpl; spot::translator& trans;
spot::postprocessor& post;
trans_processor(spot::ltl::ltl_simplifier& simpl, trans_processor(spot::translator& trans)
spot::postprocessor& post) : trans(trans)
: simpl(simpl), post(post)
{ {
} }
@ -172,12 +170,7 @@ namespace
process_formula(const spot::ltl::formula* f, process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0) const char* filename = 0, int linenum = 0)
{ {
const spot::ltl::formula* res = simpl.simplify(f); const spot::tgba* aut = trans.run(&f);
f->destroy();
f = res;
// This helps ltl_to_tgba_fm() to order BDD variables in a more
// natural way (improving the degeneralization).
simpl.clear_as_bdd_cache();
// This should not happen, because the parser we use can only // This should not happen, because the parser we use can only
// read PSL/LTL formula, but since our ltl::formula* type can // read PSL/LTL formula, but since our ltl::formula* type can
@ -191,10 +184,6 @@ namespace
s.c_str()); s.c_str());
} }
bool exprop = level == spot::postprocessor::High;
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
aut = post.run(aut, f);
if (utf8) if (utf8)
{ {
spot::tgba* a = const_cast<spot::tgba*>(aut); spot::tgba* a = const_cast<spot::tgba*>(aut);
@ -264,14 +253,12 @@ main(int argc, char** argv)
error(2, 0, "No formula to translate? Run '%s --help' for usage.", error(2, 0, "No formula to translate? Run '%s --help' for usage.",
program_name); program_name);
spot::ltl::ltl_simplifier simpl(simplifier_options()); spot::translator trans(&extra_options);
trans.set_pref(pref | comp);
trans.set_type(type);
trans.set_level(level);
spot::postprocessor postproc(&extra_options); trans_processor processor(trans);
postproc.set_pref(pref | comp);
postproc.set_type(type);
postproc.set_level(level);
trans_processor processor(simpl, postproc);
if (processor.run()) if (processor.run())
return 2; return 2;
return 0; return 0;