Equations Over Languages and Finite Automata - The Unknown Component Problem: Theory and Applications - page 29

The automaton is incomplete (3 states) and deterministic.
3 inputs 3 states 7 transitions
Inputs = { v1, v2, colours(3) }

0 - r

1

1 - g 1 0 y

0 0 g 1 1 y

2

- 1 g

0 1 g

3

Fig. 2.10 Graphical output of BALM showing the automaton traffic-ma.aut describing the
fixed automaton component of the traffic light controller problem. The notation of BALM will be
presented formally later on, but this graph can be read as any usual FSM graphical representation

The automaton is incomplete (4 states) and deterministic.
3 inputs 4 states 7 transitions
Inputs = { i1(3), i2(3), colours(3) }

- 2 r
(0,1) (1,2) r
0 - r

a

(1,2) 0 g
2 (0,1) g

- - y

- (1,2) y

b

- (1,2) g - 0 g

- 0 g

c d

Fig. 2.11 Graphical output of BALM showing the automaton traffic-mc.aut describing the
specification automaton of the traffic light controller problem

f . v 1 o1; s1; s 2/, . v 2 o2; s1; s1/, . v 1 o2; s2; s1/, . v 2 o1; s 2 ; s 2/, r A D s1,and
S C D Q C Df sa; sb; sc g , ˙ C D I O, C Df .i1 o1; s a; s b /, .i 2 o2; sa; sc/,
.i 2 o2; sb; sa/, .i1 02; sb; sc/ g , .i1 o1; s c ; s a/, .i 2 o1; s c ; s b /, r C

D sa.

Compute the largest solution of the equation A X C ,whereX has inputs

I V O.
Verify whether in this example of controller's topology the composition of the
largest solution with M A is progressive.