[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Need help in debugging a program

Hi Triveni,

Assuming your line 9 is "process variable withdraw \in 1..30"

You are missing assigning a value to the process. I changed it to the following and it worked 

process p = 1

variable withdraw \in 1..30;


P.S: I have to comment out "WithdrawNotNegative ==  >= 0". Seems like you are missing some variable there.

On Tue, Jul 31, 2018 at 10:15 PM, <s.triv...@xxxxxxxxx> wrote:

  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;
  if x_account >= withdraw then
    A: x_account := x_account - withdraw;
end if;
C: assert x_account >= 0;
end process
WithdrawNotNegative ==  >= 0

end algorithm *)


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Maneet Bansal