Re: [tlaplus] TLA+ Toolbox Error

[Stephan Merz <stephan.merz@xxxxxxxxx>]

The main code block of an algorithm must appear inside braces. See the PlusCal grammar in the manual (specifically, the definition of "CompoundStatement") and/or tutorials and examples available on the Web, such as learntla.com.

(*

--algorithm Increase {

variable x = 0;

{

x := x + 1;

print x

}

}

*)

Also, for using "print", your module must extend the TLC module.

Stephan

On 30 Jul 2024, at 09:28, YingMing Wang <yingmingw97@xxxxxxxxx> wrote:

Hi,

I am new to TLA+ and currently in the process of learning how to use it. I have installed the TLA+ Toolbox on two of my PCs, one running Ubuntu and the other running Windows. However, I've encountered some issues on both systems and am unsure if they are due to my mistakes or something else.

Problem:

This is the code from pluscal 

EXTENDS Integers

(*

--algorithm Increase {

variable x = 0;

x := x + 1;

print x

}

*)

Then, this is the error when I try to translate it. It happens on both PCs.

<error of translation.png>

Could you please advise on how to resolve this issue and how to avoid similar problems (Expected ";", but found "xxx")?

Thank you for your assistance and support.

Best regards,

Yingming

--
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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fce0f35a-4ebc-44e5-b18d-13ecc752fe63n%40googlegroups.com.
<error of translation.png>

--
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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87D6C6E7-F8A1-41C6-A8DB-E5F89704B9D8%40gmail.com.