Commit 2dda2c91 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

minimize_obligation: can complement the input TGBA if deterministic

This makes dstar2tgba able to produce a minimal WDBA when the input DRA
represent an obligation property.

* src/tgbaalgos/minimize.cc (minimize_obligation): When the
formula is not supplied but the input automaton is deterministic,
complement it to check the result of WDBA minimization.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
tests.
parent 3b10bb3b
......@@ -46,6 +46,8 @@
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/bfssteps.hh"
#include "tgbaalgos/isdet.hh"
#include "tgbaalgos/dbacomp.hh"
#include "priv/countstates.hh"
namespace spot
......@@ -647,29 +649,37 @@ namespace spot
if (is_guarantee_automaton(aut_f))
return min_aut_f;
if (!f && !aut_neg_f)
{
// We do not now if the minimization is safe.
delete min_aut_f;
return 0;
}
const tgba* to_free = 0;
// Build negation automaton if not supplied.
if (!aut_neg_f)
{
assert(f);
const ltl::formula* neg_f =
ltl::unop::instance(ltl::unop::Not, f->clone());
aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(aut_neg_f, true);
delete aut_neg_f;
to_free = aut_neg_f = tmp;
if (f)
{
// If we know the formula, simply build the automaton for
// its negation.
const ltl::formula* neg_f =
ltl::unop::instance(ltl::unop::Not, f->clone());
aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(aut_neg_f, true);
delete aut_neg_f;
to_free = aut_neg_f = tmp;
}
else if (is_deterministic(aut_f))
{
// If the automaton is deterministic, complementing is
// easy.
to_free = aut_neg_f = dba_complement(aut_f);
}
else
{
// Otherwise, we cannot check if the minimization is safe.
delete min_aut_f;
return 0;
}
}
// If the negation is a guarantee automaton, then the
......
......@@ -37,31 +37,10 @@ dstar2tgba=../../bin/dstar2tgba
$ltlfilt -f 'a U b' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
../ltl2tgba -XDB - |
$dstar2tgba --stats '%s %e %t %a %d' |
tee out
cat >expected <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1"]
1 -> 1 [label="a & !b\n"]
1 -> 2 [label="a & !b\n"]
1 -> 3 [label="b\n"]
1 -> 4 [label="b\n"]
2 [label="2"]
2 -> 2 [label="a & !b\n"]
2 -> 4 [label="b\n"]
3 [label="5"]
3 -> 3 [label="1\n"]
3 -> 4 [label="1\n"]
4 [label="6", peripheries=2]
4 -> 4 [label="1\n{Acc[1]}"]
}
EOF
diff expected out
test "`cat out`" = '2 3 7 1 1'
RAB=--automata=rabin
STR=--automata=streett
......
......@@ -35,7 +35,10 @@ randltl=../../bin/randltl
# Make sure all recurrence formulas are translated into deterministic
# Büchi automata by the DRA->TGBA converster.
# Büchi automata by the DRA->TGBA converter.
# (Note that ltl2tgba is not called with -D when want to make
# sure we get a deterministic output even if the automaton generated
# by Spot initially was non-deterministic)
$randltl -n -1 a b --tree-size=5..15 |
$ltlfilt --syntactic-recurrence --remove-wm -r -u \
......@@ -56,6 +59,26 @@ while read f; do
test $det -eq 1;
done < formulas
echo ==========================
# For obligation formulas, the output of dstar2tgba should
# have the same size as the input when option -D is used.
$randltl -n -1 a b --tree-size=5..15 |
$ltlfilt --obligation --size-min=4 --size-max=15 --relabel=abc \
--remove-wm -r -u |
head -n 20 > formulas
while read f; do
expected=`$ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
$ltlfilt -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - foo
echo "$f"
output=`$dstar2tgba foo -BD --stats '%s %e %d 1'`
# the '1 %d' matching '%d 1' makes sure input and output are deterministic.
test "$output" = "$expected";
done < formulas
echo ==========================
# Now make sure that some obviously non-deterministic property
# are not translated to deterministic.
......
Markdown is supported
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