Need help in debugging a program

[s.triv...@xxxxxxxxx]

Hi,


  When I tried to translate this program I am getting an error in line 9.please help me out this problem and here is the program

  EXTENDS Naturals, TLC

(* --algorithm withdrawl
variables x_account = 20,
          x_total = x_account - withdraw;

process variable withdraw \in 1..30;
begin
withdraw:
  if x_account >= withdraw then
    A: x_account := x_account - withdraw;
end if;
C: assert x_account >= 0;
end process
WithdrawNotNegative ==  >= 0

end algorithm *)

regards,
Triveni