diff --git a/NEWS b/NEWS index 14b21c99e..45d0c958f 100644 --- a/NEWS +++ b/NEWS @@ -6,7 +6,7 @@ New in spot 2.12.0.dev (not yet released) edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. - Library: + Library: - restrict_dead_end_edges_here() can reduce non-determinism (but not remove it) by restricting the label L of some edge (S)-L->(D) @@ -14,6 +14,10 @@ New in spot 2.12.0.dev (not yet released) itself. The conditions are detailled in the documentation of this function. + - spot::postprocessor will now call restrict_dead_end_edges_here() + in its highest setting. This can be fine-tuned with the "rde" + extra option, see the spot-x (7) man page for detail. + New in spot 2.12 (2024-05-16) Build: diff --git a/bin/spot-x.cc b/bin/spot-x.cc index d29432a36..543afeac3 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -206,6 +206,12 @@ it can cause the created temporary automata to have incompatible \ combinations of atomic propositions that will be eventually be removed. \ This relabeling is attempted after relabel-bool. By default, N=8. Setting \ this value to 0 will disable the rewriting.") }, + { DOC("rde", "Disable (0), or enable (1) the 'restrict-dead-end-edges' \ +optimization. A dead-end-edge is one that move to a state that has only \ +itself as successors. The label of such edges can be simplified in some \ +situtation, reducing non-determinism slightly. By default (-1), this is \ +enabled only in --high mode, or if both --medium and --deterministic are \ +used.") }, { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization, to 1 to \ always try it, or 2 to attempt it only on syntactic obligations or on automata \ that are weak and deterministic. The default is 1 in --high mode, else 2 in \ diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index b7f6d27de..a73ce6430 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -38,6 +38,7 @@ #include #include #include +#include #include #include @@ -108,6 +109,7 @@ namespace spot wdba_det_max_ = opt->get("wdba-det-max", 4096); simul_trans_pruning_ = opt->get("simul-trans-pruning", 512); acd_ = opt->get("acd", 1); + rde_ = opt->get("rde", -1); if (sat_acc_ && sat_minimize_ == 0) sat_minimize_ = 1; // Dicho. @@ -527,6 +529,14 @@ namespace spot } } + // Restricting dead-end edges only makes sense on non-deterministic + // automata. rde_ == 0 disable this. rde_ > 0 enable it. + // By default (rde_ < 0), we only enable this on High and Medium+Det. + if (!dba && rde_ != 0 && !is_deterministic(sim) && + (rde_ > 0 || (level_ == High || + (level_ == Medium && PREF_ == Deterministic)))) + restrict_dead_end_edges_here(sim); + // If WDBA failed, but the simulation returned a deterministic // automaton, use it as dba. assert(dba || sim); diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 73da4baab..4ce6c0262 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -271,6 +271,7 @@ namespace spot int wdba_det_max_ = 4096; bool acd_ = true; bool acd_was_used_; + int rde_ = -1; }; /// @} } diff --git a/tests/core/deadends.test b/tests/core/deadends.test index 4ecb3d552..da1a4b91f 100755 --- a/tests/core/deadends.test +++ b/tests/core/deadends.test @@ -59,7 +59,8 @@ FG((Gp2 | Xp3) & (F!p2 | X!p3)) GFp0 & FGp1 & FGp2 & GFp3 EOF -ltl2tgba -F input.ltl | tee output.aut | +# disable rde so we can apply it manually +ltl2tgba -x rde=0 -F input.ltl | tee output.aut | autfilt --restrict-dead --stats="%T %t %M" | while read in out f; do : $in : $out : "$f" @@ -68,3 +69,12 @@ ltl2tgba -F input.ltl | tee output.aut | done autcross -F output.aut --language-preserved 'autfilt --restrict-dead' + +# by default, the result of ltl2tgba is already restricted +ltl2tgba -F input.ltl | + autfilt --restrict-dead --stats="%T %t %M" | + while read in out f; do + : $in : $out : "$f" + test $in -ne $out && exit 1 + : + done diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 8c0ca1dc0..c03dbc293 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -273,7 +273,7 @@ and-fg,32, $fg42, $fg42, $fg42, $fg42, $fg42, $fg42 !sb-patterns,5, 2,7, 2,7, 2,7, 2,7, 3,12, 3,12 !sb-patterns,6, 3,11, 4,14, 3,11, 4,14, 3,11, 4,14 !sb-patterns,7, 4,16, 4,16, 4,16, 4,16, 4,16, 4,16 -!sb-patterns,9, 3,13, 3,13, 4,17, 4,17, 5,21, 5,21 +!sb-patterns,9, 3,12, 3,12, 4,17, 4,17, 5,21, 5,21 !sb-patterns,10, 2,6, 2,6, 2,6, 2,6, 2,6, 2,6 !sb-patterns,11, 1,0, 1,0, 1,0, 1,0, 1,0, 1,0 !sb-patterns,12, 1,0, 1,0, 1,0, 1,0, 1,0, 1,0 @@ -340,7 +340,7 @@ and-fg,32, $fg42, $fg42, $fg42, $fg42, $fg42, $fg42 !hkrss-patterns,53, 4,32, 4,32, 4,32, 4,32, 4,32, 4,32 !hkrss-patterns,54, 4,32, 4,32, 4,32, 4,32, 4,32, 4,32 !hkrss-patterns,55, 5,12, 6,12, 5,12, 6,12, 5,12, 6,12 -!p-patterns,2, 2,15, 2,15, 3,19, 3,19, 4,23, 4,23 +!p-patterns,2, 2,14, 2,14, 3,19, 3,19, 4,23, 4,23 !p-patterns,3, 3,41, 3,41, 3,41, 3,41, 3,41, 3,41 !p-patterns,4, 1,1, 1,1, 1,1, 1,1, 1,1, 1,1 !p-patterns,5, 2,6, 2,6, 2,6, 2,6, 2,6, 2,6 @@ -379,7 +379,7 @@ FG(a | Fb), 3,15, 3,15, 3,15, 3,15, 1,4 FG(a & Fb), 2,7, 2,7, 3,9, 3,9, 1,4 GF(a & Gb), 2,7, 2,7, 3,9, 3,9, 1,4 GF(a | Gb), 2,7, 2,7, 3,12, 3,12, 1,4 -Ge | GF(Ge & X(c & Fd)), 4,31, 4,31, 6,39, 6,39, 2,16 +Ge | GF(Ge & X(c & Fd)), 4,30, 4,30, 6,39, 6,39, 2,16 F(GF(b & Gc) | Ge), 3,22, 3,22, 4,26, 4,26, 1,8 EOF diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 77f661c40..acd935560 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -22,40 +22,43 @@ set -e cat >exp <\n", "\n", - "\n", "\n", "0->1\n", "\n", "\n", - "a | b\n", + "a\n", "\n", "\n", "\n", @@ -158,7 +158,7 @@ "\n", "\n", - "\n", "\n", "0->1\n", "\n", "\n", - "a | b\n", + "a\n", "\n", "\n", "\n", @@ -262,7 +262,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fdd801ca760> >" + " *' at 0x7f30b04c1d40> >" ] }, "execution_count": 3, @@ -345,9 +345,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.12.4" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/deadends.py b/tests/python/deadends.py index fd5f18ea3..4b19f0a98 100644 --- a/tests/python/deadends.py +++ b/tests/python/deadends.py @@ -111,7 +111,7 @@ State: 1 [0&1&2] 1 {0 1} --END--""") -a = spot.translate('GFa & (FGb | FGc) & GFc') +a = spot.translate('GFa & (FGb | FGc) & GFc', xargs='rde=0') s = a.to_str() spot.restrict_dead_end_edges_here(a) s += a.to_str()