// Author: heizmann@informatik.uni-freiburg.de // Date: 2015-07-30 // // Reveals Bug in r14916 in shrinkNwa. // Example obtained from termination analysis of CostaDouble.bpl print(numberOfStates(removeUnreachable(nwa))); print(numberOfStates(removeDeadEnds(nwa))); print(numberOfStates(removeNonLiveStates(nwa))); 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 reduceNwaDirectSimulationSize = numberOfStates(reduceNwaDirectSimulation(preprocessed)); int reduceNwaDirectSimulationBSize = numberOfStates(reduceNwaDirectSimulationB(preprocessed)); int reduceNwaDirectFullMultipebbleSimulationSize = numberOfStates(reduceNwaDirectFullMultipebbleSimulation(preprocessed)); int reduceNwaDelayedSimulationSize = numberOfStates(reduceNwaDelayedSimulation(preprocessed)); int reduceNwaDelayedSimulationBSize = numberOfStates(reduceNwaDelayedSimulationB(preprocessed)); int reduceNwaDelayedFullMultipebbleSimulationSize = numberOfStates(reduceNwaDelayedFullMultipebbleSimulation(preprocessed)); print(minimizeSevpaSize); print(shrinkNwaSize); print(minimizeNwaPmaxSatDirectBiSize); print(minimizeNwaPmaxSatDirectSize); print(reduceNwaDirectSimulationSize); print(reduceNwaDirectSimulationBSize); print(reduceNwaDirectFullMultipebbleSimulationSize); print(reduceNwaDelayedSimulationSize); print(reduceNwaDelayedSimulationBSize); print(reduceNwaDelayedFullMultipebbleSimulationSize); // assert(minimizeSevpaSize == 999); // assert(shrinkNwaSize == 999); // assert(minimizeNwaPmaxSatDirectBiSize == 999); // assert(minimizeNwaPmaxSatDirectSize == 999); // assert(reduceNwaDirectSimulationSize == 999); // assert(reduceNwaDirectSimulationBSize == 999); // assert(reduceNwaDirectFullMultipebbleSimulationSize == 999); // assert(reduceNwaDelayedSimulationSize == 999); // assert(reduceNwaDelayedSimulationBSize == 999); // assert(reduceNwaDelayedFullMultipebbleSimulationSize == 999); NestedWordAutomaton nwa = ( callAlphabet = {"call rec(y);" }, internalAlphabet = {"assume y >= k;assume true;" "assume y < k;" "y := y + 1;" "y := 0;" }, returnAlphabet = {"return;" }, states = {"14108#L17'" "14109#Block18" "14110#recENTRY" "14111#Block18" "14104#recENTRY" "14105#Block18" "14106#L17" "14107#recENTRY" "14100#L17" "14101#Block18" "14102#recENTRY" "14103#Block18" "14096#Block18" "14097#L17'" "14098#recENTRY" "14099#recEXIT" "14093#Block18" "14092#recENTRY" "14095#recENTRY" "14094#L17" "14089#L17" "14088#Block18" "14091#Block18" "14090#L17" "14085#L17" "14084#Block18" "14087#L17'" "14086#recENTRY" "14081#recENTRY" "14080#Block18" "14083#L17" "14082#Block18" "14142#L17" "14143#recENTRY" "14140#L17'" "14141#Block18" "14138#recEXIT" "14139#L17" "14136#recENTRY" "14137#Block18" "14134#L17" "14135#Block18" "14132#recEXIT" "14133#L17" "14130#L17'" "14131#L17'" "14128#Block18" "14129#L17'" "14127#Block18" "14126#Block18" "14125#L17" "14124#Block18" "14123#L17" "14122#L17" "14121#recEXIT" "14120#Block18" "14119#L17'" "14118#L17'" "14117#L17'" "14116#L17" "14115#recENTRY" "14114#Block18" "14113#Block18" "14112#Block18" "14168#L17" "14169#Block18" "14170#L17'" "14171#recENTRY" "14172#Block18" "14173#L17'" "14174#L17" "14175#L17" "14160#recEXIT" "14161#L17" "14162#Block18" "14163#L17'" "14164#L17'" "14165#recEXIT" "14166#recEXIT" "14167#L17" "14153#Block18" "14152#L17" "14155#Block18" "14154#L17" "14157#L17'" "14156#Block18" "14159#recEXIT" "14158#recENTRY" "14145#L17" "14144#Block18" "14147#recENTRY" "14146#Block18" "14149#L17" "14148#recENTRY" "14151#recENTRY" "14150#Block18" "14202#L17'" "14203#Block18" "14200#Block18" "14201#recENTRY" "14206#L17" "14207#L17" "14204#recEXIT" "14205#recEXIT" "14194#Block18" "14195#L17'" "14192#recENTRY" "14193#recEXIT" "14198#recEXIT" "14199#L17" "14196#L17'" "14197#L17" "14187#recEXIT" "14186#L17'" "14185#L17'" "14184#Block18" "14191#L17'" "14190#Block18" "14189#L17" "14188#recEXIT" "14179#Block18" "14178#L17" "14177#L17'" "14176#Block18" "14183#Block18" "14182#Block18" "14181#Block18" "14180#L17'" "14229#L17" "14228#L17" "14231#recENTRY" "14230#Block18" "14225#L17" "14224#L17'" "14227#recEXIT" "14226#L17'" "14237#recENTRY" "14236#recENTRY" "14239#Block18" "14238#L17" "14233#recENTRY" "14232#Block18" "14235#Block18" "14234#Block18" "14212#Block18" "14213#L17" "14214#L17'" "14215#Block18" "14208#Block18" "14209#L17'" "14210#recEXIT" "14211#L17" "14220#L17" "14221#Block18" "14222#L17'" "14223#Block18" "14216#recEXIT" "14217#L17" "14218#L17'" "14219#Block18" "14263#L17'" "14262#Block18" "14261#L17'" "14260#L17" "14259#L17'" "14258#Block18" "14257#Block18" "14256#Block18" "14271#recEXIT" "14270#L17'" "14269#L17'" "14268#Block18" "14267#Block18" "14266#recENTRY" "14265#Block18" "14264#L17" "14246#Block18" "14247#L17" "14244#recENTRY" "14245#Block18" "14242#Block18" "14243#L17'" "14240#L17'" "14241#L17" "14254#recENTRY" "14255#L17'" "14252#L17" "14253#Block18" "14250#Block18" "14251#recEXIT" "14248#L17'" "14249#L17'" "14289#Block18" "14288#L17" "14291#L17'" "14290#L17'" "14293#L17" "14292#recENTRY" "14295#recEXIT" "14294#Block18" "14297#recEXIT" "14296#recEXIT" "14299#L17" "14298#L17" "14301#L17'" "14300#Block18" "14303#L17" "14302#recEXIT" "14272#recEXIT" "14273#L17" "14274#L17" "14275#recEXIT" "14276#L17" "14277#Block18" "14278#Block18" "14279#L17'" "14280#Block18" "14281#L17'" "14282#L17'" "14283#L17" "14284#Block18" "14285#recENTRY" "14286#recEXIT" "14287#L17" "14323#L17'" "14322#L17'" "14321#Block18" "14320#Block18" "14327#recEXIT" "14326#L17" "14325#recEXIT" "14324#L17'" "14331#recENTRY" "14330#Block18" "14329#L17" "14328#L17" "14335#L17'" "14334#Block18" "14333#Block18" "14332#Block18" "14306#recEXIT" "14307#L17" "14304#Block18" "14305#L17'" "14310#L17" "14311#Block18" "14308#Block18" "14309#L17" "14314#L17'" "14315#recEXIT" "14312#Block18" "14313#L17'" "14318#Block18" "14319#L17" "14316#L17" "14317#L17" "14022#recENTRY" "14023#Block18" "14021#L17" "14026#L17" "14027#recENTRY" "14024#L17'" "14025#recEXIT" "14030#recEXIT" "14031#L17" "14028#Block18" "14029#L17'" "14035#L17" "14034#Block18" "14033#Block18" "14032#L17" "14039#recEXIT" "14038#L17'" "14037#recENTRY" "14036#Block18" "14043#L17'" "14042#Block18" "14041#L17" "14040#recEXIT" "14047#L17" "14046#Block18" "14045#L17" "14044#recEXIT" "14048#Block18" "14049#L17'" "14050#Block18" "14051#L17'" "14052#recEXIT" "14053#L17" "14054#L17'" "14055#Block18" "14056#recEXIT" "14057#L17" "14058#L17'" "14059#recEXIT" "14060#L17" "14061#recEXIT" "14062#L17" "14063#Block18" "14065#L17" "14064#Block18" "14067#L17'" "14066#Block18" "14069#recEXIT" "14068#L17'" "14071#recEXIT" "14070#L17" "14073#Block18" "14072#L17" "14075#Block18" "14074#recENTRY" "14077#Block18" "14076#L17'" "14079#recENTRY" "14078#recEXIT" "14422#L17" "14423#L17" "14420#recEXIT" "14421#L17" "14418#Block18" "14419#L17'" "14416#Block18" "14417#recENTRY" "14426#Block18" "14427#L17'" "14424#recEXIT" "14425#L17" "14407#Block18" "14406#L17'" "14405#Block18" "14404#L17" "14403#recEXIT" "14402#L17'" "14401#L17'" "14400#Block18" "14415#L17" "14414#L17'" "14413#Block18" "14412#L17" "14411#recENTRY" "14410#Block18" "14409#L17" "14408#L17'" "14384#L17" "14385#Block18" "14386#L17'" "14387#Block18" "14388#L17'" "14389#L17'" "14390#L17'" "14391#Block18" "14392#recENTRY" "14393#Block18" "14394#L17" "14395#L17'" "14396#Block18" "14397#L17" "14398#L17'" "14399#Block18" "14369#Block18" "14368#L17" "14371#recENTRY" "14370#Block18" "14373#Block18" "14372#Block18" "14375#L17" "14374#L17" "14377#recENTRY" "14376#recENTRY" "14379#Block18" "14378#Block18" "14381#recENTRY" "14380#L17'" "14383#Block18" "14382#Block18" "14354#recEXIT" "14355#recEXIT" "14352#L17'" "14353#L17'" "14358#L17'" "14359#Block18" "14356#L17" "14357#Block18" "14362#L17" "14363#L17" "14360#L17" "14361#Block18" "14366#L17'" "14367#recEXIT" "14364#L17'" "14365#L17" "14339#Block18" "14338#Block18" "14337#L17" "14336#recENTRY" "14343#recENTRY" "14342#recENTRY" "14341#recENTRY" "14340#Block18" "14347#Block18" "14346#recEXIT" "14345#L17" "14344#L17" "14351#Block18" "14350#L17" "14349#L17'" "14348#recENTRY" }, initialStates = {"14037#recENTRY" }, finalStates = {"14291#L17'" "14293#L17" "14292#recENTRY" "14295#recEXIT" "14294#Block18" "14297#recEXIT" "14296#recEXIT" "14299#L17" "14298#L17" "14301#L17'" "14300#Block18" "14303#L17" "14302#recEXIT" "14323#L17'" "14322#L17'" "14321#Block18" "14320#Block18" "14327#recEXIT" "14326#L17" "14325#recEXIT" "14324#L17'" "14331#recENTRY" "14330#Block18" "14329#L17" "14328#L17" "14335#L17'" "14334#Block18" "14333#Block18" "14332#Block18" "14306#recEXIT" "14307#L17" "14304#Block18" "14305#L17'" "14310#L17" "14311#Block18" "14308#Block18" "14309#L17" "14314#L17'" "14315#recEXIT" "14312#Block18" "14313#L17'" "14318#Block18" "14319#L17" "14316#L17" "14317#L17" "14422#L17" "14423#L17" "14420#recEXIT" "14421#L17" "14418#Block18" "14419#L17'" "14416#Block18" "14417#recENTRY" "14426#Block18" "14427#L17'" "14424#recEXIT" "14425#L17" "14407#Block18" "14406#L17'" "14405#Block18" "14404#L17" "14403#recEXIT" "14402#L17'" "14401#L17'" "14400#Block18" "14415#L17" "14414#L17'" "14413#Block18" "14412#L17" "14411#recENTRY" "14410#Block18" "14409#L17" "14408#L17'" "14384#L17" "14385#Block18" "14386#L17'" "14387#Block18" "14388#L17'" "14022#recENTRY" "14389#L17'" "14023#Block18" "14390#L17'" "14391#Block18" "14021#L17" "14392#recENTRY" "14393#Block18" "14394#L17" "14024#L17'" "14395#L17'" "14025#recEXIT" "14396#Block18" "14397#L17" "14031#L17" "14398#L17'" "14399#Block18" "14369#Block18" "14035#L17" "14368#L17" "14034#Block18" "14371#recENTRY" "14370#Block18" "14373#Block18" "14372#Block18" "14375#L17" "14037#recENTRY" "14374#L17" "14036#Block18" "14377#recENTRY" "14376#recENTRY" "14379#Block18" "14378#Block18" "14381#recENTRY" "14380#L17'" "14383#Block18" "14382#Block18" "14354#recEXIT" "14355#recEXIT" "14352#L17'" "14353#L17'" "14358#L17'" "14359#Block18" "14356#L17" "14357#Block18" "14362#L17" "14363#L17" "14360#L17" "14361#Block18" "14366#L17'" "14367#recEXIT" "14364#L17'" "14365#L17" "14339#Block18" "14338#Block18" "14337#L17" "14336#recENTRY" "14343#recENTRY" "14342#recENTRY" "14341#recENTRY" "14340#Block18" "14347#Block18" "14346#recEXIT" "14345#L17" "14344#L17" "14351#Block18" "14350#L17" "14349#L17'" "14348#recENTRY" }, callTransitions = { ("14106#L17" "call rec(y);" "14107#recENTRY") ("14100#L17" "call rec(y);" "14107#recENTRY") ("14094#L17" "call rec(y);" "14092#recENTRY") ("14089#L17" "call rec(y);" "14102#recENTRY") ("14090#L17" "call rec(y);" "14086#recENTRY") ("14085#L17" "call rec(y);" "14095#recENTRY") ("14083#L17" "call rec(y);" "14086#recENTRY") ("14142#L17" "call rec(y);" "14107#recENTRY") ("14139#L17" "call rec(y);" "14171#recENTRY") ("14134#L17" "call rec(y);" "14095#recENTRY") ("14133#L17" "call rec(y);" "14147#recENTRY") ("14125#L17" "call rec(y);" "14136#recENTRY") ("14123#L17" "call rec(y);" "14136#recENTRY") ("14122#L17" "call rec(y);" "14098#recENTRY") ("14116#L17" "call rec(y);" "14115#recENTRY") ("14168#L17" "call rec(y);" "14266#recENTRY") ("14174#L17" "call rec(y);" "14148#recENTRY") ("14175#L17" "call rec(y);" "14266#recENTRY") ("14161#L17" "call rec(y);" "14158#recENTRY") ("14167#L17" "call rec(y);" "14148#recENTRY") ("14152#L17" "call rec(y);" "14151#recENTRY") ("14154#L17" "call rec(y);" "14171#recENTRY") ("14145#L17" "call rec(y);" "14147#recENTRY") ("14149#L17" "call rec(y);" "14148#recENTRY") ("14206#L17" "call rec(y);" "14158#recENTRY") ("14207#L17" "call rec(y);" "14027#recENTRY") ("14199#L17" "call rec(y);" "14201#recENTRY") ("14197#L17" "call rec(y);" "14192#recENTRY") ("14189#L17" "call rec(y);" "14143#recENTRY") ("14178#L17" "call rec(y);" "14266#recENTRY") ("14229#L17" "call rec(y);" "14233#recENTRY") ("14228#L17" "call rec(y);" "14233#recENTRY") ("14225#L17" "call rec(y);" "14147#recENTRY") ("14238#L17" "call rec(y);" "14237#recENTRY") ("14213#L17" "call rec(y);" "14236#recENTRY") ("14211#L17" "call rec(y);" "14236#recENTRY") ("14220#L17" "call rec(y);" "14231#recENTRY") ("14217#L17" "call rec(y);" "14231#recENTRY") ("14260#L17" "call rec(y);" "14115#recENTRY") ("14264#L17" "call rec(y);" "14201#recENTRY") ("14247#L17" "call rec(y);" "14244#recENTRY") ("14241#L17" "call rec(y);" "14027#recENTRY") ("14252#L17" "call rec(y);" "14254#recENTRY") ("14288#L17" "call rec(y);" "14092#recENTRY") ("14293#L17" "call rec(y);" "14331#recENTRY") ("14299#L17" "call rec(y);" "14292#recENTRY") ("14298#L17" "call rec(y);" "14392#recENTRY") ("14303#L17" "call rec(y);" "14022#recENTRY") ("14273#L17" "call rec(y);" "14285#recENTRY") ("14274#L17" "call rec(y);" "14237#recENTRY") ("14276#L17" "call rec(y);" "14192#recENTRY") ("14283#L17" "call rec(y);" "14254#recENTRY") ("14287#L17" "call rec(y);" "14244#recENTRY") ("14326#L17" "call rec(y);" "14331#recENTRY") ("14329#L17" "call rec(y);" "14341#recENTRY") ("14328#L17" "call rec(y);" "14341#recENTRY") ("14307#L17" "call rec(y);" "14381#recENTRY") ("14310#L17" "call rec(y);" "14381#recENTRY") ("14309#L17" "call rec(y);" "14381#recENTRY") ("14319#L17" "call rec(y);" "14336#recENTRY") ("14316#L17" "call rec(y);" "14336#recENTRY") ("14317#L17" "call rec(y);" "14336#recENTRY") ("14422#L17" "call rec(y);" "14411#recENTRY") ("14423#L17" "call rec(y);" "14392#recENTRY") ("14421#L17" "call rec(y);" "14417#recENTRY") ("14425#L17" "call rec(y);" "14392#recENTRY") ("14404#L17" "call rec(y);" "14371#recENTRY") ("14415#L17" "call rec(y);" "14377#recENTRY") ("14412#L17" "call rec(y);" "14376#recENTRY") ("14409#L17" "call rec(y);" "14292#recENTRY") ("14384#L17" "call rec(y);" "14022#recENTRY") ("14021#L17" "call rec(y);" "14081#recENTRY") ("14026#L17" "call rec(y);" "14285#recENTRY") ("14394#L17" "call rec(y);" "14417#recENTRY") ("14397#L17" "call rec(y);" "14392#recENTRY") ("14031#L17" "call rec(y);" "14343#recENTRY") ("14035#L17" "call rec(y);" "14411#recENTRY") ("14368#L17" "call rec(y);" "14377#recENTRY") ("14032#L17" "call rec(y);" "14343#recENTRY") ("14032#L17" "call rec(y);" "14104#recENTRY") ("14375#L17" "call rec(y);" "14371#recENTRY") ("14374#L17" "call rec(y);" "14377#recENTRY") ("14041#L17" "call rec(y);" "14143#recENTRY") ("14047#L17" "call rec(y);" "14098#recENTRY") ("14045#L17" "call rec(y);" "14098#recENTRY") ("14053#L17" "call rec(y);" "14074#recENTRY") ("14356#L17" "call rec(y);" "14376#recENTRY") ("14362#L17" "call rec(y);" "14022#recENTRY") ("14363#L17" "call rec(y);" "14342#recENTRY") ("14057#L17" "call rec(y);" "14110#recENTRY") ("14360#L17" "call rec(y);" "14376#recENTRY") ("14060#L17" "call rec(y);" "14095#recENTRY") ("14062#L17" "call rec(y);" "14102#recENTRY") ("14365#L17" "call rec(y);" "14331#recENTRY") ("14065#L17" "call rec(y);" "14074#recENTRY") ("14337#L17" "call rec(y);" "14341#recENTRY") ("14070#L17" "call rec(y);" "14086#recENTRY") ("14072#L17" "call rec(y);" "14079#recENTRY") ("14345#L17" "call rec(y);" "14342#recENTRY") ("14344#L17" "call rec(y);" "14342#recENTRY") ("14350#L17" "call rec(y);" "14348#recENTRY") }, internalTransitions = { ("14108#L17'" "y := y + 1;" "14103#Block18") ("14109#Block18" "assume y < k;" "14072#L17") ("14110#recENTRY" "y := 0;" "14109#Block18") ("14111#Block18" "assume y >= k;assume true;" "14039#recEXIT") ("14111#Block18" "assume y < k;" "14211#L17") ("14104#recENTRY" "y := 0;" "14101#Block18") ("14105#Block18" "assume y >= k;assume true;" "14099#recEXIT") ("14107#recENTRY" "y := 0;" "14105#Block18") ("14101#Block18" "assume y < k;" "14100#L17") ("14102#recENTRY" "y := 0;" "14088#Block18") ("14103#Block18" "assume y < k;" "14065#L17") ("14096#Block18" "assume y < k;" "14062#L17") ("14097#L17'" "y := y + 1;" "14063#Block18") ("14098#recENTRY" "y := 0;" "14096#Block18") ("14093#Block18" "assume y < k;" "14090#L17") ("14092#recENTRY" "y := 0;" "14091#Block18") ("14095#recENTRY" "y := 0;" "14093#Block18") ("14088#Block18" "assume y >= k;assume true;" "14061#recEXIT") ("14091#Block18" "assume y < k;" "14089#L17") ("14084#Block18" "assume y >= k;assume true;" "14059#recEXIT") ("14087#L17'" "y := y + 1;" "14084#Block18") ("14086#recENTRY" "y := 0;" "14082#Block18") ("14081#recENTRY" "y := 0;" "14080#Block18") ("14080#Block18" "assume y >= k;assume true;" "14078#recEXIT") ("14082#Block18" "assume y >= k;assume true;" "14069#recEXIT") ("14143#recENTRY" "y := 0;" "14141#Block18") ("14140#L17'" "y := y + 1;" "14137#Block18") ("14141#Block18" "assume y < k;" "14139#L17") ("14136#recENTRY" "y := 0;" "14135#Block18") ("14137#Block18" "assume y < k;" "14085#L17") ("14135#Block18" "assume y < k;" "14133#L17") ("14130#L17'" "y := y + 1;" "14112#Block18") ("14131#L17'" "y := y + 1;" "14128#Block18") ("14128#Block18" "assume y < k;" "14123#L17") ("14129#L17'" "y := y + 1;" "14124#Block18") ("14127#Block18" "assume y < k;" "14125#L17") ("14126#Block18" "assume y >= k;assume true;" "14166#recEXIT") ("14126#Block18" "assume y < k;" "14047#L17") ("14124#Block18" "assume y >= k;assume true;" "14121#recEXIT") ("14120#Block18" "assume y < k;" "14260#L17") ("14119#L17'" "y := y + 1;" "14113#Block18") ("14118#L17'" "y := y + 1;" "14126#Block18") ("14117#L17'" "y := y + 1;" "14111#Block18") ("14115#recENTRY" "y := 0;" "14114#Block18") ("14114#Block18" "assume y < k;" "14083#L17") ("14113#Block18" "assume y < k;" "14134#L17") ("14112#Block18" "assume y < k;" "14122#L17") ("14169#Block18" "assume y >= k;assume true;" "14187#recEXIT") ("14169#Block18" "assume y < k;" "14168#L17") ("14170#L17'" "y := y + 1;" "14169#Block18") ("14171#recENTRY" "y := 0;" "14153#Block18") ("14172#Block18" "assume y >= k;assume true;" "14159#recEXIT") ("14172#Block18" "assume y < k;" "14174#L17") ("14173#L17'" "y := y + 1;" "14172#Block18") ("14162#Block18" "assume y >= k;assume true;" "14160#recEXIT") ("14162#Block18" "assume y < k;" "14167#L17") ("14163#L17'" "y := y + 1;" "14127#Block18") ("14164#L17'" "y := y + 1;" "14162#Block18") ("14153#Block18" "assume y >= k;assume true;" "14138#recEXIT") ("14155#Block18" "assume y < k;" "14152#L17") ("14157#L17'" "y := y + 1;" "14155#Block18") ("14156#Block18" "assume y < k;" "14154#L17") ("14158#recENTRY" "y := 0;" "14156#Block18") ("14144#Block18" "assume y >= k;assume true;" "14132#recEXIT") ("14147#recENTRY" "y := 0;" "14144#Block18") ("14146#Block18" "assume y < k;" "14106#L17") ("14148#recENTRY" "y := 0;" "14146#Block18") ("14151#recENTRY" "y := 0;" "14150#Block18") ("14150#Block18" "assume y < k;" "14142#L17") ("14202#L17'" "y := y + 1;" "14208#Block18") ("14203#Block18" "assume y < k;" "14264#L17") ("14200#Block18" "assume y >= k;assume true;" "14198#recEXIT") ("14201#recENTRY" "y := 0;" "14200#Block18") ("14194#Block18" "assume y >= k;assume true;" "14193#recEXIT") ("14195#L17'" "y := y + 1;" "14194#Block18") ("14192#recENTRY" "y := 0;" "14230#Block18") ("14196#L17'" "y := y + 1;" "14262#Block18") ("14186#L17'" "y := y + 1;" "14184#Block18") ("14185#L17'" "y := y + 1;" "14033#Block18") ("14184#Block18" "assume y < k;" "14189#L17") ("14191#L17'" "y := y + 1;" "14257#Block18") ("14190#Block18" "assume y >= k;assume true;" "14188#recEXIT") ("14190#Block18" "assume y < k;" "14207#L17") ("14179#Block18" "assume y >= k;assume true;" "14166#recEXIT") ("14179#Block18" "assume y < k;" "14178#L17") ("14177#L17'" "y := y + 1;" "14176#Block18") ("14176#Block18" "assume y >= k;assume true;" "14166#recEXIT") ("14176#Block18" "assume y < k;" "14149#L17") ("14183#Block18" "assume y < k;" "14032#L17") ("14183#Block18" "assume y < k;" "14189#L17") ("14182#Block18" "assume y >= k;assume true;" "14030#recEXIT") ("14182#Block18" "assume y < k;" "14288#L17") ("14181#Block18" "assume y < k;" "14225#L17") ("14180#L17'" "y := y + 1;" "14179#Block18") ("14231#recENTRY" "y := 0;" "14181#Block18") ("14230#Block18" "assume y < k;" "14145#L17") ("14224#L17'" "y := y + 1;" "14221#Block18") ("14226#L17'" "y := y + 1;" "14223#Block18") ("14237#recENTRY" "y := 0;" "14235#Block18") ("14236#recENTRY" "y := 0;" "14234#Block18") ("14239#Block18" "assume y >= k;assume true;" "14204#recEXIT") ("14239#Block18" "assume y < k;" "14161#L17") ("14233#recENTRY" "y := 0;" "14232#Block18") ("14232#Block18" "assume y >= k;assume true;" "14227#recEXIT") ("14235#Block18" "assume y < k;" "14229#L17") ("14234#Block18" "assume y < k;" "14228#L17") ("14212#Block18" "assume y >= k;assume true;" "14210#recEXIT") ("14214#L17'" "y := y + 1;" "14212#Block18") ("14215#Block18" "assume y >= k;assume true;" "14204#recEXIT") ("14215#Block18" "assume y < k;" "14213#L17") ("14208#Block18" "assume y >= k;assume true;" "14188#recEXIT") ("14208#Block18" "assume y < k;" "14206#L17") ("14209#L17'" "y := y + 1;" "14190#Block18") ("14221#Block18" "assume y < k;" "14217#L17") ("14222#L17'" "y := y + 1;" "14219#Block18") ("14223#Block18" "assume y < k;" "14220#L17") ("14218#L17'" "y := y + 1;" "14215#Block18") ("14219#Block18" "assume y >= k;assume true;" "14216#recEXIT") ("14263#L17'" "y := y + 1;" "14120#Block18") ("14262#Block18" "assume y < k;" "14116#L17") ("14261#L17'" "y := y + 1;" "14250#Block18") ("14259#L17'" "y := y + 1;" "14182#Block18") ("14258#Block18" "assume y >= k;assume true;" "14165#recEXIT") ("14258#Block18" "assume y < k;" "14247#L17") ("14257#Block18" "assume y >= k;assume true;" "14165#recEXIT") ("14257#Block18" "assume y < k;" "14094#L17") ("14256#Block18" "assume y < k;" "14283#L17") ("14270#L17'" "y := y + 1;" "14268#Block18") ("14269#L17'" "y := y + 1;" "14246#Block18") ("14268#Block18" "assume y >= k;assume true;" "14271#recEXIT") ("14268#Block18" "assume y < k;" "14238#L17") ("14267#Block18" "assume y >= k;assume true;" "14205#recEXIT") ("14267#Block18" "assume y < k;" "14274#L17") ("14266#recENTRY" "y := 0;" "14203#Block18") ("14265#Block18" "assume y < k;" "14199#L17") ("14246#Block18" "assume y >= k;assume true;" "14205#recEXIT") ("14246#Block18" "assume y < k;" "14273#L17") ("14244#recENTRY" "y := 0;" "14265#Block18") ("14245#Block18" "assume y < k;" "14276#L17") ("14242#Block18" "assume y >= k;assume true;" "14204#recEXIT") ("14242#Block18" "assume y < k;" "14241#L17") ("14243#L17'" "y := y + 1;" "14242#Block18") ("14240#L17'" "y := y + 1;" "14239#Block18") ("14254#recENTRY" "y := 0;" "14253#Block18") ("14255#L17'" "y := y + 1;" "14258#Block18") ("14253#Block18" "assume y >= k;assume true;" "14251#recEXIT") ("14250#Block18" "assume y >= k;assume true;" "14030#recEXIT") ("14250#Block18" "assume y < k;" "14287#L17") ("14248#L17'" "y := y + 1;" "14278#Block18") ("14249#L17'" "y := y + 1;" "14267#Block18") ("14289#Block18" "assume y >= k;assume true;" "14286#recEXIT") ("14291#L17'" "y := y + 1;" "14418#Block18") ("14290#L17'" "y := y + 1;" "14028#Block18") ("14292#recENTRY" "y := 0;" "14378#Block18") ("14294#Block18" "assume y < k;" "14409#L17") ("14301#L17'" "y := y + 1;" "14300#Block18") ("14300#Block18" "assume y >= k;assume true;" "14295#recEXIT") ("14300#Block18" "assume y < k;" "14345#L17") ("14277#Block18" "assume y >= k;assume true;" "14272#recEXIT") ("14278#Block18" "assume y < k;" "14197#L17") ("14279#L17'" "y := y + 1;" "14277#Block18") ("14280#Block18" "assume y >= k;assume true;" "14275#recEXIT") ("14281#L17'" "y := y + 1;" "14245#Block18") ("14282#L17'" "y := y + 1;" "14280#Block18") ("14284#Block18" "assume y < k;" "14252#L17") ("14285#recENTRY" "y := 0;" "14256#Block18") ("14323#L17'" "y := y + 1;" "14320#Block18") ("14322#L17'" "y := y + 1;" "14318#Block18") ("14321#Block18" "assume y < k;" "14317#L17") ("14320#Block18" "assume y < k;" "14316#L17") ("14324#L17'" "y := y + 1;" "14321#Block18") ("14331#recENTRY" "y := 0;" "14330#Block18") ("14330#Block18" "assume y >= k;assume true;" "14325#recEXIT") ("14335#L17'" "y := y + 1;" "14333#Block18") ("14334#Block18" "assume y < k;" "14326#L17") ("14333#Block18" "assume y < k;" "14319#L17") ("14332#Block18" "assume y < k;" "14329#L17") ("14304#Block18" "assume y < k;" "14303#L17") ("14305#L17'" "y := y + 1;" "14304#Block18") ("14311#Block18" "assume y >= k;assume true;" "14302#recEXIT") ("14311#Block18" "assume y < k;" "14309#L17") ("14308#Block18" "assume y >= k;assume true;" "14306#recEXIT") ("14308#Block18" "assume y < k;" "14298#L17") ("14314#L17'" "y := y + 1;" "14312#Block18") ("14312#Block18" "assume y < k;" "14310#L17") ("14313#L17'" "y := y + 1;" "14311#Block18") ("14318#Block18" "assume y >= k;assume true;" "14315#recEXIT") ("14418#Block18" "assume y >= k;assume true;" "14025#recEXIT") ("14418#Block18" "assume y < k;" "14394#L17") ("14419#L17'" "y := y + 1;" "14034#Block18") ("14416#Block18" "assume y < k;" "14374#L17") ("14417#recENTRY" "y := 0;" "14416#Block18") ("14426#Block18" "assume y >= k;assume true;" "14297#recEXIT") ("14426#Block18" "assume y < k;" "14423#L17") ("14427#L17'" "y := y + 1;" "14426#Block18") ("14407#Block18" "assume y < k;" "14375#L17") ("14406#L17'" "y := y + 1;" "14405#Block18") ("14405#Block18" "assume y >= k;assume true;" "14403#recEXIT") ("14402#L17'" "y := y + 1;" "14383#Block18") ("14401#L17'" "y := y + 1;" "14399#Block18") ("14400#Block18" "assume y >= k;assume true;" "14346#recEXIT") ("14400#Block18" "assume y < k;" "14422#L17") ("14414#L17'" "y := y + 1;" "14382#Block18") ("14413#Block18" "assume y < k;" "14360#L17") ("14411#recENTRY" "y := 0;" "14294#Block18") ("14410#Block18" "assume y < k;" "14299#L17") ("14408#L17'" "y := y + 1;" "14393#Block18") ("14385#Block18" "assume y >= k;assume true;" "14302#recEXIT") ("14385#Block18" "assume y < k;" "14384#L17") ("14386#L17'" "y := y + 1;" "14385#Block18") ("14387#Block18" "assume y >= k;assume true;" "14302#recEXIT") ("14387#Block18" "assume y < k;" "14344#L17") ("14388#L17'" "y := y + 1;" "14387#Block18") ("14022#recENTRY" "y := 0;" "14410#Block18") ("14389#L17'" "y := y + 1;" "14413#Block18") ("14023#Block18" "assume y < k;" "14425#L17") ("14390#L17'" "y := y + 1;" "14400#Block18") ("14391#Block18" "assume y < k;" "14415#L17") ("14392#recENTRY" "y := 0;" "14391#Block18") ("14393#Block18" "assume y < k;" "14404#L17") ("14027#recENTRY" "y := 0;" "14284#Block18") ("14024#L17'" "y := y + 1;" "14023#Block18") ("14395#L17'" "y := y + 1;" "14407#Block18") ("14396#Block18" "assume y >= k;assume true;" "14424#recEXIT") ("14396#Block18" "assume y < k;" "14397#L17") ("14398#L17'" "y := y + 1;" "14396#Block18") ("14028#Block18" "assume y >= k;assume true;" "14271#recEXIT") ("14028#Block18" "assume y < k;" "14026#L17") ("14399#Block18" "assume y >= k;assume true;" "14025#recEXIT") ("14399#Block18" "assume y < k;" "14035#L17") ("14029#L17'" "y := y + 1;" "14289#Block18") ("14369#Block18" "assume y < k;" "14362#L17") ("14034#Block18" "assume y >= k;assume true;" "14420#recEXIT") ("14034#Block18" "assume y < k;" "14298#L17") ("14371#recENTRY" "y := 0;" "14370#Block18") ("14033#Block18" "assume y < k;" "14032#L17") ("14370#Block18" "assume y < k;" "14293#L17") ("14373#Block18" "assume y >= k;assume true;" "14367#recEXIT") ("14372#Block18" "assume y < k;" "14365#L17") ("14038#L17'" "y := y + 1;" "14183#Block18") ("14037#recENTRY" "y := 0;" "14036#Block18") ("14036#Block18" "assume y < k;" "14021#L17") ("14377#recENTRY" "y := 0;" "14373#Block18") ("14043#L17'" "y := y + 1;" "14042#Block18") ("14376#recENTRY" "y := 0;" "14372#Block18") ("14042#Block18" "assume y >= k;assume true;" "14040#recEXIT") ("14042#Block18" "assume y < k;" "14175#L17") ("14379#Block18" "assume y < k;" "14368#L17") ("14378#Block18" "assume y >= k;assume true;" "14296#recEXIT") ("14381#recENTRY" "y := 0;" "14379#Block18") ("14380#L17'" "y := y + 1;" "14369#Block18") ("14046#Block18" "assume y >= k;assume true;" "14044#recEXIT") ("14383#Block18" "assume y >= k;assume true;" "14346#recEXIT") ("14383#Block18" "assume y < k;" "14421#L17") ("14382#Block18" "assume y < k;" "14412#L17") ("14048#Block18" "assume y < k;" "14045#L17") ("14049#L17'" "y := y + 1;" "14046#Block18") ("14352#L17'" "y := y + 1;" "14351#Block18") ("14050#Block18" "assume y < k;" "14041#L17") ("14050#Block18" "assume y < k;" "14031#L17") ("14353#L17'" "y := y + 1;" "14308#Block18") ("14051#L17'" "y := y + 1;" "14048#Block18") ("14358#L17'" "y := y + 1;" "14357#Block18") ("14359#Block18" "assume y >= k;assume true;" "14355#recEXIT") ("14054#L17'" "y := y + 1;" "14050#Block18") ("14357#Block18" "assume y >= k;assume true;" "14354#recEXIT") ("14357#Block18" "assume y < k;" "14363#L17") ("14055#Block18" "assume y < k;" "14053#L17") ("14058#L17'" "y := y + 1;" "14055#Block18") ("14361#Block18" "assume y < k;" "14356#L17") ("14366#L17'" "y := y + 1;" "14361#Block18") ("14364#L17'" "y := y + 1;" "14359#Block18") ("14063#Block18" "assume y < k;" "14060#L17") ("14339#Block18" "assume y < k;" "14328#L17") ("14338#Block18" "assume y >= k;assume true;" "14327#recEXIT") ("14064#Block18" "assume y >= k;assume true;" "14052#recEXIT") ("14067#L17'" "y := y + 1;" "14064#Block18") ("14336#recENTRY" "y := 0;" "14334#Block18") ("14066#Block18" "assume y >= k;assume true;" "14056#recEXIT") ("14343#recENTRY" "y := 0;" "14340#Block18") ("14342#recENTRY" "y := 0;" "14339#Block18") ("14068#L17'" "y := y + 1;" "14066#Block18") ("14341#recENTRY" "y := 0;" "14338#Block18") ("14340#Block18" "assume y < k;" "14337#L17") ("14347#Block18" "assume y < k;" "14307#L17") ("14073#Block18" "assume y < k;" "14070#L17") ("14075#Block18" "assume y < k;" "14057#L17") ("14074#recENTRY" "y := 0;" "14073#Block18") ("14351#Block18" "assume y < k;" "14350#L17") ("14077#Block18" "assume y >= k;assume true;" "14071#recEXIT") ("14076#L17'" "y := y + 1;" "14075#Block18") ("14349#L17'" "y := y + 1;" "14347#Block18") ("14079#recENTRY" "y := 0;" "14077#Block18") ("14348#recENTRY" "y := 0;" "14332#Block18") }, returnTransitions = { ("14099#recEXIT" "14142#L17" "return;" "14140#L17'") ("14099#recEXIT" "14106#L17" "return;" "14119#L17'") ("14099#recEXIT" "14100#L17" "return;" "14097#L17'") ("14138#recEXIT" "14154#L17" "return;" "14163#L17'") ("14138#recEXIT" "14139#L17" "return;" "14131#L17'") ("14132#recEXIT" "14225#L17" "return;" "14222#L17'") ("14132#recEXIT" "14145#L17" "return;" "14282#L17'") ("14132#recEXIT" "14133#L17" "return;" "14129#L17'") ("14121#recEXIT" "14125#L17" "return;" "14218#L17'") ("14121#recEXIT" "14123#L17" "return;" "14117#L17'") ("14160#recEXIT" "14152#L17" "return;" "14157#L17'") ("14165#recEXIT" "14168#L17" "return;" "14164#L17'") ("14165#recEXIT" "14175#L17" "return;" "14173#L17'") ("14165#recEXIT" "14178#L17" "return;" "14177#L17'") ("14166#recEXIT" "14174#L17" "return;" "14173#L17'") ("14166#recEXIT" "14149#L17" "return;" "14177#L17'") ("14166#recEXIT" "14167#L17" "return;" "14164#L17'") ("14159#recEXIT" "14032#L17" "return;" "14157#L17'") ("14204#recEXIT" "14206#L17" "return;" "14202#L17'") ("14204#recEXIT" "14161#L17" "return;" "14240#L17'") ("14205#recEXIT" "14207#L17" "return;" "14202#L17'") ("14205#recEXIT" "14241#L17" "return;" "14240#L17'") ("14193#recEXIT" "14260#L17" "return;" "14259#L17'") ("14193#recEXIT" "14116#L17" "return;" "14191#L17'") ("14198#recEXIT" "14199#L17" "return;" "14263#L17'") ("14198#recEXIT" "14264#L17" "return;" "14196#L17'") ("14187#recEXIT" "14152#L17" "return;" "14185#L17'") ("14188#recEXIT" "14189#L17" "return;" "14186#L17'") ("14227#recEXIT" "14229#L17" "return;" "14226#L17'") ("14227#recEXIT" "14228#L17" "return;" "14224#L17'") ("14210#recEXIT" "14213#L17" "return;" "14243#L17'") ("14210#recEXIT" "14211#L17" "return;" "14209#L17'") ("14216#recEXIT" "14220#L17" "return;" "14279#L17'") ("14216#recEXIT" "14217#L17" "return;" "14214#L17'") ("14271#recEXIT" "14273#L17" "return;" "14269#L17'") ("14271#recEXIT" "14026#L17" "return;" "14290#L17'") ("14251#recEXIT" "14252#L17" "return;" "14281#L17'") ("14251#recEXIT" "14283#L17" "return;" "14248#L17'") ("14295#recEXIT" "14032#L17" "return;" "14352#L17'") ("14297#recEXIT" "14423#L17" "return;" "14427#L17'") ("14297#recEXIT" "14425#L17" "return;" "14024#L17'") ("14296#recEXIT" "14299#L17" "return;" "14408#L17'") ("14296#recEXIT" "14409#L17" "return;" "14395#L17'") ("14302#recEXIT" "14363#L17" "return;" "14358#L17'") ("14302#recEXIT" "14345#L17" "return;" "14301#L17'") ("14302#recEXIT" "14344#L17" "return;" "14388#L17'") ("14272#recEXIT" "14274#L17" "return;" "14269#L17'") ("14272#recEXIT" "14238#L17" "return;" "14290#L17'") ("14275#recEXIT" "14276#L17" "return;" "14249#L17'") ("14275#recEXIT" "14197#L17" "return;" "14270#L17'") ("14286#recEXIT" "14288#L17" "return;" "14261#L17'") ("14286#recEXIT" "14094#L17" "return;" "14255#L17'") ("14327#recEXIT" "14337#L17" "return;" "14335#L17'") ("14327#recEXIT" "14329#L17" "return;" "14324#L17'") ("14327#recEXIT" "14328#L17" "return;" "14323#L17'") ("14325#recEXIT" "14293#L17" "return;" "14406#L17'") ("14325#recEXIT" "14326#L17" "return;" "14322#L17'") ("14325#recEXIT" "14365#L17" "return;" "14364#L17'") ("14306#recEXIT" "14307#L17" "return;" "14305#L17'") ("14306#recEXIT" "14310#L17" "return;" "14380#L17'") ("14306#recEXIT" "14309#L17" "return;" "14386#L17'") ("14315#recEXIT" "14319#L17" "return;" "14349#L17'") ("14315#recEXIT" "14316#L17" "return;" "14313#L17'") ("14315#recEXIT" "14317#L17" "return;" "14314#L17'") ("14420#recEXIT" "14421#L17" "return;" "14390#L17'") ("14420#recEXIT" "14394#L17" "return;" "14401#L17'") ("14424#recEXIT" "14423#L17" "return;" "14427#L17'") ("14424#recEXIT" "14298#L17" "return;" "14024#L17'") ("14424#recEXIT" "14397#L17" "return;" "14427#L17'") ("14424#recEXIT" "14425#L17" "return;" "14024#L17'") ("14403#recEXIT" "14404#L17" "return;" "14402#L17'") ("14403#recEXIT" "14375#L17" "return;" "14291#L17'") ("14025#recEXIT" "14422#L17" "return;" "14390#L17'") ("14025#recEXIT" "14035#L17" "return;" "14401#L17'") ("14030#recEXIT" "14247#L17" "return;" "14255#L17'") ("14030#recEXIT" "14287#L17" "return;" "14261#L17'") ("14039#recEXIT" "14189#L17" "return;" "14038#L17'") ("14039#recEXIT" "14041#L17" "return;" "14038#L17'") ("14040#recEXIT" "14032#L17" "return;" "14185#L17'") ("14044#recEXIT" "14122#L17" "return;" "14170#L17'") ("14044#recEXIT" "14047#L17" "return;" "14180#L17'") ("14044#recEXIT" "14045#L17" "return;" "14043#L17'") ("14354#recEXIT" "14350#L17" "return;" "14352#L17'") ("14355#recEXIT" "14356#L17" "return;" "14353#L17'") ("14355#recEXIT" "14360#L17" "return;" "14398#L17'") ("14355#recEXIT" "14412#L17" "return;" "14419#L17'") ("14052#recEXIT" "14065#L17" "return;" "14029#L17'") ("14052#recEXIT" "14053#L17" "return;" "14049#L17'") ("14056#recEXIT" "14057#L17" "return;" "14054#L17'") ("14059#recEXIT" "14134#L17" "return;" "14118#L17'") ("14059#recEXIT" "14085#L17" "return;" "14130#L17'") ("14059#recEXIT" "14060#L17" "return;" "14051#L17'") ("14367#recEXIT" "14368#L17" "return;" "14366#L17'") ("14367#recEXIT" "14374#L17" "return;" "14414#L17'") ("14367#recEXIT" "14415#L17" "return;" "14389#L17'") ("14061#recEXIT" "14089#L17" "return;" "14108#L17'") ("14061#recEXIT" "14062#L17" "return;" "14058#L17'") ("14069#recEXIT" "14090#L17" "return;" "14087#L17'") ("14069#recEXIT" "14070#L17" "return;" "14067#L17'") ("14069#recEXIT" "14083#L17" "return;" "14195#L17'") ("14071#recEXIT" "14072#L17" "return;" "14068#L17'") ("14346#recEXIT" "14384#L17" "return;" "14388#L17'") ("14346#recEXIT" "14362#L17" "return;" "14358#L17'") ("14346#recEXIT" "14303#L17" "return;" "14301#L17'") ("14078#recEXIT" "14021#L17" "return;" "14076#L17'") } );