# Generated by jabuti 0.4.2 (compiled Mar  1 2006 at 22:07:09)
# ../../src/jabuti --rrbb 3 --acm
# Wed Mar  1 22:11:36 2006
# 24 states -- 42 arcs
.model ACM
.internal writer.wrCH_2 reader.rdCH_1 writer.wrCH_0 reader.rdCH_2 writer.wrCH_1 reader.rdCH_0
.outputs reader.m01 writer.l20 reader.m11 reader.m12 writer.l01 reader.m22 reader.m20 writer.l12 reader.m00
.process 0 writer.wrCH_2 writer.l20 writer.wrCH_0 writer.l01 writer.wrCH_1 writer.l12
.process 1 reader.m01 reader.rdCH_1 reader.m11 reader.m12 reader.rdCH_2 reader.m22 reader.m20 reader.rdCH_0 reader.m00
.state graph # begin state graph
s0 writer.wrCH_2 s1
s0 reader.m01 s2
s1 reader.m01 s3
s2 writer.wrCH_2 s3
s2 reader.rdCH_1 s4
s3 writer.l20 s5
s3 reader.rdCH_1 s6
s4 writer.wrCH_2 s6
s4 reader.m11 s2
s5 writer.wrCH_0 s7
s5 reader.rdCH_1 s8
s6 writer.l20 s8
s6 reader.m11 s3
s7 reader.rdCH_1 s9
s8 writer.wrCH_0 s9
s8 reader.m12 s10
s9 reader.m12 s11
s10 writer.wrCH_0 s11
s10 reader.rdCH_2 s12
s11 writer.l01 s13
s11 reader.rdCH_2 s14
s12 writer.wrCH_0 s14
s12 reader.m22 s10
s13 writer.wrCH_1 s15
s13 reader.rdCH_2 s16
s14 writer.l01 s16
s14 reader.m22 s11
s15 reader.rdCH_2 s17
s16 writer.wrCH_1 s17
s16 reader.m20 s18
s17 reader.m20 s19
s18 writer.wrCH_1 s19
s18 reader.rdCH_0 s20
s19 writer.l12 s21
s19 reader.rdCH_0 s22
s20 writer.wrCH_1 s22
s20 reader.m00 s18
s21 writer.wrCH_2 s23
s21 reader.rdCH_0 s0
s22 writer.l12 s0
s22 reader.m00 s19
s23 reader.rdCH_0 s1
.marking{s0}
.end # end state graph
