NuSMV 적어도 5 시간 걸려 승리하려면

나는 NuSMV 프로그램을 가지고 있으며 CTL 또는 LTL에서 프로그램 (게임)을 5 단계 미만으로 획득 할 수 없다고 명시해야합니다. 또는 더 형식적 : 게임을 승리하기 위해 적어도 5 단계의 단계가 필요합니다.NuSMV 적어도 5 시간 걸려 승리하려면

나는 명시적인 시간 변수가 없으므로 확인을 위해 만들고 싶지 않습니다. 이미 만들어진 전환 양을 계산할 수있는 방법이 있습니까? 방문한 국가의 양은 어떻습니까? 순간

내가이있다 : 내 지식의

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

2013-12-17 Sven

BEST를, 당신은 시간을 지정하기위한 별도의 변수를 사용하고 각 단계에서 시간을 증가해야합니다. prisim에서는 NuSMV가 아니라 시간 간격을 지정할 수 있습니다.

2014-12-03 20:29:59 Memin

IT는 오래된 질문이지만, 그래 당신은 사용 할 수 있습니다

COMPUTE MIN [initial state, end state]

2015-10-26 19:56:57 AhlyM

이 정말 직접 지정한 공식 내에서 사용할 수 없다는 점에서, 질문에 대답하지 않습니다. 그러나 그것은 NuSMV의 매우 흥미롭고 잘 알려지지 않은 기능이며, 따라서 투표가 확정되었습니다. –

답변