關於TLA +項目的想法

Question

請給我一些關於TLA+語言項目主題的建議。我參加了一門語言課程，這是我第一年瞭解規範和驗證的一年，我不知道要在兩週內選擇實施什麼。有任何想法嗎？

Answer 1

與TLA +通常的玩具項目正在線：

• 型號電梯控制器：電梯有ñ門，你將不得不模型無論是行爲和安全條件，例如是一旦在頂部，電梯不會再向上移動，或者我們不應該同時打開兩扇門，並且當機艙不在其前面時門沒有打開，等等。
• 模型交通燈控制器：爲簡單的例子，一個簡單的交叉，有許多約束條件，例如面向燈是同步的，並且如果一個軸有綠色，那麼其他有紅色。您可以改進添加交通狀況檢測和時間的事情。
• 型號a洗衣機：特別是門鎖，簡單的程序。證明沒有辦法鎖門，即在有限的時間內（通常需要考慮用水消除步驟）免費（即使是潮溼的）衣服總是有一個解決方案，不需要過多的水你的地板。

一般來說，有趣的TLA +玩具項目應該結合一個相對簡單的行爲，結構和安全條件，以便您能夠驗證您定義的行爲不會使安全條件失效。