Commit 0ede9687 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

sat-minimize: allow different acceptances as input and output

* src/twaalgos/dtgbasat.cc (sat_minimize): Use any arbitrary
acceptance condition passed via the "acc" option.
* src/twa/acc.hh (mark_t::max_set): New method.
* src/tests/satmin2.test: Add two test cases with DRA as input
and DSA as output.
parent 3efeacb6
......@@ -24,6 +24,8 @@ set -e
# Skip if $SATSOLVE is not installed.
(${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77
autfilt=../../bin/autfilt
ltlfilt=../../bin/ltlfilt
# This is a counterexample for one of the optimization idea we had for
# the SAT-based minimization.
......@@ -63,3 +65,49 @@ diff output expected
../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
# DRA produced by ltl2dstar for GFp0 -> GFp1
cat >test.hoa <<EOF
HOA: v1
States: 4
properties: implicit-labels trans-labels no-univ-branch deterministic complete
acc-name: Rabin 2
Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3))
Start: 0
AP: 2 "p0" "p1"
--BODY--
State: 0 {0}
1
0
3
2
State: 1 {1}
1
0
3
2
State: 2 {0 3}
1
0
3
2
State: 3 {1 3}
1
0
3
2
--END--
EOF
# Let's try to find a smaller transition-based Streett automaton We
# easily really check the expected automaton, because different SAT
# solver (even different versions of glucose) can return different
# automata.
$autfilt -H --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output
test `cat output` = 1
# How about a state-based DSA?
$autfilt -H --sat-minimize='state-based,acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s > output
test `cat output` = 3
......@@ -197,6 +197,21 @@ namespace spot
#endif
}
// Return the number of the highest set used plus one.
// So if no set is used, this returns 0,
// but if the sets {1,3,8} are used, this returns 9.
unsigned max_set() const
{
auto i = id;
int res = 0;
while (i)
{
++res;
i >>= 1;
}
return res;
}
// Remove n bits that where set
mark_t& remove_some(unsigned n)
{
......
......@@ -1033,12 +1033,34 @@ namespace spot
bool dicho = om.get("dichotomy", 0);
int states = om.get("states", -1);
int nacc = om.get("gba", -1);
auto accstr = om.get_str("acc");
if (nacc != -1 && !accstr.empty())
throw std::runtime_error("options 'gba' and 'acc' cannot "
"be both passed to sat_minimize()");
acc_cond::acc_code target_acc = a->get_acceptance();
if (nacc != -1)
target_acc = acc_cond::generalized_buchi(nacc);
if (!accstr.empty())
{
target_acc = parse_acc_code(accstr.c_str());
// Just in case we were given something like
// Fin(1) | Inf(3)
// Rewrite it as
// Fin(0) | Inf(1)
// without holes in the set numbers
acc_cond::mark_t used = target_acc.used_sets();
acc_cond a(used.max_set());
target_acc = target_acc.strip(a.comp(used), true);
nacc = used.count();
}
else if (nacc != -1)
{
target_acc = acc_cond::generalized_buchi(nacc);
}
else
nacc = a->acc().num_sets();
{
nacc = a->acc().num_sets();
}
bool target_is_buchi =
(nacc == 1 && target_acc.size() == 2 &&
......
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