Resource sharing with failure

In this  model of resource sharing, the system may fall down. Each client has an additional state fail, and can go to this state via a synchronized transition from both states sleepingand using. The event $event_f$ corresponds to a failure of the system. The occurence of the event $event_r$means that the system has been repaired, and then all the clients are back in state sleeping.

An additional automaton represents the state of the system, it can be failure or active. Transitions from one state to another occur with $event_f$ and $event_r$.

This model, which we shall call Mutex3, is graphically illustrated in Figure. 

In this case, all client automata are symmetrical, so we can aggregate them even if there is some synchronizing events.

The textual .san  files describing this model are:

a.  RS-failure 

 

Figure 1: Resource Sharing Model with failure - Mutex3