A simple queue model

queue1.tla

\* Queue model where changes happen in each state
---- MODULE queue1 ----
EXTENDS Sequences

CONSTANT Val, N
VARIABLES op,arg,rval,d

none == CHOOSE v : v \notin Val


Init == /\ op = "enq"
        /\ arg \in Val
        /\ rval = "ok"
        /\ d = <<arg>>

Enq ==  /\ Len(d) < N
        /\ op' = "enq"
        /\ arg' \in Val
        /\ rval' = none
        /\ d' = Append(d, arg')

Deq == /\ d /= <<>>
          /\ op' = "deq"
          /\ arg' = none
          /\ rval' = Head(d)
          /\ d' = Tail(d)


Next == Enq \/ Deq

====