Hi,
Could you please write up the errors going forward? Thunderbird isn't downloading your PNGs properly.
Anyway, the answer to your question is on the Model Overview Page of the toolbox Help > Model Checking Creating a Model.
H
On 5/4/2023 10:20 AM, Sara Zain wrote:
Thanks! yeah fixed the empty sequence too.
However, does anyone know why there is this error now?Thanks in advance.
--On Thursday, May 4, 2023 at 9:43:12 AM UTC+2 Rosalie Defourné wrote:
Also (not related to your error), the empty sequence is << >>, which is different than the empty set { }. You probably want to change that in the definition of Init.
Le mercredi 3 mai 2023 à 20:22:42 UTC+2, Stephan Merz a écrit :
The error message is quite explicit. You probably want to write something like
\E record \in RECORD : Upload(record)
for some set RECORD that contains legal records.
Stephan
On 3 May 2023, at 19:30, Sara Zain <sara...@xxxxxxxxxxxxx> wrote:
If I type "Sequences" then I have the following error:<Screenshot from 2023-05-03 19-28-42.png>
On Wednesday, May 3, 2023 at 7:15:01 PM UTC+2 Markus Kuppe wrote:
Typo: "Sequences"
> On May 3, 2023, at 10:12 AM, Sara Zain <sara...@xxxxxxxxxxxxx> wrote:
>
> Hi!
> I am learning this tool, and I want to know why I often get the following error. Please help!
> Thanks.
--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ec8ffa18-1e0f-4a9c-99b7-8903b373e97bn%40googlegroups.com.
<Screenshot from 2023-05-03 19-28-42.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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/79cf4724-e551-4042-84c8-c897f58ca630n%40googlegroups.com.