// NWA where several call transitions and return transitions are needed to
// reach the final state.
// Author: heizmann@informatik.uni-freiburg.de
// Date: 3.8.2010

assert(accepts(determinize(a1), [b a< a >b]));
assert(!accepts(a1, [a a a b]));
assert(!accepts(determinize(a1), [a a a b]));
assert(!isEmpty(a1));
assert(!isEmpty(determinize(a1)));
assert(!isEmpty(difference(all, a1)));
assert(!isEmpty(intersect(all, complement(a1))));
assert(!isEmpty(difference(all, difference(all, a1))));
assert(!isEmpty(intersect(all, complement(intersect(all, complement(a1))))));

assert(!accepts(a1, [a a<]));
assert(!accepts(complement(a1), [b a< a >b]));
assert(accepts(all, [a a<]));
assert(!accepts(intersect(all, complement(a1)), [b a< a >b]));
assert(!accepts(complement(intersect(all, complement(a1))), [a a<]));
assert(!accepts(intersect(all, complement(intersect(all, complement(a1)))), [a a<]));
assert(accepts(difference(all, difference(all, a1)), []));

assert(isEmpty(difference(callRet, callRet)));

print(difference(all, difference(all, a1)));

NestedWordAutomaton all = (
  callAlphabet = {a b},
  internalAlphabet = {a b},
  returnAlphabet = {a b},
  states = {s},
  initialStates = {s},
  finalStates = {s},
  callTransitions = {(s a s)},
  internalTransitions = {(s a s)}, 
  returnTransitions = {(s s a s)}
);


NestedWordAutomaton a1 = (
  callAlphabet = {a b},
  internalAlphabet = {a b},
  returnAlphabet = {a b},
  states = {s0 s1 p1 p2},
  initialStates = {s0},
  finalStates = {s0},
  callTransitions = {
    (s1 a p1)
  },
  internalTransitions = {
    (s0 b s1) (p1 a p2)
  }, 
  returnTransitions = {
    (p2 s1 b s0)
  }
);



NestedWordAutomaton callRet = (
  callAlphabet = {a b},
  internalAlphabet = {a b},
  returnAlphabet = {a b},
  states = {q0 q1 q2 q3 q4 q5 q6 q8 q9 s0 s1 s2 s3 r0 r1 p},
  initialStates = {q0},
  finalStates = {p},
  callTransitions = {
      (q0 a q1)
      (q0 a s0) (q6 a s0) (q5 a s0)
      (s0 a r0) (s2 a r0)
  },
  internalTransitions = {
      (q0 a q1) (q1 a q2) (q2 a q3) (q3 a q4) (q4 a q5) (q5 a q6) (q5 a q5)
      (s0 a s1) (s1 a s2)
      (r0 a r1)
      (s0 a s3)
    
  }, 
  returnTransitions = {
      (r1 s0 a s3)
      (s3 q5 a q8) (s3 q6 a q9)
      (q9 q0 a p)
  }
);