I imagine you'd like to write something like
Next == \E ids \in SUBSET TaskID : \A id \in ids : Task(id)
In practice, this is not going to work, in particular because your state variables are probably arrays and the definition of Task contains expressions of the form
var' = [var EXCEPT ![id] = ...]
You can try to work around this problem by writing
var[id]' = ...
in the definition of Task and defining
/\ var' \in [TaskID -> ...]
/\ \E ids \in SUBSET TaskID :
/\ \A id \in ids : Task(id)
/\ \A id \in TaskID \ ids : UNCHANGED var[id]
but TLC will not handle that very well because it will generate all possible type-correct values for var' and then reduce those to the few successor values that are actually possible. Perhaps Apalache would be able to handle such definitions better because it doesn't explicitly construct states one by one. If you are mainly interested in verification using TLC, I think that your solution will work best.
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/1CA0FF7C-2326-4717-A34B-535D2E6938FB%40gmail.com.