diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 8eb6cc3cd..a94246c38 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1276,8 +1276,9 @@ namespace spot else { is_.syntactic_safety = false; - is_.syntactic_obligation = children[1]->is_syntactic_guarantee(); - is_.syntactic_recurrence = children[1]->is_syntactic_guarantee(); + bool g = children[1]->is_syntactic_guarantee(); + is_.syntactic_obligation = g; + is_.syntactic_recurrence = g; } assert(children[0]->is_sere_formula()); assert(children[1]->is_psl_formula()); @@ -1305,8 +1306,9 @@ namespace spot else { is_.syntactic_guarantee = false; - is_.syntactic_obligation = children[1]->is_syntactic_safety(); - is_.syntactic_persistence = children[1]->is_syntactic_safety(); + bool s = children[1]->is_syntactic_safety(); + is_.syntactic_obligation = s; + is_.syntactic_persistence = s; } assert(children[0]->is_sere_formula()); assert(children[1]->is_psl_formula()); diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 4e5301bdd..8aece6ad5 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2014, 2015, 2016 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), // Université Pierre et Marie Curie. @@ -373,11 +373,11 @@ namespace spot couvreur99_check_shy::dump_queue(std::ostream& os) { os << "--- TODO ---\n"; - unsigned pos = 0; + unsigned lvl = 0; for (auto& ti: todo) { - ++pos; - os << '#' << pos << " s:" << ti.s << " n:" << ti.n + ++lvl; + os << '#' << lvl << " s:" << ti.s << " n:" << ti.n << " q:{"; for (auto qi = ti.q.begin(); qi != ti.q.end();) {