前回までは通信路に歪みがないことを仮定してましたが、今回から通信路に歪みを考慮に入れます。つまり、送信した値と異なる値が相手に届くことがあると状況をつくります。 チャネルのモデリング これまではSyncStitchのチャネルをそのまま使用していました…

前回は通信路に歪みがないと仮定して、その上で 0, 1 をやり取りする送信者と受信者をモデル化してデッドロック検査を行いました。今回は仕様を状態遷移図で表し、その仕様との比較を試してみます。さて、その仕様ですが、今回のABPの設計で確認したい事は「…

以前いっしょに仕事していた先輩がSyncStitchという設計ツールを開発したので試用してみました。SyncStitchの特徴は、状態遷移図で書いたモデルの振る舞いをシミュレーションしたり検証できたりします。さらに複数の状態遷移図を組み合わせときの振る舞いに…