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

degen: add a lowinit option

Browse source 
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New argument
to disable the "jump to the accepting level if the entering
state as an accepting self-loop" optimization.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Check
the degen-lowinit option and pass it on to degeneralize().
* src/bin/spot-x.cc: Document it.
* src/tgbatest/degenlskip.test: Add some tests.
* src/tgbatest/ltl2ta.test: Update value.  We output less
accepting states now.
This commit is contained in:
Alexandre Duret-Lutz 2015-04-01 16:25:23 +02:00
parent 6e8170e386
commit 7bb183b929
7 changed files with 149 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/bin/spot-x.cc
View file

@ -83,6 +83,12 @@ states. A consequence of skipping levels is that the degeneralized \
automaton tends to have smaller cycles around the accepting states. \
Disabling skipping will produce automata with large cycles, and often \
with more states.") },
{ DOC("degen-lowinit", "Whenever the degeneralization algorihm enters \
a new SCC (or starts from the initial states), it starts on a level that \
is compatible with all outgoing transitions. If degen-lowinit is zero \
(the default) and the corresponding state (in the generalized automaton) \
has an accepting self-loop, then the level is set to the accepting \
level, as it might favor finding accepting cycles earlier.") },
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
simulation. Set to 3 to iterate both direct and reverse simulations. \

13
src/tgbaalgos/degen.cc
View file

@ -192,7 +192,7 @@ namespace spot
tgba_digraph_ptr
degeneralize_aux(const const_tgba_digraph_ptr& a, bool use_z_lvl,
bool use_cust_acc_orders, int use_lvl_cache,
bool skip_levels)
bool skip_levels, bool ignaccsl)
{
if (!a->acc().is_generalized_buchi())
throw std::runtime_error
@ -265,7 +265,7 @@ namespace spot
// As a heuristic for building SBA, if the initial state has at
// least one accepting self-loop, start the degeneralization on
// the accepting level.
if (want_sba && outgoing.has_acc_selfloop(s.first))
if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first))
s.second = order.size();
// Otherwise, check for acceptance conditions common to all
// outgoing transitions, and assume we have already seen these and
@ -443,6 +443,7 @@ namespace spot
// self-loop, start the degeneralization on
// the accepting level.
if (s_scc != scc
&& !ignaccsl
&& outgoing.has_acc_selfloop(d.first))
{
d.second = order.size();
@ -553,7 +554,7 @@ namespace spot
tgba_digraph_ptr
degeneralize(const const_tgba_digraph_ptr& a,
bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
int use_lvl_cache, bool skip_levels, bool ignaccsl)
{
// If this already a degeneralized digraph, there is nothing we
// can improve.
@ -561,13 +562,13 @@ namespace spot
return std::const_pointer_cast<tgba_digraph>(a);
return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
use_lvl_cache, skip_levels);
use_lvl_cache, skip_levels, ignaccsl);
}
tgba_digraph_ptr
degeneralize_tba(const const_tgba_digraph_ptr& a,
bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
int use_lvl_cache, bool skip_levels, bool ignaccsl)
{
// If this already a degeneralized digraph, there is nothing we
// can improve.
@ -575,6 +576,6 @@ namespace spot
return std::const_pointer_cast<tgba_digraph>(a);
return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
use_lvl_cache, skip_levels);
use_lvl_cache, skip_levels, ignaccsl);
}
}

14
src/tgbaalgos/degen.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2012, 2013, 2014 2015, Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -39,7 +39,9 @@ namespace spot
/// is entered on a state that as already been associated to some
/// level elsewhere, reuse that level (set it to 2 to keep the
/// smallest number, 3 to keep the largest level, and 1 to keep the
/// first level found).
/// first level found). If \a ignaccsl is set, we do not directly
/// jump to the accepting level if the entering state has an
/// accepting self-loop.
///
/// Any of these three options will cause the SCCs of the automaton
/// \a a to be computed prior to its actual degeneralization.
@ -51,12 +53,14 @@ namespace spot
degeneralize(const const_tgba_digraph_ptr& a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
int use_lvl_cache = 1,
bool skip_levels = true);
bool skip_levels = true,
bool ignaccsl = false);
SPOT_API tgba_digraph_ptr
degeneralize_tba(const const_tgba_digraph_ptr& a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
int use_lvl_cache = 1,
bool skip_levels = true);
bool skip_levels = true,
bool ignaccsl = false);
/// \@}
}

7
src/tgbaalgos/postproc.cc
View file

