/*
 * Small example where we can see that the Lazy-S optimization can
 * produce smaller results than the original NCSB algorithm.
 *
 * The orignal NCSB produces a complement with 12 states.
 * Using the Lazy-S optimization we can save two states.
 * 
 * 
 * Date: 2017-08-31
 * Author: Yong Li (李勇), Matthias Heizmann
 */


NestedWordAutomaton complementNCSB = buchiComplementNCSB(ba);
print(numberOfStates(complementNCSB));
assert(numberOfStates(complementNCSB) == 12);
print(numberOfTransitions(complementNCSB));
assert(numberOfTransitions(complementNCSB) == 26);

NestedWordAutomaton complementNCSBLazy3 = buchiComplementNCSBLazy3(ba);
print(numberOfStates(complementNCSBLazy3));
assert(numberOfStates(complementNCSBLazy3) == 10);
print(numberOfTransitions(complementNCSBLazy3));
assert(numberOfTransitions(complementNCSBLazy3) == 23);

NestedWordAutomaton complementNCSBLazy2 = buchiComplementNCSBLazy2(ba);
print(numberOfStates(complementNCSBLazy2));
assert(numberOfStates(complementNCSBLazy2) == 11);
print(numberOfTransitions(complementNCSBLazy2));
assert(numberOfTransitions(complementNCSBLazy2) == 26);

NestedWordAutomaton complementHeiMat2 = buchiComplementFKV(ba, "HEIMAT2", 77);
print(numberOfStates(complementHeiMat2));
assert(numberOfStates(complementHeiMat2) == 23);
print(numberOfTransitions(complementHeiMat2));
assert(numberOfTransitions(complementHeiMat2) == 56);

NestedWordAutomaton complementElastic = buchiComplementFKV(ba, "ELASTIC", 77);
print(numberOfStates(complementElastic));
assert(numberOfStates(complementElastic) == 23);
print(numberOfTransitions(complementElastic));
assert(numberOfTransitions(complementElastic) == 51);

NestedWordAutomaton complementSchewe = buchiComplementFKV(ba, "SCHEWE", 77);
print(numberOfStates(complementSchewe));
assert(numberOfStates(complementSchewe) == 23);
print(numberOfTransitions(complementSchewe));
assert(numberOfTransitions(complementSchewe) == 63);



FiniteAutomaton ba = (
	alphabet = {a b},
	states = {s0 s1 s2 s3},
	initialStates = {s0},
	finalStates = {s1 s2},
	transitions = {
		(s0 a s0)
		(s0 b s0)
		(s0 b s1)
		(s1 a s3)
		(s1 b s2)
		(s2 b s3)
		(s3 a s3)
		(s3 b s1)
	}
);