Commit 8ff86068 authored by Etienne Renault's avatar Etienne Renault

twacube: 'mark_t' is deprecated

* spot/mc/ec.hh, spot/mc/intersect.hh,
tests/core/twacube.cc: here.
parent 14a16b81
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et // Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et
// Developpement de l'Epita // Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -72,7 +72,7 @@ namespace spot ...@@ -72,7 +72,7 @@ namespace spot
bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond) bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond)
{ {
uf_.makeset(dfsnum); uf_.makeset(dfsnum);
roots_.push_back({dfsnum, cond, 0U}); roots_.push_back({dfsnum, cond, {}});
return true; return true;
} }
...@@ -146,7 +146,7 @@ namespace spot ...@@ -146,7 +146,7 @@ namespace spot
}; };
std::queue<ctrx_element*> bfs; std::queue<ctrx_element*> bfs;
acc_cond::mark_t acc = 0U; acc_cond::mark_t acc = {};
bfs.push(new ctrx_element({&this->todo.back().st, nullptr, bfs.push(new ctrx_element({&this->todo.back().st, nullptr,
this->sys_.succ(this->todo.back().st.st_kripke, this->tid_), this->sys_.succ(this->todo.back().st.st_kripke, this->tid_),
......
...@@ -89,7 +89,7 @@ namespace spot ...@@ -89,7 +89,7 @@ namespace spot
{ {
self().setup(); self().setup();
product_state initial = {sys_.initial(tid_), twa_->get_initial()}; 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_), todo.push_back({initial, sys_.succ(initial.st_kripke, tid_),
twa_->succ(initial.st_prop)}); twa_->succ(initial.st_prop)});
......
...@@ -39,12 +39,12 @@ int main() ...@@ -39,12 +39,12 @@ int main()
auto s1 = tg->new_state(); auto s1 = tg->new_state();
auto s2 = tg->new_state(); auto s2 = tg->new_state();
auto s3 = tg->new_state(); auto s3 = tg->new_state();
tg->new_edge(s1, s1, bddfalse, 0U); tg->new_edge(s1, s1, bddfalse, {});
tg->new_edge(s1, s2, p1, 0U); tg->new_edge(s1, s2, p1, {});
tg->new_edge(s1, s3, p2, tg->acc().mark(1)); tg->new_edge(s1, s3, p2, tg->acc().mark(1));
tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); 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, 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})); tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
// Test translation // Test translation
......
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