Parity Game

いちおう論文ではSafety Gameに従って充足性の形式化をしましたが、それをツールで確かめる手段がTICCしか（わるいか）なくて、単なるGameなのにInterface Automataとかを説明した上でTICC用にエンコードした事例を示すわけにもいかないなあ、とおもっていたら

Parity Game系のソルバがPGSolver単独で出ているので、これを使ってみることにする。　
以下はメモ。

• node spec ::= identifier priority owner successors [name] ;
• player0はモデル側、player1はプロパティ側とする(owner={0,1}を正しく設定)
• priorityはNGノードは1、それ以外は0に設定
• infinity oftenに訪問するノードのpriorityの最小値がevenならばplayer0の勝ちなのでそれでいい雰囲気。

まずは論文にでてくる充足しない例から、

parity 6;
0 0 0 1 "s0";
1 0 0 2,5 "s1";
2 0 1 3 "s2";
3 0 0 4 "s3";
4 0 1 0 "s4";
5 0 1 6 "s5";
6 1 0 6 "NG";

ならば、pgsolver --reursiveにかけると以下が出ます。

Parsing ..................... 0.00 sec
Chosen solver `recursive' ..... 0.00 sec

Player 0 wins from nodes:
{0,1,2,3,4}
with strategy
[0->1,1->2,3->4]

Player 1 wins from nodes:
{5,6}
with strategy
[5->6]

wining states={s0,s1,s2,s3,s4}も戦略も計算してくれて素敵。

こんな絵（右上）も出てきて素敵。