Re: [tlaplus] Need help in debugging a program

[s.triv...@xxxxxxxxx]

On Wednesday, August 1, 2018 at 1:57:09 PM UTC+5:30, Maneet Bansal wrote:
> 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.tr...@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 tlaplu...@xxxxxxxxxxxxxxxx.
> 
> 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

Hi Maneet,

   The probelem is solved and its working now.Thnq Maneet Bansal.

Regards,
Triveni.