State models and invariant discovery

Try

Two accounts hold indivisible tokens. Initially account X has 6 and account Y has 4. A request names a direction and an integer amount k. A successful request moves tokens rather than creating them. Before reading a rule, write down what you would need to check to prevent an overdraft.

Our state is the ordered pair (x,y) of current integer balances. The ambient state space is all integer pairs, including negative ones; the safety claim is that the particular process never reaches those bad balances. The initial set contains the single state (6,4). This distinction keeps the desired conclusion out of the assumptions.

For a request from X to Y, accept exactly when 1≤k≤x, and replace the state by (x−k,y+k). For Y to X, accept exactly when 1≤k≤y, and replace it by (x+k,y−k). Every other integer request is rejected and leaves the state unchanged. The conditions are guards: they say when a proposed operation is enabled. Rejection is a state-preserving step, not a transfer of zero or a partly completed transaction.

This is a mathematical model of atomic operations: both balances change together. It is not an implementation of a concurrent bank or a claim that separate writes cannot fail. Questions about interrupted writes would require a richer state model.

Predict

Predict the result of requesting 3 tokens from X to Y, then 5 more from X to Y, then 2 from Y to X. Record each guard check before the successor state.

Someone proposes the invariant “x+y=10.” An invariant is a property true initially and preserved by every permitted step. Conservation is a useful candidate, but does it imply neither account is negative? Test the pair (−1,11). It satisfies the equation while violating the intended safety property. That observation identifies a logical weakness; it does not yet show this bad pair is reachable under the guarded rules.

Try strengthening the candidate before continuing. A stronger property has more conditions and therefore admits fewer possible states. It must still be true initially and preserved by every branch; adding a desirable sentence without proving preservation is not a repair.

Experiment

Complete this trace by hand, then compare the guard and total columns. The requests are supplied choices, not a deterministic algorithm that the model promises always to use.

Before	Request	Guard check	After	Total
(6,4)	X→Y, k=3	1≤3≤6: accepted	(3,7)	10
(3,7)	X→Y, k=5	5 exceeds 3: rejected	(3,7)	10
(3,7)	Y→X, k=2	1≤2≤7: accepted	(5,5)	10
(5,5)	Y→X, k=0	k is not positive: rejected	(5,5)	10

Now change only the acceptance rule: suppose every positive X→Y request is accepted. Starting again at (6,4), request k=7. The faulty rule reaches (−1,11). Conservation survives, but safety fails. Restore the guard, and explain which inequality blocks that exact transition.

Next investigate the same initial state with a new restriction: accepted transfers move exactly two tokens. Can it reach (5,5)? Both balances start even, and every accepted change is even. Therefore this target is unreachable despite having nonnegative balances and total 10. Write a stronger parity condition. This experiment separates a useful invariant from an exact description of all reachable states.

Understand

For the original arbitrary-integer-amount process, use the strengthened assertion P(x,y): x≥0, y≥0 and x+y=10. Its three parts have separate jobs: the first two express safety, while the last accounts for all tokens.

Initialization: P(6,4) holds. Accepted X→Y: assume P(x,y) and 1≤k≤x. Then x−k≥0, y+k≥0, and (x−k)+(y+k)=10. Accepted Y→X: assume P(x,y) and 1≤k≤y. Then y−k≥0, x+k≥0, and (x+k)+(y−k)=10. Rejection: the unchanged state still satisfies P. These checks quantify over arbitrary states satisfying P and every enabled request, not merely the three amounts in the trace.

Induct on the length n of any finite execution. At length zero initialization applies. If its state after n requests satisfies P, the applicable branch above proves P after request n+1. Thus every reachable state satisfies P, regardless of which requests a scheduler chooses. This is a nondeterministic process: several next requests may be possible, and the proof must survive them all.

The proof establishes an inductive invariant: it is preserved even when checked from any state satisfying P, whether or not a separate reachability argument has been supplied. An invariant can overestimate the reachable set. For the two-token restriction, (5,5) belongs to P but not to the reachable set; adding evenness excludes it. Conversely, proving a property on a few observed reachable states does not establish its preservation universally. A mathematical property may hold on all reachable states yet require strengthening to obtain a convenient inductive proof.

Suppose a controller declares success only when x=0. The invariant then implies the exit postcondition y=10. This is conditional: if a reached state meets the exit test, the desired output follows. It does not show that the exit test will ever be met. Requests can alternate X→Y and Y→X forever, or keep requesting an unaffordable amount. Safety holds throughout such executions. Stating that an accepted step changes a balance is not a decreasing-measure argument.

To claim termination, specify an additional rule and prove progress. For example, always moving exactly one token from X to Y while x>0 decreases the nonnegative integer x by one; starting at 6 it exits after six transfers. That is a different, more restrictive process. A claim about it cannot be silently transferred to the original arbitrary scheduler.

A common-divisor invariant can be true and incomplete

Extend the capacity-guard repair in the practice below. Let each account have integer capacity C, total N, and initial balance x=a, y=N−a, with both balances between zero and C. Let S be a nonempty finite set of positive integer transfer sizes. A request chooses k in S and a direction. Accept x→y only when k is at most both x and C−y; accept the reverse only when k is at most both y and C−x. Other requests leave the state unchanged. The source guard preserves nonnegativity, the receiving-capacity guard preserves the upper bound, and equal subtraction/addition preserves the total. Rejection preserves all three.

Let g be the greatest common divisor of S. Every accepted change in x is plus or minus a multiple of g, while a rejected request changes nothing. Induction on execution length proves x≡a modulo g and y≡N−a modulo g for every reachable state. These are necessary conditions, not yet a route construction.

