From 9d34c1f5001b216219a2243da31ca88c3e490ce7 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Mon, 23 Apr 2018 14:29:41 +0200 Subject: [PATCH] fix parity game printing * spot/misc/game.cc: a state could be printed several times * tests/core/ltlsynt.test: update tests --- spot/misc/game.cc | 2 ++ tests/core/ltlsynt.test | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/spot/misc/game.cc b/spot/misc/game.cc index 3061d14fb..dde0cbb6e 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -51,6 +51,8 @@ void parity_game::print(std::ostream& os) { unsigned src = todo.back(); todo.pop_back(); + if (seen[src]) + continue; seen[src] = true; os << src << ' '; os << out(src).begin()->acc.max_set() - 1 << ' '; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index ab76a5527..aa8567850 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -37,7 +37,6 @@ parity 16; 12 1 0 9,10; 7 1 0 4,13; 13 2 1 3,6; -4 0 1 7,8; 1 3 1 3,14; 14 3 0 1,2; EOF