logic - NuSMV 至少 5 个时间步才能获胜

Question

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

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

目前我有这个：

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

score 1 · Accepted Answer

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

score 1 · Accepted Answer

1

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

COMPUTE MIN [initial state, end state]

于 2015-10-26T19:56:57.547 回答

2 回答 2