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

translate_aa: expose lf-trans option

Browse source 
* spot/twaalgos/translate_aa.cc:
This commit is contained in:
Antoine Martin 2025-10-15 14:24:08 +02:00
parent 514ef110f2
commit fbb5675986
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/twaalgos/translate_aa.cc
View file

@ -26,6 +26,7 @@
#include <spot/twaalgos/translate_aa.hh> #include <spot/twaalgos/translate_aa.hh>
#include <spot/tl/derive.hh> #include <spot/tl/derive.hh>
#include <spot/tl/expansions.hh> #include <spot/tl/expansions.hh>
#include <spot/tl/expansions2.hh>
#include <spot/tl/nenoform.hh> #include <spot/tl/nenoform.hh>
#include <iostream> #include <iostream>
@ -45,7 +46,11 @@ namespace spot
return derive_finite_automaton_with_first(f, dict); return derive_finite_automaton_with_first(f, dict);
// linear form // linear form
return expand_finite_automaton(f, dict, exp_opts::expand_opt::None); if (sere_aa_translation_options() == 2)
return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
// linear form - trans-based
return expand_finite_automaton2(f, dict, exp_opts::expand_opt::None);
} }
struct ltl_to_aa_builder struct ltl_to_aa_builder
@ -515,12 +520,14 @@ namespace spot
pref = 1; pref = 1;
else if (!strcasecmp(version, "lf")) else if (!strcasecmp(version, "lf"))
pref = 2; pref = 2;
else if (!strcasecmp(version, "lft"))
pref = 3;
else else
{ {
const char* err = ("sere_aa_translation_options(): argument" const char* err = ("sere_aa_translation_options(): argument"
" should be one of {bdd,derive,lf}"); " should be one of {bdd,derive,lf,lft}");
if (env) if (env)
err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}"; err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,lf,lft}";
throw std::runtime_error(err); throw std::runtime_error(err);
} }
} }