Skip to content

Instantly share code, notes, and snippets.

View lorin's full-sized avatar
🤷‍♂️
Nominal

Lorin Hochstein lorin

🤷‍♂️
Nominal
View GitHub Profile
@lorin
lorin / queue1.tla
Created August 17, 2024 23:41
A simple queue model
\* 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