TP1: Modeling with Automata
Exercise 1. Modeling
Model the operations in a swimming pool using an automaton
A swimming pool comprises 𝑐 cabins to change and 𝑝 baskets to deposit clothes.
A user can enter the pool only if a cabin is free.
Once he has a cabin, he has to wait for a basket to change and deposit his clothes.
Then it releases the cabin and enter the swimming pool.
He can leave only if a cabin is free.
After changing, he frees the cabin and basket.
Finally, he leaves the pool.
Model the operations in a swimming pool, using an automaton, in the case where there is only one basket. You can use the actions described in the table below.
|A user can enter the pool only if a cabin is free.||TC: Take Cabin|
|Once he has a cabin, he has to wait for a basket to change and deposit his clothes.||TB: Take Basket|
|Then it releases the cabin and enter the swimming pool.||ES: Enter Basin|
|He can leave only if a cabin is free.||LS: Leave Basin|
|After changing, he frees the cabin and basket.||LB: Leave Basket|
|Finally, he leaves the pool.||EXIT: exit pool|
Model the swimming pool with 1 cabin and 2 baskets.
Try with $𝑐=2$ cabins and $𝑝=2$ baskets. (Do not make it completely.) Would you model the system with 5 cabins and 8 baskets?
Exercise 2. SCC
Compute the DFS order and the SCC for the following graph.
Exercise 3. Synthesis
Find an example of system (a graph) with two actions, 𝑎 and 𝑏, where 𝑎 is quasi live and 𝑏 is live