# Generated by jabuti 0.4.2 (compiled Mar  1 2006 at 22:07:09)
# ../../src/jabuti --rrbb 5 --acm
# Wed Mar  1 22:11:37 2006
# 80 states -- 150 arcs
.model ACM
.internal writer.wrCH_4 reader.rdCH_1 writer.wrCH_0 reader.rdCH_2 reader.rdCH_3 writer.wrCH_1 reader.rdCH_4 writer.wrCH_2 reader.rdCH_0 writer.wrCH_3
.outputs reader.m01 writer.l40 reader.m12 reader.m23 writer.l01 reader.m33 reader.m34 writer.l12 reader.m44 reader.m40 writer.l23 reader.m00 writer.l34 reader.m11 reader.m22
.process 0 writer.wrCH_4 writer.l40 writer.wrCH_0 writer.l01 writer.wrCH_1 writer.l12 writer.wrCH_2 writer.l23 writer.wrCH_3 writer.l34
.process 1 reader.m01 reader.rdCH_1 reader.m12 reader.rdCH_2 reader.m23 reader.rdCH_3 reader.m33 reader.m34 reader.rdCH_4 reader.m44 reader.m40 reader.rdCH_0 reader.m00 reader.m11 reader.m22
.state graph # begin state graph
s0 writer.wrCH_4 s1
s0 reader.m01 s2
s1 reader.m01 s3
s2 writer.wrCH_4 s3
s2 reader.rdCH_1 s4
s3 writer.l40 s5
s3 reader.rdCH_1 s6
s4 writer.wrCH_4 s6
s4 reader.m12 s7
s5 writer.wrCH_0 s8
s5 reader.rdCH_1 s9
s6 writer.l40 s9
s6 reader.m12 s10
s7 writer.wrCH_4 s10
s7 reader.rdCH_2 s11
s8 reader.rdCH_1 s12
s9 writer.wrCH_0 s12
s9 reader.m12 s13
s10 writer.l40 s13
s10 reader.rdCH_2 s14
s11 writer.wrCH_4 s14
s11 reader.m23 s15
s12 reader.m12 s16
s13 writer.wrCH_0 s16
s13 reader.rdCH_2 s17
s14 writer.l40 s17
s14 reader.m23 s18
s15 writer.wrCH_4 s18
s15 reader.rdCH_3 s19
s16 writer.l01 s20
s16 reader.rdCH_2 s21
s17 writer.wrCH_0 s21
s17 reader.m23 s22
s18 writer.l40 s22
s18 reader.rdCH_3 s23
s19 writer.wrCH_4 s23
s19 reader.m33 s15
s20 writer.wrCH_1 s24
s20 reader.rdCH_2 s25
s21 writer.l01 s25
s21 reader.m23 s26
s22 writer.wrCH_0 s26
s22 reader.rdCH_3 s27
s23 writer.l40 s27
s23 reader.m33 s18
s24 reader.rdCH_2 s28
s25 writer.wrCH_1 s28
s25 reader.m23 s29
s26 writer.l01 s29
s26 reader.rdCH_3 s30
s27 writer.wrCH_0 s30
s27 reader.m34 s31
s28 reader.m23 s32
s29 writer.wrCH_1 s32
s29 reader.rdCH_3 s33
s30 writer.l01 s33
s30 reader.m34 s34
s31 writer.wrCH_0 s34
s31 reader.rdCH_4 s35
s32 writer.l12 s36
s32 reader.rdCH_3 s37
s33 writer.wrCH_1 s37
s33 reader.m34 s38
s34 writer.l01 s38
s34 reader.rdCH_4 s39
s35 writer.wrCH_0 s39
s35 reader.m44 s31
s36 writer.wrCH_2 s40
s36 reader.rdCH_3 s41
s37 writer.l12 s41
s37 reader.m34 s42
s38 writer.wrCH_1 s42
s38 reader.rdCH_4 s43
s39 writer.l01 s43
s39 reader.m44 s34
s40 reader.rdCH_3 s44
s41 writer.wrCH_2 s44
s41 reader.m34 s45
s42 writer.l12 s45
s42 reader.rdCH_4 s46
s43 writer.wrCH_1 s46
s43 reader.m40 s47
s44 reader.m34 s48
s45 writer.wrCH_2 s48
s45 reader.rdCH_4 s49
s46 writer.l12 s49
s46 reader.m40 s50
s47 writer.wrCH_1 s50
s47 reader.rdCH_0 s51
s48 writer.l23 s52
s48 reader.rdCH_4 s53
s49 writer.wrCH_2 s53
s49 reader.m40 s54
s50 writer.l12 s54
s50 reader.rdCH_0 s55
s51 writer.wrCH_1 s55
s51 reader.m00 s47
s52 writer.wrCH_3 s56
s52 reader.rdCH_4 s57
s53 writer.l23 s57
s53 reader.m40 s58
s54 writer.wrCH_2 s58
s54 reader.rdCH_0 s59
s55 writer.l12 s59
s55 reader.m00 s50
s56 reader.rdCH_4 s60
s57 writer.wrCH_3 s60
s57 reader.m40 s61
s58 writer.l23 s61
s58 reader.rdCH_0 s62
s59 writer.wrCH_2 s62
s59 reader.m01 s63
s60 reader.m40 s64
s61 writer.wrCH_3 s64
s61 reader.rdCH_0 s65
s62 writer.l23 s65
s62 reader.m01 s66
s63 writer.wrCH_2 s66
s63 reader.rdCH_1 s67
s64 writer.l34 s68
s64 reader.rdCH_0 s69
s65 writer.wrCH_3 s69
s65 reader.m01 s70
s66 writer.l23 s70
s66 reader.rdCH_1 s71
s67 writer.wrCH_2 s71
s67 reader.m11 s63
s68 writer.wrCH_4 s72
s68 reader.rdCH_0 s0
s69 writer.l34 s0
s69 reader.m01 s73
s70 writer.wrCH_3 s73
s70 reader.rdCH_1 s74
s71 writer.l23 s74
s71 reader.m11 s66
s72 reader.rdCH_0 s1
s73 writer.l34 s2
s73 reader.rdCH_1 s75
s74 writer.wrCH_3 s75
s74 reader.m12 s76
s75 writer.l34 s4
s75 reader.m12 s77
s76 writer.wrCH_3 s77
s76 reader.rdCH_2 s78
s77 writer.l34 s7
s77 reader.rdCH_2 s79
s78 writer.wrCH_3 s79
s78 reader.m22 s76
s79 writer.l34 s11
s79 reader.m22 s77
.marking{s0}
.end # end state graph
