[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.