// Some examples from terminationTraceAbstractionBlueGreen 
// and SizeChangeTermination2001
// Author: heizmann@informatik.uni-freiburg.de
// Date: 13.8.2012

parseAutomata("SizeChangeTermination2001.ats");

assert(buchiIsEmpty(buchiReduce(buchiComplementSVW(infeasible))));
assert(buchiIsEmpty(buchiReduce(buchiComplementFKV(infeasible))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(infeasibleN))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(infeasibleN))));

parseAutomata("TerminationTraceAbstractionBlueGreen.ats");

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(manualIA1))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(manualIA1))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(manualIA2))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(manualIA2))));



assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton1))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton1))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton2))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton2))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton3))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton3))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton4))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton4))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton5))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton5))));

assert(!buchiIsEmpty(buchiReduce(buchiComplementSVW(interpolantAutomaton6))));
assert(!buchiIsEmpty(buchiReduce(buchiComplementFKV(interpolantAutomaton6))));