// nondeterministic NWA where smallest deterministic NWA for same langauge has
// 2^n^2 states.
// See JACM2009 paper, proof of Theorem 3.4
//
//
//
// Author: heizmann@informatik.uni-freiburg.de
// Date: 25.5.2010


assert(accepts(worstCaseDeterminizationk1, [s c<  "0" m "0" e   "0" >r "0"]));
assert(!accepts(worstCaseDeterminizationk1, [s c<  "1" m "1" e  "0" m "0" e  "1" m "1" e   "0" >r "1" ]));
assert(!accepts(worstCaseDeterminizationk1, [s c<  "0" m "1" e  "0" m "0" e  "1" m "1" e   "0" >r "1" ]));
assert(accepts(worstCaseDeterminizationk1, [s c<  "0" m "0" e  "0" m "1" e  "1" m "0" e   "0" >r "1"]));
NestedWordAutomaton determinized = determinize(worstCaseDeterminizationk1);
// We assume that sink state was added.
assert(numberOfStates(determinized) == 166);

assert(accepts(determinized, [s c<  "0" m "0" e  "0" m "1" e  "1" m "0" e   "0" >r "1"]));
assert(!accepts(complement(determinized), [s c<  "0" m "0" e  "0" m "1" e  "1" m "0" e   "0" >r "1"]));


NestedWordAutomaton worstCaseDeterminizationk1 = (
	callAlphabet = {c},
	internalAlphabet = {s "0" "1" m e},
	returnAlphabet = {r},
	states = {
		p
		p0 p1
		q0 q1   q0m q1m
		q
		r
		r0 r1
		s0 s1   s0m s1m
		s
		t0 t1
		t
	},
	initialStates = {p},
	finalStates = {t},
	callTransitions = {
		(p0 c q0) (p1 c q1)
	},
	internalTransitions = {
		(p s p0) (p s p1)
      
		(q0 "0" q0) (q0 "1" q0) (q1 "0" q1) (q1 "1" q1)
		(q0 m q0m) (q1 m q1m)
		(q0m "0" q0m) (q0m "1" q0m) (q1m "0" q1m) (q1m "1" q1m)
		(q0m e q0) (q1m e q1)
      
		(q0 "0" q) (q1 "1" q)
		(q m r)
      
		(r "0" r0) (r "1" r1)
 
		(r0 e s0) (r1 e s1)
      
		(s0 "0" s0) (s0 "1" s0) (s1 "0" s1) (s1 "1" s1)
		(s0 m s0m) (s1 m s1m)
		(s0m "0" s0m) (s0m "1" s0m) (s1m "0" s1m) (s1m "1" s1m)
		(s0m e s0) (s1m e s1)
      
		(s0 "0" s) (s1 "1" s)
      
		(t0 "0" t) (t1 "1" t)
	}, 
	returnTransitions = {
		(s p0 r t0) (s p1 r t1)
	}
);