import edu.neu.ccs.demeter.dj.*; class Main { // Java Program with DJ X1 x1; Nx1 nx1; public static void main(String[] s) { ClassGraph cg = new ClassGraph(); Main m = new Main() ;// full Main object // comment these constructors out: // leave comment: Construct complete binary tree of depth 3 // with 8 leaf nodes of class Target m.x1 = new X1(); m.nx1 = new Nx1(); m.x1.x2 = new X2(); m.x1.nx2 = new Nx2(); m.nx1.x2 = new X2(); m.nx1.nx2 = new Nx2(); m.x1.x2.x3 = new X3(); m.x1.x2.nx3 = new Nx3(); m.x1.nx2.x3 = new X3(); m.x1.nx2.nx3 = new Nx3(); m.nx1.x2.x3 = new X3(); m.nx1.x2.nx3 = new Nx3(); m.nx1.nx2.x3 = new X3(); m.nx1.nx2.nx3 = new Nx3(); m.x1.x2.x3.target = new Target(); m.x1.x2.nx3.target = new Target(); m.x1.nx2.x3.target = new Target(); m.x1.nx2.nx3.target = new Target(); m.nx1.x2.x3.target = new Target(); m.nx1.x2.nx3.target = new Target(); m.nx1.nx2.x3.target = new Target(); m.nx1.nx2.nx3.target = new Target(); cg.traverse(m, "intersect(" + // union is expressed by concatenation of edges "{source: Main -> X1 X1 -> target: Target " + "source: Main ->Nx2 Nx2 -> target: Target " + "Main -> X3 X3 -> Target}," + "{source: Main -> Nx1 Nx1 -> target: Target " + "Main -> X2 X2 -> Target}," + "{source:Main -> X1 X1 -> target: Target}," + // "{source:Main -> Nx2 Nx2 -> target: Target}," + // added to make it unsatisfiable // // does not detect that it is unsatisfiable because DAJ implements intersection incorrectly? "{source:Main -> Nx3 Nx3 -> target: Target})", new Visitor(){ public void start (){System.out.println( " start traversal"); } public void finish (){System.out.println( " finish traversal"); } void before (Target host){System.out.println( host ); } void before (Nx3 host){System.out.println( host ); } void before (X2 host){System.out.println( host ); } void before (X1 host){System.out.println( host ); } } ); } } class X1 {X2 x2; Nx2 nx2; } class X2 {X3 x3; Nx3 nx3; } class X3 {Target target; } class Nx1 {X2 x2; Nx2 nx2; } class Nx2 {X3 x3; Nx3 nx3; } class Nx3 {Target target; } class Target {} // output // start traversal //X1@1efb836 //X2@126e85f //Nx3@8916a2 //Target@2ce908 // finish traversal