非決定性を含むプロセス合成, PRActice MOdel checker
ほぼ本のまま。追加作業として、typo修正とpackage整地と漸進commit。本文をコメントやドキュメントに埋めている為、private扱いにした