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

option --low should disable gf-guarantee

Browse source 
Fixes #367.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Fix it.
* NEWS: Mention the change.
* tests/core/ltl2tgba2.test: Test this.
This commit is contained in:
Alexandre Duret-Lutz 2018-10-12 13:38:30 +02:00
parent 3c86f034fc
commit 58c1a968c7
4 changed files with 19 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
spot/twaalgos/translate.cc
View file

@ -36,7 +36,6 @@ namespace spot
{
comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
relabel_bool_ = tls_impl_ = -1;
gf_guarantee_ = level_ != Low;
ltl_split_ = true;
opt_ = opt;
@ -52,7 +51,12 @@ namespace spot
skel_simul_ = opt->get("skel-simul", 1);
}
tls_impl_ = opt->get("tls-impl", -1);
gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_);
int gfg = opt->get("gf-guarantee", -1);
if (gfg >= 0)
{
gf_guarantee_ = !!gfg;
gf_guarantee_set_ = true;
}
ltl_split_ = opt->get("ltl-split", 1);
}

5
spot/twaalgos/translate.hh
View file

@ -119,6 +119,8 @@ namespace spot
delete simpl_owned_;
build_simplifier(d);
}
if (!gf_guarantee_set_)
gf_guarantee_ = level != Low;
}
/// \brief Convert \a f into an automaton.
@ -149,7 +151,8 @@ namespace spot
int skel_simul_;
int relabel_bool_;
int tls_impl_;
bool gf_guarantee_;
bool gf_guarantee_ = true;
bool gf_guarantee_set_ = false;
bool ltl_split_;
const option_map* opt_;
};