# TP1: Modeling with Automata

## Exercise 1. Modeling

Model the operations in a swimming pool using an automaton

1. A swimming pool comprises 𝑐 cabins to change and 𝑝 baskets to deposit clothes.

2. A user can enter the pool only if a cabin is free.

3. Once he has a cabin, he has to wait for a basket to change and deposit his clothes.

4. Then it releases the cabin and enter the swimming pool.

5. He can leave only if a cabin is free.

6. After changing, he frees the cabin and basket.

7. Finally, he leaves the pool.

### Question 1

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
Finally, he leaves the pool. EXIT: exit pool

### Question 2

Model the swimming pool with 1 cabin and 2 baskets.

### Question 3

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.

# id lw
0 a 0
1
2
3
4
5
6
7

## Exercise 3. Synthesis

Find an example of system (a graph) with two actions, 𝑎 and 𝑏, where 𝑎 is quasi live and 𝑏 is live