project - TLA+ プロジェクトのアイデア

Question

TLA+言語のプロジェクト トピックに関する提案をお願いします。私は言語のコースを受講しています。仕様と検証について学んでいる最初の年であり、2 週間で実装するものを選択する手がかりがありません。何か案は？

Answer 1

TLA+を使用した通常のおもちゃプロジェクトは次のとおりです。

• リフトコントローラーのモデル化：リフトにはn個のドアがあり、動作と安全条件の両方をモデル化する必要があります。たとえば、上部に来るとリフトが上に移動しなくなる、または2つのドアを開く必要がないなどです。同時に、キャビンが正面にないときはドアが開かれませんでした。
• 信号機コントローラーのモデル化：簡単な例として、向かい合ったライトが同期され、一方の軸が緑色の場合、もう一方の軸が赤色の場合など、多くの制約がある単純な交差点があります。交通状況の検知やタイミングを追加して、物事を洗練させることができます。
• 洗濯機のモデル化：特にドアロッカーと簡単なプログラム。ドアをロックする方法がないことを証明します。つまり、水をかけすぎずに、限られた時間内に（濡れていても）衣服を解放するための解決策が常にあります（水分除去ステップを検討する必要があります）。あなたの床。

一般に、TLA +の興味深いおもちゃプロジェクトでは、比較的単純な動作と、構造および安全条件を組み合わせて、定義した動作が安全条件を無効にしないことを確認できるようにする必要があります。