mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 01:30:22 +00:00
176a0e9926
* Add the TLA+ language This patch adds support for the TLA+ specification language. https://github.com/search?utf8=%E2%9C%93&q=MODULE+extension%3Atla&type=Code&ref=searchresults * Update TLA grammar license Attribution is given in the license since the grammar is based off of the TLA+ language developed by Microsoft and HP. * Sort languages.yml alphabetically * Removing duplicate entry
26 lines
676 B
Plaintext
26 lines
676 B
Plaintext
--------------------------- MODULE AsyncInterface ---------------------------
|
|
EXTENDS Naturals
|
|
|
|
CONSTANT Data
|
|
VARIABLE chan
|
|
|
|
Values == <<"foo", "bar", "baz">>
|
|
|
|
TypeInvariant == chan \in [val: Data, rdy: {0,1}, ack: {0,1}]
|
|
|
|
Init == /\ TypeInvariant
|
|
/\ chan.ack = chan.rdy
|
|
|
|
Send(d) == /\ chan.rdy = chan.ack
|
|
/\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]
|
|
|
|
Rcv == /\ chan.rdy # chan.ack
|
|
/\ chan' = [chan EXCEPT !.ack = 1 - @]
|
|
|
|
Next == (\E d \in Data : Send(d)) \/ Rcv
|
|
|
|
Spec == Init /\ [][Next]_chan
|
|
|
|
THEOREM Spec => []TypeInvariant
|
|
|
|
============================================================================= |