% java daikon.Daikon -o hanoi.inv Hanoi.dtrace Hanoi.*.decls
% java daikon.PrintInvariants --suppress_post hanoi.inv
===========================================================================
Hanoi:::OBJECT
Hanoi.stackA[] contains no duplicates
Hanoi.stackA[] elements != null
Hanoi.stackB[] contains no duplicates
Hanoi.stackB[] elements != null
Hanoi.stackC[] contains no duplicates
Hanoi.stackC[] elements != null
size(Hanoi.stackC[]) == - size(Hanoi.stackA[]) - size(Hanoi.stackB[]) + 5
===========================================================================
Hanoi.putOnA():::ENTER
===========================================================================
Hanoi.putOnA():::EXIT
size(Hanoi.stackA[])-1 == orig(size(Hanoi.stackA[]))
size(Hanoi.stackA[]) >= 1
orig(Hanoi.stackA[]) is a subsequence of Hanoi.stackA[]
Hanoi.stackB[] is a subsequence of orig(Hanoi.stackB[])
Hanoi.stackC[] is a subsequence of orig(Hanoi.stackC[])
size(Hanoi.stackB[]) <= orig(size(Hanoi.stackB[]))
size(Hanoi.stackC[]) <= orig(size(Hanoi.stackC[]))
orig(size(Hanoi.stackC[])) == - size(Hanoi.stackA[]) - orig(size(Hanoi.stackB[])) + 6
===========================================================================
Hanoi.putOnB():::ENTER
===========================================================================
Hanoi.putOnB():::EXIT
size(Hanoi.stackB[])-1 == orig(size(Hanoi.stackB[]))
size(Hanoi.stackB[]) >= 1
Hanoi.stackA[] is a subsequence of orig(Hanoi.stackA[])
orig(Hanoi.stackB[]) is a subsequence of Hanoi.stackB[]
Hanoi.stackC[] is a subsequence of orig(Hanoi.stackC[])
size(Hanoi.stackA[]) <= orig(size(Hanoi.stackA[]))
size(Hanoi.stackC[]) <= orig(size(Hanoi.stackC[]))
orig(size(Hanoi.stackC[])) == - size(Hanoi.stackB[]) - orig(size(Hanoi.stackA[])) + 6
===========================================================================
Hanoi.putOnC():::ENTER
===========================================================================
Hanoi.putOnC():::EXIT
size(Hanoi.stackC[])-1 == orig(size(Hanoi.stackC[]))
size(Hanoi.stackC[]) >= 1
Hanoi.stackA[] is a subsequence of orig(Hanoi.stackA[])
Hanoi.stackB[] is a subsequence of orig(Hanoi.stackB[])
orig(Hanoi.stackC[]) is a subsequence of Hanoi.stackC[]
size(Hanoi.stackA[]) <= orig(size(Hanoi.stackA[]))
size(Hanoi.stackB[]) <= orig(size(Hanoi.stackB[]))
orig(size(Hanoi.stackB[])) == - size(Hanoi.stackC[]) - orig(size(Hanoi.stackA[])) + 6
===========================================================================
Hanoi.start():::ENTER
size(Hanoi.stackA[]) == size(Hanoi.stackB[]) == size(Hanoi.stackC[])
Hanoi.stackA[] == []
Hanoi.stackB[] == []
Hanoi.stackC[] == []
size(Hanoi.stackA[]) == 0
===========================================================================
Hanoi.start():::EXIT
orig(size(Hanoi.stackA[])) == orig(size(Hanoi.stackB[])) == orig(size(Hanoi.stackC[]))
size(Hanoi.stackA[]) one of { 0, 5 }
size(Hanoi.stackB[]) one of { 0, 5 }
size(Hanoi.stackC[]) one of { 0, 5 }