Attempted to apply record to a non-string argument Specifying Systems 3.2

[Anand Kumar]

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      

[Isaac DeFrain]

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

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88f3075a-5ce8-4546-aae0-197d79bea7afn%40googlegroups.com.

[Anand Kumar]

Cool! Thanks