Commit 104a372c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Add a notebook illustrating decompose_strength()

* wrap/python/tests/decompose.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
* src/twaalgos/strength.cc: Fix corner cases.
* src/tests/strength.test: Adjust corner case.
* NEWS, doc/org/tut.org: Mention the notebook.
parent a7db0b54
......@@ -6,6 +6,8 @@ New in spot 1.99.5a (not yet released)
* autfilt has a new transformation: --decompose-strength,
implementing the decomposition of our TACAS'13 paper.
A demonstration of this feature via the Python bindings
can be found at https://spot.lrde.epita.fr/ipynb/decompose.html
* All tools that output HOA files accept a --check=strength option
to request automata to be marked as "weak" or "terminal" as
......
......@@ -54,5 +54,6 @@ real notebooks instead.
after acceptance simplification
- [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
- [[https://spot.lrde.epita.fr/ipynb/decompose.html][decompose.ipynb]] illustrates the =decompose_strength()= function
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing
automaton
......@@ -535,14 +535,14 @@ HOA: v1
States: 2
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
--BODY--
State: 0
State: 0 {0}
[t] 1
State: 1
State: 1 {0}
[t] 0
--END--
HOA: v1
......
......@@ -148,6 +148,33 @@ namespace spot
(std::string("unknown option for decompose_strength(): ") + c);
}
acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs
acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that
// we only want to traverse.
// If the acceptance condition is always satisfiable, we will
// consider the automaton has weak (even if that is not the
// case syntactically) and not output any strong part.
bool all_accepting = false;
if (aut->acc().is_tt())
{
all_accepting = true;
}
else if (aut->acc().uses_fin_acceptance())
{
auto p = aut->get_acceptance().unsat_mark();
if (p.first)
uacc = p.second;
else
all_accepting = true;
}
if (all_accepting)
{
keep &= ~Strong;
if (keep == Ignore)
return nullptr;
}
scc_info si(aut);
si.determine_unknown_acceptance();
......@@ -160,7 +187,7 @@ namespace spot
{
if (si.is_accepting_scc(i))
{
if (is_weak_scc(si, i))
if (all_accepting | is_weak_scc(si, i))
{
if (keep & Weak)
{
......@@ -194,23 +221,10 @@ namespace spot
res->copy_ap_of(aut);
res->prop_copy(aut, { true, false, true, false });
acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs
acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that
// we only want to traverse.
if (keep & Strong)
{
res->copy_acceptance_of(aut);
auto& ac = res->acc();
if (ac.uses_fin_acceptance())
// Note that we ignore the cases where the acceptance
// condition is always satisfiable. In that case
// uacc will be set to 0U, which will be satisfiable
uacc = ac.get_acceptance().unsat_mark().second;
}
res->copy_acceptance_of(aut);
else
{
wacc = res->set_buchi();
}
wacc = res->set_buchi();
auto fun = [&si, &want, uacc, wacc, keep]
(unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)
......
......@@ -37,6 +37,7 @@ TESTS = \
automata.ipynb \
automata-io.ipynb \
bddnqueen.py \
decompose.ipynb \
formulas.ipynb \
implies.py \
interdep.py \
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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