@ -51,7 +51,8 @@ namespace spot
postprocessor::postprocessor(const option_map* opt)
: type_(TGBA), pref_(Small), level_(High),
degen_reset_(true), degen_order_(false), degen_cache_(true),
degen_lskip_(true), simul_(-1), scc_filter_(-1), ba_simul_(-1),
degen_lskip_(true), degen_lowinit_(false), simul_(-1),
scc_filter_(-1), ba_simul_(-1),
tba_determinisation_(false), sat_minimize_(0), sat_acc_(0),
sat_states_(0), state_based_(false), wdba_minimize_(true)
{
@ -61,6 +62,7 @@ namespace spot
degen_reset_ = opt->get("degen-reset", 1);
degen_cache_ = opt->get("degen-lcache", 1);
degen_lskip_ = opt->get("degen-lskip", 1);
degen_lowinit_ = opt->get("degen-lowinit", 0);
simul_ = opt->get("simul", -1);
scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
@ -125,7 +127,8 @@ namespace spot
{
auto d = degeneralize(a,
degen_reset_, degen_order_,
degen_cache_, degen_lskip_);
degen_cache_, degen_lskip_,
degen_lowinit_);
if (ba_simul_ <= 0)
return d;
return do_ba_simul(d, ba_simul_);

1
src/tgbaalgos/postproc.hh
View file

@ -115,6 +115,7 @@ namespace spot
bool degen_order_;
int degen_cache_;
bool degen_lskip_;
bool degen_lowinit_;
int simul_;
int scc_filter_;
int ba_simul_;

58
src/tgbatest/degenlskip.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -28,6 +28,8 @@ set -e
../../bin/ltl2tgba -B 'GFa & GFb' --hoa > out1
../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' --hoa > out2
../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' --hoa > out3
../../bin/ltl2tgba -B -x degen-lskip=1,degen-lowinit=1 'GFa & GFb' --hoa > out4
../../bin/ltl2tgba -B -x degen-lskip=0,degen-lowinit=1 'GFa & GFb' --hoa > out5
diff out1 out2
cmp out2 out3 && exit 1
@ -78,5 +80,55 @@ State: 2
--END--
EOF
run 0 ../../bin/autfilt -F out2 --isomorph expected2
run 0 ../../bin/autfilt -F out3 --isomorph expected3
cat <<EOF >expected4
HOA: v1
name: "G(Fa & Fb)"
States: 3
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[0&1] 0
[!1] 1
[!0&1] 2
State: 1
[0&1] 0
[!1] 1
[!0&1] 2
State: 2
[0] 0
[!0] 2
--END--
EOF
cat <<EOF >expected5
HOA: v1
name: "G(Fa & Fb)"
States: 3
Start: 2
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 2
State: 1
[0] 0
[!0] 1
State: 2
[1] 1
[!1] 2
--END--
EOF
run 0 ../../bin/autfilt -q -F out2 --isomorph expected2
run 0 ../../bin/autfilt -q -F out3 --isomorph expected3
cat out4 out5
../../bin/autfilt -q out4 --isomorph expected2 && exit 1
../../bin/autfilt -q out5 --isomorph expected3 && exit 1
../../bin/autfilt -q out4 --isomorph expected4
../../bin/autfilt -q out5 --isomorph expected5

132
src/tgbatest/ltl2ta.test
View file

@ -124,16 +124,16 @@ in: a | b | (c U (d & (g U (h ^ i))))
-TA -sp -RT | 127 | 16342 | 1
-TA -lv -sp | 431 | 56744 | 129
-TA -lv -sp -RT | 128 | 16342 | 2
-TA -DS | 430 | 51816 | 342
-TA -DS -RT | 127 | 15478 | 120
-TA -DS -lv | 431 | 56744 | 247
-TA -DS -lv -RT | 128 | 16342 | 120
-TA -DS -sp | 430 | 56744 | 246
-TA -DS -sp -RT | 127 | 16342 | 119
-TA -DS -lv -sp | 431 | 56744 | 247
-TA -DS -lv -sp -RT | 128 | 16342 | 120
-x -TA -DS -in | 431 | 56744 | 247
-x -TA -DS -in -RT | 128 | 16342 | 120
-TA -DS | 430 | 51816 | 328
-TA -DS -RT | 127 | 15478 | 106
-TA -DS -lv | 431 | 56744 | 129
-TA -DS -lv -RT | 128 | 16342 | 2
-TA -DS -sp | 430 | 56744 | 128
-TA -DS -sp -RT | 127 | 16342 | 1
-TA -DS -lv -sp | 431 | 56744 | 129
-TA -DS -lv -sp -RT | 128 | 16342 | 2
-x -TA -DS -in | 431 | 56744 | 129
-x -TA -DS -in -RT | 128 | 16342 | 2
in: a & (b U !a) & (b U !a)
-TGTA | 8 | 30 | XXX
-TGTA -RT | 4 | 14 | XXX
@ -145,16 +145,16 @@ in: a & (b U !a) & (b U !a)
-TA -sp -RT | 3 | 10 | 1
-TA -lv -sp | 8 | 22 | 5
-TA -lv -sp -RT | 4 | 10 | 2
-TA -DS | 7 | 20 | 7
-TA -DS -RT | 3 | 8 | 3
-TA -DS -lv | 8 | 22 | 6
-TA -DS -lv -RT | 4 | 10 | 3
-TA -DS -sp | 7 | 22 | 5
-TA -DS -sp -RT | 3 | 10 | 2
-TA -DS -lv -sp | 8 | 22 | 6
-TA -DS -lv -sp -RT | 4 | 10 | 3
-x -TA -DS -in | 8 | 22 | 6
-x -TA -DS -in -RT | 4 | 10 | 3
-TA -DS | 7 | 20 | 6
-TA -DS -RT | 3 | 8 | 2
-TA -DS -lv | 8 | 22 | 5
-TA -DS -lv -RT | 4 | 10 | 2
-TA -DS -sp | 7 | 22 | 4
-TA -DS -sp -RT | 3 | 10 | 1
-TA -DS -lv -sp | 8 | 22 | 5
-TA -DS -lv -sp -RT | 4 | 10 | 2
-x -TA -DS -in | 8 | 22 | 5
-x -TA -DS -in -RT | 4 | 10 | 2
in: Fa & b & GFc & Gd
-TGTA | 21 | 219 | XXX
-TGTA -RT | 7 | 71 | XXX
@ -166,16 +166,16 @@ in: Fa & b & GFc & Gd
-TA -sp -RT | 10 | 106 | 1
-TA -lv -sp | 21 | 203 | 5
-TA -lv -sp -RT | 11 | 112 | 2
-TA -DS | 28 | 294 | 18
-TA -DS -RT | 12 | 126 | 8
-TA -DS -lv | 29 | 315 | 17
-TA -DS -lv -RT | 13 | 140 | 8
-TA -DS -sp | 28 | 309 | 16
-TA -DS -sp -RT | 12 | 137 | 7
-TA -DS -lv -sp | 29 | 315 | 17
-TA -DS -lv -sp -RT | 13 | 140 | 8
-x -TA -DS -in | 29 | 254 | 13
-x -TA -DS -in -RT | 12 | 96 | 7
-TA -DS | 28 | 294 | 15
-TA -DS -RT | 12 | 126 | 5
-TA -DS -lv | 29 | 315 | 13
-TA -DS -lv -RT | 13 | 140 | 4
-TA -DS -sp | 28 | 309 | 12
-TA -DS -sp -RT | 12 | 137 | 3
-TA -DS -lv -sp | 29 | 315 | 13
-TA -DS -lv -sp -RT | 13 | 140 | 4
-x -TA -DS -in | 29 | 254 | 9
-x -TA -DS -in -RT | 12 | 96 | 3
in: Fa & a & GFc & Gc
-TGTA | 4 | 8 | XXX
-TGTA -RT | 3 | 6 | XXX
@ -189,14 +189,14 @@ in: Fa & a & GFc & Gc
-TA -lv -sp -RT | 2 | 2 | 1
-TA -DS | 3 | 3 | 3
-TA -DS -RT | 2 | 2 | 2
-TA -DS -lv | 3 | 3 | 3
-TA -DS -lv -RT | 2 | 2 | 2
-TA -DS -sp | 3 | 3 | 3
-TA -DS -sp -RT | 2 | 2 | 2
-TA -DS -lv -sp | 3 | 3 | 3
-TA -DS -lv -sp -RT | 2 | 2 | 2
-x -TA -DS -in | 3 | 3 | 3
-x -TA -DS -in -RT | 2 | 2 | 2
-TA -DS -lv | 3 | 3 | 2
-TA -DS -lv -RT | 2 | 2 | 1
-TA -DS -sp | 3 | 3 | 2
-TA -DS -sp -RT | 2 | 2 | 1
-TA -DS -lv -sp | 3 | 3 | 2
-TA -DS -lv -sp -RT | 2 | 2 | 1
-x -TA -DS -in | 3 | 3 | 2
-x -TA -DS -in -RT | 2 | 2 | 1
in: Fc & (a | b) & GF(a | b) & Gc
-TGTA | 8 | 34 | XXX
-TGTA -RT | 8 | 34 | XXX
@ -210,14 +210,14 @@ in: Fc & (a | b) & GF(a | b) & Gc
-TA -lv -sp -RT | 7 | 21 | 3
-TA -DS | 11 | 51 | 10
-TA -DS -RT | 11 | 51 | 10
-TA -DS -lv | 11 | 51 | 10
-TA -DS -lv -RT | 11 | 51 | 10
-TA -DS -sp | 11 | 51 | 10
-TA -DS -sp -RT | 11 | 51 | 10
-TA -DS -lv -sp | 11 | 51 | 10
-TA -DS -lv -sp -RT | 11 | 51 | 10
-x -TA -DS -in | 11 | 33 | 8
-x -TA -DS -in -RT | 11 | 33 | 8
-TA -DS -lv | 11 | 51 | 7
-TA -DS -lv -RT | 11 | 51 | 7
-TA -DS -sp | 11 | 51 | 7
-TA -DS -sp -RT | 11 | 51 | 7
-TA -DS -lv -sp | 11 | 51 | 7
-TA -DS -lv -sp -RT | 11 | 51 | 7
-x -TA -DS -in | 11 | 33 | 5
-x -TA -DS -in -RT | 11 | 33 | 5
in: a R (b R c)
-TGTA | 17 | 124 | XXX
-TGTA -RT | 6 | 30 | XXX
@ -337,16 +337,16 @@ in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))
-TA -sp -RT | 16 | 70 | 3
-TA -lv -sp | 21 | 104 | 6
-TA -lv -sp -RT | 17 | 75 | 4
-TA -DS | 20 | 92 | 14
-TA -DS -RT | 18 | 81 | 13
-TA -DS -lv | 21 | 104 | 11
-TA -DS -lv -RT | 20 | 99 | 11
-TA -DS -sp | 20 | 100 | 10
-TA -DS -sp -RT | 19 | 95 | 10
-TA -DS -lv -sp | 21 | 104 | 11
-TA -DS -lv -sp -RT | 20 | 99 | 11
-x -TA -DS -in | 19 | 66 | 9
-x -TA -DS -in -RT | 15 | 52 | 9
-TA -DS | 20 | 92 | 13
-TA -DS -RT | 18 | 81 | 12
-TA -DS -lv | 21 | 104 | 7
-TA -DS -lv -RT | 20 | 99 | 7
-TA -DS -sp | 20 | 100 | 6
-TA -DS -sp -RT | 19 | 95 | 6
-TA -DS -lv -sp | 21 | 104 | 7
-TA -DS -lv -sp -RT | 20 | 99 | 7
-x -TA -DS -in | 19 | 66 | 5
-x -TA -DS -in -RT | 15 | 52 | 5
in: GFa & GFb & GFc & GFd & GFe & GFg
-TGTA | 65 | 4160 | XXX
-TGTA -RT | 65 | 4160 | XXX
@ -379,16 +379,16 @@ in: Gq|Gr|(G(q|FGp)&G(r|FG!p))
-TA -sp -RT | 22 | 280 | 6
-TA -lv -sp | 65 | 776 | 15
-TA -lv -sp -RT | 23 | 288 | 7
-TA -DS | 64 | 740 | 36
-TA -DS -RT | 26 | 366 | 22
-TA -DS -lv | 65 | 776 | 33
-TA -DS -lv -RT | 27 | 396 | 21
-TA -DS -sp | 64 | 764 | 32
-TA -DS -sp -RT | 26 | 386 | 20
-TA -DS -lv -sp | 65 | 776 | 33
-TA -DS -lv -sp -RT | 27 | 396 | 21
-x -TA -DS -in | 33 | 152 | 25
-x -TA -DS -in -RT | 21 | 112 | 17
-TA -DS | 64 | 740 | 34
-TA -DS -RT | 26 | 366 | 20
-TA -DS -lv | 65 | 776 | 25
-TA -DS -lv -RT | 27 | 396 | 13
-TA -DS -sp | 64 | 764 | 24
-TA -DS -sp -RT | 26 | 386 | 12
-TA -DS -lv -sp | 65 | 776 | 25
-TA -DS -lv -sp -RT | 27 | 396 | 13
-x -TA -DS -in | 33 | 152 | 19
-x -TA -DS -in -RT | 21 | 112 | 11
in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)
-TGTA | 45 | 730 | XXX
-TGTA -RT | 35 | 598 | XXX