[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: How to check properties on models with huge numbers of behaviours
- From: Leslie Lamport <tlaplus.ll@xxxxxxxxx>
- Date: Thu, 15 Apr 2021 09:45:53 -0700 (PDT)
- Ironport-hdrordr: A9a23:gqzvjKC4OMLZLlrlHejYsceALOonbusQ8zAX/mp2TgFYddHdqtC2kJ0gpGfJoRsyeFVlo9CPP6GcXWjRnKQe3aA9NaqvNTOHhEKGII1u5oPpwXnBNkTFh4xg/Ih6dawWMqyXMXFfreLXpDa1CMwhxt7vys6VrMPT1W1kQw0vS4wI1XYcNi+hHkd7RBZLCPMCffL22uN8uzGidX4LB/7LYUUtYu6rnayzqLvWJTYNDRg67xTLqjW06LH7GRCE3hEYFw5e2LtKyxmnryXJooum99W20AXV2WOW1YlfhdeJ8Ld+Lf3JpM4SJDDhziuLRKAkYb2NuzgpvPqigWxGrPD85zknOcp35zfqenyt5SHqxxLr3F8VhEPK+Bu+h2birszyTC87Dc1a7LgpFyfx2g4asNtx0L1G0gui1qZqMQ==
- References: <firstname.lastname@example.org>
While large sets can cause performance problems, it's rare for an algorithm to be correct for a set of 3 elements and not for a set of 1000 elements.
On Thursday, April 15, 2021 at 8:08:15 AM UTC-7 laitin...@xxxxxxxxx wrote:
In my specification at each Next step I have something like:
\E i \in Set where the set can have up to 1000 elements (no symmetry)
This causes a lot of branching so there are too many states for the model checker to find even if I let it run for years.
Is there any TLA+/TLC trick to solve this? If not do you know any model checker that could handle this? (l have heard about translating TLA+ to B to check with ProB but I'm not sure if it would help)
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/050ab4bd-26f7-4594-ba25-dc5d8d4fa291n%40googlegroups.com.