Commit 56f768f5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

remove_fin: improve behavior on unclean acceptance

Related to #188.  This is a third fix that independently
makes `'utfilt --is-unambiguous -q smaller.hoa' instantaneous.

* spot/twaalgos/remfin.cc: Clean the received automaton if
necessary.
* bin/autfilt.cc: No need to call cleanup_acceptance_here() before
remove_fin() anymore.
* tests/core/remfin.test: Add an additional test.
* NEWS: Mention the change.
parent 3dc084c4
...@@ -5,8 +5,13 @@ New in spot 2.1.2.dev (not yet released) ...@@ -5,8 +5,13 @@ New in spot 2.1.2.dev (not yet released)
* is_unambiguous() was rewritten in a more efficient way. * is_unambiguous() was rewritten in a more efficient way.
* scc_info learned to determine the acceptance of simple SCCs made * scc_info learned to determine the acceptance of simple SCCs made
of a single self-loop without ressorting to remove_fin() for complex of a single self-loop without ressorting to remove_fin() for complex
acceptance conditions. acceptance conditions.
* remove_fin() has been improved to better deal with automata with
"unclean" acceptance, i.e., acceptance sets that are declared but
not used. In particular, this helps scc_info to be more efficient
at deciding the acceptance of SCCs in presence of Fin acceptance.
New in spot 2.1.2 (2016-10-14) New in spot 2.1.2 (2016-10-14)
......
...@@ -979,7 +979,7 @@ namespace ...@@ -979,7 +979,7 @@ namespace
spot::strip_acceptance_here(aut); spot::strip_acceptance_here(aut);
if (opt_merge) if (opt_merge)
aut->merge_edges(); aut->merge_edges();
if (opt_clean_acc || opt_rem_fin) if (opt_clean_acc)
cleanup_acceptance_here(aut); cleanup_acceptance_here(aut);
if (opt_sep_sets) if (opt_sep_sets)
separate_sets_here(aut); separate_sets_here(aut);
......
...@@ -517,6 +517,20 @@ namespace spot ...@@ -517,6 +517,20 @@ namespace spot
if (auto maybe = rabin_to_buchi_maybe(aut)) if (auto maybe = rabin_to_buchi_maybe(aut))
return maybe; return maybe;
{
// We want a clean acceptance condition, i.e., one where all
// sets are useful. If that is not the case, clean it first.
acc_cond::mark_t unused = aut->acc().all_sets();
for (auto& t: aut->edges())
{
unused -= t.acc;
if (!unused)
break;
}
if (unused)
return remove_fin(cleanup_acceptance(aut));
}
std::vector<acc_cond::acc_code> code; std::vector<acc_cond::acc_code> code;
std::vector<acc_cond::mark_t> rem; std::vector<acc_cond::mark_t> rem;
std::vector<acc_cond::mark_t> keep; std::vector<acc_cond::mark_t> keep;
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -206,8 +206,40 @@ deterministic complete stutter-insensitive comment: "Safra[NBA=3]" ...@@ -206,8 +206,40 @@ deterministic complete stutter-insensitive comment: "Safra[NBA=3]"
acc-name: Rabin 2 Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: acc-name: Rabin 2 Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start:
1 AP: 2 "p0" "p1" --BODY-- State: 0 {2} 2 0 2 3 State: 1 {0 2} 2 1 2 2 1 AP: 2 "p0" "p1" --BODY-- State: 0 {2} 2 0 2 3 State: 1 {0 2} 2 1 2 2
State: 2 {1 2} 2 0 2 2 State: 3 {3} 2 0 2 3 --END-- State: 2 {1 2} 2 0 2 2 State: 3 {3} 2 0 2 3 --END--
/* This is the square of smaller.hoa from #188. */
HOA: v1 States: 37 Start: 0 AP: 2 "a" "b" Acceptance: 24 (Inf(11) |
Fin(5)) & (Inf(10) | Fin(4)) & (Inf(9) | Fin(3)) & (Inf(8) | Fin(2)) &
(Inf(7) | Fin(1)) & (Inf(6) | Fin(0)) & (Inf(23) | Fin(17)) & (Inf(22)
| Fin(16)) & (Inf(21) | Fin(15)) & (Inf(20) | Fin(14)) & (Inf(19) |
Fin(13)) & (Inf(18) | Fin(12)) properties: trans-labels explicit-labels
trans-acc complete --BODY-- State: 0 [!0] 0 {0 12} [0] 1 [0&1] 2 [0&1]
3 [0&1] 4 State: 1 [t] 1 {1 13} [1] 2 {1} [1] 3 {13} [1] 4 State: 2
[t] 2 {1 14} [!1] 5 {1} [1] 4 {14} State: 3 [t] 3 {2 13} [1] 4 {2} [!1]
6 {13} State: 4 [t] 4 {2 14} [!1] 7 {2} [!1] 8 {14} [!1] 9 State: 5 [t]
5 {1 15} [1] 10 {1} [1] 7 {15} [1] 11 State: 6 [t] 6 {3 13} [1] 8 {3}
[1] 12 {13} [1] 13 State: 7 [t] 7 {2 15} [1] 11 {2} [!1] 9 {15} State:
8 [t] 8 {3 14} [!1] 9 {3} [1] 13 {14} State: 9 [t] 9 {3 15} [1] 14 {3}
[1] 15 {15} [1] 16 State: 10 [t] 10 {1 16} [!1] 17 {1} [1] 11 {16}
State: 11 [t] 11 {2 16} [!1] 18 {2} [!1] 14 {16} [!1] 19 State: 12 [t]
12 {4 13} [1] 13 {4} [!1] 20 {13} State: 13 [t] 13 {4 14} [!1] 15 {4}
[!1] 21 {14} [!1] 22 State: 14 [t] 14 {3 16} [!1] 19 {3} [1] 16 {16}
State: 15 [t] 15 {4 15} [1] 16 {4} [!1] 22 {15} State: 16 [t] 16 {4 16}
[!1] 23 {4} [!1] 24 {16} [!1] 25 State: 17 [1] 26 {1 23} [!1] 17 {1 17}
[1] 27 {23} State: 18 [1] 27 {2 23} [!1] 18 {2 17} [!1] 19 {17} State:
19 [1] 28 {3 23} [!1] 19 {3 17} [1] 29 {23} State: 20 [1] 30 {11 13}
[1] 31 {11} [!1] 20 {5 13} State: 21 [1] 31 {11 14} [!1] 21 {5 14} [!1]
22 {5} State: 22 [1] 32 {11 15} [1] 33 {11} [!1] 22 {5 15} State: 23
[1] 29 {4 23} [!1] 23 {4 17} [!1] 25 {17} State: 24 [1] 33 {11 16} [!1]
24 {5 16} [!1] 25 {5} State: 25 [1] 34 {11 23} [!1] 25 {5 17} State: 26
[t] 26 {1} [1] 27 State: 27 [t] 27 {2} [!1] 28 State: 28 [t] 28 {3} [1]
29 State: 29 [t] 29 {4} [!1] 35 State: 30 [t] 30 {13} [1] 31 State: 31
[t] 31 {14} [!1] 32 State: 32 [t] 32 {15} [1] 33 State: 33 [t] 33 {16}
[!1] 36 State: 34 [t] 34 State: 35 [1] 34 {11} [!1] 35 {5} State: 36
[1] 34 {23} [!1] 36 {17} --END--
EOF EOF
acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
acctwelve=$acctwelve'&Inf(6)&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11)'
cat >expected <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
States: 3 States: 3
...@@ -527,6 +559,160 @@ State: 3 ...@@ -527,6 +559,160 @@ State: 3
State: 4 {0} State: 4 {0}
[0&1] 4 [0&1] 4
--END-- --END--
HOA: v1
States: 37
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 12
Acceptance: 12 $acctwelve
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[!0] 0
[0] 1
[0&1] 2
[0&1] 3
[0&1] 4
State: 1
[t] 1
[1] 2
[1] 3
[1] 4
State: 2
[t] 2
[1] 4
[!1] 5
State: 3
[t] 3
[1] 4
[!1] 6
State: 4
[t] 4
[!1] 7
[!1] 8
[!1] 9
State: 5
[t] 5
[1] 7
[1] 10
[1] 11
State: 6
[t] 6
[1] 8
[1] 12
[1] 13
State: 7
[t] 7
[!1] 9
[1] 11
State: 8
[t] 8
[!1] 9
[1] 13
State: 9
[t] 9
[1] 14
[1] 15
[1] 16
State: 10
[t] 10
[1] 11
[!1] 17
State: 11
[t] 11
[!1] 14
[!1] 18
[!1] 19
State: 12
[t] 12
[1] 13
[!1] 20
State: 13
[t] 13
[!1] 15
[!1] 21
[!1] 22
State: 14
[t] 14
[1] 16
[!1] 19
State: 15
[t] 15
[1] 16
[!1] 22
State: 16
[t] 16
[!1] 23
[!1] 24
[!1] 25
State: 17
[!1] 17
[1] 26
[1] 27
State: 18
[!1] 18
[!1] 19
[1] 27
State: 19
[!1] 19
[1] 28
[1] 29
State: 20
[!1] 20
[1] 30
[1] 31
State: 21
[!1] 21
[!1] 22
[1] 31
State: 22
[!1] 22
[1] 32
[1] 33
State: 23
[!1] 23
[!1] 25
[1] 29
State: 24
[!1] 24
[!1] 25
[1] 33
State: 25
[!1] 25 {0 1 2 3 4 6 7 8 9 10}
[1] 34
State: 26
[t] 26
[1] 27
State: 27
[t] 27
[!1] 28
State: 28
[t] 28
[1] 29
State: 29
[t] 29
[!1] 35
State: 30
[t] 30
[1] 31
State: 31
[t] 31
[!1] 32
State: 32
[t] 32
[1] 33
State: 33
[t] 33
[!1] 36
State: 34
[t] 34 {0 1 2 3 4 5 6 7 8 9 10 11}
State: 35
[1] 34
[!1] 35 {0 1 2 3 4 6 7 8 9 10 11}
State: 36
[1] 34
[!1] 36 {0 1 2 3 4 5 6 7 8 9 10}
--END--
EOF EOF
cat >expected-tgba <<EOF cat >expected-tgba <<EOF
...@@ -816,6 +1002,160 @@ State: 3 ...@@ -816,6 +1002,160 @@ State: 3
State: 4 {0} State: 4 {0}
[0&1] 4 [0&1] 4
--END-- --END--
HOA: v1
States: 37
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[!0] 0
[0] 1
[0&1] 2
[0&1] 3
[0&1] 4
State: 1
[t] 1
[1] 2
[1] 3
[1] 4
State: 2
[t] 2
[1] 4
[!1] 5
State: 3
[t] 3
[1] 4
[!1] 6
State: 4
[t] 4
[!1] 7
[!1] 8
[!1] 9
State: 5
[t] 5
[1] 7
[1] 10
[1] 11
State: 6
[t] 6
[1] 8
[1] 12
[1] 13
State: 7
[t] 7
[!1] 9
[1] 11
State: 8
[t] 8
[!1] 9
[1] 13
State: 9
[t] 9
[1] 14
[1] 15
[1] 16
State: 10
[t] 10
[1] 11
[!1] 17
State: 11
[t] 11
[!1] 14
[!1] 18
[!1] 19
State: 12
[t] 12
[1] 13
[!1] 20
State: 13
[t] 13
[!1] 15
[!1] 21
[!1] 22
State: 14
[t] 14
[1] 16
[!1] 19
State: 15
[t] 15
[1] 16
[!1] 22
State: 16
[t] 16
[!1] 23
[!1] 24
[!1] 25
State: 17
[!1] 17
[1] 26
[1] 27
State: 18
[!1] 18
[!1] 19
[1] 27
State: 19
[!1] 19
[1] 28
[1] 29
State: 20
[!1] 20
[1] 30
[1] 31
State: 21
[!1] 21
[!1] 22
[1] 31
State: 22
[!1] 22
[1] 32
[1] 33
State: 23
[!1] 23
[!1] 25
[1] 29
State: 24
[!1] 24
[!1] 25
[1] 33
State: 25
[!1] 25
[1] 34
State: 26
[t] 26
[1] 27
State: 27
[t] 27
[!1] 28
State: 28
[t] 28
[1] 29
State: 29
[t] 29
[!1] 35
State: 30
[t] 30
[1] 31
State: 31
[t] 31
[!1] 32
State: 32
[t] 32
[1] 33
State: 33
[t] 33
[!1] 36
State: 34 {0}
[t] 34
State: 35
[1] 34
[!1] 35
State: 36
[1] 34
[!1] 36
--END--
EOF EOF
run 0 $autfilt -H --remove-fin test1 > output run 0 $autfilt -H --remove-fin test1 > output
......
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