问构造有效的CTL或LTL表达式(在NuSMV中)
EN

Stack Overflow用户

提问于 2013-12-12 22:44:04

回答 1查看 481关注 0票数 2

我正在尝试为NuSMV中的模型检查创建一个有效的CTL或LTL表达式。

我在游戏中有一个变量，玩家们跑来跑去试图抓住对方。变量为，State_Of_Game：{Win，Lose，Playing}

我想表达的是，从每个开始状态来看，游戏可能会赢，也可能会输。

那么，我该如何在CTL或LTL中实现它呢？

我在想像AG (S_O_G = Win | S_O_G = Lose)这样的东西，但不知道如何实现它，从每个开始状态都可以看到它。

发布于 2019-05-31 07:57:38

试试这个: AF(State_of_Game=Win| State_of_Game=Lose)

票数 -1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/20546499

复制

相似问题

问构造有效的CTL或LTL表达式(在NuSMV中)EN