Toy model

talex5 · Dec 17, 2018 · 75a846d5c83d86ba7be42b5c3b9f98635bcc544d · 75a846d
commit 75a846d5c83d86ba7be42b5c3b9f98635bcc544d
Unified Split

Showing with 50 additions and 0 deletions.

+50 −0 vchan.tla
diff --git a/vchan.tla b/vchan.tla
@@ -0,0 +1,50 @@
+  
+------------------------------- MODULE vchan -------------------------------
+  
+
+  
+EXTENDS Naturals, Sequences   \* Library imports
+  
+CONSTANT BufferSize
+  
+Byte == 0..255
+  
+MSG  == Seq(Byte)
+  
+
+  
+Take(m, i) == SubSeq(m, 1, i)
+  
+Drop(m, i) == SubSeq(m, i + 1, Len(m))
+  
+
+  
+VARIABLES Got, Buffer, Sent
+  
+vars == << Got, Buffer, Sent >> 
+  
+
+  
+\* Desired properties
+  
+
+  
+Integrity       == Take(Sent, Len(Got)) = Got
+  
+
+  
+AvailabilityNat == Nat
+  
+Availability    == \A x \in AvailabilityNat :
+  
+                    Len(Sent) = x ~> Len(Got) >= x
+  
+
+  
+\* Algorithm
+  
+
+  
+Read  == \E n \in 1..Len(Buffer) :
+  
+          /\ Got' = Got \o Take(Buffer, n)
+  
+          /\ Buffer' = Drop(Buffer, n)
+  
+          /\ UNCHANGED Sent
+  
+
+  
+Write == \E m \in MSG :
+  
+          /\ Buffer' = Buffer \o m
+  
+          /\ Len(Buffer') <= BufferSize
+  
+          /\ Sent' = Sent \o m
+  
+          /\ UNCHANGED Got
+  
+
+  
+Next  == Read \/ Write
+  
+
+  
+Init  == /\ Sent   = << >>
+  
+         /\ Buffer = << >>
+  
+         /\ Got    = << >>
+  
+
+  
+Spec  == Init /\ [][Next]_vars /\ WF_vars(Read)
+  
+
+  
+BufferOK == Len(Buffer) <= BufferSize
+  
+
+  
+\* Model checking
+  
+
+  
+MSG_SEQ(max) == { [ x \in 1..N |-> Len(Sent) + x ] : N \in 1..max }
+  
+
+  
+=============================================================================
+  
+