alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

CAR: Correct the value of the max color of the acceptance condition

Browse source 
* spot/twaalgos/car.cc: Update the max_color in apply_to_Buchi.
* tests/python/car.py: Add some tests that showed this issue.
This commit is contained in:
Florian Renkin 2020-02-25 12:59:45 +01:00
parent 4b9704a072
commit 6f3208a783
2 changed files with 60 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/car.cc
View file

@ -711,7 +711,10 @@ public:
col = inf_fin_prefix[c] + is_odd; col = inf_fin_prefix[c] + is_odd;
} }
if (col != -1) if (col != -1)
{
acc = { (unsigned) col }; acc = { (unsigned) col };
max_color = std::max(max_color, (unsigned) col);
}
else else
acc = {}; acc = {};
res_->new_edge(src_state, dst_state, e.cond, acc); res_->new_edge(src_state, dst_state, e.cond, acc);
@ -1048,6 +1051,7 @@ private:
bool scc_acc_clean, bool parity_equiv, bool use_last, bool parity_prefix, bool scc_acc_clean, bool parity_equiv, bool use_last, bool parity_prefix,
bool rabin_to_buchi, bool pretty_print) bool rabin_to_buchi, bool pretty_print)
{ {
auto new_aut = remove_false_transitions(aut); auto new_aut = remove_false_transitions(aut);
return car_generator(new_aut, search_ex, partial_degen, scc_acc_clean, return car_generator(new_aut, search_ex, partial_degen, scc_acc_clean,
parity_equiv, use_last, parity_prefix, parity_equiv, use_last, parity_prefix,

56
tests/python/car.py
View file

@ -194,3 +194,59 @@ State: 3
[0&1] 3 {0} [0&1] 3 {0}
--END-- --END--
""")) """))
test(spot.automaton("""
HOA: v1
States: 5
Start: 0
AP: 2 "p1" "p0"
Acceptance: 5 (Fin(0) & Fin(1)) | (Fin(3) & (Inf(2)&Inf(4)))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0] 1
[0] 2
State: 1
[!0&!1] 1 {0 1}
[!0&1] 3
[0] 4
State: 2
[!0&1] 1
[0&!1] 2
[0&1] 2 {0 1 2 4}
[!0&!1] 3
State: 3
[!0&1] 3 {1 2 3}
[!0&!1] 3 {4}
[0&!1] 4 {3}
[0&1] 4 {1 2 3}
State: 4
[!0&!1] 3 {3}
[!0&1] 3 {1 2 3}
[0&!1] 4
[0&1] 4 {1 2 4}
--END--
"""))
test(spot.automaton("""
HOA: v1
States: 2
Start: 0
AP: 2 "p1" "p0"
Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&!1] 0 {2 3}
[!0&!1] 0 {2 3 4}
[!0&1] 1
[0&1] 1 {2 4}
State: 1
[!0&!1] 0 {0 2 3 4}
[!0&1] 1 {1}
[0&!1] 1 {2 3}
[0&1] 1 {1 2 4}
--END--
"""))