// Amod2 accepts all binary numbers that are divisible by two.
// Amod3 accepts all binary numbers that are divisible by three.
// Author: heizmann@informatik.uni-freiburg.de
// Date: 19.12.2011

assert(accepts(Amod3, [ "0" "0" "0" ]));
assert(accepts(Amod3, [ "0" "1" "1" ]));
assert(accepts(Amod3, [ "1" "1" "0" ]));
assert(accepts(Amod3, [ "1" "0" "0" "1" ]));
assert(!accepts(Amod3, [ "1" "0" "0" "0" ]));
assert(!accepts(Amod3, [ "1" "0" "1" "0" ]));
assert(!accepts(Amod3, [ "1" "1" "0" "0" "1" "0" "1" ]));
assert(isEmpty(difference(difference(Amod2, complement(Amod3)), intersect(Amod2, Amod3))));
assert(isEmpty(difference(intersect(Amod2, Amod3), difference(Amod2, complement(Amod3)) )));

assert(isEmpty(intersect(
  intersect(Amod2, Amod3),
  complement(difference(Amod2, complement(Amod3)))
)));

assert(isEmpty(intersect(
  complement(difference(Amod2, complement(Amod3))),
  intersect(Amod2, Amod3)
)));


//print(intersect(Amod2 Amod3));
print(difference(Amod2, complement(Amod3)));

NestedWordAutomaton Amod3 = (
  callAlphabet = { },
  internalAlphabet = { "0" "1" },
  returnAlphabet = { },
  states = {q0 q1 q2 },
  initialStates = {q0},
  finalStates = {q0},
  callTransitions = {},
  internalTransitions = {
	(q0 "0" q0)
	(q0 "1" q1)
	(q1 "0" q2)
	(q1 "1" q0)
	(q2 "0" q1)
	(q2 "1" q2)},
  returnTransitions = {}
);

NestedWordAutomaton Amod2 = (
  callAlphabet = { },
  internalAlphabet = { "0" "1"},
  returnAlphabet = { },
  states = {p0 p1},
  initialStates = {p0},
  finalStates = {p0},
  callTransitions = {},
  internalTransitions = {
	(p0 "0" p0)
	(p0 "1" p1)
	(p1 "0" p0)
	(p1 "1" p1)},
  returnTransitions = {}
);