Always in Bounds

Starting from the completed TwoCounters spec, add a temporal property AlwaysSafe that claims, using [], that TypeOK holds and that x + y never exceeds 4 — a single compound claim about every reachable state, phrased as a temporal formula instead of an INVARIANT.

Requirements:

• AlwaysSafe == [](TypeOK /\ x + y <= 4).
• Add PROPERTY AlwaysSafe to TwoCounters.cfg (you can drop the INVARIANT TypeOK line — AlwaysSafe already implies it).

Fill in starter.tla where marked, then click Run Model Checker. Since x and y each cap out at 2, their sum can never exceed 4 — TLC should report no violations. Try lowering the bound to 3 and re-running, to see what a [] violation trace looks like (then put it back to 4 before submitting).