From 176a0e9926253c9447c23f8b1c0f6b85c434e692 Mon Sep 17 00:00:00 2001 From: Arfon Smith Date: Fri, 6 May 2016 13:19:44 -0600 Subject: [PATCH] TLA revisited (#2990) * 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 --- .gitmodules | 3 +++ grammars.yml | 2 ++ lib/linguist/languages.yml | 7 +++++ samples/TLA/AsyncInterface.tla | 26 ++++++++++++++++++ samples/TLA/fifo.tla | 47 +++++++++++++++++++++++++++++++++ vendor/grammars/TLA | 1 + vendor/licenses/grammar/TLA.txt | 26 ++++++++++++++++++ 7 files changed, 112 insertions(+) create mode 100644 samples/TLA/AsyncInterface.tla create mode 100644 samples/TLA/fifo.tla create mode 160000 vendor/grammars/TLA create mode 100644 vendor/licenses/grammar/TLA.txt diff --git a/.gitmodules b/.gitmodules index 551b9450..d7f792e4 100644 --- a/.gitmodules +++ b/.gitmodules @@ -716,3 +716,6 @@ [submodule "vendor/grammars/sublime-autoit"] path = vendor/grammars/sublime-autoit url = https://github.com/AutoIt/SublimeAutoItScript +[submodule "vendor/grammars/TLA"] + path = vendor/grammars/TLA + url = https://github.com/agentultra/TLAGrammar diff --git a/grammars.yml b/grammars.yml index 90c6ebcf..978ed064 100755 --- a/grammars.yml +++ b/grammars.yml @@ -129,6 +129,8 @@ vendor/grammars/SublimePuppet/: - source.puppet vendor/grammars/SublimeXtend: - source.xtend +vendor/grammars/TLA: +- source.tla vendor/grammars/TXL/: - source.txl vendor/grammars/Textmate-Gosu-Bundle: diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 4d33b31d..9e2cb887 100755 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -3531,6 +3531,13 @@ SystemVerilog: - .vh ace_mode: verilog +TLA: + type: programming + extensions: + - .tla + tm_scope: source.tla + ace_mode: text + TOML: type: data extensions: diff --git a/samples/TLA/AsyncInterface.tla b/samples/TLA/AsyncInterface.tla new file mode 100644 index 00000000..78d34e1b --- /dev/null +++ b/samples/TLA/AsyncInterface.tla @@ -0,0 +1,26 @@ +--------------------------- 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 + +============================================================================= \ No newline at end of file diff --git a/samples/TLA/fifo.tla b/samples/TLA/fifo.tla new file mode 100644 index 00000000..34fce0a7 --- /dev/null +++ b/samples/TLA/fifo.tla @@ -0,0 +1,47 @@ +-------------------------------- 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 <> + +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 <> + +Next == \/ \E msg \in Message : SSend(msg) + \/ BufRcv + \/ BufSend + \/ RRcv + +Spec == Init /\ [][Next]_<> + +----------------------------------------------------------------------------- + +THEOREM Spec => []TypeInvariant + +============================================================================= \ No newline at end of file diff --git a/vendor/grammars/TLA b/vendor/grammars/TLA new file mode 160000 index 00000000..7e351a9c --- /dev/null +++ b/vendor/grammars/TLA @@ -0,0 +1 @@ +Subproject commit 7e351a9cdf6fbf3132e35246ce190bad237fb39c diff --git a/vendor/licenses/grammar/TLA.txt b/vendor/licenses/grammar/TLA.txt new file mode 100644 index 00000000..882d33bc --- /dev/null +++ b/vendor/licenses/grammar/TLA.txt @@ -0,0 +1,26 @@ +--- +type: grammar +name: TLA +license: mit +--- +The MIT License (MIT) + +Copyright (c) 2013 Microsoft and HP + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE.