Feedback wanted: Modeling Debian's New Member Process

[Arian Ott]

Hi,

I'm a software developer, 3 days into TLA+. As a learning exercise I
modeled Debian's New Member process (Steps 1-7) based on
https://www.debian.org/devel/join/nm-step1 ff.

The shift from "how do I build this" to "what must always be true"
is new to me, so I wanted to try it on a real process I care about.

The spec covers:

- Prerequisite checks (key signing by >= 2 DDs, >= 2 advocates,
DFSG/SC agreement, Salsa account, free time)
- Application submission with guards enforcing all prerequisites
- AM task/skills verification and report
- Front desk review with reject/resubmit loop
- DAM approval or rejection

9 variables, 13 actions, 9 invariants. TLC explores 368 states, all
invariants hold.

One result that surprised me: the DAM reject path is unreachable.
All rejection grounds from the wiki (inadequate identification,
failure to agree to principles, incomplete tasks) are enforced as
guards before submission. So by the time the DAM sees the application,
there's nothing left to reject. I didn't plan for that, however TLC found
it.

Feedback and patches welcome :D

Link to spec:

https://github.com/Arian-Ott/debian-process/blob/master/nmprocess/
nmprocess.tla

Happy Hacking!
--
Arian Ott
aria...@ieee.org