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 68a155a818
commit 34f9fb5d68
4 changed files with 19 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -7,6 +7,9 @@ New in spot 2.6.2.dev (not yet released)
This in turn caused "ltl2tgba -U -B" to not produce unambiguous This in turn caused "ltl2tgba -U -B" to not produce unambiguous
automata. automata.
- ltl2tgba --low now disables the "gf-guarantee" feature, as
documented.
New in spot 2.6.2 (2018-09-28) New in spot 2.6.2 (2018-09-28)
Build: Build:

8
spot/twaalgos/translate.cc
View file

@ -36,7 +36,6 @@ namespace spot
{ {
comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
relabel_bool_ = tls_impl_ = -1; relabel_bool_ = tls_impl_ = -1;
gf_guarantee_ = level_ != Low;
ltl_split_ = true; ltl_split_ = true;
opt_ = opt; opt_ = opt;
@ -52,7 +51,12 @@ namespace spot
skel_simul_ = opt->get("skel-simul", 1); skel_simul_ = opt->get("skel-simul", 1);
} }
tls_impl_ = opt->get("tls-impl", -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); ltl_split_ = opt->get("ltl-split", 1);
} }

5
spot/twaalgos/translate.hh
View file

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

6
tests/core/ltl2tgba2.test
View file

@ -381,6 +381,12 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
diff formulas output diff formulas output
# Issue #367.
test 4 = `ltl2tgba 'GF(a<->XXa)' --stats=%s`
test 9 = `ltl2tgba --low 'GF(a<->XXa)' --stats=%s`
test 9 = `ltl2tgba -x gf-guarantee=0 'GF(a<->XXa)' --stats=%s`
test 4 = `ltl2tgba --low -x gf-guarantee=1 'GF(a<->XXa)' --stats=%s`
# Regression test for issue #357. The second formula used to # Regression test for issue #357. The second formula used to
# incorrectly produce 13 edges when translated after the first one # incorrectly produce 13 edges when translated after the first one
# because the transition were explored in a different order. # because the transition were explored in a different order.