diff --git a/spot/twaalgos/car.cc b/spot/twaalgos/car.cc index e4e26177f..87f42f4f2 100644 --- a/spot/twaalgos/car.cc +++ b/spot/twaalgos/car.cc @@ -711,7 +711,10 @@ public: col = inf_fin_prefix[c] + is_odd; } if (col != -1) + { acc = { (unsigned) col }; + max_color = std::max(max_color, (unsigned) col); + } else 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 rabin_to_buchi, bool pretty_print) { + auto new_aut = remove_false_transitions(aut); return car_generator(new_aut, search_ex, partial_degen, scc_acc_clean, parity_equiv, use_last, parity_prefix, diff --git a/tests/python/car.py b/tests/python/car.py index c4cb1992f..7050010c2 100644 --- a/tests/python/car.py +++ b/tests/python/car.py @@ -194,3 +194,59 @@ State: 3 [0&1] 3 {0} --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-- +""")) \ No newline at end of file