Lobsters: Can we have reachability properties in TLA⁺?