Typo in example or guard semantics unclear?

[asolove]

The conceptual overview starts with pseudocode:

and naively I read this as python-ish code, where the if is controlling whether the other two lines run, in which case I think the guard expression is backwards (from.balance should be greater than or equal to the amount for it to work?)

(but perhaps some other pseudo-code format is intended, in which case I just got confused? or perhaps the typo is intentional and a later section will describe how model-checking interacts with things like unit tests or other ways to check for typos in the non-model real code? or perhaps I am doing the logic wrong myself?)

[hwayne]

Nope, it's a bug. Someone else pushed a fix, so should be clear now!