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

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

• From: Igor Konnov <igor.konnov@xxxxxxxxx>
• Date: Thu, 15 Apr 2021 18:00:47 +0200
• Cc: Igor Konnov <igor.konnov@xxxxxxxxx>
• Ironport-hdrordr: A9a23:pd2F6Kqo9qphDoSXLMCPRXoaV5vtLNV00zAX/kB9WHVpW+SFisGjm+ka3xfoiDAXHEotg8yEJbPoewK4ybde6+AqTPSfdSPhv3alK5wnyIPkzSHpFSGWzJ8p6Y5Lda9iBNrsSWVrlMqS2nj7L/8M4vmitJqpi+DX0mt3QWhRAcAQljtRJw6HHiRNNXd7LLc0EZqC6tFKqn6cfx0sH6eGL1UfRO7ZvZn3kvvdEFs7LjE97g3mt0Lo1JfeEwKEmj8EWTJO3rtKyxmJryXd5r+/99C2zwa07R6d071ymMH9jvtPbfb8wfQ9DzX3l0KQYp59Mofy8AwdheG09RIRjNLXqQwhNMgb0QKeQkiRoQHxnzXmyiok8XX4yVSV6EGT6/DRYBIfJ45/iZlCch3fgnBQzO1U9K5QxWqWu952IHr77VXAzuHSWxtnm0ayq3ZKq59as1VlXYETaKBcoOUklSs/fuZjbUWKjvFaLMBUAMvR5OlbfBehVl+xhBgK/PWWUm03DlO6RCE5y4yo+gJbm3101CIjtYgit00d/5EwQYQs3ZWyDo1UlapDRsJTTaVxCPZpe7rENkXxR3v3QR2vCGWiP60KPE/Np4X6iY9Fkt2CSdgnyN8XlI7aWF1V8VQuc1/jYPf+p6Fjw1TiRmOyWDio5+N/w9xCurP6TKf2KiHrciFXr+KQ59sYBMPfV7KIPI9OR8XkMXDlFe9yrnfDcqgXDXEfVcEP0+xLKG6mk4buIo3usuTdNMneP6DsFzFMYBK3PlIzGB7pJMtB6UivHkL/6SKwZ1rdPnfy955xD6TWltJjtbQlB8l3qwAQzX656suIJSYHjaAsZkt5J9rc/5+TlC2N5G7Nq0BkJRZZZ3w43JzQF0lSrQtPCV79bKoY0u/xRUlXxnufEBp2RM/SCmdk1iBKxZ4=
• References: <68d2e11a-0ca9-43a3-bb0a-8d6051d6c4d8n@googlegroups.com>

Hi Edi,

You could try Apalache: https://apalache.informal.systems/

However, if you have 1000 elements, your specification is probably large as well. It’s hard to tell without seeing your TLA+ specification. Usually, one has to apply abstraction to deal with very large state spaces and specs.

Best regards,
Igor

> On 15.04.2021, at 17:08, Eduard Laitin <laitineduard@xxxxxxxxx> wrote:
>
> Hello,
>
> 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,
> Edi
>
> --
> 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.

--
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/8EA9D430-1FDB-4B93-B502-09A3BC46C0DB%40gmail.com.