Spec describing simultaneity of events

[Mariusz Ryndzionek]

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

[Stephan Merz]

Hi Mariusz,

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

Next ==

  /\ 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.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/aaef82d5-f62e-4e50-b87c-15aad19c6cc9n%40googlegroups.com.

[Mariusz Ryndzionek]

Thanks Stephan. Your suggestions are very interesting.

I would definitely not think about such solutions and they might be useful in other situations.

[Leslie Lamport]

Something TLC can handle more easily and may work for your example is:

   \E ids \in SUBSET TaskID :

     var' = [id \in TaskID |-> IF id \in ids THEN ... ELSE var[id]]

[Mariusz Ryndzionek]

Thanks Leslie. Yes, I would like to check with TLC, so I'll use this.