/*
 * Bug introduced in some refactoring
 * 
 * Date: 2015-12-31
 * Author: Matthias Heizmann
 */

NestedWordAutomaton dFKV = buchiComplementFKV(nwa);
// NestedWordAutomaton dFKV = buchiDifferenceFKV(prg, nwa);
print(numberOfStates(dFKV));
print(numberOfTransitions(dFKV));
// print(dFKV);
NestedWordAutomaton dFKVl = removeNonLiveStates(dFKV);
print(numberOfStates(dFKVl));

NestedWordAutomaton dNCSB = buchiComplementNCSB(nwa);
// NestedWordAutomaton dNCSB = buchiDifferenceNCSB(prg, nwa);
// print(dNCSB);
print(numberOfStates(dNCSB));
print(numberOfTransitions(dNCSB));
NestedWordAutomaton dNCSBl = removeNonLiveStates(dNCSB);
print(numberOfStates(dNCSBl));


NestedWordAutomaton nwa = (
	callAlphabet = {"call main_#t~ret3 := g(main_~x~3);" "call #t~ret1 := g(#t~ret0 - 1);" "call #t~ret0 := g(~x - 1);" },
	internalAlphabet = {"havoc main_#t~ret3;" "~x := #in~x;assume !(~x == 0);" "#res := #t~ret1;havoc #t~ret0;havoc #t~ret1;" "havoc main_#res;havoc main_#t~nondet2, main_#t~ret3, main_~x~3;main_~x~3 := main_#t~nondet2;havoc main_#t~nondet2;assume main_~x~3 < 0;main_#res := 0;" "#t~ret4 := main_#res;assume true;" "~x := #in~x;assume ~x == 0;#res := 1;" "assume true;" "havoc main_#res;havoc main_#t~nondet2, main_#t~ret3, main_~x~3;main_~x~3 := main_#t~nondet2;havoc main_#t~nondet2;assume !(main_~x~3 < 0);" },
	returnAlphabet = {"return;" "return;" "return;" },
	states = {"49#unseeded" "65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))" "66#(and (<= 0 |g_#in~x|) (<= |g_#in~x| oldRank0))" "69#(and (distinct g_~x 0) (<= 0 g_~x) (<= 0 |g_#in~x|) (<= g_~x oldRank0) (<= |g_#in~x| oldRank0))" "56#(and unseeded (<= 0 ULTIMATE.start_main_~x~3))" },
	initialStates = {"49#unseeded" },
	finalStates = {"65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))" },
	callTransitions = {
		 ("69#(and (distinct g_~x 0) (<= 0 g_~x) (<= 0 |g_#in~x|) (<= g_~x oldRank0) (<= |g_#in~x| oldRank0))" "call #t~ret0 := g(~x - 1);" "65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))")
		 ("56#(and unseeded (<= 0 ULTIMATE.start_main_~x~3))" "call main_#t~ret3 := g(main_~x~3);" "65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))")
	},
	internalTransitions = {
		 ("49#unseeded" "havoc main_#res;havoc main_#t~nondet2, main_#t~ret3, main_~x~3;main_~x~3 := main_#t~nondet2;havoc main_#t~nondet2;assume main_~x~3 < 0;main_#res := 0;" "49#unseeded")
		 ("49#unseeded" "#t~ret4 := main_#res;assume true;" "49#unseeded")
		 ("49#unseeded" "havoc main_#res;havoc main_#t~nondet2, main_#t~ret3, main_~x~3;main_~x~3 := main_#t~nondet2;havoc main_#t~nondet2;assume !(main_~x~3 < 0);" "56#(and unseeded (<= 0 ULTIMATE.start_main_~x~3))")
		 ("65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))" "~x := #in~x;assume !(~x == 0);" "69#(and (distinct g_~x 0) (<= 0 g_~x) (<= 0 |g_#in~x|) (<= g_~x oldRank0) (<= |g_#in~x| oldRank0))")
		 ("65#(and (<= 0 |g_#in~x|) (<= (+ |g_#in~x| 1) oldRank0))" "~x := #in~x;assume ~x == 0;#res := 1;" "66#(and (<= 0 |g_#in~x|) (<= |g_#in~x| oldRank0))")
		 ("66#(and (<= 0 |g_#in~x|) (<= |g_#in~x| oldRank0))" "assume true;" "66#(and (<= 0 |g_#in~x|) (<= |g_#in~x| oldRank0))")
	},
	returnTransitions = {
	}
);