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 5156ac1286
commit 8c6b1d90c6
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/tl/derive.hh>
#include <spot/tl/expansions.hh>
#include <spot/tl/expansions2.hh>
#include <spot/tl/nenoform.hh>
#include <iostream>
@ -45,7 +46,11 @@ namespace spot
return derive_finite_automaton_with_first(f, dict);
// 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
@ -515,12 +520,14 @@ namespace spot
pref = 1;
else if (!strcasecmp(version, "lf"))
pref = 2;
else if (!strcasecmp(version, "lft"))
pref = 3;
else
{
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)
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);
}
}