NuSMV 至少 5 个时间步才能获胜答案

【问题标题】：NuSMV at least 5 time steps to winNuSMV 至少 5 个时间步才能获胜
【发布时间】：2013-12-17 10:26:48
【问题描述】：

我有一个 NuSMV 程序，我需要在 CTL 或 LTL 中指定该程序（这是一个游戏）不能在少于 5 个时间步长内获胜。或更正式：赢得比赛至少需要 5 个时间步长。

我没有明确的时间变量，也不想为验证创建一个。有什么方法可以计算已经进行的转换数量吗？访问状态的数量，诸如此类？

目前我有这个：

SPEC ( (gameState != WIN) U (how to count time steps?))

【问题讨论】：

【解决方案1】：

据我所知，您必须使用一个额外的变量来指定时间，并在每一步增加时间。在 prisim 中，您可以指定时间间隔，但在 NuSMV 中则不能。

【讨论】：

【解决方案2】：

这是一个老问题，但是你可以使用：

COMPUTE MIN [initial state, end state]

【讨论】：