These screenshots show Korat's visualization of generated structures. The specific example illustrates how visualization can assist users in correcting repOk (invariant) methods. The example considers a simple binary tree. The first incorrect repOk only checks that every node reachable from itself is not reachable from the root. While this prevents cycles, it does allow sharing (and effectively checks that the input structure is a DAG).