Re: [tlaplus] Attempted to apply record to a non-string argument Specifying Systems 3.2

[Isaac DeFrain <isaacdefrain@xxxxxxxxx>]

Hello Anand,

Get rid of the square brackets around chan and everything works. Like this:

Send(data) ==

/\ chan.ready = chan.ack

/\ chan' = [ chan EXCEPT !.val = data, !.ack = 1 - chan.ack ]

Receive ==

/\ chan.ready # chan.ack

/\ chan' = [ chan EXCEPT !.ack = 1 - chan.ack ]

Isaac DeFrain

On Mon, Aug 29, 2022 at 7:37 AM Anand Kumar <akkeshavan@xxxxxxxxx> wrote:

Any  idea why?

Data <- {"john", "paul", "ringo" }

EXTENDS  Naturals

CONSTANT Data

VARIABLE chan

TypeInvariant == chan \in [ val : Data, ready: {0,1} , ack : {0,1}]

Init == /\ TypeInvariant

        /\ chan.ack = chan.ready

Send(data) == /\ chan.ready = chan.ack

              /\ chan' = [chan EXCEPT ![chan].val = data, ![chan].ack = 1 - chan.ack]

Receive == /\ chan.ready # chan.ack

           /\ chan' = [ chan EXCEPT ![chan].ack = 1 - chan.ack ]

Next == (\E d \in Data : Send(d)) \/ Receive

Spec == Init /\ [] [Next]_chan      

--
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/88f3075a-5ce8-4546-aae0-197d79bea7afn%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/CAM3xQxH6nLddNqs_59Oc%2Bsqg79aLimm0M2_nHT335%2BLDASUfjQ%40mail.gmail.com.