モデル検査器 Spin の動作実験 1. モデルの作成 まず検査対象のモデルを作成する．モデルは Promela と言う言語で作成する．ここでは，例えば，以下のようなOn とOff を繰り返すトグルスイッチのPromela コードを用意した．このコードを switch.p として適当…