alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

fix parity game printing

Browse source 
* spot/misc/game.cc: a state could be printed several times
* tests/core/ltlsynt.test: update tests
This commit is contained in:
Maximilien Colange 2018-04-23 14:29:41 +02:00
parent 9698363ef5
commit 9d34c1f500
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/misc/game.cc
View file

@ -51,6 +51,8 @@ void parity_game::print(std::ostream& os)
{ {
unsigned src = todo.back(); unsigned src = todo.back();
todo.pop_back(); todo.pop_back();
if (seen[src])
continue;
seen[src] = true; seen[src] = true;
os << src << ' '; os << src << ' ';
os << out(src).begin()->acc.max_set() - 1 << ' '; os << out(src).begin()->acc.max_set() - 1 << ' ';

1
tests/core/ltlsynt.test
View file

@ -37,7 +37,6 @@ parity 16;
12 1 0 9,10; 12 1 0 9,10;
7 1 0 4,13; 7 1 0 4,13;
13 2 1 3,6; 13 2 1 3,6;
4 0 1 7,8;
1 3 1 3,14; 1 3 1 3,14;
14 3 0 1,2; 14 3 0 1,2;
EOF EOF