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
arian.ott@xxxxxxxx
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5119411.GXAFRqVoOG%40office.arianott.com.
Attachment:
signature.asc
Description: This is a digitally signed message part.