// Author: heizmann@informatik.uni-freiburg.de // Date: 2016-09-08 NestedWordAutomaton result = removeNonLiveStates(nwa); print(numberOfStates(result)); //assert(numberOfStates(result) == 4); NestedWordAutomaton nwa = ( callAlphabet = {"call res := McCarthy(x + 11);" "call res := McCarthy(res);" }, internalAlphabet = {"assume x > 100;res := x - 10;" "assume !(x > 100);" "assume !(res == 91 || x > 101);" "assume res == 91 || x > 101;" "assume true;" }, returnAlphabet = {"return;" "return;" }, states = {"516#L20" "517#L20" "518#L20" "519#L20" "520#L20'" "521#McCarthyFINAL" "523#McCarthyFINAL" "524#McCarthyFINAL" "525#McCarthyFINAL" "527#McCarthyENTRY" "529#McCarthyENTRY" "530#McCarthyENTRY" "531#McCarthyEXIT" "532#McCarthyEXIT" "533#McCarthyEXIT" "534#McCarthyEXIT" "543#L21" "544#L21" "545#L21" "546#L21" "547#L21" "548#L21" "549#L21" "550#L21" "559#L20" "560#L20" "561#L20" "562#L20" "563#L20" "564#L20" "565#L20" "566#L20" "567#L21" "568#L20" "569#L20" "570#L20'" "571#McCarthyFINAL" "573#McCarthyFINAL" "574#McCarthyFINAL" "576#McCarthyFINAL" "577#McCarthyFINAL" "579#McCarthyFINAL" "580#McCarthyFINAL" "581#McCarthyFINAL" "582#McCarthyFINAL" "584#McCarthyENTRY" "585#McCarthyENTRY" "587#McCarthyENTRY" "588#McCarthyENTRY" "589#McCarthyEXIT" "590#McCarthyEXIT" "591#McCarthyEXIT" "592#McCarthyEXIT" "593#McCarthyEXIT" "594#McCarthyEXIT" "595#McCarthyEXIT" "596#McCarthyEXIT" "597#McCarthyEXIT" "600#L20" "601#L20" "604#L21" "605#L21" "606#L20" "607#L20" "608#L21" "609#L20" "610#L20" "611#L20'" "612#L21" "613#McCarthyENTRY" "614#McCarthyFINAL" "615#McCarthyFINAL" "616#McCarthyENTRY" "617#McCarthyFINAL" "618#McCarthyFINAL" "619#L20" "620#L20" "621#L20" "622#L20" "623#McCarthyEXIT" "624#McCarthyEXIT" "625#L21" "626#L21" "627#L21" "628#L21" "629#L20" "630#L20" "631#L20" "632#L20" "633#McCarthyEXIT" "634#McCarthyEXIT" "635#McCarthyENTRY" "636#L20'" "637#McCarthyFINAL" "638#McCarthyFINAL" "639#McCarthyFINAL" "640#McCarthyFINAL" "641#McCarthyENTRY" "642#L21" "643#L20" "644#L20" "645#L20" "646#L20" "647#L20" "648#L20" "649#L20" "650#L20" "651#McCarthyEXIT" "652#McCarthyEXIT" "653#McCarthyEXIT" "654#McCarthyEXIT" "655#L21" "656#L21" "657#L21" "658#L21" "659#L21" "660#L21" "661#L21" "662#L21" "663#L20" "664#L20" "665#L20" "666#L20" "667#L20" "668#L20" "669#L20" "670#L20" "671#McCarthyFINAL" "672#L20'" "673#McCarthyFINAL" "674#McCarthyFINAL" "675#McCarthyFINAL" "676#McCarthyFINAL" "677#McCarthyFINAL" "678#McCarthyFINAL" "679#McCarthyFINAL" "680#McCarthyFINAL" "681#McCarthyEXIT" "682#McCarthyEXIT" "683#McCarthyEXIT" "684#McCarthyEXIT" "685#McCarthyEXIT" "686#McCarthyEXIT" "687#McCarthyEXIT" "688#McCarthyEXIT" "689#McCarthyEXIT" "690#L20'" "691#McCarthyENTRY" "692#L20" "693#McCarthyENTRY" "694#L21" "695#L21" "696#L20" "697#L20" "698#McCarthyFINAL" "699#McCarthyFINAL" "700#McCarthyENTRY" "701#McCarthyEXIT" "702#McCarthyEXIT" "703#L21" "704#L21" "705#L21" "706#L21" "707#L20" "708#L20" "709#L20" "710#L20" "711#L20'" "712#McCarthyFINAL" "713#McCarthyFINAL" "714#McCarthyFINAL" "715#McCarthyFINAL" "716#McCarthyENTRY" "717#McCarthyENTRY" "718#McCarthyEXIT" "719#McCarthyEXIT" "720#McCarthyEXIT" "721#McCarthyEXIT" "722#L21" "723#L21" "724#L21" "725#L21" "726#L21" "727#L21" "728#L21" "729#L21" "730#L20" "731#L20" "732#L20" "733#L20" "734#L20" "735#L20" "736#L20" "737#L20" "738#L21" "739#L20" "740#L20'" "741#McCarthyFINAL" "742#McCarthyFINAL" "743#McCarthyFINAL" "744#McCarthyFINAL" "745#McCarthyFINAL" "746#McCarthyFINAL" "747#McCarthyFINAL" "748#McCarthyFINAL" "749#McCarthyFINAL" "750#McCarthyEXIT" "751#McCarthyEXIT" "752#McCarthyEXIT" "753#McCarthyEXIT" "754#McCarthyEXIT" "755#McCarthyEXIT" "756#McCarthyEXIT" "757#McCarthyEXIT" "758#McCarthyEXIT" "759#L20'" "482#McCarthyENTRY" "483#L20" "488#McCarthyENTRY" "491#L21" "492#L21" "496#L20" "497#L20" "498#McCarthyFINAL" "499#McCarthyFINAL" "501#McCarthyENTRY" "502#McCarthyEXIT" "503#McCarthyEXIT" "508#L21" "509#L21" "510#L21" "511#L21" }, initialStates = {"482#McCarthyENTRY" }, finalStates = {"520#L20'" "523#McCarthyFINAL" "525#McCarthyFINAL" "529#McCarthyENTRY" "534#McCarthyEXIT" "543#L21" "544#L21" "545#L21" "546#L21" "547#L21" "548#L21" "549#L21" "550#L21" "567#L21" "568#L20" "570#L20'" "573#McCarthyFINAL" "576#McCarthyFINAL" "579#McCarthyFINAL" "581#McCarthyFINAL" "582#McCarthyFINAL" "584#McCarthyENTRY" "587#McCarthyENTRY" "596#McCarthyEXIT" "597#McCarthyEXIT" "608#L21" "609#L20" "611#L20'" "612#L21" "617#McCarthyFINAL" "618#McCarthyFINAL" "633#McCarthyEXIT" "634#McCarthyEXIT" "642#L21" "671#McCarthyFINAL" "681#McCarthyEXIT" "690#L20'" "691#McCarthyENTRY" "692#L20" "693#McCarthyENTRY" "699#McCarthyFINAL" "702#McCarthyEXIT" "711#L20'" "713#McCarthyFINAL" "715#McCarthyFINAL" "717#McCarthyENTRY" "721#McCarthyEXIT" "738#L21" "739#L20" "740#L20'" "742#McCarthyFINAL" "744#McCarthyFINAL" "746#McCarthyFINAL" "748#McCarthyFINAL" "749#McCarthyFINAL" "757#McCarthyEXIT" "758#McCarthyEXIT" "482#McCarthyENTRY" "491#L21" "492#L21" "499#McCarthyFINAL" "503#McCarthyEXIT" "508#L21" "509#L21" "510#L21" "511#L21" }, callTransitions = { ("516#L20" "call res := McCarthy(x + 11);" "527#McCarthyENTRY") ("520#L20'" "call res := McCarthy(res);" "529#McCarthyENTRY") ("520#L20'" "call res := McCarthy(res);" "530#McCarthyENTRY") ("559#L20" "call res := McCarthy(x + 11);" "527#McCarthyENTRY") ("568#L20" "call res := McCarthy(x + 11);" "584#McCarthyENTRY") ("569#L20" "call res := McCarthy(x + 11);" "585#McCarthyENTRY") ("570#L20'" "call res := McCarthy(res);" "587#McCarthyENTRY") ("570#L20'" "call res := McCarthy(res);" "588#McCarthyENTRY") ("600#L20" "call res := McCarthy(x + 11);" "613#McCarthyENTRY") ("606#L20" "call res := McCarthy(x + 11);" "616#McCarthyENTRY") ("609#L20" "call res := McCarthy(x + 11);" "584#McCarthyENTRY") ("610#L20" "call res := McCarthy(x + 11);" "585#McCarthyENTRY") ("611#L20'" "call res := McCarthy(res);" "587#McCarthyENTRY") ("611#L20'" "call res := McCarthy(res);" "588#McCarthyENTRY") ("619#L20" "call res := McCarthy(x + 11);" "635#McCarthyENTRY") ("629#L20" "call res := McCarthy(x + 11);" "641#McCarthyENTRY") ("636#L20'" "call res := McCarthy(res);" "587#McCarthyENTRY") ("636#L20'" "call res := McCarthy(res);" "588#McCarthyENTRY") ("643#L20" "call res := McCarthy(x + 11);" "635#McCarthyENTRY") ("663#L20" "call res := McCarthy(x + 11);" "641#McCarthyENTRY") ("672#L20'" "call res := McCarthy(res);" "587#McCarthyENTRY") ("672#L20'" "call res := McCarthy(res);" "588#McCarthyENTRY") ("690#L20'" "call res := McCarthy(res);" "691#McCarthyENTRY") ("692#L20" "call res := McCarthy(x + 11);" "693#McCarthyENTRY") ("696#L20" "call res := McCarthy(x + 11);" "700#McCarthyENTRY") ("707#L20" "call res := McCarthy(x + 11);" "716#McCarthyENTRY") ("711#L20'" "call res := McCarthy(res);" "717#McCarthyENTRY") ("730#L20" "call res := McCarthy(x + 11);" "716#McCarthyENTRY") ("739#L20" "call res := McCarthy(x + 11);" "693#McCarthyENTRY") ("740#L20'" "call res := McCarthy(res);" "717#McCarthyENTRY") ("759#L20'" "call res := McCarthy(res);" "587#McCarthyENTRY") ("759#L20'" "call res := McCarthy(res);" "588#McCarthyENTRY") ("483#L20" "call res := McCarthy(x + 11);" "488#McCarthyENTRY") ("496#L20" "call res := McCarthy(x + 11);" "501#McCarthyENTRY") }, internalTransitions = { ("521#McCarthyFINAL" "assume true;" "531#McCarthyEXIT") ("523#McCarthyFINAL" "assume true;" "532#McCarthyEXIT") ("524#McCarthyFINAL" "assume true;" "533#McCarthyEXIT") ("525#McCarthyFINAL" "assume true;" "534#McCarthyEXIT") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "544#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "545#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "546#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "547#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "548#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "549#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "550#L21") ("527#McCarthyENTRY" "assume x > 100;res := x - 10;" "543#L21") ("527#McCarthyENTRY" "assume !(x > 100);" "560#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "561#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "562#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "563#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "564#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "565#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "566#L20") ("527#McCarthyENTRY" "assume !(x > 100);" "559#L20") ("529#McCarthyENTRY" "assume x > 100;res := x - 10;" "567#L21") ("529#McCarthyENTRY" "assume !(x > 100);" "568#L20") ("530#McCarthyENTRY" "assume !(x > 100);" "569#L20") ("543#L21" "assume res == 91 || x > 101;" "571#McCarthyFINAL") ("544#L21" "assume res == 91 || x > 101;" "573#McCarthyFINAL") ("545#L21" "assume res == 91 || x > 101;" "574#McCarthyFINAL") ("546#L21" "assume res == 91 || x > 101;" "576#McCarthyFINAL") ("547#L21" "assume res == 91 || x > 101;" "577#McCarthyFINAL") ("548#L21" "assume res == 91 || x > 101;" "579#McCarthyFINAL") ("549#L21" "assume res == 91 || x > 101;" "580#McCarthyFINAL") ("550#L21" "assume res == 91 || x > 101;" "581#McCarthyFINAL") ("567#L21" "assume res == 91 || x > 101;" "582#McCarthyFINAL") ("571#McCarthyFINAL" "assume true;" "589#McCarthyEXIT") ("573#McCarthyFINAL" "assume true;" "590#McCarthyEXIT") ("574#McCarthyFINAL" "assume true;" "591#McCarthyEXIT") ("576#McCarthyFINAL" "assume true;" "592#McCarthyEXIT") ("577#McCarthyFINAL" "assume true;" "593#McCarthyEXIT") ("579#McCarthyFINAL" "assume true;" "594#McCarthyEXIT") ("580#McCarthyFINAL" "assume true;" "595#McCarthyEXIT") ("581#McCarthyFINAL" "assume true;" "596#McCarthyEXIT") ("582#McCarthyFINAL" "assume true;" "597#McCarthyEXIT") ("584#McCarthyENTRY" "assume !(x > 100);" "600#L20") ("584#McCarthyENTRY" "assume !(x > 100);" "601#L20") ("585#McCarthyENTRY" "assume x > 100;res := x - 10;" "604#L21") ("585#McCarthyENTRY" "assume x > 100;res := x - 10;" "605#L21") ("585#McCarthyENTRY" "assume !(x > 100);" "606#L20") ("585#McCarthyENTRY" "assume !(x > 100);" "607#L20") ("587#McCarthyENTRY" "assume x > 100;res := x - 10;" "608#L21") ("587#McCarthyENTRY" "assume !(x > 100);" "609#L20") ("588#McCarthyENTRY" "assume !(x > 100);" "610#L20") ("604#L21" "assume res == 91 || x > 101;" "614#McCarthyFINAL") ("605#L21" "assume res == 91 || x > 101;" "615#McCarthyFINAL") ("608#L21" "assume res == 91 || x > 101;" "617#McCarthyFINAL") ("612#L21" "assume res == 91 || x > 101;" "618#McCarthyFINAL") ("613#McCarthyENTRY" "assume !(x > 100);" "619#L20") ("613#McCarthyENTRY" "assume !(x > 100);" "620#L20") ("613#McCarthyENTRY" "assume !(x > 100);" "621#L20") ("613#McCarthyENTRY" "assume !(x > 100);" "622#L20") ("614#McCarthyFINAL" "assume true;" "623#McCarthyEXIT") ("615#McCarthyFINAL" "assume true;" "624#McCarthyEXIT") ("616#McCarthyENTRY" "assume x > 100;res := x - 10;" "625#L21") ("616#McCarthyENTRY" "assume x > 100;res := x - 10;" "626#L21") ("616#McCarthyENTRY" "assume x > 100;res := x - 10;" "627#L21") ("616#McCarthyENTRY" "assume x > 100;res := x - 10;" "628#L21") ("616#McCarthyENTRY" "assume !(x > 100);" "629#L20") ("616#McCarthyENTRY" "assume !(x > 100);" "630#L20") ("616#McCarthyENTRY" "assume !(x > 100);" "631#L20") ("616#McCarthyENTRY" "assume !(x > 100);" "632#L20") ("617#McCarthyFINAL" "assume true;" "633#McCarthyEXIT") ("618#McCarthyFINAL" "assume true;" "634#McCarthyEXIT") ("625#L21" "assume res == 91 || x > 101;" "637#McCarthyFINAL") ("626#L21" "assume res == 91 || x > 101;" "638#McCarthyFINAL") ("627#L21" "assume res == 91 || x > 101;" "639#McCarthyFINAL") ("628#L21" "assume res == 91 || x > 101;" "640#McCarthyFINAL") ("635#McCarthyENTRY" "assume !(x > 100);" "643#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "644#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "645#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "646#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "647#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "648#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "649#L20") ("635#McCarthyENTRY" "assume !(x > 100);" "650#L20") ("637#McCarthyFINAL" "assume true;" "651#McCarthyEXIT") ("638#McCarthyFINAL" "assume true;" "652#McCarthyEXIT") ("639#McCarthyFINAL" "assume true;" "653#McCarthyEXIT") ("640#McCarthyFINAL" "assume true;" "654#McCarthyEXIT") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "656#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "657#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "658#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "659#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "660#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "661#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "662#L21") ("641#McCarthyENTRY" "assume x > 100;res := x - 10;" "655#L21") ("641#McCarthyENTRY" "assume !(x > 100);" "663#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "664#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "665#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "666#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "667#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "668#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "669#L20") ("641#McCarthyENTRY" "assume !(x > 100);" "670#L20") ("642#L21" "assume res == 91 || x > 101;" "671#McCarthyFINAL") ("655#L21" "assume res == 91 || x > 101;" "673#McCarthyFINAL") ("656#L21" "assume res == 91 || x > 101;" "674#McCarthyFINAL") ("657#L21" "assume res == 91 || x > 101;" "675#McCarthyFINAL") ("658#L21" "assume res == 91 || x > 101;" "676#McCarthyFINAL") ("659#L21" "assume res == 91 || x > 101;" "677#McCarthyFINAL") ("660#L21" "assume res == 91 || x > 101;" "678#McCarthyFINAL") ("661#L21" "assume res == 91 || x > 101;" "679#McCarthyFINAL") ("662#L21" "assume res == 91 || x > 101;" "680#McCarthyFINAL") ("671#McCarthyFINAL" "assume true;" "681#McCarthyEXIT") ("673#McCarthyFINAL" "assume true;" "682#McCarthyEXIT") ("674#McCarthyFINAL" "assume true;" "683#McCarthyEXIT") ("675#McCarthyFINAL" "assume true;" "684#McCarthyEXIT") ("676#McCarthyFINAL" "assume true;" "685#McCarthyEXIT") ("677#McCarthyFINAL" "assume true;" "686#McCarthyEXIT") ("678#McCarthyFINAL" "assume true;" "687#McCarthyEXIT") ("679#McCarthyFINAL" "assume true;" "688#McCarthyEXIT") ("680#McCarthyFINAL" "assume true;" "689#McCarthyEXIT") ("691#McCarthyENTRY" "assume x > 100;res := x - 10;" "642#L21") ("691#McCarthyENTRY" "assume !(x > 100);" "692#L20") ("693#McCarthyENTRY" "assume x > 100;res := x - 10;" "694#L21") ("693#McCarthyENTRY" "assume x > 100;res := x - 10;" "695#L21") ("693#McCarthyENTRY" "assume !(x > 100);" "696#L20") ("693#McCarthyENTRY" "assume !(x > 100);" "697#L20") ("694#L21" "assume res == 91 || x > 101;" "698#McCarthyFINAL") ("695#L21" "assume res == 91 || x > 101;" "699#McCarthyFINAL") ("698#McCarthyFINAL" "assume true;" "701#McCarthyEXIT") ("699#McCarthyFINAL" "assume true;" "702#McCarthyEXIT") ("700#McCarthyENTRY" "assume x > 100;res := x - 10;" "704#L21") ("700#McCarthyENTRY" "assume x > 100;res := x - 10;" "705#L21") ("700#McCarthyENTRY" "assume x > 100;res := x - 10;" "706#L21") ("700#McCarthyENTRY" "assume x > 100;res := x - 10;" "703#L21") ("700#McCarthyENTRY" "assume !(x > 100);" "707#L20") ("700#McCarthyENTRY" "assume !(x > 100);" "708#L20") ("700#McCarthyENTRY" "assume !(x > 100);" "709#L20") ("700#McCarthyENTRY" "assume !(x > 100);" "710#L20") ("703#L21" "assume res == 91 || x > 101;" "712#McCarthyFINAL") ("704#L21" "assume res == 91 || x > 101;" "713#McCarthyFINAL") ("705#L21" "assume res == 91 || x > 101;" "714#McCarthyFINAL") ("706#L21" "assume res == 91 || x > 101;" "715#McCarthyFINAL") ("712#McCarthyFINAL" "assume true;" "718#McCarthyEXIT") ("713#McCarthyFINAL" "assume true;" "719#McCarthyEXIT") ("714#McCarthyFINAL" "assume true;" "720#McCarthyEXIT") ("715#McCarthyFINAL" "assume true;" "721#McCarthyEXIT") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "722#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "723#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "724#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "725#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "726#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "727#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "728#L21") ("716#McCarthyENTRY" "assume x > 100;res := x - 10;" "729#L21") ("716#McCarthyENTRY" "assume !(x > 100);" "736#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "737#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "730#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "731#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "732#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "733#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "734#L20") ("716#McCarthyENTRY" "assume !(x > 100);" "735#L20") ("717#McCarthyENTRY" "assume x > 100;res := x - 10;" "738#L21") ("717#McCarthyENTRY" "assume !(x > 100);" "739#L20") ("722#L21" "assume res == 91 || x > 101;" "741#McCarthyFINAL") ("723#L21" "assume res == 91 || x > 101;" "742#McCarthyFINAL") ("724#L21" "assume res == 91 || x > 101;" "743#McCarthyFINAL") ("725#L21" "assume res == 91 || x > 101;" "744#McCarthyFINAL") ("726#L21" "assume res == 91 || x > 101;" "745#McCarthyFINAL") ("727#L21" "assume res == 91 || x > 101;" "746#McCarthyFINAL") ("728#L21" "assume res == 91 || x > 101;" "747#McCarthyFINAL") ("729#L21" "assume res == 91 || x > 101;" "748#McCarthyFINAL") ("738#L21" "assume res == 91 || x > 101;" "749#McCarthyFINAL") ("741#McCarthyFINAL" "assume true;" "750#McCarthyEXIT") ("742#McCarthyFINAL" "assume true;" "751#McCarthyEXIT") ("743#McCarthyFINAL" "assume true;" "752#McCarthyEXIT") ("744#McCarthyFINAL" "assume true;" "753#McCarthyEXIT") ("745#McCarthyFINAL" "assume true;" "754#McCarthyEXIT") ("746#McCarthyFINAL" "assume true;" "755#McCarthyEXIT") ("747#McCarthyFINAL" "assume true;" "756#McCarthyEXIT") ("748#McCarthyFINAL" "assume true;" "757#McCarthyEXIT") ("749#McCarthyFINAL" "assume true;" "758#McCarthyEXIT") ("482#McCarthyENTRY" "assume !(x > 100);" "483#L20") ("488#McCarthyENTRY" "assume x > 100;res := x - 10;" "491#L21") ("488#McCarthyENTRY" "assume x > 100;res := x - 10;" "492#L21") ("488#McCarthyENTRY" "assume !(x > 100);" "496#L20") ("488#McCarthyENTRY" "assume !(x > 100);" "497#L20") ("491#L21" "assume res == 91 || x > 101;" "498#McCarthyFINAL") ("492#L21" "assume res == 91 || x > 101;" "499#McCarthyFINAL") ("498#McCarthyFINAL" "assume true;" "502#McCarthyEXIT") ("499#McCarthyFINAL" "assume true;" "503#McCarthyEXIT") ("501#McCarthyENTRY" "assume x > 100;res := x - 10;" "508#L21") ("501#McCarthyENTRY" "assume x > 100;res := x - 10;" "509#L21") ("501#McCarthyENTRY" "assume x > 100;res := x - 10;" "510#L21") ("501#McCarthyENTRY" "assume x > 100;res := x - 10;" "511#L21") ("501#McCarthyENTRY" "assume !(x > 100);" "516#L20") ("501#McCarthyENTRY" "assume !(x > 100);" "517#L20") ("501#McCarthyENTRY" "assume !(x > 100);" "518#L20") ("501#McCarthyENTRY" "assume !(x > 100);" "519#L20") ("508#L21" "assume res == 91 || x > 101;" "521#McCarthyFINAL") ("509#L21" "assume res == 91 || x > 101;" "523#McCarthyFINAL") ("510#L21" "assume res == 91 || x > 101;" "524#McCarthyFINAL") ("511#L21" "assume res == 91 || x > 101;" "525#McCarthyFINAL") }, returnTransitions = { ("534#McCarthyEXIT" "496#L20" "return;" "570#L20'") ("596#McCarthyEXIT" "516#L20" "return;" "611#L20'") ("596#McCarthyEXIT" "559#L20" "return;" "611#L20'") ("597#McCarthyEXIT" "520#L20'" "return;" "612#L21") ("624#McCarthyEXIT" "610#L20" "return;" "759#L20'") ("624#McCarthyEXIT" "569#L20" "return;" "636#L20'") ("633#McCarthyEXIT" "672#L20'" "return;" "738#L21") ("633#McCarthyEXIT" "611#L20'" "return;" "738#L21") ("633#McCarthyEXIT" "759#L20'" "return;" "738#L21") ("633#McCarthyEXIT" "570#L20'" "return;" "642#L21") ("633#McCarthyEXIT" "636#L20'" "return;" "642#L21") ("654#McCarthyEXIT" "606#L20" "return;" "672#L20'") ("681#McCarthyEXIT" "483#L20" "return;" "690#L20'") ("681#McCarthyEXIT" "690#L20'" "return;" "612#L21") ("681#McCarthyEXIT" "520#L20'" "return;" "612#L21") ("689#McCarthyEXIT" "629#L20" "return;" "672#L20'") ("689#McCarthyEXIT" "663#L20" "return;" "672#L20'") ("702#McCarthyEXIT" "739#L20" "return;" "740#L20'") ("702#McCarthyEXIT" "692#L20" "return;" "711#L20'") ("721#McCarthyEXIT" "696#L20" "return;" "740#L20'") ("757#McCarthyEXIT" "707#L20" "return;" "740#L20'") ("757#McCarthyEXIT" "730#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "610#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "739#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "707#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "516#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "559#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "496#L20" "return;" "711#L20'") ("758#McCarthyEXIT" "692#L20" "return;" "711#L20'") ("758#McCarthyEXIT" "629#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "663#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "696#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "569#L20" "return;" "711#L20'") ("758#McCarthyEXIT" "730#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "606#L20" "return;" "740#L20'") ("758#McCarthyEXIT" "672#L20'" "return;" "738#L21") ("758#McCarthyEXIT" "611#L20'" "return;" "738#L21") ("758#McCarthyEXIT" "740#L20'" "return;" "738#L21") ("758#McCarthyEXIT" "711#L20'" "return;" "642#L21") ("758#McCarthyEXIT" "759#L20'" "return;" "738#L21") ("758#McCarthyEXIT" "570#L20'" "return;" "642#L21") ("758#McCarthyEXIT" "636#L20'" "return;" "642#L21") ("503#McCarthyEXIT" "483#L20" "return;" "520#L20'") } );