TReX's Examples

Description of the example

Fischer's algorithm is a timed mutual exclusion algorithm. It allows n timed processes (identical up to renaming) to access in mutual exclusion a shared ressource.
The algorithm uses a shared variable id ranging from 0 to n saying which process (indexed from 1 to n) requested access to the shared ressource. If id is 0, it means that no process wants this ressource. When a process i wants the shared ressource, it tests the shared variable id. If id= 0, in the next D time units it sets id to its identifier, i.e., i. Then, it waits at least T time units before testing again id. If id is not equal to its identifier i (meaning that another process has requested access) then process i retries later. Otherwise, it enters in the critical section.
The algorithm is parameterized by the two real parameters D and T corresponding to the waiting times.

The following figure represents the timed automaton for process i. Each process has its own clock xi to model the waiting intervals.

Experimental results

TReX allows us to obtain two kind of results:
• Generate automatically the constraint between the parameters D and T such that the algorithm satisfies the mutual exclusion (safety) property.
For this, we compute with TReX the reachable configurations set and the symbolic graph of the system with 2 (fischer_22.scf, fischer_22.aut) and 3 processes when the initial constraint on parameters is the most general one D > 0 and T > 0. We obtain that the state cs1 cs2 is reached (so the mutual exclusion property is not verified) when T < D. We infer that the necessary constraint on parameters to obtain mutual exclusion is : T >= D.
• Verify the constraint obtained above as being sufficient.
For this, we compute with TReX the reachable configurations set when the initial constraint on parameters is T >= D. The results obtained for the system with 2 (fischer_21.scf, fischer_21.aut) and 3 (fischer_31.scf, fischer_31.aut) processes, show that the mutual exclusion property is satisfied (states of the form csi * csj are not reached).