Commit 09e47d64 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

decompose: merge decompose_strength() and decompose_scc()

These two functions were doing almost identical work, the only
difference was the way to select the SCC to keep.  Now we have a more
uniform way to do that.  Closes #172.

* bin/autfilt.cc: Offer a unique --decompose-scc option, but keep
--decompose-strength as an alias for backward compatibility.
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: Rename
decompose_strength as decompose_scc, and handle a way to list
all SCC numers in the string specifier.  This gets rid
of the nearly identical
* tests/core/scc.test, tests/core/strength.test,
tests/python/decompose.ipynb, tests/python/decompose_scc.py: Adjust
test cases.
* NEWS: Adjust.
parent fba3c782
......@@ -21,6 +21,10 @@ New in spot 2.3.5.dev (not yet released)
- autfilt learned --simplify-acceptance to simplify some acceptance
conditions. (See spot::simplify_acceptance() below.)
- autfilt --decompote-strength has been renamed to --decompose-scc
because it can now extract the subautomaton leading to an SCC
specified by number. (The old name is still kept as an alias.)
Library:
- A new library, libspotgen, gathers all functions used to generate
......@@ -41,6 +45,12 @@ New in spot 2.3.5.dev (not yet released)
- spot::dtwa_complement now simply returns the result of dualize()
- spot::decompose_strength() was extended and renamed to
spot::decompose_scc() as it can now also extract a subautomaton
leading to a particular SCC. A demonstration of this feature via
the Python bindings can be found at
https://spot.lrde.epita.fr/ipynb/decompose.html
- A new named property for automata called "original-states" can be
used to record the origin of a state before transformation. It is
currently defined by the degeneralization algorithms, and by
......@@ -161,6 +171,9 @@ New in spot 2.3.5.dev (not yet released)
Deprecation notice:
- spot::decompose_strength() is deprecated, it has been renamed
to spot::decompose_scc().
- spot::dtwa_complement() is deprecated. Prefer the more generic
spot::dualize() instead.
......@@ -330,11 +343,6 @@ New in spot 2.3.1 (2017-02-20)
Kupferman & Rosenberg [MoChArt'10] are recognizable by
deterministic Büchi automata with at least 2^2^n states.
- autfilt has a new transformation: --decompose-scc, which allows
decomposition of automata through their accepting SCCs.
A demonstration of this feature via the Python bindings
can be found at https://spot.lrde.epita.fr/ipynb/decompose.html
Library:
- spot::twa_run::as_twa() has an option to preserve state names.
......
......@@ -89,7 +89,6 @@ enum {
OPT_COMPLEMENT,
OPT_COMPLEMENT_ACC,
OPT_COUNT,
OPT_DECOMPOSE_STRENGTH,
OPT_DECOMPOSE_SCC,
OPT_DESTUT,
OPT_DUALIZE,
......@@ -300,11 +299,12 @@ 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,
{ "decompose-scc", OPT_DECOMPOSE_SCC, "t|w|s|N|aN", 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 },
{ "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting"
" SCC as accepting", 0 },
" or (N) the subautomaton leading to the Nth SCC, or (aN) to the Nth "
"accepting SCC (option can be combined with ccomas to extract multiple "
"parts)", 0 },
{ "decompose-strength", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "dualize", OPT_DUALIZE, nullptr, 0,
"dualize each automaton", 0 },
{ "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
......@@ -495,8 +495,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 int opt_decompose_scc = -1;
static char* opt_decompose_scc = nullptr;
static bool opt_dualize = false;
static spot::acc_cond::mark_t opt_mask_acc = 0U;
static std::vector<bool> opt_keep_states = {};
......@@ -595,11 +594,8 @@ 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_DECOMPOSE_SCC:
opt_decompose_scc = to_pos_int(arg);
opt_decompose_scc = arg;
break;
case OPT_DESTUT:
opt_destut = true;
......@@ -1259,16 +1255,9 @@ namespace
if (opt->sum_and)
aut = spot::sum_and(std::move(aut), opt->sum_and);
if (opt_decompose_strength)
{
aut = decompose_strength(aut, opt_decompose_strength);
if (!aut)
return 0;
}
if (opt_decompose_scc != -1)
if (opt_decompose_scc)
{
aut = decompose_acc_scc(aut, opt_decompose_scc);
aut = decompose_scc(aut, opt_decompose_scc);
if (!aut)
return 0;
}
......
......@@ -201,11 +201,11 @@ namespace spot
twa_graph_ptr
decompose_strength(const const_twa_graph_ptr& aut, const char* keep_opt)
decompose_scc(scc_info& si, 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"));
(std::string("option for decompose_scc() should not be empty"));
enum strength {
Ignore = 0,
......@@ -213,13 +213,70 @@ namespace spot
WeakStrict = 2,
Weak = Terminal | WeakStrict,
Strong = 4,
Needed = 8, // Needed SCCs are those that lead to
// the SCCs we want to keep.
Needed = 8, // Needed SCCs are those that lead to the SCCs we
// want to keep, and also unaccepting SCC we were
// asked to keep.
};
auto aut = si.get_aut();
si.determine_unknown_acceptance();
unsigned n = si.scc_count();
std::vector<unsigned char> want(n, Ignore);
unsigned char keep = Ignore;
while (auto c = *keep_opt++)
switch (c)
{
case ',':
case ' ':
break;
case '0': // SCC number N.
case '1':
case '2':
case '3':
case '4':
case '5':
case '6':
case '7':
case '8':
case '9':
{
char* endptr;
long int scc = strtol(keep_opt - 1, &endptr, 10);
if (scc >= n)
{
throw std::runtime_error
(std::string("decompose_scc(): there is no SCC ")
+ std::to_string(scc) + " in this automaton");
}
keep_opt = endptr;
want[scc] = Needed;
break;
}
case 'a': // Accepting SCC number N.
{
char* endptr;
long int scc = strtol(keep_opt, &endptr, 10);
if (endptr == keep_opt)
throw std::runtime_error
("decompose_scc(): 'a' should be followed by an SCC number");
int j = 0;
for (unsigned s = 0; s < n; ++s)
if (si.is_accepting_scc(s))
if (j++ == scc)
{
want[s] = Needed;
break;
}
if (j != scc + 1)
{
throw std::runtime_error
(std::string("decompose_scc(): there is no SCC 'a")
+ std::to_string(scc) + "' in this automaton");
}
keep_opt = endptr;
break;
}
case 's':
keep |= Strong;
break;
......@@ -231,12 +288,12 @@ namespace spot
break;
default:
throw std::runtime_error
(std::string("unknown option for decompose_strength(): ") + c);
(std::string("unknown option for decompose_scc(): ") + c);
}
auto p = aut->acc().unsat_mark();
bool all_accepting = !p.first;
acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs
acc_cond::mark_t wacc = 0U; // acceptance for weak SCCs
acc_cond::mark_t uacc = p.second; // Acceptance for "needed" SCCs, that
// we only want to traverse.
......@@ -244,42 +301,38 @@ namespace spot
// consider the automaton as weak (even if that is not the
// case syntactically) and not output any strong part.
if (all_accepting)
{
keep &= ~Strong;
if (keep == Ignore)
return nullptr;
}
keep &= ~Strong;
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;
bool kept_scc_are_weak = true;
bool kept_scc_are_terminal = true;
for (unsigned i = 0; i < n; ++i) // SCC are topologically ordered
{
if (si.is_accepting_scc(i))
{
strength scc_strength = Ignore;
if (all_accepting | is_inherently_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);
}
}
scc_strength = is_complete_scc(si, i) ? Terminal : WeakStrict;
else
scc_strength = Strong;
if (want[i] == Needed)
want[i] = scc_strength;
else
want[i] = scc_strength & keep;
if (want[i])
{
want[i] = keep & Strong;
strong_seen = true;
if (!(scc_strength & Weak))
kept_scc_are_weak = false;
if (!(scc_strength & Terminal))
kept_scc_are_terminal = false;
}
nonempty |= want[i];
}
nonempty |= want[i]; // also works "Needed" rejecting SCCs
// An SCC is needed if one of its successor is.
for (unsigned j: si.succ(i))
if (want[j])
......@@ -296,12 +349,12 @@ namespace spot
res->copy_ap_of(aut);
res->prop_copy(aut, { true, false, false, true, false, false });
if (keep & Strong)
res->copy_acceptance_of(aut);
else
if (kept_scc_are_weak)
wacc = res->set_buchi();
else
res->copy_acceptance_of(aut);
auto fun = [&si, &want, uacc, wacc, keep]
auto fun = [&si, &want, uacc, wacc, kept_scc_are_weak]
(unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)
{
if (want[si.scc_of(dst)] == Ignore)
......@@ -314,99 +367,35 @@ namespace spot
acc = uacc;
return;
}
if (keep & Strong)
return;
acc = wacc;
if (kept_scc_are_weak)
acc = wacc;
};
transform_accessible(aut, res, fun);
if (!(keep & Strong))
{
res->prop_weak(true);
if (!(keep & WeakStrict))
{
assert(keep & Terminal);
res->prop_terminal(true);
}
}
else
{
res->prop_weak(!strong_seen);
}
res->prop_weak(kept_scc_are_weak);
res->prop_terminal(kept_scc_are_terminal);
return res;
}
twa_graph_ptr
decompose_scc(scc_info& sm, unsigned scc_num)
decompose_scc(const const_twa_graph_ptr& aut, const char* keep_opt)
{
unsigned n = sm.scc_count();
if (n <= scc_num)
throw std::invalid_argument
(std::string("decompose_scc(): requested SCC index is out of bounds"));
std::vector<bool> want(n, false);
want[scc_num] = true;
// mark all the SCCs that can reach scc_num as wanted
for (unsigned i = scc_num + 1; i < n; ++i)
for (unsigned succ : sm.succ(i))
if (want[succ])
{
want[i] = true;
break;
}
const_twa_graph_ptr aut = sm.get_aut();
twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
res->prop_copy(aut, { true, false, false, true, false, false });
res->copy_acceptance_of(aut);
auto um = aut->acc().unsat_mark();
// If aut has an unsatisfying mark, we are going to use it to remove the
// acceptance of some transitions. If it doesn't, we make res a rejecting
// Büchi automaton, and get back an accepting mark that we are going to set
// on the transitions of the SCC we selected.
auto new_mark = um.first ? um.second : res->set_buchi();
auto fun = [sm, &want, um, new_mark, scc_num]
(unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)
{
if (!want[sm.scc_of(dst)])
{
cond = bddfalse;
return;
}
// no need to check if src is wanted, we already know dst is.
// if res is accepting, make only the upstream SCCs rejecting
// if res is rejecting, make only the requested SCC accepting
if (um.first != (sm.scc_of(src) == scc_num))
acc = new_mark;
};
transform_accessible(aut, res, fun);
scc_info si(aut);
return decompose_scc(si, keep_opt);
}
return res;
twa_graph_ptr
decompose_strength(const const_twa_graph_ptr& aut, const char* keep_opt)
{
return decompose_scc(aut, keep_opt);
}
twa_graph_ptr
decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index)
decompose_scc(scc_info& sm, unsigned scc_num, bool accepting)
{
scc_info si(aut);
unsigned scc_num = 0;
for (; scc_num < si.scc_count(); ++scc_num)
{
if (si.is_accepting_scc(scc_num))
{
if (!scc_index)
break;
--scc_index;
}
}
return decompose_scc(si, scc_num);
std::string num = std::to_string(scc_num);
return decompose_scc(sm, (accepting ? ('a' + num) : num).c_str());
}
}
......@@ -137,10 +137,14 @@ namespace spot
/// are not terminal.
/// - 't': keep terminal SCCs (i.e., inherently weak SCCs that are complete)
/// - 's': keep strong SCCs (i.e., SCCs that are not inherently weak).
/// Additionally, the string may contain comma-separated numbers representing
/// SCC number, optionally prefixed by 'a' to denote the Nth accepting SCC.
///
/// This algorithm returns a subautomaton that contains all SCCs of the
/// requested strength, plus any upstream SCC (but adjusted not to be
/// accepting).
/// This algorithm returns a subautomaton that contains all SCCs of
/// the requested strength (or given SCC numbers), plus any upstream
/// SCC (but adjusted not to be accepting). The output may be null if
/// no SCC match a given strength. An exception will be raised if
/// an incorrect SCC number is supplied.
///
/// The definition are basically those used in the following paper,
/// except that we extra the "inherently weak" part instead of the
......@@ -168,27 +172,33 @@ namespace spot
\endverbatim */
///
/// \param aut the automaton to decompose
/// \param keep a string specifying the strengths to keep: it should
/// \param keep a string specifying the strengths/SCCs to keep
SPOT_API twa_graph_ptr
decompose_scc(const const_twa_graph_ptr& aut, const char* keep);
/// \brief Extract a sub-automaton of a given strength
///
/// This works exactly like
/// decompose_scc(const const_twa_graph_ptr&, const char*)
/// but takes an \c scc_info as first argument. This avoids
/// wasting time to reconstruct that object if one is already
/// available.
SPOT_API twa_graph_ptr
decompose_scc(scc_info& sm, const char* keep);
SPOT_DEPRECATED("use decompose_scc() instead")
SPOT_API twa_graph_ptr
decompose_strength(const const_twa_graph_ptr& aut, const char* keep);
/// \brief Extract a sub-automaton of a SCC
/// \brief Extract a sub-automaton above an SCC
///
/// This algorithm returns a subautomaton that contains the requested SCC,
/// plus any upstream SCC (but adjusted not to be accepting).
///
/// \param sm the SCC info map of the automaton
/// \param scc_num the index in the map of the SCC to keep
/// \param accepting if true, scc_num is interpreted as the Nth
/// accepting SCC instead of the Nth SCC
SPOT_API twa_graph_ptr
decompose_scc(scc_info& sm, unsigned scc_num);
/// \brief Extract a sub-automaton of an accepting SCC
///
/// This algorithm returns a subautomaton that contains the `scc_index'th
/// accepting SCC, plus any upstream SCC (but adjusted not to be accepting).
///
/// \param aut the automaton to decompose
/// \param scc_index the ID of the accepting SCC to keep
SPOT_API twa_graph_ptr
decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index);
decompose_scc(scc_info& sm, unsigned scc_num, bool accepting = false);
}
......@@ -44,6 +44,7 @@ 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
......@@ -53,7 +54,7 @@ State: 1 {0}
--END--
EOF
run 0 autfilt --decompose-scc=0 -F aut> out
run 0 autfilt --decompose-scc=a0 aut> out
cat out
diff out ref
......@@ -65,20 +66,23 @@ AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
properties: deterministic weak
--BODY--
State: 0 {0}
[0&!1] 0
--END--
EOF
run 0 autfilt --decompose-scc=1 -F aut> out
cat out
run 0 autfilt --decompose-scc=a1 aut> out
diff out ref
autfilt --decompose-scc=2 -F aut 2>stderr && exit 1
autfilt --decompose-scc=a2 aut 2>stderr && exit 1
[ $? -eq 2 ]
grep "no SCC 'a2'" stderr
autfilt --decompose-scc=2 aut 2>stderr && exit 1
[ $? -eq 2 ]
grep "out of bounds" stderr
grep "no SCC 2" stderr
# always satisfied acceptance
ltl2tgba 'Ga R b | Gc R b' > aut
......@@ -90,7 +94,7 @@ Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
properties: trans-labels explicit-labels state-acc weak
--BODY--
State: 0
[0] 0
......@@ -100,7 +104,7 @@ State: 1 {0}
--END--
EOF
run 0 autfilt --decompose-scc=1 -F aut> out
run 0 autfilt --decompose-scc=a1 -F aut> out
cat out
diff out ref
......
......@@ -368,7 +368,8 @@ Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic weak
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[1] 1
......@@ -383,7 +384,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
properties: deterministic terminal
--BODY--
State: 0 {0}
[0] 1
......@@ -398,7 +399,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
properties: deterministic terminal
--BODY--
State: 0 {0}
[0] 1
......@@ -413,7 +414,7 @@ AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
properties: deterministic terminal
--BODY--
State: 0 {0}
[t] 1
......@@ -496,7 +497,8 @@ Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic weak
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[1] 1
......@@ -511,7 +513,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
properties: deterministic terminal
--BODY--
State: 0 {0}
[0] 1
......@@ -523,15 +525,16 @@ 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 weak
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
......@@ -540,7 +543,7 @@ AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
properties: deterministic terminal
--BODY--
State: 0 {0}
[t] 1
......
This diff is collapsed.