Unknown Location Error

[Sara Zain]

Hi!

I am learning this tool, and I want to know why I often get the following error. Please help!

Thanks.

[Markus Kuppe]

Typo: "Sequences"

[Sara Zain]

If I type "Sequences" then I have the following error:

[Stephan Merz]

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...@tu-dresden.de> 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...@tu-dresden.de> 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...@googlegroups.com.
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>

[Rosalie Defourné]

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.

[Sara Zain]

Thanks! yeah fixed the empty sequence too. 
However, does anyone know why there is this error now? 

Thanks in advance. 

[Hillel Wayne]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/79cf4724-e551-4042-84c8-c897f58ca630n%40googlegroups.com.

[Sara Zain]

Hi,

So basically, I can't run TLC on the model. These are the following errors. 

Provide a value for constant MAX_RECORDS.

Next: The Next formula must be provided. 

Thanks.

Sara

[Martin]

Hello!

There's a box to the middle-right with MAX_RECORDS <- where you can enter the
initial value for max records. If you are working on a temporal specification,
you would have an Init and Next predicate, although differently named? The drop
down menu also allwos you to pick a whole temporal formula as behaviour
specification or - in the case that you are only checking a constant expression
- lets you disable the specification formula completely.

cheers,
Martin

On 5/5/23 12:17, Sara Zain wrote:
> Hi,
> So basically, I can't run TLC on the model. These are the following errors.
> Provide a value for constant MAX_RECORDS.
> Next: The Next formula must be provided.
> Thanks.
>
> Sara

> Screenshot from 2023-05-05 12-05-29.png
>
>
> On Thursday, May 4, 2023 at 6:53:30 PM UTC+2 Hillel Wayne wrote:
>
> 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:

>> Screenshot from 2023-05-04 17-13-24.pngThanks! yeah fixed the empty

>>> https://groups.google.com/d/msgid/tlaplus/ec8ffa18-1e0f-4a9c-99b7-8903b373e97bn%40googlegroups.com <https://groups.google.com/d/msgid/tlaplus/ec8ffa18-1e0f-4a9c-99b7-8903b373e97bn%40googlegroups.com?utm_medium=email&utm_source=footer>.

>>> <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...@googlegroups.com.
>> To view this discussion on the web visit

>> https://groups.google.com/d/msgid/tlaplus/79cf4724-e551-4042-84c8-c897f58ca630n%40googlegroups.com <https://groups.google.com/d/msgid/tlaplus/79cf4724-e551-4042-84c8-c897f58ca630n%40googlegroups.com?utm_medium=email&utm_source=footer>.

>
> --
> 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...@googlegroups.com

> <mailto:tlaplus+u...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/tlaplus/35c2f6ed-5d8a-474a-97e3-1f06a2ac6f1cn%40googlegroups.com <https://groups.google.com/d/msgid/tlaplus/35c2f6ed-5d8a-474a-97e3-1f06a2ac6f1cn%40googlegroups.com?utm_medium=email&utm_source=footer>.