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