1
00:00:00,160 --> 00:00:02,320
The model that we will consider, is a very well

2
00:00:02,320 --> 00:00:05,330
known one. Which is finite state machines. And you might have

3
00:00:05,330 --> 00:00:08,320
seen them before. At a high level, a state machine is

4
00:00:08,320 --> 00:00:11,990
a graph in which nodes represent states of the system. For

5
00:00:11,990 --> 00:00:15,650
example, in this case, state 1, state 2, and state 3.

6
00:00:15,650 --> 00:00:19,950
Edges represent transitions between states. For instance, in this case we

7
00:00:19,950 --> 00:00:22,850
have one edge from state 1, to state 2. That means

8
00:00:22,850 --> 00:00:25,640
that the system can go from state 1, to state 2.

9
00:00:25,640 --> 00:00:29,530
And finally, the labels on the edges represent events

10
00:00:29,530 --> 00:00:32,800
and actions. For example, what this label means is that

11
00:00:32,800 --> 00:00:35,400
the system goes from state three to state two

12
00:00:35,400 --> 00:00:39,140
when event five occurs. And when going from state three

13
00:00:39,140 --> 00:00:42,190
to state two, it generates action four. And does

14
00:00:42,190 --> 00:00:45,430
reacher model, sir reacher's kind of state machines, but we're

15
00:00:45,430 --> 00:00:48,160
just going to stick to this ones which are enough. For

16
00:00:48,160 --> 00:00:50,760
our purpose. So how do we build such a final

17
00:00:50,760 --> 00:00:53,530
state machine starting from a specification? The first thing

18
00:00:53,530 --> 00:00:56,660
we need to do is to identify the system's boundaries

19
00:00:56,660 --> 00:00:59,250
and the input and output to the system. Once we

20
00:00:59,250 --> 00:01:01,960
have done that, we can identify, within the boundaries of

21
00:01:01,960 --> 00:01:06,070
the system, the relevant states and transitions. So we split

22
00:01:06,070 --> 00:01:09,670
this single state We'll refine it into several states. And

23
00:01:09,670 --> 00:01:12,640
we also identify how the system can go from one

24
00:01:12,640 --> 00:01:16,830
state to another. Including which inputs cause which transition, and

25
00:01:16,830 --> 00:01:19,350
which result in outputs we can obtain. To

26
00:01:19,350 --> 00:01:21,810
better illustrate that, let's look at a concrete example.