// Author: heizmann@informatik.uni-freiburg.de
// Date: 11.06.2013 (Guardian published story about PRISM few days before)


// This file contains some automaton definitions produced by proving
// termination of the Boogie program wrongBFS.bpl using Büchi Automizer
// in revision r9053. 

NestedWordAutomaton complement1 = buchiComplementFKV(InterpolantAutomatonBuchi1);
NestedWordAutomaton difference1 = buchiIntersect(BuchiCegarLoopAbstraction0, complement1);
NestedLassoWord nw1 = [ a4 c0<,  a0 a1 c1<  ];
//NestedLassoWord nw1 = [ a4 c0<,  a0 a2 a3 >r0 a6 a7  ];
assert(buchiAccepts(BuchiCegarLoopAbstraction0, nw1));
assert(buchiAccepts(InterpolantAutomatonBuchi1, nw1));
assert(!buchiAccepts(complement1, nw1));

// assert(!buchiIsEmpty(complement1));
// assert(!buchiIsEmpty(BuchiCegarLoopAbstraction0));
// assert(!buchiIsEmpty(difference1));

// NestedWordAutomaton complement2 = buchiComplementFKV(InterpolantAutomatonBuchi2);
// NestedWordAutomaton difference2 = buchiIntersect(difference1, complement2);
// assert(!buchiIsEmpty(difference2));
// NestedWordAutomaton complement3 = buchiComplementFKV(InterpolantAutomatonBuchi3);
// NestedWordAutomaton difference3 = buchiIntersect(difference2, complement3);
// assert(!buchiIsEmpty(difference3));
// NestedWordAutomaton complement4 = buchiComplementFKV(InterpolantAutomatonBuchi4);
// NestedWordAutomaton difference4 = buchiIntersect(difference3, complement4);
// assert(!buchiIsEmpty(difference4));
// NestedWordAutomaton complement5 = buchiComplementFKV(InterpolantAutomatonBuchi5);
// NestedWordAutomaton difference5 = buchiIntersect(difference4, complement5);
// assert(buchiIsEmpty(difference5));


// Testfile dumped by Ultimate at 2013/06/11 13:49:38



