Can we have reachability properties in TLA⁺? (by ahelwer) — discussion

#formalmethods