Commit a7db0b54 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Add a decompose_strength() function.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(decompose_stregth): New function.
* src/bin/autfilt.cc: Add a --decompose-strength option.
* src/bin/man/autfilt.x: Add bibliography.
* src/tests/strength.test: Test it.
* NEWS: Mention it.
parent 3428fb32
......@@ -2,7 +2,10 @@ New in spot 1.99.5a (not yet released)
Command-line tools:
* autfilt has two now filters: --is-weak and --is-terminal.
* autfilt has two new filters: --is-weak and --is-terminal.
* autfilt has a new transformation: --decompose-strength,
implementing the decomposition of our TACAS'13 paper.
* All tools that output HOA files accept a --check=strength option
to request automata to be marked as "weak" or "terminal" as
......
......@@ -75,6 +75,7 @@ enum {
OPT_COMPLEMENT,
OPT_COMPLEMENT_ACC,
OPT_COUNT,
OPT_DECOMPOSE_STRENGTH,
OPT_DESTUT,
OPT_DNF_ACC,
OPT_EDGES,
......@@ -153,6 +154,9 @@ static const argp_option options[] =
{ "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
"complement the acceptance condition (without touching the automaton)",
0 },
{ "decompose-strength", OPT_DECOMPOSE_STRENGTH, "t|w|s", 0,
"extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
" (letters may be combined to combine more strengths in the output)", 0 },
{ "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
"if any of those APs occur in the automaton, restrict all edges to "
"ensure two of them may not be true at the same time. Use this option "
......@@ -279,6 +283,7 @@ static bool opt_rem_fin = false;
static bool opt_clean_acc = false;
static bool opt_complement = false;
static bool opt_complement_acc = false;
static char* opt_decompose_strength = nullptr;
static spot::acc_cond::mark_t opt_mask_acc = 0U;
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
......@@ -338,6 +343,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_COMPLEMENT_ACC:
opt_complement_acc = true;
break;
case OPT_DECOMPOSE_STRENGTH:
opt_decompose_strength = arg;
break;
case OPT_DESTUT:
opt_destut = true;
break;
......@@ -627,6 +635,13 @@ namespace
if (opt->product_or)
aut = spot::product_or(std::move(aut), opt->product_or);
if (opt_decompose_strength)
{
aut = decompose_strength(aut, opt_decompose_strength);
if (!aut)
return 0;
}
if (opt_sat_minimize)
{
aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
......
.\" -*- coding: utf-8 -*-
[NAME]
autfilt \- filter, convert, and transform Büchi automata
[DESCRIPTION]
.\" Add any additional description here
[BIBLIOGRAPHY]
The following papers are related to some of the transformations implemented
in autfilt.
.TP
\(bu
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud:
Strength-based decomposition of the property Büchi automaton for faster
model checking. Proceedings of TACAS'13. LNCS 7795.
The \fB\-\-strength\-decompose\fR option implements the definitions
given in the above paper.
.TP
\(bu
František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, and Jan Strejček:
On refinement of Büchi automata for explicit model checking.
Proceedings of SPIN'15. LNCS 9232.
That paper gives the motivation for options \fB\-\-exclusive\-ap\fR
and \fB\-\-simplify\-exclusive\-ap\fR.
[SEE ALSO]
.BR spot-x (7)
.BR dstar2tgba (1)
......@@ -83,6 +83,34 @@ State: 0 {0}
State: 1
[!0] 1 {0}
--END--
/* The example from the TACAS'13 paper. */
HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
run 0 $autfilt -H --check=strength in | tee out
......@@ -161,6 +189,400 @@ State: 0 {0}
State: 1 {0}
[!0] 1
--END--
HOA: v1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
diff out expected
run 0 $autfilt -H --decompose=t in | tee out.t
run 0 $autfilt -H --decompose=w in | tee out.w
run 0 $autfilt -H --decompose=s in | tee out.s
run 0 $autfilt -H --decompose=tw in | tee out.tw
run 0 $autfilt -H --decompose=ws in | tee out.ws
run 0 $autfilt -H --decompose=tws in | tee out.tws
echo '/******************************/' > sep
cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out
cat >expected <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 4
Start: 0
AP: 2 "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
--BODY--
State: 0
[!0&!1] 0
[0&!1] 1
[1] 2
State: 1
[!0&!1] 0
[0&!1] 1
[!0&1] 2
[0&1] 3
State: 2 {0}
[t] 2
State: 3
[!0] 2
[0] 3
--END--
/******************************/
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1
States: 3
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc weak
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0
[1&!2] 2
State: 1 {0}
[0] 1
State: 2
[!1&!2] 0
[1&!2] 2
--END--
/******************************/
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1
States: 2
Start: 0
AP: 2 "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0&!1] 0 {0}
[0&!1] 1
State: 1
[!0&!1] 0 {0}
[0&!1] 1
--END--
/******************************/
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic weak
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc weak
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0
[1&!2] 2
[2] 3
State: 1 {0}
[0] 1
State: 2
[!1&!2] 0
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3 {0}
[t] 3
State: 4
[!1] 3
[1] 4
--END--
/******************************/
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1
States: 3
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
State: 1
[0] 1 {0}
State: 2
[!1&!2] 0 {0}
[1&!2] 2
--END--
/******************************/
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic weak
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1
States: 2
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
properties: deterministic weak
--BODY--
State: 0
[t] 1
State: 1
[t] 0
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
--BODY--
State: 0 {0}
[!0] 0
--END--
HOA: v1
States: 5
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1&!2] 1
[!1&!2] 0 {0}
[1&!2] 2
[2] 3
State: 1
[0] 1 {0}
State: 2
[!1&!2] 0 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
diff out expected
......@@ -20,6 +20,7 @@
#include "strength.hh"
#include "misc/hash.hh"
#include "isweakscc.hh"
#include "mask.hh"
#include <deque>
namespace spot
......@@ -113,5 +114,137 @@ namespace spot
}
twa_graph_ptr
decompose_strength(const const_twa_graph_ptr& aut, const char* keep_opt)
{
if (keep_opt == nullptr || *keep_opt == 0)
throw std::runtime_error
(std::string("option for decompose_strength() should not be empty"));
enum strength {
Ignore = 0,
Terminal = 1,
WeakStrict = 2,
Weak = Terminal | WeakStrict,
Strong = 4,
Needed = 8, // Needed SCCs are those that lead to
// the SCCs we want to keep.
};
unsigned char keep = Ignore;
while (auto c = *keep_opt++)
switch (c)
{
case 's':
keep |= Strong;
break;
case 't':
keep |= Terminal;
break;
case 'w':
keep |= WeakStrict;
break;
default:
throw std::runtime_error
(std::string("unknown option for decompose_strength(): ") + c);
}
scc_info si(aut);
si.determine_unknown_acceptance();
unsigned n = si.scc_count();
std::vector<unsigned char> want(n, Ignore);
bool nonempty = false;
bool strong_seen = false;
for (unsigned i = 0; i < n; ++i) // SCC are topologically ordered
{
if (si.is_accepting_scc(i))
{
if (is_weak_scc(si, i))
{
if (keep & Weak)
{
if ((keep & Weak) == Weak)
want[i] = Weak;
else
want[i] = keep &
(is_complete_scc(si, i) ? Terminal : WeakStrict);
}
}
else
{
want[i] = keep & Strong;
strong_seen = true;
}
nonempty |= want[i];
}
// An SCC is needed if one of its successor is.
for (unsigned j: si.succ(i))
if (want[j])
{
want[i] |= Needed;
break;
}
}
if (!nonempty)
return nullptr;
twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
res->prop_copy(aut, { true, false, true, false });
acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs