// 2015-07-30, Matthias Heizmann
// reveals bug in buchiComplementNCSB and buchiComplementFKV
// obtained from termination analysis of CostaDouble.bpl


NestedLassoWord nlw = [  "a" "a" , "c"< "c"< >"r" >"r" "a" "a" ];
boolean accepted = buchiAccepts(ia, nlw);
NestedWordAutomaton complementNCSB = buchiComplementNCSB(ia);
assert(numberOfStates(complementNCSB) == 13);
boolean acceptedComplementNCSB = buchiAccepts(complementNCSB, nlw);
NestedWordAutomaton complementFKV = buchiComplementFKV(ia);
assert(numberOfStates(complementFKV) == 32);
boolean acceptedComplementFKV = buchiAccepts(complementFKV, nlw);
assert(!accepted);
assert(acceptedComplementNCSB);
assert(acceptedComplementFKV);



NestedWordAutomaton ia = (
	callAlphabet = {"c" },
	internalAlphabet = {"a" },
	returnAlphabet = {"r" },
	states = {"q" "f" "s" "t" },
	initialStates = {"q" },
	finalStates = {"f" },
	callTransitions = {
		 ("q" "c" "t")
		 ("t" "c" "t")
		 ("s" "c" "t")
	},
	internalTransitions = {
		 ("q" "a" "q")
		 ("q" "a" "f")
		 ("f" "a" "s")
		 ("s" "a" "s")
		 ("t" "a" "t")
	},
	returnTransitions = {
		 ("t" "q" "r" "q")
		 ("t" "t" "r" "t")
		 ("t" "s" "r" "s")
	}
);