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


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

assert(isDeterministic(sameCalldifferentReturns));
assert(!isDeterministic(wBenjamin));
assert(isDeterministic(pendingReturnNwa));
assert(!isDeterministic(bugBfsEmptinessLowPriorityCallQueue));


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

assert(!isDeterministic(finitelyManyA));
assert(!isDeterministic(finitelyManyB));
assert(isDeterministic(infinitelyManyA));
assert(isDeterministic(infinitelyManyB));
assert(isDeterministic(AfollowedByB));
assert(isDeterministic(all));
assert(!isDeterministic(allTwoState));


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

assert(!isDeterministic(finitelyManyAInEachContext));
assert(isDeterministic(infinitelyManyAWithCallReturn));


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

assert(isDeterministic(all));
assert(isDeterministic(a1));
assert(!isDeterministic(callRet));


parseAutomata("../../../../benchmarks/nwa/ProgramVerification-Ministerprasident.ats");
assert(isDeterministic(McCarthyAbstraction16));
assert(isDeterministic(Ackermann_Abstraction19));
assert(isDeterministic(Ackermann_Abstraction24));
assert(!isDeterministic(McCarthyInterpolantAutomaton_Iteration12));
assert(!isDeterministic(McCarthyInterpolantAutomaton_Iteration16));
assert(!isDeterministic(Ackermann_InterpolantAutomaton_Iteration39));