restructure the complementation code
The previous code was sometime doing the work of remove_fin() in addition to complementing the acceptance conditions. This separate the two operations clearly. Also the specialized code for complementing weak automata is now a specialized code for remove_fin() on weak automata. * src/twaalgos/dtgbacomp.hh, src/twaalgos/dtgbacomp.cc: Rename as ... * src/twaalgos/complement.hh, src/twaalgos/complement.cc: ... these. * src/twaalgos/Makefile.am: Adjust. * src/twaalgos/complement.hh (dtgba_complement): Rename as ... (dtwa_complement): ... this, and restrict the purpose to completion and accetance complementation. Further acceptance simplification can be done with remove_fin() and to_generalized_buchi(). * src/twaalgos/remfin.cc (remove_fin): Specialize handling of weak automata using the code that was originally in dtgba_complement(). Also mark the output as state-based when the input has to Inf. * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Make sure scc_filter is always called after to_generalized_buchi(). * bench/stutter/stutter_invariance_randomgraph.cc, src/bin/ltlcross.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc, src/twaalgos/powerset.cc, src/twaalgos/stutter.cc: Adjust usage. * src/tests/dstar.test, src/tests/ltl2dstar4.test, src/tests/remfin.test: Adjust expected outputs. * wrap/python/spot_impl.i: Export dtwa_complement().
This commit is contained in:
Alexandre Duret-Lutz
parent
fb642c6df5
commit
06d3bc67ea
18 changed files with 336 additions and 448 deletions
|
|
@ -53,7 +53,7 @@
|
|||
#include "twaalgos/isweakscc.hh"
|
||||
#include "twaalgos/reducerun.hh"
|
||||
#include "twaalgos/word.hh"
|
||||
#include "twaalgos/dtgbacomp.hh"
|
||||
#include "twaalgos/complement.hh"
|
||||
#include "twaalgos/cleanacc.hh"
|
||||
#include "misc/formater.hh"
|
||||
#include "twaalgos/stats.hh"
|
||||
|
|
@ -1016,7 +1016,7 @@ namespace
|
|||
if (!no_complement && pos[n]
|
||||
&& ((want_stats && !(*pstats)[n].nondeterministic)
|
||||
|| (!want_stats && is_deterministic(pos[n]))))
|
||||
comp_pos[n] = dtgba_complement(pos[n]);
|
||||
comp_pos[n] = dtwa_complement(pos[n]);
|
||||
}
|
||||
|
||||
// ---------- Negative Formula ----------
|
||||
|
|
@ -1056,7 +1056,7 @@ namespace
|
|||
if (!no_complement && neg[n]
|
||||
&& ((want_stats && !(*nstats)[n].nondeterministic)
|
||||
|| (!want_stats && is_deterministic(neg[n]))))
|
||||
comp_neg[n] = dtgba_complement(neg[n]);
|
||||
comp_neg[n] = dtwa_complement(neg[n]);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -244,7 +244,7 @@ digraph G {
|
|||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 [label="0", peripheries=2]
|
||||
0 -> 1 [label="!a & !b"]
|
||||
0 -> 2 [label="a & !b"]
|
||||
1 [label="1", peripheries=2]
|
||||
|
|
|
|||
|
|
@ -60,7 +60,8 @@
|
|||
#include "twaalgos/simulation.hh"
|
||||
#include "twaalgos/compsusp.hh"
|
||||
#include "twaalgos/powerset.hh"
|
||||
#include "twaalgos/dtgbacomp.hh"
|
||||
#include "twaalgos/complement.hh"
|
||||
#include "twaalgos/remfin.hh"
|
||||
#include "twaalgos/complete.hh"
|
||||
#include "twaalgos/dtbasat.hh"
|
||||
#include "twaalgos/dtgbasat.hh"
|
||||
|
|
@ -338,7 +339,7 @@ checked_main(int argc, char** argv)
|
|||
bool opt_determinize = false;
|
||||
unsigned opt_determinize_threshold = 0;
|
||||
unsigned opt_o_threshold = 0;
|
||||
bool opt_dtgbacomp = false;
|
||||
bool opt_dtwacomp = false;
|
||||
bool reject_bigger = false;
|
||||
bool opt_monitor = false;
|
||||
bool containment = false;
|
||||
|
|
@ -411,7 +412,7 @@ checked_main(int argc, char** argv)
|
|||
}
|
||||
else if (!strcmp(argv[formula_index], "-DC"))
|
||||
{
|
||||
opt_dtgbacomp = true;
|
||||
opt_dtwacomp = true;
|
||||
}
|
||||
else if (!strncmp(argv[formula_index], "-DS", 3)
|
||||
|| !strncmp(argv[formula_index], "-DT", 3))
|
||||
|
|
@ -1203,14 +1204,14 @@ checked_main(int argc, char** argv)
|
|||
a = satminimized;
|
||||
}
|
||||
|
||||
if (opt_dtgbacomp)
|
||||
if (opt_dtwacomp)
|
||||
{
|
||||
tm.start("DTGBA complement");
|
||||
a = dtgba_complement(ensure_digraph(a));
|
||||
tm.stop("DTGBA complement");
|
||||
tm.start("DTωA complement");
|
||||
a = remove_fin(dtwa_complement(ensure_digraph(a)));
|
||||
tm.stop("DTωA complement");
|
||||
}
|
||||
|
||||
if (opt_determinize || opt_dtgbacomp || opt_dtbasat >= 0
|
||||
if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0
|
||||
|| opt_dtgbasat >= 0)
|
||||
{
|
||||
if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
|
||||
|
|
|
|||
|
|
@ -41,13 +41,13 @@ $ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
|
|||
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
|
||||
$autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
|
||||
tee out
|
||||
test "`cat out`" = '9 144 4 25 416 416 2 0'
|
||||
test "`cat out`" = '9 144 4 25 149 416 2 0'
|
||||
|
||||
$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
|
||||
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
|
||||
SPOT_STREETT_CONV_MIN=1 $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
|
||||
tee out
|
||||
test "`cat out`" = '9 144 4 25 482 482 2 0'
|
||||
test "`cat out`" = '9 144 4 25 218 482 2 0'
|
||||
|
||||
|
||||
LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L"
|
||||
|
|
|
|||
|
|
@ -218,20 +218,13 @@ Acceptance: 1 Inf(0)
|
|||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&1] 0
|
||||
[!0&!1] 0
|
||||
[!0&1] 0
|
||||
[0&!1] 0
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[t] 0
|
||||
[!0] 1
|
||||
[!1] 2
|
||||
State: 1 {0}
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
[!0] 1
|
||||
State: 2 {0}
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[!1] 2
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 4
|
||||
|
|
@ -275,7 +268,7 @@ State: 2
|
|||
[!1] 0
|
||||
[0&!1] 1 {0}
|
||||
[!0&!1] 2 {0}
|
||||
[!0&!1] 3 {0}
|
||||
[!0&!1] 3
|
||||
State: 3
|
||||
[!0&!1] 3 {0 1 4}
|
||||
--END--
|
||||
|
|
@ -325,31 +318,30 @@ Acceptance: 2 Inf(1) | Inf(0)
|
|||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 6
|
||||
[0] 0
|
||||
[!0] 6
|
||||
[0] 8
|
||||
[0] 9
|
||||
State: 1 {0 1}
|
||||
[!0] 3
|
||||
[0] 3
|
||||
[t] 3
|
||||
State: 2 {0 1}
|
||||
[!0] 5
|
||||
[0] 1
|
||||
[!0] 5
|
||||
State: 3 {0 1}
|
||||
[!0] 6
|
||||
[0] 0
|
||||
[!0] 6
|
||||
State: 4 {0 1}
|
||||
[!0] 6
|
||||
[0] 4
|
||||
[!0] 6
|
||||
State: 5 {0 1}
|
||||
[!0] 7
|
||||
[0] 3
|
||||
[!0] 7
|
||||
State: 6
|
||||
[!0] 6
|
||||
[0] 0
|
||||
State: 7 {1}
|
||||
[!0] 6
|
||||
State: 7 {1}
|
||||
[0] 4
|
||||
[!0] 6
|
||||
State: 8
|
||||
[0] 8
|
||||
State: 9 {1}
|
||||
|
|
@ -547,68 +539,61 @@ Acceptance: 1 Inf(0)
|
|||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&1] 0
|
||||
[!0&!1] 0
|
||||
[!0&1] 0
|
||||
[0&!1] 0
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[t] 0
|
||||
[!0] 1
|
||||
[!1] 2
|
||||
State: 1 {0}
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
[!0] 1
|
||||
State: 2 {0}
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[!1] 2
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 4
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 Inf(0)&Inf(1)
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0 {0 1}
|
||||
[0] 1 {0 1}
|
||||
[!0] 2 {0 1}
|
||||
[t] 0 {0}
|
||||
[0] 1 {0}
|
||||
[!0] 2 {0}
|
||||
State: 1
|
||||
[1] 0 {1}
|
||||
[0&1] 1 {1}
|
||||
[!0&1] 2 {0 1}
|
||||
[1] 0
|
||||
[0&1] 1
|
||||
[!0&1] 2 {0}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[0&!1] 1
|
||||
[!0&!1] 2
|
||||
[!0&!1] 3
|
||||
State: 3
|
||||
[!0&!1] 3 {0 1}
|
||||
[!0&!1] 3 {0}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 4
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Buchi 2
|
||||
Acceptance: 2 Inf(0)&Inf(1)
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0 {1}
|
||||
[0] 1 {1}
|
||||
[!0] 2 {0 1}
|
||||
[t] 0
|
||||
[0] 1
|
||||
[!0] 2 {0}
|
||||
State: 1
|
||||
[1] 0 {1}
|
||||
[0&1] 1 {0 1}
|
||||
[!0&1] 2 {0 1}
|
||||
[1] 0
|
||||
[0&1] 1 {0}
|
||||
[!0&1] 2 {0}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[0&!1] 1 {0 1}
|
||||
[!0&!1] 2 {0 1}
|
||||
[!0&!1] 3 {0 1}
|
||||
[0&!1] 1 {0}
|
||||
[!0&!1] 2 {0}
|
||||
[!0&!1] 3
|
||||
State: 3
|
||||
[!0&!1] 3 {0 1}
|
||||
[!0&!1] 3 {0}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
|
|
@ -646,47 +631,42 @@ State: 0
|
|||
[!0] 0
|
||||
[0] 1
|
||||
State: 1 {0}
|
||||
[!0] 1
|
||||
[0] 1
|
||||
[t] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 10
|
||||
States: 9
|
||||
Start: 2
|
||||
AP: 1 "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 6
|
||||
[0] 0
|
||||
[!0] 6
|
||||
[0] 8
|
||||
[0] 9
|
||||
State: 1 {0}
|
||||
[!0] 3
|
||||
[0] 3
|
||||
State: 2 {0}
|
||||
[!0] 5
|
||||
State: 1
|
||||
[t] 3
|
||||
State: 2
|
||||
[0] 1
|
||||
State: 3 {0}
|
||||
[!0] 6
|
||||
[!0] 5
|
||||
State: 3
|
||||
[0] 0
|
||||
State: 4 {0}
|
||||
[!0] 6
|
||||
[0] 4
|
||||
State: 5 {0}
|
||||
[!0] 7
|
||||
State: 4
|
||||
[0] 4 {0}
|
||||
[!0] 6
|
||||
State: 5
|
||||
[0] 3
|
||||
[!0] 7
|
||||
State: 6
|
||||
[!0] 6
|
||||
[0] 0
|
||||
State: 7 {0}
|
||||
[!0] 6
|
||||
[0] 4
|
||||
State: 7
|
||||
[0] 4 {0}
|
||||
[!0] 6
|
||||
State: 8
|
||||
[0] 8
|
||||
State: 9 {0}
|
||||
[0] 9
|
||||
[0] 8 {0}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 15
|
||||
|
|
@ -694,83 +674,75 @@ Start: 13
|
|||
AP: 2 "p1" "p0"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
State: 0
|
||||
[0&1] 0 {0}
|
||||
[!0&1] 1 {0}
|
||||
[0&!1] 11 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&1] 1
|
||||
[0&1] 0
|
||||
State: 1 {0}
|
||||
State: 1
|
||||
[0&1] 0 {0}
|
||||
[!0&1] 1 {0}
|
||||
[0&!1] 11 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&1] 1
|
||||
[0&1] 0
|
||||
State: 2 {0}
|
||||
[!0&!1] 10
|
||||
[0&!1] 11
|
||||
[!0&1] 2
|
||||
State: 2
|
||||
[!0&1] 2 {0}
|
||||
[0&1] 9
|
||||
State: 3 {0}
|
||||
[!0&!1] 10 {0}
|
||||
[0&!1] 11 {0}
|
||||
State: 3
|
||||
[!0&1] 1 {0}
|
||||
[0&1] 3 {0}
|
||||
[0&!1] 11 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&1] 1
|
||||
[0&1] 3
|
||||
State: 4 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 12
|
||||
[!0&1] 4
|
||||
[0&1] 7
|
||||
State: 5 {0}
|
||||
[!0&!1] 10
|
||||
[0&!1] 12
|
||||
[!0&1] 5
|
||||
State: 4
|
||||
[!0&1] 4 {0}
|
||||
[0&1] 7 {0}
|
||||
[!1] 12
|
||||
State: 5
|
||||
[!0&1] 5 {0}
|
||||
[0&1] 8
|
||||
State: 6 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&1] 4
|
||||
[0&1] 6
|
||||
State: 7 {0}
|
||||
[!0&!1] 12
|
||||
[!0&!1] 10 {0}
|
||||
[0&!1] 12
|
||||
[!0&1] 4
|
||||
[0&1] 7
|
||||
State: 6
|
||||
[!0&1] 4 {0}
|
||||
[0&1] 6 {0}
|
||||
[0&!1] 11 {0}
|
||||
[!0&!1] 12
|
||||
State: 7
|
||||
[!0&1] 4 {0}
|
||||
[0&1] 7 {0}
|
||||
[!1] 12
|
||||
State: 8
|
||||
[!0&!1] 12
|
||||
[0&!1] 12
|
||||
[!0&1] 8
|
||||
[0&1] 8
|
||||
[!0&1] 14
|
||||
[0&1] 14
|
||||
[1] 8
|
||||
[!1] 12
|
||||
[1] 14
|
||||
State: 9
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&1] 1
|
||||
[0&1] 3
|
||||
State: 10 {0}
|
||||
[!0&!1] 10
|
||||
[0&!1] 12
|
||||
[!0&1] 5
|
||||
[0&1] 8
|
||||
State: 11 {0}
|
||||
[!0&!1] 12
|
||||
[0&!1] 11
|
||||
[!0&!1] 12
|
||||
State: 10
|
||||
[!0&1] 5 {0}
|
||||
[0&1] 8
|
||||
[!0&!1] 10 {0}
|
||||
[0&!1] 12
|
||||
State: 11
|
||||
[0&1] 6 {0}
|
||||
[!0&1] 8
|
||||
[0&1] 6
|
||||
[0&!1] 11 {0}
|
||||
[!0&!1] 12
|
||||
State: 12
|
||||
[!0&!1] 12
|
||||
[0&!1] 12
|
||||
[!0&1] 8
|
||||
[0&1] 8
|
||||
[1] 8
|
||||
[!1] 12
|
||||
State: 13
|
||||
[!0&!1] 10
|
||||
[0&!1] 11
|
||||
[!0&1] 2
|
||||
[0&1] 3
|
||||
State: 14 {0}
|
||||
[!0&1] 14
|
||||
[0&1] 14
|
||||
[!0&!1] 10
|
||||
[0&!1] 11
|
||||
State: 14
|
||||
[1] 14 {0}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 4
|
||||
|
|
@ -797,44 +769,26 @@ State: 3 {0}
|
|||
[!0&1] 3
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 6
|
||||
Start: 5
|
||||
States: 5
|
||||
Start: 4
|
||||
AP: 2 "p0" "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
properties: trans-labels explicit-labels trans-acc deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0
|
||||
[0&!1] 0
|
||||
[!0&1] 0
|
||||
[0&1] 0
|
||||
[0] 1
|
||||
State: 1
|
||||
[!0&!1] 0
|
||||
[0&!1] 2
|
||||
[t] 1 {0}
|
||||
State: 2
|
||||
[!0&1] 0
|
||||
[0&1] 2
|
||||
State: 2 {0}
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
[!0&1] 2
|
||||
[0&1] 2
|
||||
State: 3 {0}
|
||||
[!0&!1] 3
|
||||
[0&!1] 2
|
||||
[!0&1] 1
|
||||
[0&1] 2
|
||||
[0] 1 {0}
|
||||
[!0&!1] 2 {0}
|
||||
State: 3
|
||||
[1] 0
|
||||
[!1] 2
|
||||
State: 4
|
||||
[!0&!1] 3
|
||||
[0&!1] 3
|
||||
[!0&1] 1
|
||||
[0&1] 1
|
||||
State: 5
|
||||
[!0&!1] 4
|
||||
[0&!1] 4
|
||||
[!0&1] 4
|
||||
[0&1] 4
|
||||
[t] 3
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 5
|
||||
|
|
@ -845,24 +799,18 @@ Acceptance: 1 Inf(0)
|
|||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 2
|
||||
[0&!1] 0
|
||||
[!0&1] 2
|
||||
[!0] 2
|
||||
[0&1] 3
|
||||
State: 1
|
||||
[!0&!1] 2
|
||||
[0&!1] 1
|
||||
[!0&1] 2
|
||||
[0&1] 2
|
||||
[!0 | 1] 2
|
||||
State: 2 {0}
|
||||
[!0&!1] 2
|
||||
[0&!1] 0
|
||||
[!0&1] 2
|
||||
[0&1] 2
|
||||
[!0 | 1] 2
|
||||
State: 3
|
||||
[!0&!1] 2
|
||||
[0&!1] 0
|
||||
[!0&1] 2
|
||||
[!0] 2
|
||||
[0&1] 3
|
||||
[0&1] 4
|
||||
State: 4 {0}
|
||||
|
|
|
|||
|
|
@ -33,10 +33,10 @@ twaalgos_HEADERS = \
|
|||
canonicalize.hh \
|
||||
cleanacc.hh \
|
||||
complete.hh \
|
||||
complement.hh \
|
||||
compsusp.hh \
|
||||
copy.hh \
|
||||
cycles.hh \
|
||||
dtgbacomp.hh \
|
||||
degen.hh \
|
||||
dot.hh \
|
||||
dtbasat.hh \
|
||||
|
|
@ -90,10 +90,10 @@ libtwaalgos_la_SOURCES = \
|
|||
canonicalize.cc \
|
||||
cleanacc.cc \
|
||||
complete.cc \
|
||||
complement.cc \
|
||||
compsusp.cc \
|
||||
copy.cc \
|
||||
cycles.cc \
|
||||
dtgbacomp.cc \
|
||||
degen.cc \
|
||||
dot.cc \
|
||||
dtbasat.cc \
|
||||
|
|
|
|||
35
src/twaalgos/complement.cc
Normal file
35
src/twaalgos/complement.cc
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 3 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "complement.hh"
|
||||
#include "sccinfo.hh"
|
||||
#include "complete.hh"
|
||||
#include "cleanacc.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
twa_graph_ptr
|
||||
dtwa_complement(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
// Simply complete the automaton, and complement its acceptance.
|
||||
auto res = cleanup_acceptance_here(complete(aut));
|
||||
res->set_acceptance(res->num_sets(), res->get_acceptance().complement());
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
|
@ -23,13 +23,19 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Complement a deterministic TGBA
|
||||
/// \brief Complement a deterministic TωA
|
||||
///
|
||||
/// The automaton \a aut should be deterministic. It does no need
|
||||
/// to be complete. Acceptance can be transition-based, or
|
||||
/// state-based. Unless the input automaton is marked as weak (in
|
||||
/// which case the output will also be weak and deterministic) the
|
||||
/// resulting automaton is very unlikely to be deterministic.
|
||||
/// The automaton \a aut should be deterministic. It will be
|
||||
/// completed if it isn't already. In these conditions,
|
||||
/// complementing the automaton can be done by just complementing
|
||||
/// the acceptance condition.
|
||||
///
|
||||
/// In particular, this implies that an input that use
|
||||
/// generalized Büchi will be output as generalized co-Büchi.
|
||||
///
|
||||
/// Functions like to_generalized_buchi() or remove_fin() are
|
||||
/// frequently called after dtwa_complement() to obtain an easier
|
||||
/// acceptance condition (maybe at the cost of loosing determinism.)
|
||||
SPOT_API twa_graph_ptr
|
||||
dtgba_complement(const const_twa_graph_ptr& aut);
|
||||
dtwa_complement(const const_twa_graph_ptr& aut);
|
||||
}
|
||||
|
|
@ -1,187 +0,0 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 3 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "dtgbacomp.hh"
|
||||
#include "sccinfo.hh"
|
||||
#include "complete.hh"
|
||||
#include "cleanacc.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
static twa_graph_ptr
|
||||
dtgba_complement_nonweak(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
// Clone the original automaton.
|
||||
auto res = make_twa_graph(aut,
|
||||
{ false, // state based
|
||||
false, // inherently_weak
|
||||
false, // deterministic
|
||||
true, // stutter inv.
|
||||
});
|
||||
// Copy the old acceptance condition before we replace it.
|
||||
acc_cond oldacc = aut->acc(); // Copy it!
|
||||
|
||||
// We will modify res in place, and the resulting
|
||||
// automaton will only have one acceptance set.
|
||||
// This changes aut->acc();
|
||||
res->set_buchi();
|
||||
// The resulting automaton is weak.
|
||||
res->prop_inherently_weak();
|
||||
res->prop_state_based_acc();
|
||||
|
||||
unsigned num_sets = oldacc.num_sets();
|
||||
unsigned n = res->num_states();
|
||||
// We will duplicate the automaton as many times as we have
|
||||
// acceptance sets, and we need one extra sink state.
|
||||
res->new_states(num_sets * n + 1);
|
||||
unsigned sink = res->num_states() - 1;
|
||||
// The sink state has an accepting self-loop.
|
||||
res->new_acc_edge(sink, sink, bddtrue);
|
||||
|
||||
for (unsigned src = 0; src < n; ++src)
|
||||
{
|
||||
// Keep track of all conditions on edge leaving state
|
||||
// SRC, so we can complete it.
|
||||
bdd missingcond = bddtrue;
|
||||
for (auto& t: res->out(src))
|
||||
{
|
||||
if (t.dst >= n) // Ignore edges we added.
|
||||
break;
|
||||
missingcond -= t.cond;
|
||||
acc_cond::mark_t curacc = t.acc;
|
||||
// The original edge must not accept anymore.
|
||||
t.acc = 0U;
|
||||
|
||||
// Edge that were fully accepting are never cloned.
|
||||
if (oldacc.accepting(curacc))
|
||||
continue;
|
||||
// Save t.cond and t.dst as the reference to t
|
||||
// is invalided by calls to new_edge().
|
||||
unsigned dst = t.dst;
|
||||
bdd cond = t.cond;
|
||||
|
||||
// Iterate over all the acceptance conditions in 'curacc',
|
||||
// an duplicate it for each clone for which it does not
|
||||
// belong to the acceptance set.
|
||||
unsigned add = 0;
|
||||
for (unsigned set = 0; set < num_sets; ++set)
|
||||
{
|
||||
add += n;
|
||||
if (!oldacc.has(curacc, set))
|
||||
{
|
||||
// Clone the edge
|
||||
res->new_acc_edge(src + add, dst + add, cond);
|
||||
assert(dst + add < sink);
|
||||
// Using `t' is disallowed from now on as it is a
|
||||
// reference to a edge that may have been
|
||||
// reallocated.
|
||||
|
||||
// At least one edge per cycle should have a
|
||||
// nondeterministic copy from the original clone.
|
||||
// We use state numbers to select it, as any cycle
|
||||
// is guaranteed to have at least one edge
|
||||
// with dst <= src. FIXME: Computing a feedback
|
||||
// arc set would be better.
|
||||
if (dst <= src)
|
||||
res->new_edge(src, dst + add, cond);
|
||||
}
|
||||
}
|
||||
assert(add == num_sets * n);
|
||||
}
|
||||
// Complete the original automaton.
|
||||
if (missingcond != bddfalse)
|
||||
res->new_edge(src, sink, missingcond);
|
||||
}
|
||||
res->merge_edges();
|
||||
res->purge_dead_states();
|
||||
return res;
|
||||
}
|
||||
|
||||
static twa_graph_ptr
|
||||
dtgba_complement_weak(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
// Clone the original automaton.
|
||||
auto res = make_twa_graph(aut,
|
||||
{ true, // state based
|
||||
true, // inherently weak
|
||||
true, // determinisitic
|
||||
true, // stutter inv.
|
||||
});
|
||||
scc_info si(res);
|
||||
|
||||
// We will modify res in place, and the resulting
|
||||
// automaton will only have one acceptance set.
|
||||
acc_cond::mark_t all_acc = res->set_buchi();
|
||||
res->prop_state_based_acc();
|
||||
|
||||
unsigned sink = res->num_states();
|
||||
|
||||
for (unsigned src = 0; src < sink; ++src)
|
||||
{
|
||||
acc_cond::mark_t acc = 0U;
|
||||
unsigned scc = si.scc_of(src);
|
||||
if (si.is_rejecting_scc(scc) && !si.is_trivial(scc))
|
||||
acc = all_acc;
|
||||
|
||||
// Keep track of all conditions on edge leaving state
|
||||
// SRC, so we can complete it.
|
||||
bdd missingcond = bddtrue;
|
||||
for (auto& t: res->out(src))
|
||||
{
|
||||
missingcond -= t.cond;
|
||||
t.acc = acc;
|
||||
}
|
||||
// Complete the original automaton.
|
||||
if (missingcond != bddfalse)
|
||||
{
|
||||
if (res->num_states() == sink)
|
||||
{
|
||||
res->new_state();
|
||||
res->new_acc_edge(sink, sink, bddtrue);
|
||||
}
|
||||
res->new_edge(src, sink, missingcond);
|
||||
}
|
||||
}
|
||||
//res->merge_edges();
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
twa_graph_ptr dtgba_complement(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
if (aut->acc().is_generalized_buchi())
|
||||
{
|
||||
if (aut->is_inherently_weak())
|
||||
return dtgba_complement_weak(aut);
|
||||
else
|
||||
return dtgba_complement_nonweak(aut);
|
||||
}
|
||||
else
|
||||
{
|
||||
// Simply complete the automaton, and complement its
|
||||
// acceptance.
|
||||
auto res = cleanup_acceptance_here(complete(aut));
|
||||
res->set_acceptance(res->num_sets(),
|
||||
res->get_acceptance().complement());
|
||||
return res;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -44,7 +44,8 @@
|
|||
#include "twaalgos/ltl2tgba_fm.hh"
|
||||
#include "twaalgos/bfssteps.hh"
|
||||
#include "twaalgos/isdet.hh"
|
||||
#include "twaalgos/dtgbacomp.hh"
|
||||
#include "twaalgos/complement.hh"
|
||||
#include "twaalgos/remfin.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -632,7 +633,7 @@ namespace spot
|
|||
{
|
||||
// If the automaton is deterministic, complementing is
|
||||
// easy.
|
||||
aut_neg_f = dtgba_complement(aut_f);
|
||||
aut_neg_f = remove_fin(dtwa_complement(aut_f));
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -654,7 +655,7 @@ namespace spot
|
|||
{
|
||||
// Complement the minimized WDBA.
|
||||
assert(min_aut_f->is_inherently_weak());
|
||||
auto neg_min_aut_f = dtgba_complement(min_aut_f);
|
||||
auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
|
||||
if (product(aut_f, neg_min_aut_f)->is_empty())
|
||||
// Finally, we are now sure that it was safe
|
||||
// to minimize the automaton.
|
||||
|
|
|
|||
|
|
@ -139,6 +139,23 @@ namespace spot
|
|||
return do_sba_simul(d, ba_simul_);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg)
|
||||
{
|
||||
if (scc_filter_ == 0)
|
||||
return a;
|
||||
if (state_based_ && a->has_state_based_acc())
|
||||
return scc_filter_states(a);
|
||||
else
|
||||
return scc_filter(a, arg);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
postprocessor::do_scc_filter(const twa_graph_ptr& a)
|
||||
{
|
||||
return do_scc_filter(a, scc_filter_ > 1);
|
||||
}
|
||||
|
||||
#define PREF_ (pref_ & (Small | Deterministic))
|
||||
#define COMP_ (pref_ & Complete)
|
||||
#define SBACC_ (pref_ & SBAcc)
|
||||
|
|
@ -146,22 +163,6 @@ namespace spot
|
|||
twa_graph_ptr
|
||||
postprocessor::run(twa_graph_ptr a, formula f)
|
||||
{
|
||||
if (type_ != Generic && !a->acc().is_generalized_buchi())
|
||||
a = to_generalized_buchi(a);
|
||||
|
||||
if (PREF_ == Any && level_ == Low)
|
||||
if (type_ == Generic
|
||||
|| type_ == TGBA
|
||||
|| (type_ == BA && a->is_sba())
|
||||
|| (type_ == Monitor && a->num_sets() == 0))
|
||||
{
|
||||
if (COMP_)
|
||||
a = complete(a);
|
||||
if (SBACC_)
|
||||
a = sbacc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
if (simul_ < 0)
|
||||
simul_ = (level_ == Low) ? 1 : 3;
|
||||
if (ba_simul_ < 0)
|
||||
|
|
@ -171,6 +172,28 @@ namespace spot
|
|||
if (type_ == BA || SBACC_)
|
||||
state_based_ = true;
|
||||
|
||||
bool tgb_used = false;
|
||||
if (type_ != Generic && !a->acc().is_generalized_buchi())
|
||||
{
|
||||
a = to_generalized_buchi(a);
|
||||
tgb_used = true;
|
||||
}
|
||||
|
||||
if (PREF_ == Any && level_ == Low)
|
||||
if (type_ == Generic
|
||||
|| type_ == TGBA
|
||||
|| (type_ == BA && a->is_sba())
|
||||
|| (type_ == Monitor && a->num_sets() == 0))
|
||||
{
|
||||
if (tgb_used)
|
||||
a = do_scc_filter(a);
|
||||
if (COMP_)
|
||||
a = complete(a);
|
||||
if (SBACC_)
|
||||
a = sbacc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
int original_acc = a->num_sets();
|
||||
|
||||
// Remove useless SCCs.
|
||||
|
|
@ -178,13 +201,8 @@ namespace spot
|
|||
// Do not bother about acceptance conditions, they will be
|
||||
// ignored.
|
||||
a = scc_filter_states(a);
|
||||
else if (scc_filter_ > 0)
|
||||
{
|
||||
if (state_based_ && a->has_state_based_acc())
|
||||
a = scc_filter_states(a);
|
||||
else
|
||||
a = scc_filter(a, scc_filter_ > 1);
|
||||
}
|
||||
else
|
||||
a = do_scc_filter(a);
|
||||
|
||||
if (type_ == Monitor)
|
||||
{
|
||||
|
|
@ -380,7 +398,7 @@ namespace spot
|
|||
in = dba;
|
||||
}
|
||||
|
||||
const_twa_graph_ptr res = complete(in);
|
||||
twa_graph_ptr res = complete(in);
|
||||
if (target_acc == 1)
|
||||
{
|
||||
if (sat_states_ != -1)
|
||||
|
|
@ -408,14 +426,7 @@ namespace spot
|
|||
|
||||
if (res)
|
||||
{
|
||||
if (state_based_)
|
||||
// FIXME: This does not simplify generalized acceptance
|
||||
// conditions, but calling scc_filter() would break the
|
||||
// BA-typeness of res by removing acceptance marks from
|
||||
// out-of-SCC transitions.
|
||||
dba = scc_filter_states(res);
|
||||
else
|
||||
dba = scc_filter(res, true);
|
||||
dba = do_scc_filter(res, true);
|
||||
dba_is_minimal = true;
|
||||
}
|
||||
}
|
||||
|
|
@ -438,18 +449,12 @@ namespace spot
|
|||
{
|
||||
if (dba && !dba_is_minimal) // WDBA is already clean.
|
||||
{
|
||||
if (state_based_ && dba->has_state_based_acc())
|
||||
dba = scc_filter_states(dba);
|
||||
else
|
||||
dba = scc_filter(dba, true);
|
||||
dba = do_scc_filter(dba, true);
|
||||
assert(!sim);
|
||||
}
|
||||
else if (sim)
|
||||
{
|
||||
if (state_based_ && sim->has_state_based_acc())
|
||||
sim = scc_filter_states(sim);
|
||||
else
|
||||
sim = scc_filter(sim, true);
|
||||
sim = do_scc_filter(sim, true);
|
||||
assert(!dba);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -105,6 +105,8 @@ namespace spot
|
|||
twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt);
|
||||
twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt);
|
||||
twa_graph_ptr do_degen(const twa_graph_ptr& input);
|
||||
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg);
|
||||
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a);
|
||||
|
||||
output_type type_;
|
||||
int pref_;
|
||||
|
|
|
|||
|
|
@ -34,7 +34,8 @@
|
|||
#include "twaalgos/gtec/gtec.hh"
|
||||
#include "twaalgos/sccfilter.hh"
|
||||
#include "twaalgos/ltl2tgba_fm.hh"
|
||||
#include "twaalgos/dtgbacomp.hh"
|
||||
#include "twaalgos/complement.hh"
|
||||
#include "twaalgos/remfin.hh"
|
||||
#include "misc/bitvect.hh"
|
||||
#include "misc/bddlt.hh"
|
||||
|
||||
|
|
@ -426,7 +427,7 @@ namespace spot
|
|||
|
||||
if (product(det, neg_aut)->is_empty())
|
||||
// Complement the DBA.
|
||||
if (product(aut, dtgba_complement(det))->is_empty())
|
||||
if (product(aut, remove_fin(dtwa_complement(det)))->is_empty())
|
||||
// Finally, we are now sure that it was safe
|
||||
// to determinize the automaton.
|
||||
return det;
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@
|
|||
#include <iostream>
|
||||
#include "cleanacc.hh"
|
||||
#include "totgba.hh"
|
||||
#include "isdet.hh"
|
||||
#include "mask.hh"
|
||||
|
||||
//#define TRACE
|
||||
|
|
@ -450,6 +451,54 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
static twa_graph_ptr
|
||||
remove_fin_det_weak(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
// Clone the original automaton.
|
||||
auto res = make_twa_graph(aut,
|
||||
{
|
||||
true, // state based
|
||||
true, // inherently weak
|
||||
true, // determinisitic
|
||||
true, // stutter inv.
|
||||
});
|
||||
scc_info si(res);
|
||||
|
||||
// We will modify res in place, and the resulting
|
||||
// automaton will only have one acceptance set.
|
||||
acc_cond::mark_t all_acc = res->set_buchi();
|
||||
res->prop_state_based_acc();
|
||||
res->prop_deterministic();
|
||||
|
||||
unsigned sink = res->num_states();
|
||||
for (unsigned src = 0; src < sink; ++src)
|
||||
{
|
||||
acc_cond::mark_t acc = 0U;
|
||||
unsigned scc = si.scc_of(src);
|
||||
if (si.is_accepting_scc(scc) && !si.is_trivial(scc))
|
||||
acc = all_acc;
|
||||
// Keep track of all conditions on edge leaving state
|
||||
// SRC, so we can complete it.
|
||||
bdd missingcond = bddtrue;
|
||||
for (auto& t: res->out(src))
|
||||
{
|
||||
missingcond -= t.cond;
|
||||
t.acc = acc;
|
||||
}
|
||||
// Complete the original automaton.
|
||||
if (missingcond != bddfalse)
|
||||
{
|
||||
if (res->num_states() == sink)
|
||||
{
|
||||
res->new_state();
|
||||
res->new_acc_edge(sink, sink, bddtrue);
|
||||
}
|
||||
res->new_edge(src, sink, missingcond);
|
||||
}
|
||||
}
|
||||
//res->merge_edges();
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
|
||||
|
|
@ -457,6 +506,10 @@ namespace spot
|
|||
if (!aut->acc().uses_fin_acceptance())
|
||||
return std::const_pointer_cast<twa_graph>(aut);
|
||||
|
||||
// FIXME: we should check whether the automaton is weak.
|
||||
if (aut->is_inherently_weak() && is_deterministic(aut))
|
||||
return remove_fin_det_weak(aut);
|
||||
|
||||
if (auto maybe = streett_to_generalized_buchi_maybe(aut))
|
||||
return maybe;
|
||||
|
||||
|
|
@ -609,13 +662,13 @@ namespace spot
|
|||
unsigned nst = aut->num_states();
|
||||
auto res = make_twa_graph(aut->get_dict());
|
||||
res->copy_ap_of(aut);
|
||||
res->prop_copy(aut, { false, false, false, true });
|
||||
res->prop_copy(aut, { true, false, false, true });
|
||||
res->new_states(nst);
|
||||
res->set_acceptance(aut->num_sets() + extra_sets, new_code);
|
||||
res->set_init_state(aut->get_init_state_number());
|
||||
|
||||
bool sbacc = aut->has_state_based_acc();
|
||||
scc_info si(aut);
|
||||
|
||||
unsigned nscc = si.scc_count();
|
||||
std::vector<unsigned> state_map(nst);
|
||||
for (unsigned n = 0; n < nscc; ++n)
|
||||
|
|
@ -643,7 +696,12 @@ namespace spot
|
|||
// Create the main copy
|
||||
for (auto s: states)
|
||||
for (auto& t: aut->out(s))
|
||||
res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add);
|
||||
{
|
||||
acc_cond::mark_t a = 0U;
|
||||
if (sbacc || SPOT_LIKELY(si.scc_of(t.dst) == n))
|
||||
a = (t.acc & main_sets) | main_add;
|
||||
res->new_edge(s, t.dst, t.cond, a);
|
||||
}
|
||||
|
||||
// We do not need any other copy if the SCC is non-accepting,
|
||||
// of if it does not intersect any Fin.
|
||||
|
|
@ -673,22 +731,27 @@ namespace spot
|
|||
// We need only one non-deterministic jump per
|
||||
// cycle. As an approximation, we only do
|
||||
// them on back-links.
|
||||
//
|
||||
// The acceptance marks on these edge
|
||||
// are useless, but we keep them to preserve
|
||||
// state-based acceptance if any.
|
||||
if (t.dst <= s)
|
||||
res->new_edge(s, nd, t.cond,
|
||||
(t.acc & main_sets) | main_add);
|
||||
{
|
||||
acc_cond::mark_t a = 0U;
|
||||
if (sbacc)
|
||||
a = (t.acc & main_sets) | main_add;
|
||||
res->new_edge(s, nd, t.cond, a);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// If the input had no Inf, the output is a state-based automaton.
|
||||
if (allinf == 0U)
|
||||
res->prop_state_based_acc();
|
||||
|
||||
res->purge_dead_states();
|
||||
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
||||
cleanup_acceptance_here(res);
|
||||
trace << "after cleanup: " << res->get_acceptance() << '\n';
|
||||
res->merge_edges();
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,7 +27,8 @@
|
|||
#include "twaalgos/product.hh"
|
||||
#include "twaalgos/ltl2tgba_fm.hh"
|
||||
#include "twaalgos/isdet.hh"
|
||||
#include "twaalgos/dtgbacomp.hh"
|
||||
#include "twaalgos/complement.hh"
|
||||
#include "twaalgos/remfin.hh"
|
||||
#include "twa/twaproduct.hh"
|
||||
#include "twa/bddprint.hh"
|
||||
#include <deque>
|
||||
|
|
@ -635,8 +636,7 @@ namespace spot
|
|||
aut->prop_deterministic(is_deterministic(aut));
|
||||
if (!aut->is_deterministic())
|
||||
return false;
|
||||
|
||||
neg = dtgba_complement(aut);
|
||||
neg = remove_fin(dtwa_complement(aut));
|
||||
}
|
||||
|
||||
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue