Re: [tlaplus] When TLC error trace send with stuttering

Hello David,

you are not showing us the full specification. A TLA+ specifications of the form

Init /\ [][Next]_v

allows for infinite stuttering. Adding fairness conditions WF_v(A) or SF_v(A) enforces action <<A>>_v to occur infinitely often if it is "often enough" enabled and therefore in particular rules out infinite stuttering in those cases. But infinite stuttering is still possible when A is disabled at the state where stuttering occurs.

The absence of deadlocks does not rule out infinite stuttering. For example, consider the specification

Init == x=0

Inc == x<5 /\ x'=x+1

Reset == x=5 /\ x'=0

Spec == Init /\ [][Inc \/ Reset]_x /\ WF_x(Inc)

The spec has no deadlock, since at least one action is possible at any reachable state. However, it fails to satisfy the property

[]<>(x=0)

because there is a behavior that stutters infinitely at the state where x=5: since Inc is disabled at that state, the fairness property is trivially satisfied.

More to the point, your next-state relation contains a disjunct that prevents deadlock (as indicated by the comment), but it may very well allow for infinite stuttering.

Hope this helps,

Stephan

On 30 Mar 2019, at 07:44, david streader <davidistreader@xxxxxxxxx> wrote:

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.

--
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.

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