 # TReX's Examples

## Fischer's Algorithm ## 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).