Skip to main content

TP1: Modeling with Automata

Table of Contents
Model-Checking - This article is part of a series.
Part 1: This Article

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
After changing, he frees the cabin and basket.LB: Leave Basket
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.

a
a
e
e
b
b
f
f
g
g
h
h
c
c
d
d

#idlw
0a0
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

Model-Checking - This article is part of a series.
Part 1: This Article