// Date: May 2014
// Matthias Heizmann
// typical(?) Büchi interpolant automaton that is not easy to complement

buchiComplementFKV(bia);

NestedWordAutomaton bia = (
  callAlphabet = { },
  internalAlphabet = { "a" "b" },
  returnAlphabet = { },
  states = {s0 s1 l0 l1 l2 l3 l4 l5 l6 l7 l8 l9 sink afterSink},
  initialStates = {s0},
  finalStates = {l0 afterSink},
  callTransitions = { },
  internalTransitions = { 
    (s0 "a" s1) 
	(s1 "b" s0) 
    (s1 "b" l0) 
    (l0 "a" l1)
    (l1 "b" l2)
    (l2 "a" l3)
    (l3 "b" l0)
	    (l3 "a" sink)
		(sink "a" sink)
		(sink "b" sink)
		(sink "a" afterSink)
    (l4 "a" l5)
    (l5 "b" l6)
    (l6 "a" l7)
    (l7 "b" l8)
    (l8 "a" l9)
    (l9 "b" l0)
  }, 
  returnTransitions = { }
);
//7591 states and 18770In 0Ca 0Re transitions.
//3838 states and 4990In 0Ca 0Re transitions