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

[tlaplus] How to check properties on models with huge numbers of behaviours


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)

Thank you,

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/68d2e11a-0ca9-43a3-bb0a-8d6051d6c4d8n%40googlegroups.com.