// Author: heizmann@informatik.uni-freiburg.de
// Date: 02.06.2013


// parseAutomata("../../../PathologicalExamples.ats");

// NestedWordAutomaton nwa = buchiComplementDeterministic(emptyAutomaton);
// assert(numberOfStates(nwa) == 4);
// assert(!buchiIsEmpty(nwa));
// print(numberOfStates(nwa));


// parseAutomata("../../../simpleBuchiAutomata.ats");
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(infinitelyManyA);
// assert(numberOfStates(nwa) == 3);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(AfollowedByB);
// assert(numberOfStates(nwa) == 5);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(all);
// assert(numberOfStates(nwa) == 1);
// assert(buchiIsEmpty(nwa));

parseAutomata("../../../Xiaolin.ats");

NestedWordAutomaton nwa = buchiComplementDeterministic(eNoether);
assert(numberOfStates(nwa) == 9);
assert(!buchiIsEmpty(nwa));
print(numberOfStates(nwa));

NestedWordAutomaton nwa = buchiComplementDeterministic(rSchumann);
assert(numberOfStates(nwa) == 10);
assert(!buchiIsEmpty(nwa));
print(numberOfStates(nwa));

NestedWordAutomaton nwa = buchiComplementDeterministic(cKistner);
assert(numberOfStates(nwa) == 7);
assert(!buchiIsEmpty(nwa));
print(numberOfStates(nwa));

NestedWordAutomaton nwa = buchiComplementDeterministic(cKistnerSelfLoopFree);
assert(numberOfStates(nwa) == 11);
assert(!buchiIsEmpty(nwa));
print(numberOfStates(nwa));

// parseAutomata("../BuchiAutomata/SizeChangeTermination2001.ats");
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(infeasible);
// assert(numberOfStates(nwa) == 145);
// assert(buchiIsEmpty(nwa));
// 
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(infeasibleN);
// assert(numberOfStates(nwa) == 15);
// assert(!buchiIsEmpty(nwa));
// 
// 
// 
// parseAutomata("../BuchiAutomata/terminationTraceAbstractionBlueGreen.ats");
// 
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(manualIA1);
// assert(numberOfStates(nwa) == 5);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(manualIA2);
// assert(numberOfStates(nwa) == 19);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton1);
// assert(numberOfStates(nwa) == 5);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton2);
// assert(numberOfStates(nwa) == 8);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton3);
// assert(numberOfStates(nwa) == 11);
// assert(!buchiIsEmpty(nwa));
// print(numberOfStates(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton4);
// assert(numberOfStates(nwa) == 12);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton5);
// assert(numberOfStates(nwa) == 18);
// assert(!buchiIsEmpty(nwa));
// 
// NestedWordAutomaton nwa = buchiComplementDeterministic(interpolantAutomaton6);
// assert(numberOfStates(nwa) == 18);
// assert(!buchiIsEmpty(nwa));