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

*From*: Andrew Samokish <asam.mail@xxxxxxxxx>*Date*: Sun, 10 Sep 2023 06:42:07 -0700 (PDT)*References*: <ea6c08df-da01-40bc-8e2e-4dce8e3c882bn@googlegroups.com> <CAJ-b8swgbBSF8np207q6spsLEVbye0sqVz=BPkZZ3WWJcnz4VA@mail.gmail.com>

Thank you very much! this description is enough for me )

Sincerely yours, Andrew

воскресенье, 10 сентября 2023 г. в 09:57:31 UTC+2, Hillel Wayne:

Hi Andrew,I don't know what's going wrong for certain, but here are two fixes that both by themselves work:- writing `p3' \in 0..97` instead of `0..100`- adding the flag `-maxSetSize 1030301`. `-maxSetSize 1030300` doesnotwork.Given this behavior, my best hypothesis is that TLC doesn't like it when a state generates more next states than can fit into maxSetSize. By default the maxSetSize is 1 million. Without p3, p1' and p2' combinatorically generate 10201 states; floor(1e6 / 10201) = 98 = Cardinality(0..97).HOn Sun, Sep 10, 2023 at 12:43 AM Andrew Samokish <asam...@xxxxxxxxx> wrote:Hello everyone,I`m making first steps with TLA and wrote a simple program, supposed to find some numbers with the given logic (i.e. x1 > x2, x = 5). I did setup it in such way: each step it expects 'random' value in variables the way numbers are choosen supposed to be improved later. The problem is: when (in next) I do set p3' \in 0..100 model checker answers that invariant is violated even before the init step. but when i do set something like p3' = 0 - it works. Program works with two variables without problems. Can you please help me? Seems question is trivial, but still not clear to me :(. here is my code:EXTENDS Naturals

VARIABLES p1, p2, p3

TypeOK == /\ p1 \in 0..100

/\ p2 \in 0..100

/\ p3 \in 0..100

Init == /\ p1 = 0

/\ p2 = 0

/\ p3 = 0

x1 == /\ p1' \in 0..100

/\ p2' \in 0..100

/\ p3' \in 0..100

Next == x1

Spec == Init /\ [][Next]_<<p1, p2, p3>>

NotSolved == ~( /\ p1 > p2 + 10

/\ p2 = 10)--

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/ea6c08df-da01-40bc-8e2e-4dce8e3c882bn%40googlegroups.com.

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/815daec2-6ab6-4c13-bd19-d3854ef29181n%40googlegroups.com.

**References**:**[tlaplus] question about invariant and random numbers***From:*Andrew Samokish

**Re: [tlaplus] question about invariant and random numbers***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] Interactive exploration of the TLC state graph?** - Next by Date:
**[tlaplus] A CHOOSE+TLC conundrum** - Previous by thread:
**Re: [tlaplus] question about invariant and random numbers** - Next by thread:
**[tlaplus] A CHOOSE+TLC conundrum** - Index(es):