Skip to content

Instantly share code, notes, and snippets.

@mdmarek

mdmarek/Chan.cfg

Created November 3, 2016 16:12
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mdmarek/15ad6f68d10f584b9dd741b3bee2a6ac to your computer and use it in GitHub Desktop.
Save mdmarek/15ad6f68d10f584b9dd741b3bee2a6ac to your computer and use it in GitHub Desktop.
Download ZIP
TLA+ Channel
Raw
Chan.cfg
INIT
Init
NEXT
Next
INVARIANT
TypeOK
CONSTANTS
Data = { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 }
Raw
Chan.tla
---- MODULE Chan ----
EXTENDS Integers, TLC
CONSTANT Data
VARIABLE chan
TypeOK == chan \in [val: Data, rdy: {0,1}, ack: {0,1}]
Init == /\ TypeOK
/\ chan.ack = chan.rdy
Tx(d) == /\ chan.rdy = chan.ack
/\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]
Rx == /\ chan.rdy /= chan.ack
/\ chan' = [chan EXCEPT !.ack = 1 - @]
Next == (\E d \in Data : Tx(d)) \/ Rx
Spec == Init /\ [][Next]_chan
----
THEOREM Spec => []TypeOK
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment