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
47 lines
1.3 KiB
Plaintext
47 lines
1.3 KiB
Plaintext
-------------------------------- MODULE fifo --------------------------------
|
|
EXTENDS Naturals, Sequences
|
|
CONSTANT Message
|
|
VARIABLES in, out, q
|
|
|
|
InChan == INSTANCE AsyncInterface WITH Data <- Message, chan <- in
|
|
OutChan == INSTANCE AsyncInterface WITH Data <- Message, chan <- out
|
|
|
|
-----------------------------------------------------------------------------
|
|
|
|
Init == /\ InChan!Init
|
|
/\ OutChan!Init
|
|
/\ q = <<>>
|
|
|
|
TypeInvariant == /\ InChan!TypeInvariant
|
|
/\ OutChan!TypeInvariant
|
|
/\ q \in Seq(Message)
|
|
/\ Len(q) <= 10
|
|
|
|
SSend(msg) == /\ InChan!Send(msg) \* Send msg on channel in
|
|
/\ UNCHANGED <<out, q>>
|
|
|
|
BufRcv == /\ InChan!Rcv
|
|
/\ Len(q) < 10
|
|
/\ q' = Append(q, in.val)
|
|
/\ UNCHANGED out
|
|
|
|
BufSend == /\ q # <<>>
|
|
/\ OutChan!Send(Head(q))
|
|
/\ q' = Tail(q)
|
|
/\ UNCHANGED in
|
|
|
|
RRcv == /\ OutChan!Rcv
|
|
/\ UNCHANGED <<in, q>>
|
|
|
|
Next == \/ \E msg \in Message : SSend(msg)
|
|
\/ BufRcv
|
|
\/ BufSend
|
|
\/ RRcv
|
|
|
|
Spec == Init /\ [][Next]_<<in, out, q>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
|
|
THEOREM Spec => []TypeInvariant
|
|
|
|
============================================================================= |