// Example of a .fat file that is used in the documentation of the
// AutomataParser
// https://sotec.informatik.uni-freiburg.de/trac/ultimate/wiki/AutomataParser
// please do not change it.
// Author: heizmann@informatik.uni-freiburg.de
// Date: 7.3.2010
// Adapted & Extended by: musab@informatik.uni-freiburg.de
// Date: 9.02.2013

// The answer of the first test should be no, since every symbol of the nested 
// word aabb is an internal symbol.
assert(!accepts(a1, [a a b b]));
assert(accepts(a1, [a< a< >b >b]));


// A nested word automaton that has no internal transitions.
// This was the definition in the old syntax.
NestedWordAutomaton a1 = (
  callAlphabet = {a b},
  internalAlphabet = {a b},
  returnAlphabet = {a b},
  states = {q0 q1},
  initialStates = {q0},
  finalStates = {q1},
  callTransitions = {(q0 a q0) (q0 a q1)},
  internalTransitions = {}, 
  returnTransitions = {(q1 q0 b q1)}
);


// A nested word automaton, that represents a finite automaton. It accepts
// nested words that have only internal positions. The call alphabet and the 
// return alphabet are empty. 
assert(accepts(a2, [a a b b]));


NestedWordAutomaton a2 = (
 callAlphabet = { },
 internalAlphabet = {a b},
 returnAlphabet = { },
 states = {q0 q1},
 initialStates = {q0},
 finalStates = {q0},
 callTransitions = {},
 internalTransitions = {(q0 a q1) (q1 a q0) (q0 b q0) (q1 b q1)}, 
 returnTransitions = {}
);