[tlaplus] When TLC error trace send with stuttering - what does this mean?

[david streader <davidistreader@xxxxxxxxx>]

Hi I am trying to debug liveness properties and realised I lack some understanding:

My module  includes:

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.