我是NuSMV的新手，我嘗試從Kripke結構創建自動售貨機實現，我有三個布爾（硬幣，選擇，釀造）以及三個狀態。但是，當我編譯代碼I收到「第25行：at token」：「：語法錯誤」如果任何人在我的代碼中看到任何錯誤，我將不勝感激。 Kripke structure 我嘗試寫的代碼如下： MODULE main
VAR
location : {s1,s2,s3};
coi
我是NuSMV的新手，並嘗試對這個簡單的回合制遊戲進行建模。一堆中有10塊磚，每個玩家每回合可以拿1-3塊磚，誰拿走最後一塊磚就贏得比賽。假設玩家A先去，這是我的嘗試。我想表達的是，「最終有一個勝利者」，但是我的代碼不起作用，因爲它不阻止玩家在磚塊= 0之後採取磚塊，所以最終玩家a，b都會成爲贏家。 這裏是我的代碼： MODULE main
VAR
bricks : 0..10;
i :
我的教授決定給我們數學學生一個代碼，以改變成NuSMV，我似乎無法找到其他任何地方的幫助，我閱讀的教科書只有6頁，只描述某些屬性。 Module main是NuSMV代碼的一個例子，他說用這個格式的例子來編寫僞代碼。 我不知道如何編寫while循環，並設置什麼是真實的？並將旗1成爲一個國家，併成爲另一個國家？ while(true) do
flag1 := true
while