diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 98fef72ff..2ce3b2dec 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -71,9 +71,6 @@ namespace spot // it is also used as a key in H. std::stack todo; - std::unordered_map colour; - trace << "PASS 1" << std::endl; @@ -159,7 +156,6 @@ namespace spot inc_depth(); // set the h value of the Backtracked state to negative value. - // colour[curr] = BLUE; i->second = -std::abs(i->second); // Backtrack livelock_roots. @@ -175,7 +171,7 @@ namespace spot { // removing states for (auto j: scc.rem()) - h[j] = -1; //colour[*i] = BLACK; + h[j] = -1; dec_depth(scc.rem().size()); scc.pop(); assert(!arc.empty()); @@ -227,7 +223,6 @@ namespace spot ta_succ_iterator_product* iter = a_->succ_iter(dest); iter->first(); todo.emplace(dest, iter); - //colour[dest] = GREY; inc_depth(); //push potential root of live-lock accepting cycle @@ -329,7 +324,6 @@ namespace spot return true; } - std::set::const_iterator it; for (const state* succ: liveset_dest) if (heuristic_livelock_detection(succ, h, h_livelock_root, liveset_curr)) @@ -357,7 +351,7 @@ namespace spot { int hu = h[u]; - if (hu > 0) // colour[u] == GREY + if (hu > 0) { if (hu >= h_livelock_root) diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 870ecb4e8..900628be3 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -241,7 +241,6 @@ namespace spot if (sscc.top().index == i->second) { // removing states - std::list::iterator i; bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) && ((sscc.top().is_accepting) || (testing_aut->acc(). diff --git a/src/twa/acc.cc b/src/twa/acc.cc index 6c3777295..1b0bdd771 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -355,7 +355,6 @@ namespace spot auto sz = c->size; auto start = c - sz - 1; auto op = c->op; - std::set res; switch (op) { case acc_cond::acc_op::Or: diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index 24de80fdf..8c868010a 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -145,7 +145,6 @@ namespace spot for (sit = sets.begin(); sit != sets.end(); ++sit) { - hash_set::iterator hit; hash_set* h = *sit; // Pick one state. diff --git a/src/twaalgos/neverclaim.cc b/src/twaalgos/neverclaim.cc index b3231a63a..38daf1a2c 100644 --- a/src/twaalgos/neverclaim.cc +++ b/src/twaalgos/neverclaim.cc @@ -106,7 +106,6 @@ namespace spot void print_state(unsigned n) const { - std::string label; bool acc = aut_->state_is_accepting(n); if (n == aut_->get_init_state_number()) { diff --git a/src/twaalgos/remprop.cc b/src/twaalgos/remprop.cc index cb3ae613d..b6819c606 100644 --- a/src/twaalgos/remprop.cc +++ b/src/twaalgos/remprop.cc @@ -58,7 +58,6 @@ namespace spot void remove_ap::add_ap(const char* arg) { auto& env = spot::ltl::default_environment::instance(); - std::vector group; auto start = arg; while (*start) { diff --git a/src/twaalgos/sccinfo.cc b/src/twaalgos/sccinfo.cc index fe68e57de..3b6bae76b 100644 --- a/src/twaalgos/sccinfo.cc +++ b/src/twaalgos/sccinfo.cc @@ -52,8 +52,6 @@ namespace spot typedef std::list stack_type; stack_type root_; // Stack of SCC roots. - std::stack> arc_; // A stack of acceptance conditions - // between each of these SCC. std::vector h_(n, 0); // Map of visited states. Values > 0 designate maximal SCC. // Values < 0 number states that are part of incomplete SCCs being