diff --git a/NEWS b/NEWS index 8a9f897b9..12b724fe0 100644 --- a/NEWS +++ b/NEWS @@ -119,6 +119,9 @@ New in spot 2.8.7.dev (not yet released) - Relabeling automata could introduce false edges. Those are now removed. + - Emptiness checks, and scc_info should now ignore edges labeled + with false. + New in spot 2.8.7 (2020-03-13) Bugs fixed: diff --git a/spot/twaalgos/bfssteps.cc b/spot/twaalgos/bfssteps.cc index 131596117..af722d5a6 100644 --- a/spot/twaalgos/bfssteps.cc +++ b/spot/twaalgos/bfssteps.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2018 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2018, 2020 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -78,6 +78,10 @@ namespace spot todo.pop_front(); for (auto i: a_->succ(src)) { + // skip false transitions + if (SPOT_UNLIKELY(i->cond() == bddfalse)) + continue; + const state* dest = filter(i->dst()); if (!dest) diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index 1f0d3c495..1414060ef 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -41,7 +41,8 @@ namespace spot public: explicitproxy(explicit_iterator it) : it_(it) - {} + { + } const explicitproxy* operator->() const @@ -73,6 +74,12 @@ namespace spot return it_->acc; } + bdd + cond() const + { + return it_->cond; + } + void next() { @@ -704,7 +711,7 @@ namespace spot assert(ecs_->root.size() == arc.size()); // We are looking at the next successor in SUCC. - auto succ = todo.top().second; + auto& succ = todo.top().second; // If there are no more successors, backtrack. if (succ->done()) @@ -744,6 +751,14 @@ namespace spot // We have a successor to look at. inc_transitions(); + + // Ignore false edges + if (SPOT_UNLIKELY(succ->cond() == bddfalse)) + { + succ->next(); + continue; + } + // Fetch the values we are interested in... auto acc = succ->acc(); if (!need_accepting_run) @@ -763,7 +778,7 @@ namespace spot state_t dest = succ->dst(); // ... and point the iterator to the next successor, for // the next iteration. - todo.top().second->next(); + succ->next(); // We do not need succ from now on. diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 4b4a827de..12eba32c8 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014-2016, 2018-2019 Laboratoire de +// Copyright (C) 2008, 2011, 2014-2016, 2018-2020 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -109,6 +109,8 @@ namespace spot do { inc_transitions(); + if (SPOT_UNLIKELY(i->cond() == bddfalse)) + continue; const state* s = i->dst(); auto j = ecs_->h.find(s); @@ -219,9 +221,15 @@ namespace spot // of the arc) we are interested in... const state* dest = succ->dst(); acc_cond::mark_t acc = succ->acc(); + trace << "-> " << dest << ' ' << acc << ' ' << succ->cond(); // ... and point the iterator to the next successor, for // the next iteration. - succ->next(); + { + bdd cond = succ->cond(); + succ->next(); + if (SPOT_UNLIKELY(cond == bddfalse)) + continue; + } // We do not need SUCC from now on. // Are we going to a new state? @@ -321,10 +329,12 @@ namespace spot { for (auto iter: shy->ecs_->aut->succ(s)) { + shy->inc_transitions(); + if (SPOT_UNLIKELY(iter->cond() == bddfalse)) + continue; q.emplace_back(iter->acc(), iter->dst()); shy->inc_depth(); - shy->inc_transitions(); } } @@ -372,24 +382,28 @@ namespace spot } #ifdef TRACE - couvreur99_check_shy::dump_queue(std::ostream& os) + namespace { - os << "--- TODO ---\n"; - unsigned lvl = 0; - for (auto& ti: todo) - { - ++lvl; - os << '#' << lvl << " s:" << ti.s << " n:" << ti.n - << " q:{"; - for (auto qi = ti.q.begin(); qi != ti.q.end();) - { - os << qi->s; - ++qi; - if (qi != ti.q.end()) - os << ", "; - } - os << "}\n"; - } + template + void dump_queue(const T& todo) + { + trace << "--- TODO ---\n"; + unsigned lvl = 0; + for (auto& ti: todo) + { + ++lvl; + trace << '#' << lvl << " s:" << ti.s << " n:" << ti.n + << " q:{"; + for (auto qi = ti.q.begin(); qi != ti.q.end();) + { + trace << qi->s; + ++qi; + if (qi != ti.q.end()) + trace << ", "; + } + trace << "}\n"; + } + } } #endif @@ -410,7 +424,7 @@ namespace spot for (;;) { #ifdef TRACE - dump_queue(); + dump_queue(todo); #endif assert(ecs_->root.size() == 1 + arc.size()); diff --git a/spot/twaalgos/gtec/gtec.hh b/spot/twaalgos/gtec/gtec.hh index c3ddcb0c1..a9e3e8292 100644 --- a/spot/twaalgos/gtec/gtec.hh +++ b/spot/twaalgos/gtec/gtec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013-2016, 2018-2019 Laboratoire de Recherche +// Copyright (C) 2008, 2013-2016, 2018-2020 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -218,11 +218,6 @@ namespace spot void clear_todo(); -#ifdef SPOT_TRACE - /// Dump the queue for debugging. - void dump_queue(std::ostream& os = std::cerr); -#endif - /// Whether successors should be grouped for states in the same SCC. bool group_; // If the "group2" option is set (it implies "group"), we diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index d756a1bc4..fceec436a 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013-2019 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013-2020 Laboratoire de // recherche et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -120,6 +120,10 @@ namespace spot trace << " No more successors" << std::endl; pop(); } + else if (SPOT_UNLIKELY(iter->cond() == bddfalse)) + { + continue; + } else { const state* s_prime = iter->dst(); diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 50be6086b..b8b472af7 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2019 Laboratoire de recherche et +// Copyright (C) 2011, 2013-2020 Laboratoire de recherche et // développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -199,6 +199,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { @@ -286,6 +288,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index e3375c7e4..024051bcb 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -158,24 +158,25 @@ namespace spot // Gather all successor SCCs if (track_succs) for (auto& t: aut->out(*s)) - for (unsigned d: aut->univ_dests(t)) - { - unsigned n = sccof_[d]; - if (n == num || n == -1U) - continue; - // If edges are cut, we are not able to - // maintain proper successor information. - if (filter_) - switch (filter_(t, d, filter_data_)) - { - case edge_filter_choice::keep: - break; - case edge_filter_choice::ignore: - case edge_filter_choice::cut: - continue; - } - succ.emplace_back(n); - } + if (SPOT_LIKELY(t.cond != bddfalse)) + for (unsigned d: aut->univ_dests(t)) + { + unsigned n = sccof_[d]; + if (n == num || n == -1U) + continue; + // If edges are cut, we are not able to + // maintain proper successor information. + if (filter_) + switch (filter_(t, d, filter_data_)) + { + case edge_filter_choice::keep: + break; + case edge_filter_choice::ignore: + case edge_filter_choice::cut: + continue; + } + succ.emplace_back(n); + } } while (*s++ != curr); @@ -251,6 +252,13 @@ namespace spot // Fetch the values we are interested in... auto& e = gr.edge_storage(tr_succ); + // Skip false edges. + if (SPOT_UNLIKELY(e.cond == bddfalse)) + { + todo_.top().out_edge = e.next_succ; + continue; + } + unsigned dest = e.dst; if ((int) dest < 0) { @@ -412,7 +420,7 @@ namespace spot auto& s = result[src_scc]; for (auto& t: aut_->out(src)) { - if (scc_of(t.dst) != src_scc) + if (scc_of(t.dst) != src_scc || SPOT_UNLIKELY(t.cond == bddfalse)) continue; s.insert(t.acc); } @@ -502,7 +510,7 @@ namespace spot bfs_queue.pop_front(); for (auto& t: aut->out(src)) { - if (filter(t)) + if (SPOT_UNLIKELY(t.cond == bddfalse) || filter(t)) continue; if (match(t)) @@ -573,7 +581,8 @@ namespace spot if (scc_of(s) != scc) continue; for (auto& e: aut_->out(s)) - if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc)) + if (e.src == e.dst && SPOT_LIKELY(e.cond != bddfalse) + && !filter(e) && acccond.accepting(e.acc)) { // We have found an accepting self-loop. That's the cycle // part of our accepting run. diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index fbea7dfae..508a1dca1 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2019 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2020 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -195,6 +195,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { @@ -286,6 +288,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c = h.get_color_ref(s_prime); if (c.is_white()) { diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index 4ea8ab0bb..1fef18fe9 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2019 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2020 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -167,6 +167,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { @@ -194,11 +196,13 @@ namespace spot { inc_transitions(); const state *s_prime = i->dst(); + bdd label = i->cond(); + auto acc = i->acc(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; trace << "DFS_BLUE rescanning the arc from " << a_->format_state(f.s) << " to " << a_->format_state(s_prime) << std::endl; - bdd label = i->cond(); - auto acc = i->acc(); typename heap::color_ref c_prime = h.get_color_ref(s_prime); assert(!c_prime.is_white()); auto acu = acc | c.get_acc(); @@ -247,6 +251,8 @@ namespace spot // Go down the edge (f.s, , s_prime) f.it->next(); inc_transitions(); + if (SPOT_UNLIKELY(label == bddfalse)) + continue; typename heap::color_ref c_prime = h.get_color_ref(s_prime); if (c_prime.is_white()) { diff --git a/tests/Makefile.am b/tests/Makefile.am index 58c140e41..b39a54be8 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -377,6 +377,7 @@ TESTS_python = \ python/declenv.py \ python/decompose_scc.py \ python/dualize.py \ + python/ecfalse.py \ python/except.py \ python/gen.py \ python/genem.py \ diff --git a/tests/core/neverclaimread.test b/tests/core/neverclaimread.test index 377d605b4..fb94a066a 100755 --- a/tests/core/neverclaimread.test +++ b/tests/core/neverclaimread.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010-2015, 2017-2018 Laboratoire +# Copyright (C) 2010-2015, 2017-2018, 2020 Laboratoire # de Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -340,7 +340,7 @@ digraph "-" { 1 [label="1", peripheries=2] } subgraph cluster_1 { - color=red + color=black label="" 0 [label="0"] } diff --git a/tests/python/ecfalse.py b/tests/python/ecfalse.py new file mode 100644 index 000000000..36301914b --- /dev/null +++ b/tests/python/ecfalse.py @@ -0,0 +1,86 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# 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 . + +import spot +from buddy import bddfalse, bddtrue + +a = spot.automaton(""" +HOA: v1 +States: 2 +Start: 1 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[!0 | 1] 0 {0} +[0&!1] 1 +State: 1 +/* we want this edge to be false, but the parser + would ignore it if we wrote it here */ +[0] 0 {0} +[!1] 1 +--END-- +""") +# Make the false edge. +for e in a.out(1): + if e.dst == 0: + e.cond = bddfalse + +assert a.accepting_run() is None +assert a.is_empty() + +for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']: + print(name) + ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(a) + res = ec.check() + if res is not None: + print(res.accepting_run()) + assert res is None + +si = spot.scc_info(a) +assert si.scc_count() == 1 # only one accessible SCC +a.set_init_state(0) +si = spot.scc_info(a) +assert si.scc_count() == 2 + +a = spot.automaton("""HOA: v1 States: 11 Start: 0 AP: 2 "a" "b" Acceptance: 8 +(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & ((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) +properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [!0&!1] 1 +{0 4 6 7} [!0&!1] 2 {0 5 6} [!0&!1] 3 {3 4 6 7} [!0&!1] 4 {3 5 6} State: 1 +[0&1] 5 {2 5 7} [0&1] 6 {2 7} [0&1] 7 {2 3 5 7} [0&1] 8 {2 3 7} [0&1] 0 {2 5 7} +[0&1] 9 {2 7} State: 2 [0&1] 1 {2} [0&1] 3 {2 3} [0&1] 10 {2} State: 3 [0&1] 0 +{3 5 7} [0&1] 9 {3 7} State: 4 [!0&!1] 5 {4 6} [!0&!1] 6 {7} [0&1] 10 {3} +State: 5 State: 6 State: 7 [!0&!1] 1 {4 6 7} [!0&!1] 2 {5 6} State: 8 [!0&!1] 2 +{4} State: 9 [!0&!1] 2 {0 4} [!0&!1] 4 {3 4} State: 10 --END-- """) + +r = a.accepting_run() +assert r is not None +assert r.replay(spot.get_cout()) +for e in a.out(7): + if e.dst == 2: + e.cond = bddfalse +s = a.accepting_run() +assert s is not None +assert s.replay(spot.get_cout()) +for e in a.out(2): + if e.dst == 1: + e.cond = bddfalse +s = a.accepting_run() +assert s is None