我是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個布爾值爲NS/EW紅色，黃色，綠色。但是，當我指定它們在未來狀態中總是爲真時，它會返回錯誤。如果有人在我的代碼中看到任何錯誤，我將不勝感激。謝謝。 MODULE main
VAR
nsRed : boolean;
nsYellow : boolean;
nsGreen : boolean;
time
當我使用NuSMV工具來驗證我的CTL是否正確時，我遇到一個讓我如此困惑的問題。 我的模型是 和這裏的NuSMV代碼： MODULE main
VAR
state : {ROOT, A1, B1, C1, D1, F1, M1};
ASSIGN
init(state) := ROOT;
next(state) := case
state = ROOT
我的教授決定給我們數學學生一個代碼，以改變成NuSMV，我似乎無法找到其他任何地方的幫助，我閱讀的教科書只有6頁，只描述某些屬性。 Module main是NuSMV代碼的一個例子，他說用這個格式的例子來編寫僞代碼。 我不知道如何編寫while循環，並設置什麼是真實的？並將旗1成爲一個國家，併成爲另一個國家？ while(true) do
flag1 := true
while
我正在使用LTL爲開放式交互協議定義規則。然後我想檢查特定交互是否遵循規範，或者是否有任何規則被破壞。我的直接方法是使用NuSMV，但問題是我沒有我想要檢查的交互模型，但只有一個特定的有限痕跡（所有狀態中的所有變量的值）。 有沒有什麼方法可以在NuSMV中指定？我基本上想輸入NuSMV輸出的模型之一作爲反例： -> State: 1.1 <-
a = TRUE
b = FALSE
-> St