Hardware Reference
In-Depth Information
17.2. Wolf-Goat-Cabbage
The problem is to find a strategy to transport across a river by boat, three items
(wolf, goat, cabbage), without having one of them eat another in the process (wolf
eats goat or goat eats cabbage if the boatman is absent). The boat can hold only one
item in addition to the boatman, thus leaving the other two on a shore unsupervised.
We must not leave (wolf, goat) or (goat, cabbage) on the same shore alone. The
fixed part,
fixed.mv
, is a finite-state machine that describes the dynamics of a
boat going back and forth across the river; it has an input
in
from the controller
(finite state machine implementing the winning strategy) and issues an output
out
to
the controller. The input
in
decides which item is loaded in the boat on the next trip,
and it has 4 possible values,
f
empty, wolf, goat, cabbage
g
. The output
out
describes
the state of the systems as follows:
out = notOK
if it enters a bad state, e.g., wolf
and goat are left together on the same bank; if the state is such that all three objects
are on the opposite shore,
out = done
;otherwise
out = OK
.
The specification
spec.aut
follows:
# 00 = null, 10 = OK, 01 = notOK, 11 = done
.i 2
.o 0
.s 3
.p 5
.ilb out_0 out_1
.ob
.accepting a c
-0aa
01ab
11ac
--bb
--cc
.e
(a) Design the automaton that encodes the fixed part of the Wolf-Goat-Cabbage
game and describe it in the format
BLIF-MV
for BALM.
(b) The script
solve script
to synthesize the winning strategy follows:
rl fixed.mv
io_encode
stg_extract fixed.kiss
read_fsm fixed.kiss fixed.aut
determinize -lc spec.aut spec_det.aut
complement spec_det.aut spec_det_compl.aut
support in_0,in_1,out_0,out_1 spec_det_compl.aut spec_det_compl
_supp.aut
support in_0,in_1,out_0,out_1 fixed.aut fixed_supp.aut
product -l fixed_supp.aut spec_det_compl_supp.aut p.aut
support out_0,out_1,in_0,in_1 p.aut p_supp.aut
determinize -lc p_supp.aut p_det_com.aut
complement p_det_com.aut p_det_com_compl.aut
progressive -i 2 p_det_com_compl.aut x.aut
write_fsm -i 2 x.aut x.kiss2
dot x.aut x.dot
Search WWH ::
Custom Search