From 8ff8606847ecd3e04721f85bc0cbf8e23bfbebd2 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 4 Jul 2018 11:14:27 +0200 Subject: [PATCH] twacube: 'mark_t' is deprecated * spot/mc/ec.hh, spot/mc/intersect.hh, tests/core/twacube.cc: here. --- spot/mc/ec.hh | 6 +++--- spot/mc/intersect.hh | 2 +- tests/core/twacube.cc | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh index 58b69646a..1dafb1407 100644 --- a/spot/mc/ec.hh +++ b/spot/mc/ec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et // Developpement de l'Epita // // This file is part of Spot, a model checking library. @@ -72,7 +72,7 @@ namespace spot bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond) { uf_.makeset(dfsnum); - roots_.push_back({dfsnum, cond, 0U}); + roots_.push_back({dfsnum, cond, {}}); return true; } @@ -146,7 +146,7 @@ namespace spot }; std::queue bfs; - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; bfs.push(new ctrx_element({&this->todo.back().st, nullptr, this->sys_.succ(this->todo.back().st.st_kripke, this->tid_), diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh index d7219068b..c73d6cd77 100644 --- a/spot/mc/intersect.hh +++ b/spot/mc/intersect.hh @@ -89,7 +89,7 @@ namespace spot { self().setup(); product_state initial = {sys_.initial(tid_), twa_->get_initial()}; - if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U))) + if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {}))) { todo.push_back({initial, sys_.succ(initial.st_kripke, tid_), twa_->succ(initial.st_prop)}); diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc index bb88d6691..fa4b57fe4 100644 --- a/tests/core/twacube.cc +++ b/tests/core/twacube.cc @@ -39,12 +39,12 @@ int main() auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); - tg->new_edge(s1, s1, bddfalse, 0U); - tg->new_edge(s1, s2, p1, 0U); + tg->new_edge(s1, s1, bddfalse, {}); + tg->new_edge(s1, s2, p1, {}); tg->new_edge(s1, s3, p2, tg->acc().mark(1)); tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1})); - tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s2, p1 >> p2, {}); tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1})); // Test translation -- GitLab