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

[tlaplus] add fairness properties to a specification with PlusCal INSTANCEs

    I have encoded the Alternating Bit Protocol as several PlusCal processes in a style that hopefully would be familiar to anyone with a back ground in Process algebras. The specification is in the attached  single Module abpPar.tla. It includes some fairness properties and has been shown to satisfy the liveness property Fin.

I decomposed the problem into separate processes that can be found in separate modules, abpSender.tla, abpReceiver.tla  and abpWire.tla Then I wrote a module for a one place buffer, onePlaceBufferSpec.tla then showed that abpModular.tla satisfied the one place buffer.  But only if neither included fairness properties.  Although I was able to specify fairness on onePlaceBufferSpec.tla I can not see how to do this on abpModular.tla.  Any offers of how to specify fairness on abpModular.tla  would be greatly appreciated.  
     Also any comments on how the specifications might be improved while still having Sender Receiver and Channels in seperate process would also be very usful.

many thanks in advance previous discussions have been very helpful. 

kind regards david

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.

Attachment: abpPar.tla
Description: Binary data

Attachment: ABPModular.zip
Description: Zip archive