Next == sData \/ sendD \/ sendA \/ rData \/ receiveD \/
receiveC \/ receiveA \/ dataChannel \/ ackChannel
\/ (* Disjunct to prevent deadlock on completion *)
(( messOut=Message) /\ UNCHANGED vars)
(* with out Fin the model never deadlocks *)
Fin == <>(messOut = Message) (* NOT a property of every behaviour *)
(* I interpreted these two experiments as meaning the system was busy looping between more that one state and not stuttering
But TLC error-trace is
<stuttering> State num=8
<sendD > State num7 *)
Without property Fin but with deadlock checked TLC reports no errors.
With Fin TLC reports that the temporal property fails.
Am I correct that if no deadlock is found then no infinite sequence of stuttering steps are possible ??
My problem is that when a termoral property fails and an error trace ends with <stuttering> together meant that an infinite sequence of stuttering steps was the cause of the filure ??
thanks in advance