From e592832a3eb0927c24476ad955dc0b611ee3e49a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Mar 2015 16:33:33 +0100 Subject: [PATCH] maskacc: reverse the way the acceptance condition is stripped It makes more sense to assume that the removed set cannot be visited. * src/tgbaalgos/mask.cc: Flip a Boolean. * src/tgbatest/maskacc.test: Adjust test case. * doc/org/autfilt.org: Add an example. --- doc/org/autfilt.org | 115 +++++++++++++++++++++++++++++++++----- src/tgbaalgos/mask.cc | 2 +- src/tgbatest/maskacc.test | 21 +++---- 3 files changed, 112 insertions(+), 26 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 22d0eec0b..90ddb9817 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -238,11 +238,18 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' #+RESULTS: #+begin_example --cleanup-acceptance remove unused acceptance sets from the automaton + --cnf-acceptance put the acceptance condition in Conjunctive Normal + Form --complement-acceptance complement the acceptance condition (without touching the automaton) --destut allow less stuttering --dnf-acceptance put the acceptance condition in Disjunctive Normal Form + --exclusive-ap=AP,AP,... 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 + multiple times to declare independent groups of + exclusive propositions. --instut[=1|2] allow more stuttering (two possible algorithms) --keep-states=NUM[,NUM...] only keep specified states. The first state will be the new initial state @@ -272,7 +279,7 @@ States: 3 Start: 0 AP: 2 "a" "b" acc-name: Buchi -Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0) +Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(1) --BODY-- State: 0 {3} [t] 0 @@ -305,7 +312,7 @@ autfilt aut-ex1.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(⓿)> + label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> labelloc="t" fontname="Lato" node [fontname="Lato"] @@ -346,7 +353,7 @@ autfilt --sbacc aut-ex1.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(⓿)> + label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> labelloc="t" fontname="Lato" node [fontname="Lato"] @@ -396,21 +403,18 @@ $txt #+RESULTS: [[file:autfilt-ex2.png]] - -Using =--remove-fin= will transform the automaton to remove all traces -of Fin-acceptance: this usually requires adding non-deterministic jumps to -altered copies of strongly-connected components. +Using =--cnf-acceptance= simply rewrites the acceptance condition in Conjunctive Normal Form: #+NAME: autfilt-ex3 #+BEGIN_SRC sh :results verbatim :export code -autfilt --remove-fin aut-ex1.hoa --dot=.a +autfilt --cnf-acceptance aut-ex1.hoa --dot=.a #+END_SRC #+RESULTS: autfilt-ex3 #+begin_example digraph G { rankdir=LR - label=<(Inf(⓿)&Inf(❶)&Inf(❹)) | Inf(⓿) | (Inf(❷)&Inf(❸))> + label=<(Inf(⓿) | Inf(❶) | Inf(❸)) & (Fin(❸) | Inf(❶) | Inf(❷))> labelloc="t" fontname="Lato" node [fontname="Lato"] @@ -420,7 +424,7 @@ digraph G { I -> 0 0 [label="0"] 0 -> 0 [label=<1
❸>] - 0 -> 1 [label=❸>] + 0 -> 1 [label=❶❸>] 0 -> 2 [label=⓿❸>] 1 [label="1"] 1 -> 0 [label=❸>] @@ -430,9 +434,6 @@ digraph G { 2 -> 0 [label=] 2 -> 1 [label=⓿>] 2 -> 2 [label=⓿>] - 2 -> 3 [label=⓿>] - 3 [label="3"] - 3 -> 3 [label=⓿❶❹>] } #+end_example @@ -442,3 +443,91 @@ $txt #+RESULTS: [[file:autfilt-ex3.png]] + + +Using =--remove-fin= transforms the automaton to remove all traces +of Fin-acceptance: this usually requires adding non-deterministic jumps to +altered copies of strongly-connected components. + +#+NAME: autfilt-ex4 +#+BEGIN_SRC sh :results verbatim :export code +autfilt --remove-fin aut-ex1.hoa --dot=.a +#+END_SRC + +#+RESULTS: autfilt-ex4 +#+begin_example +digraph G { + rankdir=LR + label=⓿) | Inf(❶) | (Inf(❷)&Inf(❸))> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=<1
❸>] + 0 -> 1 [label=❶❸>] + 0 -> 2 [label=❸>] + 1 [label="1"] + 1 -> 0 [label=❸>] + 1 -> 1 [label=❸>] + 1 -> 2 [label=❷❸>] + 2 [label="2"] + 2 -> 0 [label=] + 2 -> 1 [label=] + 2 -> 2 [label=] + 2 -> 3 [label=] + 3 [label="3"] + 3 -> 3 [label=⓿>] +} +#+end_example + +#+BEGIN_SRC dot :file autfilt-ex4.png :cmdline -Tpng :var txt=autfilt-ex4 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:autfilt-ex4.png]] + +Use =--mask-acc=NUM= to remove some acceptances sets and all +transitions they contain. The acceptance condition will be updated to +reflect the fact that these sets can never be visited. + +#+NAME: autfilt-ex5 +#+BEGIN_SRC sh :results verbatim :export code +autfilt --mask-acc=1,2 aut-ex1.hoa --dot=.a +#+END_SRC + +#+RESULTS: autfilt-ex5 +#+begin_example +digraph G { + rankdir=LR + label=❶) & Inf(⓿)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=<1
❶>] + 0 -> 1 [label=⓿❶>] + 1 [label="1"] + 1 -> 0 [label=] + 1 -> 2 [label=⓿>] + 1 -> 1 [label=⓿>] + 2 [label="2"] + 2 -> 0 [label=❶>] + 2 -> 2 [label=⓿❶>] +} +#+end_example + +#+BEGIN_SRC dot :file autfilt-ex5.png :cmdline -Tpng :var txt=autfilt-ex5 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:autfilt-ex5.png]] diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index 4218bf04a..d7c024a9d 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -31,7 +31,7 @@ namespace spot unsigned tr = to_remove.count(); assert(tr <= na); res->set_acceptance(na - tr, - in->get_acceptance().strip(to_remove, false)); + in->get_acceptance().strip(to_remove, true)); transform_accessible(in, res, [&](unsigned, bdd& cond, acc_cond::mark_t& acc, diff --git a/src/tgbatest/maskacc.test b/src/tgbatest/maskacc.test index f449df7e2..1ee55b08e 100755 --- a/src/tgbatest/maskacc.test +++ b/src/tgbatest/maskacc.test @@ -28,8 +28,7 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +Acceptance: 2 Fin(0)&Fin(1) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -51,8 +50,7 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: Buchi -Acceptance: 1 Inf(0) +Acceptance: 1 Fin(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -74,8 +72,7 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: Buchi -Acceptance: 1 Inf(0) +Acceptance: 1 Fin(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -121,14 +118,14 @@ Acceptance: 3 Inf(1)|Fin(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[0] 1 {0} -[1] 2 {1} +[0] 1 {1} +[1] 2 {0} State: 1 [0] 2 -[0] 3 {1} +[0] 3 {0} State: 2 [1] 1 -[1] 3 {0} +[1] 3 {1} State: 3 [0] 3 {0 1} --END-- @@ -139,7 +136,7 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Inf(0) +Acceptance: 2 Fin(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -153,7 +150,7 @@ State: 3 --END-- EOF -run 0 ../../bin/autfilt --mask-acc=0 input4 -H >output +run 0 ../../bin/autfilt --mask-acc=1 input4 -H >output diff output expect4 # Errors