Starting the document on TLA+ idioms

[konnov]

This document has been living in a separate branch for several months. Let's start writing it. The first two idioms are in.

[lemmy]

Perhaps, the definition of NotifyOther below could serve as an example of when to add additional variables to make a spec human-friendly:

--------------------------- MODULE BlockingQueueFair ---------------------------

...

VARIABLES buffer, waitSeq
vars == <<buffer, waitSeq>>


Range(f) == { f[i]: i \in DOMAIN f }
waitSet == Range(waitSeq)

RunningThreads == (Producers \cup Consumers) \ waitSet

NotifyOther(t) == 
          LET S == IF t \in Producers THEN waitSet \ Producers ELSE waitSet \ Consumers
              R == SelectSeq(waitSeq, LAMBDA u:u \in S)
              T == SelectSeq(waitSeq, LAMBDA u:u \notin S)
          IN IF R # <<>>
             THEN waitSeq' = Tail(R) \o T
             ELSE UNCHANGED waitSeq

(* @see java.lang.Object#wait *)
Wait(t) == /\ waitSeq' = Append(waitSeq, t)
           /\ UNCHANGED <<buffer>>
           
-----------------------------------------------------------------------------

Put(t, d) ==
   \/ /\ Len(buffer) < BufCapacity
      /\ buffer' = Append(buffer, d)
      /\ NotifyOther(t)
   \/ /\ Len(buffer) = BufCapacity
      /\ Wait(t)
      
Get(t) ==
   \/ /\ buffer # <<>>
      /\ buffer' = Tail(buffer)
      /\ NotifyOther(t)
   \/ /\ buffer = <<>>
      /\ Wait(t)

...
=============================================================================

In contrast, this is the variant with one more variable that separates wait into Producers and Consumers.

[konnov]

Nice example, @lemmy. It indeed looks cleaner with one more variable. By the way, I am also violating this rule from time to time :-)

[adizere]

Very cool!

I initially wanted to ask if this repo is the right place to collect the idioms (VDD might have been better), but I understand that some idioms are actually Apalache-specific.

[konnov]

I will merge this PR so it becomes more visible. Feel free to propose changes.

[lemmy]

Perhaps, auxiliary (history/prophecy) variables deserve mention too.