// Testfile dumped by Ultimate at 2016/05/17 00:05:25 // Source: fibo_2calls_4_true-unreach-call.c Abstraction3 // NestedWordAutomaton nwa = ( callAlphabet = {c0 c1 c2 c3 c4 }, internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 }, returnAlphabet = {r0 r1 r2 r3 r4 }, states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 s25 s26 s27 s28 s29 s30 s31 s32 s33 s34 s35 s36 s37 s38 s39 s40 s41 s42 s43 s44 s45 s46 s47 s48 s49 s50 s51 s52 s53 s54 s55 s56 s57 s58 s59 s60 s61 s62 s63 s64 s65 s66 s67 s68 s69 s70 s71 s72 s73 s74 s75 s76 s77 s78 s79 s80 s81 s82 s83 s84 s85 s86 s87 s88 s89 s90 s91 s92 s93 s94 s95 s96 s97 s98 s99 s100 s101 s102 s103 s104 s105 s106 s107 s108 s109 s110 s111 s112 s113 s114 s115 s116 s117 s118 s119 s120 s121 s122 s123 s124 s125 s126 s127 s128 s129 s130 s131 s132 s133 s134 s135 s136 s137 s138 s139 s140 s141 s142 s143 s144 s145 s146 s147 s148 s149 s150 s151 s152 s153 s154 s155 s156 s157 s158 s159 s160 s161 s162 s163 s164 s165 s166 s167 s168 s169 s170 s171 s172 s173 s174 s175 s176 s177 s178 }, initialStates = {s48 }, finalStates = {s0 s3 s4 s5 s6 s8 s9 s10 s11 s12 s14 s15 s16 s17 s22 s23 s24 s25 s26 s27 s28 s32 s33 s34 s35 s36 s37 s38 s39 s40 s44 s45 s46 s47 s48 s49 s50 s58 s60 s61 s63 s64 s66 s70 s71 s74 s75 s77 s79 s81 s83 s84 s85 s86 s87 s88 s89 s90 s92 s94 s96 s97 s98 s100 s101 s102 s104 s105 s106 s109 s110 s111 s113 s115 s116 s117 s119 s121 s122 s123 s126 s127 s128 s131 s132 s133 s134 s137 s138 s139 s140 s144 s145 s146 s147 s148 s152 s153 s154 s155 s156 s157 s158 s162 s163 s164 s165 s166 s167 s168 s169 s173 s174 s175 s176 s177 s178 }, callTransitions = { (s0 c3 s140) (s7 c3 s151) (s9 c3 s154) (s12 c3 s91) (s12 c3 s92) (s13 c1 s99) (s15 c1 s101) (s18 c1 s130) (s23 c1 s132) (s47 c3 s140) (s49 c0 s50) (s52 c2 s53) (s55 c4 s56) (s59 c2 s62) (s61 c2 s64) (s68 c4 s56) (s76 c1 s78) (s77 c1 s79) (s82 c4 s56) (s90 c3 s91) (s90 c3 s92) (s95 c2 s99) (s97 c2 s101) (s107 c4 s112) (s107 c4 s113) (s117 c1 s123) (s120 c1 s99) (s121 c1 s123) (s122 c1 s101) (s125 c2 s130) (s127 c2 s132) (s134 c4 s140) (s135 c3 s141) (s137 c3 s144) (s143 c4 s151) (s146 c4 s154) (s157 c2 s123) (s159 c2 s99) (s160 c1 s130) (s163 c2 s101) (s165 c1 s132) (s171 c2 s130) (s176 c2 s132) }, internalTransitions = { (s3 a5 s8) (s6 a3 s10) (s8 a3 s11) (s14 a14 s16) (s16 a9 s17) (s19 a14 s20) (s20 a9 s21) (s22 a14 s24) (s24 a9 s25) (s26 a5 s27) (s27 a3 s28) (s29 a5 s30) (s30 a3 s31) (s32 a5 s33) (s33 a3 s34) (s35 a5 s36) (s36 a3 s37) (s38 a14 s39) (s39 a9 s40) (s41 a14 s42) (s42 a9 s43) (s44 a14 s45) (s45 a9 s46) (s48 a10 s49) (s50 a7 s51) (s51 a13 s52) (s53 a1 s54) (s54 a4 s55) (s56 a7 s57) (s56 a7 s58) (s57 a13 s59) (s58 a8 s60) (s58 a13 s61) (s60 a9 s63) (s62 a1 s65) (s64 a1 s66) (s65 a2 s67) (s65 a4 s68) (s65 a6 s69) (s66 a2 s70) (s66 a6 s71) (s67 a3 s72) (s69 a3 s73) (s70 a3 s74) (s71 a3 s75) (s78 a1 s80) (s79 a1 s81) (s80 a4 s82) (s81 a2 s83) (s81 a6 s84) (s83 a3 s85) (s84 a3 s86) (s87 a14 s88) (s88 a9 s89) (s91 a7 s93) (s92 a7 s94) (s93 a13 s95) (s94 a8 s96) (s94 a13 s97) (s94 a16 s98) (s96 a9 s100) (s98 a9 s102) (s99 a1 s103) (s101 a1 s105) (s103 a2 s106) (s103 a4 s107) (s103 a6 s108) (s104 a5 s109) (s105 a6 s110) (s106 a3 s111) (s108 a3 s114) (s109 a3 s115) (s110 a3 s116) (s112 a7 s118) (s113 a7 s119) (s118 a8 s124) (s118 a13 s125) (s119 a8 s126) (s119 a13 s127) (s123 a1 s128) (s124 a9 s129) (s126 a9 s131) (s128 a2 s133) (s128 a4 s134) (s128 a6 s133) (s130 a1 s136) (s132 a1 s138) (s133 a3 s139) (s136 a2 s142) (s136 a4 s143) (s136 a6 s142) (s138 a2 s145) (s138 a4 s146) (s138 a6 s145) (s140 a7 s148) (s141 a7 s149) (s142 a3 s150) (s144 a7 s152) (s145 a3 s153) (s147 a14 s155) (s148 a8 s156) (s148 a13 s157) (s148 a16 s158) (s149 a13 s159) (s151 a7 s161) (s152 a8 s162) (s152 a13 s163) (s152 a16 s164) (s154 a7 s166) (s155 a9 s167) (s156 a9 s168) (s158 a9 s169) (s161 a8 s170) (s161 a13 s171) (s161 a16 s172) (s162 a9 s173) (s164 a9 s174) (s166 a8 s175) (s166 a13 s176) (s166 a16 s177) (s170 a9 s1) (s172 a9 s2) (s175 a9 s4) (s177 a9 s5) (s178 a5 s6) }, returnTransitions = { (s1 s143 r1 s7) (s1 s7 r2 s29) (s2 s7 r2 s29) (s4 s146 r1 s9) (s4 s9 r2 s32) (s5 s9 r2 s32) (s10 s52 r3 s121) (s11 s95 r3 s117) (s11 s159 r3 s117) (s11 s120 r4 s147) (s11 s13 r4 s147) (s17 s90 r2 s104) (s17 s12 r2 s35) (s21 s107 r1 s135) (s25 s107 r1 s137) (s28 s59 r3 s117) (s28 s157 r3 s117) (s28 s95 r3 s117) (s28 s159 r3 s117) (s28 s120 r4 s147) (s28 s76 r4 s147) (s28 s13 r4 s147) (s28 s117 r4 s147) (s31 s125 r3 s160) (s31 s171 r3 s18) (s31 s18 r4 s41) (s31 s160 r4 s19) (s34 s127 r3 s165) (s34 s176 r3 s23) (s34 s165 r4 s22) (s34 s23 r4 s44) (s37 s59 r3 s117) (s37 s76 r4 s147) (s40 s137 r2 s3) (s43 s143 r1 s7) (s43 s7 r2 s29) (s46 s146 r1 s9) (s46 s9 r2 s32) (s63 s82 r1 s12) (s63 s68 r1 s12) (s72 s59 r3 s76) (s73 s59 r3 s76) (s74 s61 r3 s77) (s75 s61 r3 s77) (s85 s77 r4 s87) (s86 s77 r4 s87) (s89 s55 r1 s90) (s89 s82 r1 s12) (s89 s68 r1 s12) (s100 s90 r2 s104) (s100 s12 r2 s35) (s102 s90 r2 s104) (s102 s12 r2 s35) (s111 s95 r3 s117) (s111 s159 r3 s117) (s111 s120 r4 s147) (s111 s13 r4 s147) (s114 s95 r3 s120) (s114 s159 r3 s13) (s115 s52 r3 s121) (s116 s97 r3 s122) (s116 s163 r3 s15) (s116 s122 r4 s14) (s116 s15 r4 s38) (s129 s107 r1 s135) (s131 s107 r1 s137) (s139 s157 r3 s117) (s139 s117 r4 s147) (s150 s125 r3 s160) (s150 s171 r3 s18) (s150 s18 r4 s41) (s150 s160 r4 s19) (s153 s127 r3 s165) (s153 s176 r3 s23) (s153 s165 r4 s22) (s153 s23 r4 s44) (s167 s134 r1 s0) (s167 s55 r1 s47) (s167 s82 r1 s0) (s167 s68 r1 s0) (s167 s0 r2 s26) (s167 s135 r2 s26) (s167 s90 r2 s178) (s167 s12 r2 s26) (s167 s47 r2 s178) (s168 s134 r1 s0) (s168 s0 r2 s26) (s168 s47 r2 s178) (s169 s0 r2 s26) (s169 s47 r2 s178) (s173 s137 r2 s3) (s174 s137 r2 s3) } ); minimizeSevpa(removeUnreachable(nwa)); shrinkNwa(removeUnreachable(nwa)); minimizeNwaPmaxSatDirectBi(removeUnreachable(nwa)); ReduceNwaDirectSimulation(removeUnreachable(nwa)); ReduceNwaDelayedSimulation(removeUnreachable(nwa)); ReduceNwaDirectSimulationB(removeUnreachable(nwa)); ReduceNwaDelayedSimulationB(removeUnreachable(nwa));