1

我正在使用 LTL 来定义开放交互协议的规则。然后我想检查一个特定的交互是否遵循规范，或者是否有任何规则被破坏。我的直接方法是使用 NuSMV，但问题是我没有要检查的交互模型，而只有一个特定的有限迹线（所有状态下所有变量的值）。

有什么方法可以在 NuSMV 中指定它吗？我基本上想输入 NuSMV 输出的模型之一作为反例：

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

并验证它。或者 NuSMV 是不是这个错误的工具？

谢谢！

4

1 回答 1

1

经过一番思考，我找到了一种在 NuSMV 模型中对特定轨迹进行编码的解决方案。这很简单，诀窍是为跟踪的每个状态使用一个变量。

例如，我想对交互进行编码，并且我只希望最后发出的消息在每个状态下都是真实的。如果要编码的交互是 ['a','b','a']，则 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-22T17:12:46.970 回答