[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Unknown Location Error

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
    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 <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...@xxxxxxxxxxxxxxxx.
    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+unsubscribe@xxxxxxxxxxxxxxxx <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. 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>. 

--
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/2e1ba102-ba7f-004f-71db-a0c0683752e0%40gmail.com.