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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 26 Aug 2019 17:43:41 +0200*References*: <1daed939-2987-4871-a059-9c223d0dd1a3@googlegroups.com>

Hello, you have not shown what the status of identifier Oid is. TLC can only evaluate quantification over finite constant sets [1]. If you have a constant parameter Oid that represents (a superset of) all potential object identifiers [2] then your first formulation \A oid \in Oid, r \in Replica: oid \in doset[r] ~> (\A s \in Replica : oid \in uset[s]) should be fine since both Replica and Oid will be instantiated by finite sets in your model. The second formulation [](\A r \in Replica: \A oid \in doset[r]:<>(\A s \in Replica: oid \in uset[s])) cannot be evaluated because the range of the second quantifier `doset[r]' is not a constant set. Regards, Stephan [1] Please see section 14.2.4 of Specifying Systems for the precise definition of temporal formulas that TLC can handle. [2] Since you can only submit finite instances to TLC anyway, you must have bounded this set for model checking. This will probably mean that at some point no new object ID is available and the action that introduces new IDs will be disabled.
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/F8997554-7C5B-4D00-807E-D162C74AFBD1%40gmail.com. |

**References**:

- Prev by Date:
**[tlaplus] How to express liveness in my spec?Why TLC cannot handle this temporal formula?** - Next by Date:
**[tlaplus] Scaling up model checking** - Previous by thread:
**[tlaplus] How to express liveness in my spec?Why TLC cannot handle this temporal formula?** - Next by thread:
**[tlaplus] Scaling up model checking** - Index(es):