[tlaplus] Spec describing simultaneity of events

[Mariusz Ryndzionek <mryndzionek@xxxxxxxxx>]

I'm writing a simple spec for a task scheduler. Most of the spec I've seen do something like this:

Task(task_id) == /* handles one task at a time

Next == \E task_id \in TaskID : Task(task_id) ...

This models/describes a situation where each task gets activatedbone at a time. I would like to model a situation where any combination of tasks can become active at any instant. Something like this seems to work:

Tasks(task_ids) == /* handles multiple tasks at a time

Next == \E task_ids \in SUBSET TaskID \ {{}} : Tasks(task_ids)

However is there a maybe another way to accomplish this? Preferably a way that would not require to turn Task(taks_id) into Tasks(task_ids).

Regards,

Mariusz

-- 
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/aaef82d5-f62e-4e50-b87c-15aad19c6cc9n%40googlegroups.com.