Hardware Reference
In-Depth Information
Cat
Mouse
c
3
2
0
m
4
4
m
1
c
4
c
6
m
5
c
1
m
2
c
2
m
3
m
6
c
5
c
7
1
3
Fig. 15.7
Maze for cat and mouse for Example
15.22
by the cat (door of type
m
j
). Cat
and mouse can be modeled each by an automaton whose states are the rooms, and
whose transitions represent moving from one room to the other. The automaton
in Fig.
15.8
is obtained by the intersection of the automata of the cat and mouse,
assuming that initially the cat is in room 2 and the mouse is in room 4; each state of
the composed automaton corresponds to the pair of rooms
c
i
) or exclusively by the mouse (door of type
.r
c
;r
m
/
,where
r
c
is the
current room of the cat and
r
m
is the current room of the mouse; there is a transition
.r
c
;r
m
/
.r
c
;r
0
m
/
from state
.r
c
;r
m
/
to state
(state
) under
c
i
(
m
j
) if the cat (mouse)
r
c
r
0
m
crosses door
). Notice that we did not draw the whole
automaton for lack of space, however what is shown is sufficient to understand the
trimming procedure below. All doors can be open or closed, except the bidirectional
door
c
i
(
m
j
)togotoroom
(
c
7
is uncontrollable while all the other doors are
controllable. The goal is to design a controller that allows the maximal freedom to
the cat and mouse while satisfying the following two properties:
c
7
that is always open, i.e.,
1. The cat and mouse never occupy the same room at the same time.
2. It is always possible for the cat and mouse to return to the initial state
.2; 4/
.
The controller can be obtained by an iteration of trimming steps on the maze
automaton, until nothing changes. Initially the maze automaton is intersected with
the automaton representing the specifications of the system (no cat and mouse in
the same room, and existence of a path to the initial state). The result is that all
states with the cat and mouse in the same room are deleted (states (0,0), (1,1), (2,2),
(3,3), (4,4)); no state is deleted initially due to inability to reach the initial state.
In general, deleting a state requires also deleting all transitions from it. Once the
initial trimming step has been performed, the following step is iterated:
•
If an uncontrollable transition has been deleted from a state (because directed to
a deleted state), delete that state and all transitions from it.
Search WWH ::
Custom Search