scc_filter: do not remove Fin sets from rejecting SCCs
* src/twaalgos/sccfilter.cc (acc_filter_some, acc_filter_all): Merge into... (acc_filter_mask): ... this single parametrized class, and only remove sets that are only used as Inf. * src/twa/acc.hh: Add missing operator~. * src/tests/sccsimpl.test: Add test case. * src/tests/sccdot.test: Adjust. * NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz
parent
5d9e7d1f93
commit
5cb19a290b
5 changed files with 148 additions and 50 deletions
2
NEWS
2
NEWS
|
|
@ -2,6 +2,8 @@ New in spot 1.99.1a (not yet released)
|
|||
|
||||
* Bugs fixed:
|
||||
- p[+][:*2] was not detected as belonging to siPSL
|
||||
- scc_filter() would incorrectly remove Fin marks from
|
||||
rejecting SCCs.
|
||||
|
||||
New in spot 1.99.1 (2015-06-23)
|
||||
|
||||
|
|
|
|||
|
|
@ -168,7 +168,7 @@ State: 2
|
|||
[0&1] 0 {0 1}
|
||||
State: 3
|
||||
[1] 1
|
||||
[!1] 3
|
||||
[!1] 3 {2}
|
||||
State: 4
|
||||
[!0&1] 4 {0 1}
|
||||
[0&1] 4 {0 2}
|
||||
|
|
|
|||
|
|
@ -240,3 +240,105 @@ grep 'Acceptance: 2 ' out8.txt
|
|||
run 0 ../ikwiad -R3 -s -RDS -ks \
|
||||
'(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt
|
||||
grep 'states: 6$' out9.txt
|
||||
|
||||
|
||||
# Spot 1.99.1 used to incorrectly remove Fin sets from rejecting SCCs
|
||||
# in scc_filter().
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 1
|
||||
Acceptance: 1 Fin(0)
|
||||
AP: 1 "p0"
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0
|
||||
State: 1
|
||||
[!0] 1 {0}
|
||||
[0] 0
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 1
|
||||
Acceptance: 2 Fin(0)&Inf(1)
|
||||
AP: 1 "p0"
|
||||
--BODY--
|
||||
State: 0 {1}
|
||||
[t] 0
|
||||
State: 1
|
||||
[!0] 1 {0 1}
|
||||
[0] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
# run 0 ../../bin/autfilt -C -H --any --high input >output
|
||||
# cat >expected <<EOF
|
||||
# HOA: v1
|
||||
# States: 2
|
||||
# Start: 1
|
||||
# AP: 1 "p0"
|
||||
# acc-name: Buchi
|
||||
# Acceptance: 1 Inf(0)
|
||||
# properties: trans-labels explicit-labels state-acc complete
|
||||
# properties: deterministic inherently-weak
|
||||
# --BODY--
|
||||
# State: 0 {0}
|
||||
# [t] 0
|
||||
# State: 1
|
||||
# [0] 0
|
||||
# [!0] 1
|
||||
# --END--
|
||||
# HOA: v1
|
||||
# States: 2
|
||||
# Start: 1
|
||||
# AP: 1 "p0"
|
||||
# acc-name: Buchi
|
||||
# Acceptance: 1 Inf(0)
|
||||
# properties: trans-labels explicit-labels state-acc complete
|
||||
# properties: deterministic inherently-weak
|
||||
# --BODY--
|
||||
# State: 0 {0}
|
||||
# [t] 0
|
||||
# State: 1
|
||||
# [0] 0
|
||||
# [!0] 1
|
||||
# --END--
|
||||
# EOF
|
||||
# cat output
|
||||
# diff output expected
|
||||
|
||||
run 0 ../../bin/autfilt -C -H --det --high input >output
|
||||
cat >expected <<EOF
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 1
|
||||
AP: 1 "p0"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic inherently-weak
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[0] 0
|
||||
[!0] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 1
|
||||
AP: 1 "p0"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic inherently-weak
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[0] 0
|
||||
[!0] 1
|
||||
--END--
|
||||
EOF
|
||||
cat output
|
||||
diff output expected
|
||||
|
|
|
|||
|
|
@ -157,6 +157,11 @@ namespace spot
|
|||
return id & ~r.id;
|
||||
}
|
||||
|
||||
mark_t operator~() const
|
||||
{
|
||||
return ~id;
|
||||
}
|
||||
|
||||
mark_t operator^(mark_t r) const
|
||||
{
|
||||
return id ^ r.id;
|
||||
|
|
|
|||
|
|
@ -125,14 +125,24 @@ namespace spot
|
|||
};
|
||||
|
||||
// Remove acceptance conditions from all edges outside of
|
||||
// non-accepting SCCs.
|
||||
template <class next_filter = id_filter>
|
||||
struct acc_filter_all: next_filter
|
||||
// non-accepting SCCs. If "RemoveAll" is false, keep those on
|
||||
// transitions entering accepting SCCs.
|
||||
template <bool RemoveAll, class next_filter = id_filter>
|
||||
struct acc_filter_mask: next_filter
|
||||
{
|
||||
acc_cond::mark_t accmask;
|
||||
|
||||
template<typename... Args>
|
||||
acc_filter_all(scc_info* si, Args&&... args)
|
||||
acc_filter_mask(scc_info* si, Args&&... args)
|
||||
: next_filter(si, std::forward<Args>(args)...)
|
||||
{
|
||||
acc_cond::mark_t fin;
|
||||
acc_cond::mark_t inf;
|
||||
std::tie(inf, fin) =
|
||||
si->get_aut()->acc().get_acceptance().used_inf_fin_sets();
|
||||
// If an SCC is rejecting, we can mask all the sets that are
|
||||
// used only as Inf in the acceptance.
|
||||
accmask = ~(inf - fin);
|
||||
}
|
||||
|
||||
filtered_trans trans(unsigned src, unsigned dst,
|
||||
|
|
@ -144,41 +154,18 @@ namespace spot
|
|||
|
||||
if (keep)
|
||||
{
|
||||
unsigned u = this->si->scc_of(src);
|
||||
unsigned u = this->si->scc_of(dst);
|
||||
// If the edge is between two SCCs, or in a
|
||||
// non-accepting SCC. Remove the acceptance sets.
|
||||
if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst))
|
||||
acc = 0U;
|
||||
if ((this->si->is_rejecting_scc(u))
|
||||
|| (RemoveAll && u != this->si->scc_of(src)))
|
||||
acc &= accmask;
|
||||
}
|
||||
|
||||
return filtered_trans(keep, cond, acc);
|
||||
}
|
||||
};
|
||||
|
||||
// Remove acceptance conditions from all edges whose
|
||||
// destination is not an accepting SCCs.
|
||||
template <class next_filter = id_filter>
|
||||
struct acc_filter_some: next_filter
|
||||
{
|
||||
template<typename... Args>
|
||||
acc_filter_some(scc_info* si, Args&&... args)
|
||||
: next_filter(si, std::forward<Args>(args)...)
|
||||
{
|
||||
}
|
||||
|
||||
filtered_trans trans(unsigned src, unsigned dst,
|
||||
bdd cond, acc_cond::mark_t acc)
|
||||
{
|
||||
bool keep;
|
||||
std::tie(keep, cond, acc) =
|
||||
this->next_filter::trans(src, dst, cond, acc);
|
||||
|
||||
if (this->si->is_rejecting_scc(this->si->scc_of(dst)))
|
||||
acc = 0U;
|
||||
return filtered_trans(keep, cond, acc);
|
||||
}
|
||||
};
|
||||
|
||||
// Simplify redundant acceptance sets used in each SCCs.
|
||||
template <class next_filter = id_filter>
|
||||
struct acc_filter_simplify: next_filter
|
||||
|
|
@ -329,22 +316,24 @@ namespace spot
|
|||
if (aut->acc().is_generalized_buchi())
|
||||
{
|
||||
if (remove_all_useless)
|
||||
res = scc_filter_apply<state_filter
|
||||
<acc_filter_all
|
||||
<acc_filter_simplify<>>>>(aut, given_si);
|
||||
res =
|
||||
scc_filter_apply<state_filter
|
||||
<acc_filter_mask
|
||||
<true, acc_filter_simplify<>>>>(aut, given_si);
|
||||
else
|
||||
res = scc_filter_apply<state_filter
|
||||
<acc_filter_some
|
||||
<acc_filter_simplify<>>>>(aut, given_si);
|
||||
res =
|
||||
scc_filter_apply<state_filter
|
||||
<acc_filter_mask
|
||||
<false, acc_filter_simplify<>>>>(aut, given_si);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (remove_all_useless)
|
||||
res = scc_filter_apply<state_filter
|
||||
<acc_filter_all<>>>(aut, given_si);
|
||||
<acc_filter_mask<true>>>(aut, given_si);
|
||||
else
|
||||
res = scc_filter_apply<state_filter
|
||||
<acc_filter_some<>>>(aut, given_si);
|
||||
<acc_filter_mask<false>>>(aut, given_si);
|
||||
}
|
||||
res->merge_edges();
|
||||
res->prop_copy(aut,
|
||||
|
|
@ -365,19 +354,19 @@ namespace spot
|
|||
if (remove_all_useless)
|
||||
res = scc_filter_apply<susp_filter
|
||||
<state_filter
|
||||
<acc_filter_all
|
||||
<acc_filter_simplify<>>>>>(aut, given_si,
|
||||
suspvars,
|
||||
ignoredvars,
|
||||
early_susp);
|
||||
<acc_filter_mask
|
||||
<true, acc_filter_simplify<>>>>>(aut, given_si,
|
||||
suspvars,
|
||||
ignoredvars,
|
||||
early_susp);
|
||||
else
|
||||
res = scc_filter_apply<susp_filter
|
||||
<state_filter
|
||||
<acc_filter_some
|
||||
<acc_filter_simplify<>>>>>(aut, given_si,
|
||||
suspvars,
|
||||
ignoredvars,
|
||||
early_susp);
|
||||
<acc_filter_mask
|
||||
<false, acc_filter_simplify<>>>>>(aut, given_si,
|
||||
suspvars,
|
||||
ignoredvars,
|
||||
early_susp);
|
||||
res->merge_edges();
|
||||
res->prop_copy(aut,
|
||||
{ false, // state-based acceptance is not preserved
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue