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

Hello David,

nice work – I had a quick look at your specs and confirmed that the spec in abpPar can be shown to refine the one-place buffer. The result is attached to this message, here are a few comments:

- You are assuming strong fairness for all processes, which is clearly stronger than necessary. Weak fairness is enough for all processes except for data transmission (which competes with data loss). No fairness should be assumed for data loss since we don't want to assume that any data loss actually occurs. Similarly, weak fairness is enough for the high-level spec.

- I reduced the state space by assuming that the loop bodies of all processes are executed atomically. However, I checked that refinement still holds when your additional labels are added back.

- I used a refinement mapping instead of a history (ghost) variable for defining the variable read_state.

I assume that refinement for the decomposed specification can be verified in a similar way, since my understanding is that this specification generates the same behaviors – but I haven't actually checked this or even looked at the decomposed specification in much detail.

Initially, I was a little confused by the fact that process sendData sets the channel to a singleton sequence when sending data, and similarly for the other message sending operations. I then noticed (and verified using TLC) that your specification ensures that both channels hold at most one message. This depends on the somewhat unrealistic assumption that processes can test emptiness of communication channels that they send on – cf. the test on Len(sendDataQueue) in process sendData – but of course it simplifies model checking.

–––

I attach an alternative specification (AlternatingBit.tla) of the alternating-bit protocol that I wrote a few years ago, where I also check refinement w.r.t. a higher-level channel specification (Transmission.tla). Perhaps one could similarly decompose that specification into separate pieces. Instead of transmitting a fixed sequence of data, it continually sends arbitrary data over the channel and one verifies that infinitely often the sent data is received. Since channel sizes are unbounded in that specification, you'll have to use a state constraint to bound the state space for TLC.

Cheers,

Stephan

--
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: OnePlaceBufferSpec.tla
Description: Binary data

Attachment: AlternatingBit.tla
Description: Binary data

Attachment: Transmission.tla
Description: Binary data

On 17 Feb 2019, at 02:25, david streader <davidistreader@xxxxxxxxx> wrote:

Hi
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.
<abpPar.tla><ABPModular.zip>