/*
 * Example where the result of buchiDifferenceFKV is better than the result of
 * buchiDifferenceNCSB.
 * 
 * Date: 2015-12-18
 * Author: Matthias Heizmann
 */


// print(numberOfStates(nwa));
// print(isDeterministic(nwa));
// 
// NestedWordAutomaton cFKV = buchiComplementFKV(nwa);
// print(numberOfStates(cFKV));
// NestedWordAutomaton cFKVl = removeNonLiveStates(cFKV);
// print(numberOfStates(cFKVl));
// NestedWordAutomaton cDet = buchiComplementDeterministic(nwa);
// print(numberOfStates(cDet));
// NestedWordAutomaton cDetl = removeNonLiveStates(cDet);
// print(numberOfStates(cDetl));
// NestedWordAutomaton cNCSB = buchiComplementNCSB(nwa);
// print(numberOfStates(cNCSB));
// NestedWordAutomaton cNCSBl = removeNonLiveStates(nwa);
// print(numberOfStates(cNCSBl));

// NestedWordAutomaton dFKV = buchiComplementFKV(prg);
NestedWordAutomaton dFKV = buchiDifferenceFKV(prg, nwa);
print(numberOfStates(dFKV));
// print(numberOfTransitions(dFKV));
// print(dFKV);
NestedWordAutomaton dFKVl = removeNonLiveStates(dFKV);
print(numberOfStates(dFKVl));

// NestedWordAutomaton dNCSB = buchiComplementNCSB(prg);
NestedWordAutomaton dNCSB = buchiDifferenceNCSB(prg, nwa);
print(dNCSB);
print(numberOfStates(dNCSB));
// print(numberOfTransitions(dNCSB));
NestedWordAutomaton dNCSBl = removeNonLiveStates(dNCSB);
print(numberOfStates(dNCSBl));


NestedWordAutomaton nwa = (
	callAlphabet = { },
	internalAlphabet = {"p1" "p2" "fe" "a1" "a2" "a3" },
	returnAlphabet = { },
	states = {"l1" "l2" "l3" "l4" "l0" },
	initialStates = {"l0" },
	finalStates = {"l1" },
	callTransitions = {
	},
	internalTransitions = {
		("l0" "fe" "l1")
		("l1" "a1" "l2")
		("l2" "a2" "l3")
		("l3" "a3" "l4")
		("l4" "p1" "l1")
// 		("l4" "p2" "l1")
	},
	returnTransitions = {
	}
);

NestedWordAutomaton prg = (
	callAlphabet = { },
	internalAlphabet = {"p1" "p2" "fe" "a1" "a2" "a3" },
	returnAlphabet = { },
	states = {"l1" "l2" "l3" "l4"  "l0" },
	initialStates = {"l0" },
	finalStates = {"l1" "l2" "l3" "l4" "l0" },
	callTransitions = {
	},
	internalTransitions = {
		("l0" "fe" "l1")
		("l1" "a1" "l2")
		("l2" "a2" "l3")
		("l3" "a3" "l4")
		("l4" "p1" "l1")
 		("l4" "p2" "l1")
	},
	returnTransitions = {
	}
);