CODEWITHSUNDEEP
ctlnusmv
Desmond
Desmond

Reputation: 9

NuSMV Realtime CTL

I'm using NuSMV and i'm trying to write a Real Time CTL property.
I would like to know if there is a way to set the steps from a state, like:
((s.state = on) ABG (0..5 s.state = off))

Is read as: if (s.state=on) is true, from this state and for other 5 steps the property (s.state= off) is true.
I tried to write something like this but it doesn't work. Can you help me?

Otherwise, is it possible to check the same property starting from a state that isn't the first?

Upvotes: 0

Views: 155

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

Question. write if (s.state=on) is true, from this state and for other 5 steps the property (s.state= off) is true.

CTL.

CTLSPEC AG ((s.state = on) -> 
            ((AX s.state = off) &
             (AX AX s.state = off) &
             (AX AX AX s.state = off) &
             (AX AX AX AX s.state = off) &
             (AX AX AX AX AX s.state = off)
           ));

With this formula, you test whether it is true that each time you hit s.state = on condition s.state = off will be true for at least 5 states following the current one, regardless of your path choice.

The initial AG ensures that this property must hold anywhere on the execution path, and not only in the initial state.

Real Time CTL.

From nusmv mailing list:

((s.state = on) ABG (1..5 s.state = off))

Note: the rest of your question isn't clear to me, so please if there is still some unanswered part just edit your question and clarify a bit.

Upvotes: 0

Related Questions