Commit ff2a96cc authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

fix a bug in streett_to_generalized_buchi

Fixes #320.

* spot/twaalgos/totgba.cc: Fix the bug.
* NEWS: Mention the problem.
* tests/core/streett.test: Add test case.
parent c68b04a9
New in spot 2.5.0.dev (not yet released)
Nothing yet.
Bugs fixed:
- streett_to_generalized_buchi() could produce incorrect result on
Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1)
where some Fin(x) is used both with and without a paired Fin(y).
New in spot 2.5 (2018-01-20)
......
......@@ -551,6 +551,7 @@ namespace spot
// At some point we will remove anything that is not used as Inf.
acc_cond::mark_t to_strip = in->acc().all_sets() - inf;
acc_cond::mark_t inf_alone = 0U;
acc_cond::mark_t fin_alone = 0U;
if (!p)
return remove_fin(in);
......@@ -569,7 +570,14 @@ namespace spot
if (pair.inf)
for (unsigned mark: pair.inf.sets())
inf_to_finpairs[mark] |= pair.fin;
else
fin_alone |= pair.fin;
}
// If we have something like (Fin(0)|Inf(1))&Fin(0), then 0 is in
// fin_alone, but we also have fin_to_infpair[0] = {1}. This should
// really be simplified to Fin(0).
for (auto mark: fin_alone.sets())
fin_to_infpairs[mark] = 0U;
scc_info si(in, scc_info_options::NONE);
......@@ -583,10 +591,10 @@ namespace spot
auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9}
auto acc_fin = acc & fin; // {0, 2, 4,6}
auto acc_inf = acc & inf; // { 1, 3, 7,9}
acc_cond::mark_t fin_wo_inf = 0U;
// Fin sets that are alone either because the acceptance
// condition has not matching Inf, or because the SCC the not
// intersect the matching inf.
// condition has no matching Inf, or because the SCC does not
// intersect the matching Inf.
acc_cond::mark_t fin_wo_inf = 0U;
for (unsigned mark: acc_fin.sets())
if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf))
fin_wo_inf.set(mark);
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -113,3 +113,25 @@ EOF
run 0 autcross --language-preserved \
'autfilt --tgba %H | tee out.hoa >%O' -F streett.hoa
grep 'generalized-Buchi 2' out.hoa
# Issue #320
autfilt -q --reject-word='cycle{!a;a;a;!a}' <<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: Streett 3
Acceptance: 6 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0] 0 {1 3}
[0] 1 {}
State: 1
[0] 2 {2}
State: 2
[!0] 0 {0 4}
[0] 2 {}
--END--
EOF
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