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

*From*: "c.burge...@xxxxxxxxx" <c.burge.glasgow@xxxxxxxxx>*Date*: Tue, 27 Apr 2021 08:09:09 -0700 (PDT)*References*: <6b4b773b-6c16-4f7b-a35d-6736d5c70db8n@googlegroups.com> <D95FD7E0-3A3F-434B-A7E9-B960C2A39220@gmail.com> <20231f17-6609-404a-8c72-8ed390cef4ban@googlegroups.com>

I see that I was not yet familiar with the concepts of stuttering and fairness, but a quick google has enlightened me :)

On Tuesday, April 27, 2021 at 4:05:18 PM UTC+1 c.burge...@xxxxxxxxx wrote:

Thanks, that's very helpful!On Tuesday, April 27, 2021 at 2:52:58 PM UTC+1 Stephan Merz wrote:Your algorithm may fail to terminate due to stuttering: any TLA+ specification of the formInit /\ [][Next]_varsmay take stuttering steps, even infinitely many. In order to rule out infinite stuttering, add a fairness assumption of the formWF_vars(Next)to the specification generated by the PlusCal translator. If you write "fair algorithm" instead of "algorithm", the PlusCal translator will generate that fairness condition for you.StephanOn 27 Apr 2021, at 15:45, c.burge...@gmail.com <c.burge...@xxxxxxxxx> wrote:Hi again :)I am trying out different implementations of a while loop, and I have this little pluscal algorithm:--------------------------------

MODULEloop --------------------------------

EXTENDSNaturals, TLC(*

--algorithm loop {

variables y;

{

A:

goto C;

B:

y:=y-1;

C:

if (y > 0){

goto B };

D: skip;

}

}

end algorithm;

*)

I give y an initial value of 10, but when I ask TLC to check for termination, it fails. Why would that be? The error trace shows the loop working as expected, with y decreasing from 10 to 0 in increments of 1.

--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6b4b773b-6c16-4f7b-a35d-6736d5c70db8n%40googlegroups.com.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/76a2f7de-a307-48f6-a8a2-6070e1a4a9ffn%40googlegroups.com.

**References**:**[tlaplus] Loop not terminating***From:*c.burge...@xxxxxxxxx

**Re: [tlaplus] Loop not terminating***From:*Stephan Merz

**Re: [tlaplus] Loop not terminating***From:*c.burge...@xxxxxxxxx

- Prev by Date:
**Re: [tlaplus] Loop not terminating** - Next by Date:
**[tlaplus] Different trace for a temporal property violation (stuttering) using same seed and fp** - Previous by thread:
**Re: [tlaplus] Loop not terminating** - Next by thread:
**[tlaplus] Different trace for a temporal property violation (stuttering) using same seed and fp** - Index(es):