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

translate: add a branch-post option

Browse source 
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Here.
* NEWS, bin/spot-x.cc: Mention it.
* tests/core/genltl.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2022-09-22 15:44:18 +02:00
parent 7ed62f7eed
commit 3729dfad90
5 changed files with 29 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -159,6 +159,11 @@ New in spot 2.10.6.dev (not yet released)
further simplification. This was introduced to help with automata further simplification. This was introduced to help with automata
produced from formulas output by "genltl --eil-gsi" (see above). produced from formulas output by "genltl --eil-gsi" (see above).
- spot::postproc has new configuration variable branch-post that
can be used to control the use of branching-postponement (diabled
by default) or delayed-branching (see above, enabled by default).
See the spot-x(7) man page for details.
- spot::parallel_policy is an object that can be passed to some - spot::parallel_policy is an object that can be passed to some
algorithm to specify how many threads can be used if Spot has been algorithm to specify how many threads can be used if Spot has been
compiled with --enable-pthread. Currently, only compiled with --enable-pthread. Currently, only

5
bin/spot-x.cc
View file

@ -50,6 +50,11 @@ implication checks for formula simplifications. Defaults to 64.") },
{ nullptr, 0, nullptr, 0, "Translation options:", 0 }, { nullptr, 0, nullptr, 0, "Translation options:", 0 },
{ DOC("ltl-split", "Set to 0 to disable the translation of automata \ { DOC("ltl-split", "Set to 0 to disable the translation of automata \
as product or sum of subformulas.") }, as product or sum of subformulas.") },
{ DOC("branch-prop", "Set to 0 to disable branching-postponement \
(done during translation, may create more states) and delayed-branching \
(almost similar, but done after translation to only remove states). \
Set to 1 to force branching-postponement, and to 2 \
to force delayed-branching. By default delayed-branching is used.") },
{ DOC("comp-susp", "Set to 1 to enable compositional suspension, \ { DOC("comp-susp", "Set to 1 to enable compositional suspension, \
as described in our SPIN'13 paper (see Bibliography below). Set to 2, \ as described in our SPIN'13 paper (see Bibliography below). Set to 2, \
to build only the skeleton TGBA without composing it. Set to 0 (the \ to build only the skeleton TGBA without composing it. Set to 0 (the \

13
spot/twaalgos/translate.cc
View file

@ -65,6 +65,7 @@ namespace spot
int tls_max_states = opt->get("tls-max-states", 64); int tls_max_states = opt->get("tls-max-states", 64);
tls_max_states_ = std::max(0, tls_max_states); tls_max_states_ = std::max(0, tls_max_states);
exprop_ = opt->get("exprop", -1); exprop_ = opt->get("exprop", -1);
branchpost_ = opt->get("branch-post", -1);
} }
void translator::build_simplifier(const bdd_dict_ptr& dict) void translator::build_simplifier(const bdd_dict_ptr& dict)
@ -399,10 +400,18 @@ namespace spot
bool exprop = unambiguous bool exprop = unambiguous
|| (level_ == postprocessor::High && exprop_ != 0) || (level_ == postprocessor::High && exprop_ != 0)
|| exprop_ > 0; || exprop_ > 0;
// branch-post: 1 == force branching postponement
// 0 == disable branching post. and delay_branching
// 2 == force delay_branching
// -1 == auto (delay_branching)
// Some quick experiments suggests that branching postponement
// can produce larger automata on non-obligations formulas, and
// that even on obligation formulas, delay_branching is faster.
bool bpost = branchpost_ == 1;
aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop, aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
true, false, false, nullptr, nullptr, true, bpost, false, nullptr, nullptr,
unambiguous); unambiguous);
if (delay_branching_here(aut)) if (!bpost && branchpost_ != 0 && delay_branching_here(aut))
{ {
aut->purge_unreachable_states(); aut->purge_unreachable_states();
aut->merge_edges(); aut->merge_edges();

3
spot/twaalgos/translate.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement // Copyright (C) 2013-2018, 2020, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -154,6 +154,7 @@ namespace spot
bool gf_guarantee_ = true; bool gf_guarantee_ = true;
bool gf_guarantee_set_ = false; bool gf_guarantee_set_ = false;
bool ltl_split_; bool ltl_split_;
int branchpost_ = -1;
unsigned tls_max_states_ = 0; unsigned tls_max_states_ = 0;
int exprop_; int exprop_;
const option_map* opt_; const option_map* opt_;

7
tests/core/genltl.test
View file

@ -280,7 +280,8 @@ diff range1.ltl range2.ltl
# I introduced delay_branching_here(), a cheap function that is called # I introduced delay_branching_here(), a cheap function that is called
# before simplification. In this case, this is enough to determinize # before simplification. In this case, this is enough to determinize
# the automaton, simplifying simulation-based reduction greatly. # the automaton, simplifying simulation-based reduction greatly.
genltl --eil-gsi=1..25 | ltlfilt --from-ltlf | ltl2tgba --stats=%s,%e >output genltl --eil-gsi=1..25 | ltlfilt --from-ltlf > formulas.ltl
ltl2tgba -F formulas.ltl --stats=%s,%e >output
cat >expected <<EOF cat >expected <<EOF
5,9 5,9
7,15 7,15
@ -309,3 +310,7 @@ cat >expected <<EOF
53,153 53,153
EOF EOF
diff expected output diff expected output
# branching postponement should work as well
ltl2tgba -F formulas.ltl -x branch-post=1 --stats=%s,%e >output
diff expected output