A two-door airlock is modelled by Boolean variables L and R, each 1 when that door is…

A two-door airlock is modelled by Boolean variables $L$ and $R$, each $1$ when that door is open and $0$ when it is closed. Write a state as the bit pair $LR$. The safety invariant is \[ I:\quad \lnot(L\land R). \] The intended controller exposes four guarded commands, evaluated against the current state and executed atomically: \begin{align*} \mathrm{openL}&:\ \textbf{if }R=0\textbf{ then }L\leftarrow 1,\\ \mathrm{openR}&:\ \textbf{if }L=0\textbf{ then }R\leftarrow 1,\\ \mathrm{closeL}&:\ L\leftarrow 0,\\ \mathrm{closeR}&:\ R\leftarrow 0. \end{align*} The system starts at $00$. A command whose guard fails is a no-op. A proposed firmware defect implements $\mathrm{openL}$ and $\mathrm{openR}$ as two independent check-then-write actions in the same evaluation cycle. Both guards are evaluated against the same \emph{pre-cycle} values of $L$ and $R$, and both passing writes commit. 1. Starting from $00$, enumerate every state reachable by a finite sequence of the four guarded commands. Prove that the reachable set is exactly $\{00,10,01\}$. 2. Prove $I$ by induction on guarded executions. Then exhibit one buggy simultaneous pair of independent opens from $00$ that reaches $11$, and confirm that $11$ falsifies $I$. 3. Audit both sentences: (i) “$11$ is reachable under the guards, because one can open $L$ and then open $R$”; (ii) “even the non-atomic simultaneous pair cannot reach $11$, because one action must observe the sibling's committed post-state before evaluating its own guard.” Do not replace the interlock by a watchdog, CRC, or lockstep-core argument, and do not encode the doors as a continuous hybrid automaton.

From $00$ the guarded opens reach $10$ and $01$. From $10$, $\mathrm{openR}$ is disabled and $\mathrm{closeL}$ returns to $00$. The symmetric statement holds at $01$.