Debugging and checking the edge cases

[s.triv...@xxxxxxxxx]

Hi,

   When I am model checking the following program x_account is going negative how to resolve that problem and also how to check the edge cases and how to use invariants and properties in model checking.
  Can you please figerout the problem in the following code.


------------------------------ MODULE transfer -----------------------------
EXTENDS Naturals, TLC

(* --algorithm transfer
variables x_account = 10, y_account = 10,money \in 1..20,
          account_total = x_account + y_account;

process Transfer \in 1..2 
begin
Transfer:
  if x_account >= money then
    A: x_account := x_account - money;
       y_account := y_account + money;
end if;
C: assert x_account >= 0;
end process

end algorithm *)
============================================================================


Thanks,
Triveni.