使用模型檢查器檢查一個特定跟蹤

我正在使用LTL爲開放式交互協議定義規則。然後我想檢查特定交互是否遵循規範，或者是否有任何規則被破壞。我的直接方法是使用NuSMV，但問題是我沒有我想要檢查的交互模型，但只有一個特定的有限痕跡（所有狀態中的所有變量的值）。使用模型檢查器檢查一個特定跟蹤

有沒有什麼方法可以在NuSMV中指定？我基本上想輸入NuSMV輸出的模型之一作爲反例：

-> State: 1.1 <- 
a = TRUE 
b = FALSE 
-> State: 1.2 <- 
a = FALSE 
-> State: 1.3 <- 
a = TRUE

並驗證它。還是NuSMV是這個錯誤的工具？

謝謝！

來源

2016-09-19 adivinanza

你的問題不清楚給我。你有'假'痕跡或'假'狀態？爲什麼你不能將這種'虛假'的痕跡形式化爲NuSMV模型？你的困難在哪裏？你能編輯你的問題，並提供你的源代碼的全部範圍？ –

是的，其實我可以正式跟蹤到NuSMV模型（我只需要指定一個變量中的每個狀態），但這個問題被張貼後，我才意識到。對不起，我真的沒有看到它。感謝你的回答！！ – adivinanza

我建議你用你的代碼和解決方案的詳細例子來回答你自己的問題，這可能對其他人有幫助。 –

經過一番思考，我找到了一個解決方案來編碼NuSMV模型中的特定軌跡。這很簡單，訣竅是對每個跟蹤狀態使用一個變量。

例如，我想編碼相互作用，我想只有最後說出的消息中的每個狀態是真實的。如果互動編碼爲[「一」，「B」，「一」]，在NuSMV模型應該是：

MODULE main 
VAR 
a : boolean; 
b : boolean; 
state : {s0,s1,s2}; 

ASSIGN 
init(a) := FALSE; 
init(state) := s0; 
next(a) := 
    case 
     state = s0 : TRUE; 
     state = s1 : FALSE; 
     state = s2 : TRUE; 
    esac; 
next(b) := 
    case 
     state = s0 : FALSE; 
     state = s1 : TRUE; 
     state = s2 : FALSE; 
    esac; 
next(state) := 
    case 
     state = s0 : s1; 
     state = s1 : s2; 
     state = s2 : s2; 
    esac;

我希望，也許這是有用的人！

來源

2016-09-22 17:12:46 adivinanza

使用模型檢查器檢查一個特定跟蹤

回答

相關問題