1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
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.
|
