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;

begin

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:

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

--
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.

Regards
Maneet Bansal