# Generated by jabuti 0.4.2 (compiled Mar  1 2006 at 22:07:09)
# ../../src/jabuti --rrbb 4 --acm
# Wed Mar  1 22:11:36 2006
# 48 states -- 88 arcs
.model ACM
.internal writer.wrCH_3 reader.rdCH_1 writer.wrCH_0 reader.rdCH_2 writer.wrCH_1 reader.rdCH_3 writer.wrCH_2 reader.rdCH_0
.outputs reader.m01 writer.l30 reader.m12 reader.m22 writer.l01 reader.m23 reader.m33 writer.l12 reader.m30 reader.m00 writer.l23 reader.m11
.process 0 writer.wrCH_3 writer.l30 writer.wrCH_0 writer.l01 writer.wrCH_1 writer.l12 writer.wrCH_2 writer.l23
.process 1 reader.m01 reader.rdCH_1 reader.m12 reader.rdCH_2 reader.m22 reader.m23 reader.rdCH_3 reader.m33 reader.m30 reader.rdCH_0 reader.m00 reader.m11
.state graph # begin state graph
s0 writer.wrCH_3 s1
s0 reader.m01 s2
s1 reader.m01 s3
s2 writer.wrCH_3 s3
s2 reader.rdCH_1 s4
s3 writer.l30 s5
s3 reader.rdCH_1 s6
s4 writer.wrCH_3 s6
s4 reader.m12 s7
s5 writer.wrCH_0 s8
s5 reader.rdCH_1 s9
s6 writer.l30 s9
s6 reader.m12 s10
s7 writer.wrCH_3 s10
s7 reader.rdCH_2 s11
s8 reader.rdCH_1 s12
s9 writer.wrCH_0 s12
s9 reader.m12 s13
s10 writer.l30 s13
s10 reader.rdCH_2 s14
s11 writer.wrCH_3 s14
s11 reader.m22 s7
s12 reader.m12 s15
s13 writer.wrCH_0 s15
s13 reader.rdCH_2 s16
s14 writer.l30 s16
s14 reader.m22 s10
s15 writer.l01 s17
s15 reader.rdCH_2 s18
s16 writer.wrCH_0 s18
s16 reader.m23 s19
s17 writer.wrCH_1 s20
s17 reader.rdCH_2 s21
s18 writer.l01 s21
s18 reader.m23 s22
s19 writer.wrCH_0 s22
s19 reader.rdCH_3 s23
s20 reader.rdCH_2 s24
s21 writer.wrCH_1 s24
s21 reader.m23 s25
s22 writer.l01 s25
s22 reader.rdCH_3 s26
s23 writer.wrCH_0 s26
s23 reader.m33 s19
s24 reader.m23 s27
s25 writer.wrCH_1 s27
s25 reader.rdCH_3 s28
s26 writer.l01 s28
s26 reader.m33 s22
s27 writer.l12 s29
s27 reader.rdCH_3 s30
s28 writer.wrCH_1 s30
s28 reader.m30 s31
s29 writer.wrCH_2 s32
s29 reader.rdCH_3 s33
s30 writer.l12 s33
s30 reader.m30 s34
s31 writer.wrCH_1 s34
s31 reader.rdCH_0 s35
s32 reader.rdCH_3 s36
s33 writer.wrCH_2 s36
s33 reader.m30 s37
s34 writer.l12 s37
s34 reader.rdCH_0 s38
s35 writer.wrCH_1 s38
s35 reader.m00 s31
s36 reader.m30 s39
s37 writer.wrCH_2 s39
s37 reader.rdCH_0 s40
s38 writer.l12 s40
s38 reader.m00 s34
s39 writer.l23 s41
s39 reader.rdCH_0 s42
s40 writer.wrCH_2 s42
s40 reader.m01 s43
s41 writer.wrCH_3 s44
s41 reader.rdCH_0 s0
s42 writer.l23 s0
s42 reader.m01 s45
s43 writer.wrCH_2 s45
s43 reader.rdCH_1 s46
s44 reader.rdCH_0 s1
s45 writer.l23 s2
s45 reader.rdCH_1 s47
s46 writer.wrCH_2 s47
s46 reader.m11 s43
s47 writer.l23 s4
s47 reader.m11 s45
.marking{s0}
.end # end state graph
