Commit 64aee87d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

postproc: option to wdba-minimize only when sure

Fixes #15.

* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1.  Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
parent 8744751e
......@@ -7,6 +7,17 @@ New in spot 2.9.0.dev (not yet released)
ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
now produces a 16-state automaton (instead of 31 in Spot 2.9).
- Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
Please register or sign in to reply
It can now take three values:
0: never attempt this optimization,
1: always try to determinize and minimize automata as WDBA,
and check (if needed) that the result is correct,
2: determinize and minimize automata as WDBA only if it is known
beforehand (by cheap syntactic means) that the result will be
correct (e.g., the input formula is a syntactic obligation).
The default is 1 in "--high" mode, 2 in "--medium" mode or in
"--deterministic --low" mode, and 0 in other "--low" modes.
Library:
- product_xor() and product_xnor() are two new versions of the
......
......@@ -152,8 +152,10 @@ abstracted as atomic propositions during the translation to automaton. \
This relabeling can speeds the translation if a few Boolean subformulas \
use a large number of atomic propositions. By default N=4. Setting \
this value to 0 will disable the rewriting.") },
{ DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \
Enabled by default.") },
{ 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 \
--medium or --deterministic modes, else 0 in --low mode.") },
{ DOC("tba-det", "Set to 1 to attempt a powerset determinization \
if the TGBA is not already deterministic. Doing so will degeneralize \
the automaton. This is disabled by default, unless sat-minimize is set.") },
......
// -*- coding: utf-8 -*-
// Copyright (C) 2010-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2010-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -567,6 +567,16 @@ namespace spot
return product(min_aut, aut_neg)->is_empty();
}
bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f,
formula f)
{
// WDBA-minimization necessarily work for obligations
return ((f && f.is_syntactic_obligation())
// Weak deterministic automata are obligations
|| (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
// Guarantee automata are obligations as well.
|| is_terminal_automaton(aut_f));
}
twa_graph_ptr
minimize_obligation(const const_twa_graph_ptr& aut_f,
......@@ -580,12 +590,7 @@ namespace spot
("minimize_obligation() does not support alternation");
bool minimization_will_be_correct = false;
// WDBA-minimization necessarily work for obligations
if ((f && f.is_syntactic_obligation())
// Weak deterministic automata are obligations
|| (aut_f->prop_weak() && is_deterministic(aut_f))
// Guarantee automata are obligations as well.
|| is_terminal_automaton(aut_f))
if (minimize_obligation_garanteed_to_work(aut_f, f))
{
minimization_will_be_correct = true;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018, 2019
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009-2016, 2018-2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -116,5 +116,23 @@ namespace spot
const_twa_graph_ptr aut_neg_f = nullptr,
bool reject_bigger = false,
const output_aborter* aborter = nullptr);
/// \brief Whether calling minimize_obligation is sure to work
///
/// This checks whether \a f is a syntactic obligation, or if \a
/// aut_f obviously corresponds to an obligation (for instance if
/// this is a terminal automaton, or if it is both weak and
/// deterministic). In this case, calling minimize_obligation()
/// should not be a waste of time, as it will return a new
/// automaton.
///
/// If this function returns false, the input property might still
/// be a pathological obligation. The only way to know is to call
/// minimize_obligation(), but as it is less likely, you might
/// decide to save time.
SPOT_API
bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f,
formula f = nullptr);
/// @}
}
......@@ -83,7 +83,7 @@ namespace spot
sat_acc_ = opt->get("sat-acc", 0);
sat_states_ = opt->get("sat-states", 0);
state_based_ = opt->get("state-based", 0);
wdba_minimize_ = opt->get("wdba-minimize", 1);
wdba_minimize_ = opt->get("wdba-minimize", -1);
gen_reduce_parity_ = opt->get("gen-reduce-parity", 1);
if (sat_acc_ && sat_minimize_ == 0)
......@@ -371,9 +371,19 @@ namespace spot
output_aborter* aborter =
(det_max_states_ >= 0 || det_max_edges_ >= 0) ? &aborter_ : nullptr;
// (Small,Low) is the only configuration where we do not run
// WDBA-minimization.
if ((PREF_ != Small || level_ != Low) && wdba_minimize_)
int wdba_minimize = wdba_minimize_;
if (wdba_minimize == -1)
{
if (level_ == High)
wdba_minimize = 1;
else if (level_ == Medium || PREF_ == Deterministic)
wdba_minimize = 2;
else
wdba_minimize = 0;
}
if (wdba_minimize == 2)
wdba_minimize = minimize_obligation_garanteed_to_work(a, f);
if (wdba_minimize)
{
bool reject_bigger = (PREF_ == Small) && (level_ <= Medium);
dba = minimize_obligation(a, f, nullptr, reject_bigger, aborter);
......
......@@ -253,7 +253,7 @@ namespace spot
int sat_states_ = 0;
int gen_reduce_parity_ = 1;
bool state_based_ = false;
bool wdba_minimize_ = true;
int wdba_minimize_ = -1;
};
/// @}
}
......@@ -132,12 +132,12 @@ genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
--pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f |
ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
cat >exp<<EOF
kv-psi=1,15
kv-psi=2,106
kr-nlogn=1,19
kr-nlogn=2,147
kr-n=1,12
kr-n=2,82
kv-psi=1,10
kv-psi=2,24
kr-nlogn=1,16
kr-nlogn=2,44
kr-n=1,10
kr-n=2,25
gxf-and=0,1
gxf-and=1,1
gxf-and=2,1
......
......@@ -458,4 +458,15 @@ res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
f='G(p1 | G!p0) M Xp1'
test "6,1" = `ltl2tgba "$f" --stats=%s,%d`
test "6,0" = `ltl2tgba -x wdba-minimize=2 "$f" --stats=%s,%d`
test "6,0" = `ltl2tgba -x wdba-minimize=0 "$f" --stats=%s,%d`
test "6,0" = `ltl2tgba --med "$f" --stats=%s,%d`
f='X((p1 & Xp1) M Fp1)'
test "4,1" = `ltl2tgba -D "$f" --stats=%s,%d`
test "4,1" = `ltl2tgba -D -x wdba-minimize=2 "$f" --stats=%s,%d`
test "4,0" = `ltl2tgba -D -x wdba-minimize=0 "$f" --stats=%s,%d`
test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d`
:
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment