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

@@ -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

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:

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:

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
+
+=============================================================================

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 <<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
+
+=============================================================================

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.