Flaky Signal

Write a spec for a flaky network link and a sender that delivers a message only while the link happens to be up.

Requirements:

• Variables link \in {"up", "down"} and sent \in BOOLEAN, starting at link = "down", sent = FALSE.
• TypeOK: both variables stay in those sets.
• Toggle: flips link from "up" to "down" or back; sent unchanged.
• Send: enabled only when link = "up"; sets sent' = TRUE; link unchanged.
• Next == Toggle \/ Send.
• Spec: Init conjoined with [][Next]_vars, WF_vars(Toggle) (so the link keeps flipping), and SF_vars(Send) (so the message gets through despite Send never being continuously enabled).
• Delivered == <>sent.

Fill in starter.tla where marked, then click Run Model Checker. TLC should report no violations. If you're curious what goes wrong with the weaker promise, try swapping SF_vars(Send) for WF_vars(Send) locally and re-running — then put SF_vars(Send) back before submitting.