A residue class is not a route

Predict whether the target can be reached. Compare a closed reachable set with a residue-compatible state that has no legal path.

Transfer case Gcd permits two, guards block itWider interval unlocks the Bezout routeSmallest gcd step is availableNonzero lower bound and shifted residueChanged coprime sizes still cannot leave Target x 01234 Reset

Total 4; each capacity 4; allowed sizes 4, 6. Start (0, 4); feasible x interval [0, 4]; gcd 2.

Target residue condition: passes. No legal path: the complete reached set excludes the target.

Reached x values: 0, 4. Work: 8 signed size/guard attempts across 2 expanded states, including rejected attempts.

State (x,y)	Residue	Reached	Parent	All accepted successor x values
(0, 4)	Pass	Yes	Start	4
(1, 3)	Fail	No	—	none
(2, 2)	Pass	No	—	none
(3, 1)	Fail	No	—	none
(4, 0)	Pass	Yes	0	0

Check that every successor of a reached row is reached. Together with parent paths, this is an exact finite certificate. Temporary examples have at most seven states and 42 signed guard attempts; they do not prove an unrestricted reachability theorem or learner mastery.

For C=N=4, a=0 and S=6, the feasible states correspond to x in the integer interval [0,4]. The residue condition permits x=2. But the only reachable x values are zero and four: size six never fits, and size four merely swaps those endpoints. Although 6−4=2 is a Bézout combination of the permitted sizes, its first positive step would require leaving the feasible interval. Starting with the negative step also fails. Bézout proves an unrestricted integer combination, not a valid order of guarded operations. Widening to C=N=6 unlocks the route x=0→6→2, which preserves every capacity guard.

Prove what a finite reachability certificate establishes

Conservation reduces the state space to x in [L,U], where L=max(0,N−C) and U=min(C,N). The successor x+k is accepted exactly when it remains in this interval, and likewise for x−k. Thus a finite graph describes all accepted transitions; rejected requests add self-loops and no new states.

Start a queue with a, mark it reached, and for each reached state inspect both signs of every allowed size. Mark each previously unseen legal successor and record its parent. There are U−L+1 possible vertices, so each is expanded at most once. The signed guard-attempt bound is 2·|S|·(U−L+1); it is not a timing measurement. Parent edges certify that each discovered vertex is reachable, by induction on discovery. At queue exhaustion every legal successor of every reached vertex is reached. Conversely, induction on any execution length shows that a set containing a and closed under successors contains every reachable state. These two directions prove the computed set exact. A mere failed search stopped before exhaustion would not prove impossibility.

A useful sufficient special case is g itself belongs to S. Every feasible target t congruent to a modulo g can then be reached by repeatedly adding or subtracting g toward t. All intermediate x values lie between a and t inside [L,U], so every step is legal. This proves necessity and sufficiency under the added hypothesis. Without it, gcd one can still be insufficient: C=N=4, a=2 and S=5 allow no first move, although every integer target passes the residue test.

Apply

A transfer service now uses a holding account h between reservation and delivery. The ambient states are integer triples (x,y,h), initially (6,4,0). All amounts are positive integers; an unaffordable or nonpositive request is rejected without changing the state.

Operation	Additional guard	Successor
Reserve from X	k≤x	(x−k,y,h+k)
Deliver to Y	k≤h	(x,y+k,h−k)
Cancel back to X	k≤h	(x+k,y,h−k)

First reserve 2. The resulting state (4,4,2) has x+y=8, so the earlier two-account conservation assertion is no longer an invariant. Discover a replacement that reflects the changed state rather than declaring that tokens disappeared. Then prove it branch by branch, including cancellation and rejection. State what follows at an exit satisfying x=h=0.

Worked repair and a failed implementation rule

Use x,y,h≥0 and x+y+h=10. Initialization is immediate. Reserve moves k from a source at least k to h; delivery and cancellation move k from h, again only when h≥k. In each case the source remains nonnegative, the recipient increases, and one subtraction cancels one addition in the total. Rejection is the identity. Induction proves every finite execution safe and fully accounted for. At an exit with x=h=0, conservation forces y=10.

A faulty delivery (x,y+k,h) would add credit without releasing the held amount. After reserving 2 from the initial state, this faulty delivery of 2 yields (4,6,2), whose total is 12. The counterexample diagnoses the transition rule, not the correct invariant. Repair the transition by subtracting k from h; do not repair the evidence by ignoring held tokens.

This triple records aggregate quantities only. It cannot establish that each named customer receives a particular reservation exactly once: reservation identities and ownership are not in the state. Even a complete proof answers only properties expressible under the specified model. Write one extra state field and rule you would need before asserting that stronger business requirement.

Continue

Keep five items together: state space, initial set, guarded transition rules, proposed invariant and exit test. Your proof should show initialization and every preservation case before using the invariant to infer safety or an exit postcondition. If a claim fails, decide whether the problem is a weak assertion, a faulty operation, an omitted branch or a conclusion stronger than the model permits.

The six tasks change initial balances, add escrow, restrict transfer sizes and impose capacities. Some ask for a reachability proof in both directions, going beyond invariant preservation. Their worked solutions are public guidance and require human critique; recording a response does not verify a universal argument.

For the existing algorithmic recap, revisit loop invariants and termination. For the proof mechanism itself, revisit ordinary and strong induction. The next kinds of progress arguments may need more than one decreasing quantity; conservation and safety alone do not provide them.