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

parseAutomata("buchiComplement/ba/TerminationTraceAbstractionBlueGreen.ats");

assert(!buchiIsEmpty(controlAutomaton));
assert(buchiAccepts(controlAutomaton, [blue, blue]));
assert(buchiAccepts(interpolantAutomaton1, [blue, blue]));

NestedWordAutomaton diff1 = buchiDifferenceFKV(controlAutomaton, interpolantAutomaton1);
assert(!buchiIsEmpty(diff1));
assert(buchiAccepts(diff1, [ green, blue blue]));
assert(buchiAccepts(interpolantAutomaton2, [ green, blue blue]));

NestedWordAutomaton diff2 = buchiDifferenceFKV(diff1, interpolantAutomaton2);
assert(!buchiIsEmpty(diff2));
assert(buchiAccepts(diff2, [ green, green green]));
assert(buchiAccepts(interpolantAutomaton3, [ green, green green]));

NestedWordAutomaton diff3 = buchiDifferenceFKV(diff2, interpolantAutomaton3);
assert(!buchiIsEmpty(diff3));
assert(buchiAccepts(diff3, [blue green, blue blue ]));
assert(buchiAccepts(interpolantAutomaton4, [blue green, blue blue ]));

NestedWordAutomaton diff4 = buchiDifferenceFKV(diff3, interpolantAutomaton4);
assert(!buchiIsEmpty(diff4));
assert(buchiAccepts(diff4, [blue blue green, green blue green green ]));
assert(buchiAccepts(interpolantAutomaton5, [blue blue green, green blue green green ]));

NestedWordAutomaton diff5 = buchiDifferenceFKV(diff4, interpolantAutomaton5);
assert(!buchiIsEmpty(diff5));
assert(buchiAccepts(diff5, [blue blue green, blue blue blue green ]));
assert(buchiAccepts(interpolantAutomaton6, [blue blue green, blue blue blue green ]));

NestedWordAutomaton diff6 = buchiDifferenceFKV(diff5, interpolantAutomaton6);
assert(buchiIsEmpty(diff6));