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

Make sure PSL formulae are translated with the FM translation.

Browse source 
* src/tgbatest/ltl2tgba.cc: Diagnose attempt to use -l and -taa
on PSL formulae.  Switch back to -f for these formulae.
This commit is contained in:
Alexandre Duret-Lutz 2011-12-05 17:29:39 +01:00
parent 9e92267c70
commit 3dfde9e85f
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tgbatest/ltl2tgba.cc
View file

@ -826,6 +826,15 @@ main(int argc, char** argv)
std::cout << spot::ltl::to_string(f) << std::endl;
}
if (f->is_psl_formula()
&& !f->is_ltl_formula()
&& translation != TransFM)
{
std::cerr << "Only the FM algorithm can translate PSL formulae;"
<< " I'm using it for this formula." << std::endl;
translation = TransFM;
}
tm.start("translating formula");
switch (translation)
{