// Date: end of 2011 // Simplified version of some intermediate result of terminationBlueGreen. // // Contains 5 dead end states. NestedWordAutomaton preprocessed = removeUnreachable(nwa); int minimizeSevpaSize = numberOfStates(minimizeSevpa(preprocessed)); int shrinkNwaSize = numberOfStates(shrinkNwa(preprocessed)); int minimizeNwaPmaxSatDirectBiSize = numberOfStates(minimizeNwaPmaxSatDirectBi(preprocessed)); int minimizeNwaPmaxSatDirectSize = numberOfStates(minimizeNwaPmaxSatDirect(preprocessed)); int minimizeDfaSimulationSize = numberOfStates(minimizeDfaSimulation(preprocessed)); int reduceNwaDirectSimulationSize = numberOfStates(reduceNwaDirectSimulation(preprocessed)); int reduceNwaDirectSimulationBSize = numberOfStates(reduceNwaDirectSimulationB(preprocessed)); int reduceNwaDirectFullMultipebbleSimulationSize = numberOfStates(reduceNwaDirectFullMultipebbleSimulation(preprocessed)); int buchiReduceSize = numberOfStates(buchiReduce(preprocessed)); int reduceNwaDelayedSimulationSize = numberOfStates(reduceNwaDelayedSimulation(preprocessed)); int reduceNwaDelayedSimulationBSize = numberOfStates(reduceNwaDelayedSimulationB(preprocessed)); int reduceNwaDelayedFullMultipebbleSimulationSize = numberOfStates(reduceNwaDelayedFullMultipebbleSimulation(preprocessed)); // int reduceBuchiFairDirectSimulationSize = numberOfStates(reduceBuchiFairDirectSimulation(preprocessed)); // TODO error; Warning: this runs for 6 minutes // int reduceBuchiFairSimulationSize = numberOfStates(reduceBuchiFairSimulation(preprocessed)); // TODO this runs like forever; I canceled it after 21 minutes assert(minimizeSevpaSize == 14); assert(shrinkNwaSize == 14); assert(minimizeNwaPmaxSatDirectBiSize == 14); assert(minimizeNwaPmaxSatDirectSize == 14); assert(minimizeDfaSimulationSize == 13); assert(reduceNwaDirectSimulationSize == 14); assert(reduceNwaDirectSimulationBSize == 13); assert(reduceNwaDirectFullMultipebbleSimulationSize == 14); assert(buchiReduceSize == 13); assert(reduceNwaDelayedSimulationSize == 14); assert(reduceNwaDelayedSimulationBSize == 13); assert(reduceNwaDelayedFullMultipebbleSimulationSize == 20); // assert(reduceBuchiFairDirectSimulationSize == 999); // TODO add correct number after error is fixed // assert(reduceBuchiFairSimulationSize == 999); // TODO add correct number after error is fixed NestedWordAutomaton nwa = ( callAlphabet = {}, internalAlphabet = { b g }, returnAlphabet = {}, states = { Q1 Q2 Init Q3 Q4 Q5 Q6 Q7 Q8 F1 Q9 Q10 F4 F5 F2 F3 Q11 Q12 Q13 Q14 Q15 Q16 Q17 Q18 Q19 Q20 Q21 Q22 Q26 Q25 Q24 Q23 F6 F7 F8 F9 Q27 Q28 Q29 Q30 F14 F15 Q31 Q32 F10 F11 F12 F13 Q37 Q36 Q39 Q38 Q33 F16 Q35 Q34 Q45 Q44 Q47 Q46 Q41 Q40 Q43 Q42 F18 Q53 Q52 F17 Q50 Q51 Q48 Q49 F19 Q60 Q58 Q59 Q56 Q57 Q54 Q55 }, initialStates = { Init }, finalStates = { Init F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 F14 F15 F16 F17 F18 F19 }, callTransitions = { }, internalTransitions = { (Init b Q3) (Init b Q1) (Init b Q2) (Init b Q6) (Init g Q7) (Init g Q4) (Init g Q5) (Init g Q9) (Q3 b Q3) (Q3 b Q1) (Q3 b Q2) (Q3 b Q6) (Q3 g Q7) (Q3 g Q4) (Q3 g Q5) (Q3 g Q9) (Q1 b Q1) (Q1 b Q6) (Q1 g Q10) (Q1 g Q8) (Q2 b F1) (Q2 b F2) (Q2 g F3) (Q2 g F4) (Q6 b F2) (Q6 g F5) (Q7 b Q14) (Q7 b Q13) (Q7 b Q12) (Q7 b Q11) (Q7 b Q18) (Q7 b Q17) (Q7 b Q16) (Q7 b Q15) (Q7 g Q22) (Q7 g Q21) (Q7 g Q20) (Q7 g Q19) (Q7 g Q23) (Q7 g Q24) (Q7 g Q25) (Q7 g Q26) (Q4 b Q27) (Q4 b Q28) (Q4 g Q29) (Q4 g Q30) (Q5 b F6) (Q5 b F7) (Q5 b F8) (Q5 b F9) (Q5 g F10) (Q5 g F11) (Q5 g F12) (Q5 g F13) (Q9 b F14) (Q9 g F15) (Q10 b Q27) (Q10 b Q28) (Q10 g Q31) (Q10 g Q32) (Q8 b F14) (Q8 g F16) (F1 b Q33) (F1 b Q34) (F1 g Q35) (F1 g Q36) (F2 b Q37) (F2 g Q8) (F3 b Q38) (F3 b Q39) (F3 b Q40) (F3 b Q41) (F3 g Q42) (F3 g Q43) (F3 g Q44) (F3 g Q45) (F4 b Q46) (F4 g Q30) (F5 b Q47) (F5 g Q48) (Q14 b Q14) (Q14 b Q13) (Q14 b Q12) (Q14 b Q11) (Q14 b Q18) (Q14 b Q17) (Q14 b Q16) (Q14 b Q15) (Q14 g Q7) (Q14 g Q4) (Q14 g Q5) (Q14 g Q9) (Q13 b Q13) (Q13 b Q17) (Q13 g Q10) (Q13 g Q8) (Q12 b Q13) (Q12 b Q12) (Q12 b Q17) (Q12 b Q16) (Q12 g Q10) (Q12 g Q8) (Q11 b Q13) (Q11 b Q11) (Q11 b Q17) (Q11 b Q15) (Q11 g Q10) (Q11 g Q8) (Q18 b F6) (Q18 b F7) (Q18 b F8) (Q18 b F9) (Q18 g F3) (Q18 g F4) (Q17 b F7) (Q17 g F5) (Q16 b F7) (Q16 b F8) (Q16 g F5) (Q15 b F7) (Q15 b F9) (Q15 g F5) (Q22 b Q14) (Q22 b Q13) (Q22 b Q12) (Q22 b Q11) (Q22 b Q18) (Q22 b Q17) (Q22 b Q16) (Q22 b Q15) (Q22 g Q22) (Q22 g Q21) (Q22 g Q20) (Q22 g Q19) (Q22 g Q23) (Q22 g Q24) (Q22 g Q25) (Q22 g Q26) (Q21 b Q27) (Q21 b Q28) (Q21 g Q29) (Q21 g Q30) (Q20 b Q13) (Q20 b Q17) (Q20 g Q49) (Q20 g Q50) (Q19 b Q13) (Q19 b Q11) (Q19 b Q17) (Q19 b Q15) (Q19 g Q49) (Q19 g Q50) (Q19 g Q51) (Q19 g Q52) (Q23 b F6) (Q23 b F7) (Q23 b F8) (Q23 b F9) (Q23 g F10) (Q23 g F11) (Q23 g F12) (Q23 g F13) (Q24 b F14) (Q24 g F15) (Q25 b F7) (Q25 g F17) (Q26 b F7) (Q26 b F9) (Q26 g F17) (Q26 g F18) (Q27 b Q27) (Q27 b Q28) (Q27 g Q10) (Q27 g Q8) (Q28 b F14) (Q28 g F5) (Q29 b Q27) (Q29 b Q28) (Q29 g Q29) (Q29 g Q30) (Q30 b F14) (Q30 g F15) (F6 b Q38) (F6 b Q39) (F6 b Q40) (F6 b Q41) (F6 g Q35) (F6 g Q36) (F7 b Q53) (F7 g Q8) (F8 b Q53) (F8 b Q54) (F8 g Q8) (F9 b Q53) (F9 b Q55) (F9 g Q8) (F10 b Q38) (F10 b Q39) (F10 b Q40) (F10 b Q41) (F10 g Q42) (F10 g Q43) (F10 g Q44) (F10 g Q45) (F11 b Q46) (F11 g Q30) (F12 b Q53) (F12 g Q50) (F13 b Q53) (F13 b Q55) (F13 g Q50) (F13 g Q52) (F14 b Q47) (F14 g Q56) (F15 b Q47) (F15 g Q57) (Q31 b Q27) (Q31 b Q28) (Q31 g Q58) (Q31 g Q59) (Q32 b F14) (Q32 g F19) (F16 b Q47) (F16 g Q60) (Q33 b Q33) (Q33 b Q34) (Q33 g Q35) (Q33 g Q36) (Q34 b Q37) (Q34 g Q8) (Q35 b Q38) (Q35 b Q39) (Q35 b Q40) (Q35 b Q41) (Q35 g Q42) (Q35 g Q43) (Q35 g Q44) (Q35 g Q45) (Q36 b Q46) (Q36 g Q30) (Q37 b Q37) (Q37 g Q8) (Q38 b Q38) (Q38 b Q39) (Q38 b Q40) (Q38 b Q41) (Q38 g Q35) (Q38 g Q36) (Q39 b Q53) (Q39 g Q8) (Q40 b Q53) (Q40 b Q54) (Q40 g Q8) (Q41 b Q53) (Q41 b Q55) (Q41 g Q8) (Q42 b Q38) (Q42 b Q39) (Q42 b Q40) (Q42 b Q41) (Q42 g Q42) (Q42 g Q43) (Q42 g Q44) (Q42 g Q45) (Q43 b Q46) (Q43 g Q30) (Q44 b Q53) (Q44 g Q50) (Q45 b Q53) (Q45 b Q55) (Q45 g Q50) (Q45 g Q52) (Q46 b Q46) (Q46 g Q8) (Q47 b Q47) (Q47 g Q56) (Q48 b Q47) (Q48 g Q60) (Q49 b Q27) (Q49 b Q28) (Q49 g Q31) (Q49 g Q32) (Q50 b F14) (Q50 g F16) (Q51 b Q27) (Q51 b Q28) (Q51 g Q31) (Q51 g Q32) (Q52 b F14) (Q52 g F16) (F17 b Q47) (F17 g Q48) (F18 b Q47) (F18 g Q48) (Q53 b Q53) (Q53 g Q8) (Q54 b Q53) (Q54 b Q54) (Q54 g Q8) (Q55 b Q53) (Q55 b Q55) (Q55 g Q8) (Q56 b Q47) (Q56 g Q48) (Q57 b Q47) (Q57 g Q57) (Q58 b Q27) (Q58 b Q28) (Q58 g Q31) (Q58 g Q32) (Q59 b F14) (Q59 g F16) (F19 b Q47) (F19 g Q48) (Q60 b Q47) (Q60 g Q48) }, returnTransitions = { } );