|Hi Abel and Igor,|
you can also try using our ProB validation tool.
It can handle Addition2.tla that Igor sent. It can also deal with the commented out version of the existential quantifier without filter set:
\E m \in (msgs \intersect ServerMsgs); see the screenshot below.
(Note: The orange infinity symbol states that not all transitions for ClientSend were computed due to an unbounded quantification.)
ProB, however, requires that its type inference can infer a type for all variables.
The original Addition.tla from Abel raises a type error.
The TLA mode would also benefit from making it more accessible to persons not familier with B (the TLA models are translated to the
B language, and this shines through in various places in the tool).
On 4 Feb 2020, at 16:13, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
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/631B29BF-F81D-45ED-99FC-F0DECD64A141%40gmail.com.