carlehewitt

   http://web.stanford.edu/class/ee380/Abstracts/190123.html

    * activities can be suspended and later resumed
    * other activities can use the region of mutual
      exclusion while a message is being processed by
      another Actor

    * Receipt of a communication activated sending other communications
    * An Actor received one communication before it received another communication

  http://web.stanford.edu/class/ee380/Abstracts/190123.html

     anAccount.deposit[$5]

     Account.send[anAccount. deposit[$5]

  http://web.stanford.edu/class/ee380/Abstracts/190123.html

    * Receipt of a communication activated sending other communications
    * An Actor received one communication before it received another communication

   https://professorhewitt.blogspot.com/

   1. Suppose that an Actor x has property P when it is created.

   2. Further suppose that if x has property P when it receives a communication, 
      then it has property P when it has processed the communication.

   3. Then x always has the property P.

  ReadPriority[aDatabase:*ReadersWriter*]:*ReadersWriterManager*
       //  Invariant: **Nonempty** #writing# ⇨ **IsEmpty** #reading#
   **Locals**(Queue(#writersQ#, #readersQ#),
              Crowd(#reading#),
              AtMostOne(#writing#)),
   **Handlers**( 
       ⟦scheduler⟧ ↦ **As** myScheduler, // myScheduler facet of this manager
       upgrade[newVersion] ↦ 
            (**CancellAll**  #readersQ# **and** #writersQ# **and** #reading# **and** #writing#
                  **for** **Become** newVersion)
   myScheduler **implements** *ReadersWriter* **Handlers**( 
      read[aQuery] ↦ 
         **Enqueue** #readersQ# **when** **Nonempty** #writing# **or** #writersQ# **or** #readersQ# 
             **for** aDatabase.read[aQuery] **thru** #reading#
                    **permit** #readersQ#
                       **afterward** **Permit** #writersQ# **when** **IsEmpty** #reading#
                                                **else** #readersQ# **when** **IsEmpty** #writersQ#,
      write[anUpdate] ↦    
         **Enqueue** #writersQ# **when** **Nonempty** #reading# **or** #readersQ# **or** #writing# **or** #writersQ#  
              **for** aDatabase.write[anUpdate] **thru** #writing#
                   **afterward** **Permit** #readersQ# **else** #writersQ#)▮