// Some automata from our SAS09 paper. No automaton contains calls or returns.
// Author: heizmann@informatik.uni-freiburg.de
// Date: 27.12.2010

assert(!isEmpty(Acontrol));
assert(!isEmpty(intersect(complement(A1), Acontrol)));
assert(!isEmpty(difference(Acontrol, A1)));

print(difference(Acontrol, A1));

NestedWordAutomaton Acontrol = (
  callAlphabet = { },
  internalAlphabet = { xto0 yto0 xInc xIsNegative yIsNegative},
  returnAlphabet = { },
  states = {l0 l1 l2 lerr},
  initialStates = {l0},
  finalStates = {lerr},
  callTransitions = {},
  internalTransitions = {(l0 xto0 l1) (l1 yto0 l2) (l2 xInc l2) (l2 xIsNegative lerr) (l2 yIsNegative lerr)}, 
  returnTransitions = {}
);

NestedWordAutomaton A1 = (
  callAlphabet = { },
  internalAlphabet = {xto0 yto0 xInc xIsNegative yIsNegative},
  returnAlphabet = { },
  states = {q0 q1 q2 q3 q4},
  initialStates = {q0},
  finalStates = {q4},
  callTransitions = {},
  internalTransitions = {(q0 xto0 q1) (q1 yto0 q2) (q2 xInc q2) (q2 xInc q3) (q3 xIsNegative q4)}, 
  returnTransitions = {}
);