NestedWordAutomaton BuchiCegarLoopAbstraction0 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 },
	initialStates = {s0 s9 },
	finalStates = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 },
	callTransitions = {
		 (s8 c1 s9)
		 (s10 c0 s9)
	},
	internalTransitions = {
		 (s0 a4 s10)
		 (s1 a5 s6)
		 (s1 a6 s3)
		 (s2 a3 s5)
		 (s3 a7 s4)
		 (s7 a1 s8)
		 (s7 a2 s2)
		 (s9 a0 s7)
	},
	returnTransitions = {
		 (s5 s10 r0 s1)
		 (s5 s8 r1 s2)
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:54



NestedWordAutomaton InterpolantAutomatonBuchi1 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 },
	initialStates = {s2 },
	finalStates = {s0 },
	callTransitions = {
		 (s1 c1 s1)
		 (s2 c0 s2)
	},
	internalTransitions = {
		 (s0 a1 s1)
		 (s1 a0 s0)
		 (s2 a0 s0)
		 (s2 a4 s2)
	},
	returnTransitions = {
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:56



NestedWordAutomaton InterpolantAutomatonBuchi2 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 },
	initialStates = {s2 },
	finalStates = {s1 },
	callTransitions = {
		 (s0 c1 s0)
	},
	internalTransitions = {
		 (s0 a0 s1)
		 (s1 a1 s0)
		 (s2 a0 s1)
	},
	returnTransitions = {
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:58



NestedWordAutomaton InterpolantAutomatonBuchi3 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 },
	initialStates = {s0 },
	finalStates = {s1 },
	callTransitions = {
		 (s1 c1 s2)
	},
	internalTransitions = {
		 (s0 a0 s0)
		 (s0 a1 s1)
		 (s2 a0 s3)
		 (s3 a1 s1)
	},
	returnTransitions = {
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:50:00



NestedWordAutomaton InterpolantAutomatonBuchi4 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 },
	initialStates = {s2 },
	finalStates = {s1 },
	callTransitions = {
		 (s0 c1 s1)
		 (s2 c1 s1)
	},
	internalTransitions = {
		 (s0 a1 s0)
		 (s1 a0 s0)
		 (s2 a0 s2)
		 (s2 a1 s2)
	},
	returnTransitions = {
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:50:01



NestedWordAutomaton InterpolantAutomatonBuchi5 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 },
	initialStates = {s0 },
	finalStates = {s1 },
	callTransitions = {
		 (s1 c1 s2)
	},
	internalTransitions = {
		 (s0 a0 s0)
		 (s0 a1 s1)
		 (s2 a0 s3)
		 (s3 a1 s1)
	},
	returnTransitions = {
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:54



NestedWordAutomaton Abstraction1 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 },
	initialStates = {s8 s13 },
	finalStates = {s0 s1 s4 s5 s6 s7 s8 s9 s13 },
	callTransitions = {
		 (s3 c1 s9)
		 (s10 c0 s9)
		 (s11 c0 s8)
		 (s12 c1 s8)
	},
	internalTransitions = {
		 (s2 a1 s3)
		 (s2 a1 s12)
		 (s2 a2 s5)
		 (s4 a5 s1)
		 (s4 a6 s6)
		 (s5 a3 s0)
		 (s6 a7 s7)
		 (s8 a0 s2)
		 (s13 a4 s10)
		 (s13 a4 s11)
	},
	returnTransitions = {
		 (s0 s11 r0 s4)
		 (s0 s12 r1 s5)
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:56



NestedWordAutomaton Abstraction2 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 },
	initialStates = {s4 s13 },
	finalStates = {s1 s4 s5 s6 s7 s8 s9 s10 s13 },
	callTransitions = {
		 (s0 c0 s1)
		 (s2 c1 s4)
		 (s3 c0 s4)
		 (s11 c1 s1)
	},
	internalTransitions = {
		 (s4 a0 s12)
		 (s5 a3 s10)
		 (s6 a5 s9)
		 (s6 a6 s8)
		 (s8 a7 s7)
		 (s12 a1 s2)
		 (s12 a1 s11)
		 (s12 a2 s5)
		 (s13 a4 s0)
		 (s13 a4 s3)
	},
	returnTransitions = {
		 (s10 s3 r0 s6)
		 (s10 s2 r1 s5)
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:49:58



NestedWordAutomaton Abstraction3 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 },
	initialStates = {s2 s16 },
	finalStates = {s1 s2 s9 s10 s12 s14 s15 s16 s17 s18 },
	callTransitions = {
		 (s0 c1 s1)
		 (s4 c0 s1)
		 (s5 c0 s10)
		 (s7 c1 s2)
		 (s7 c1 s18)
		 (s11 c1 s10)
	},
	internalTransitions = {
		 (s1 a0 s6)
		 (s2 a0 s3)
		 (s2 a0 s8)
		 (s3 a1 s7)
		 (s3 a2 s13)
		 (s6 a1 s0)
		 (s6 a1 s11)
		 (s6 a2 s13)
		 (s8 a2 s13)
		 (s12 a7 s14)
		 (s13 a3 s15)
		 (s16 a4 s4)
		 (s16 a4 s5)
		 (s17 a5 s9)
		 (s17 a6 s12)
		 (s18 a0 s8)
	},
	returnTransitions = {
		 (s15 s4 r0 s17)
		 (s15 s0 r1 s13)
		 (s15 s7 r1 s13)
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:50:00



NestedWordAutomaton Abstraction4 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 },
	initialStates = {s13 s18 },
	finalStates = {s0 s1 s2 s3 s5 s8 s12 s13 s16 s18 },
	callTransitions = {
		 (s4 c0 s5)
		 (s6 c1 s5)
		 (s10 c1 s12)
		 (s10 c1 s13)
		 (s11 c0 s8)
		 (s15 c1 s8)
	},
	internalTransitions = {
		 (s3 a7 s1)
		 (s7 a2 s17)
		 (s8 a0 s9)
		 (s9 a1 s6)
		 (s9 a1 s15)
		 (s9 a2 s17)
		 (s12 a0 s7)
		 (s13 a0 s7)
		 (s13 a0 s14)
		 (s14 a1 s10)
		 (s14 a2 s17)
		 (s16 a5 s0)
		 (s16 a6 s3)
		 (s17 a3 s2)
		 (s18 a4 s4)
		 (s18 a4 s11)
	},
	returnTransitions = {
		 (s2 s11 r0 s16)
		 (s2 s10 r1 s17)
		 (s2 s15 r1 s17)
	}
);
// Testfile dumped by Ultimate at 2013/06/11 13:50:02



NestedWordAutomaton Abstraction5 = (
	callAlphabet = {c0 c1 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {r0 r1 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 },
	initialStates = {s13 s3 },
	finalStates = {s0 s2 s3 s9 s10 s11 },
	callTransitions = {
		 (s4 c0 s17)
		 (s5 c0 s6)
		 (s7 c1 s6)
		 (s15 c1 s13)
		 (s15 c1 s14)
		 (s18 c1 s17)
	},
	internalTransitions = {
		 (s0 a7 s10)
		 (s1 a3 s11)
		 (s2 a5 s9)
		 (s2 a6 s0)
		 (s3 a4 s4)
		 (s3 a4 s5)
		 (s8 a2 s1)
		 (s12 a1 s15)
		 (s12 a2 s1)
		 (s13 a0 s12)
		 (s13 a0 s8)
		 (s14 a0 s8)
		 (s16 a1 s18)
		 (s16 a1 s7)
		 (s16 a2 s1)
		 (s17 a0 s16)
	},
	returnTransitions = {
		 (s11 s4 r0 s2)
		 (s11 s15 r1 s1)
		 (s11 s18 r1 s1)
	}
);