// add Intersection and Negation
Main { {{
  static void p(String s){ System.out.println(s); }
  public static void main(String args[]) throws Exception {

    // to say that Node is a builtIn class
    edu.neu.ccs.demeterf.util.Util.addBuiltIn(Node.class);

    // for debugging traversals
    edu.neu.ccs.demeterf.util.Util.setDebug(true);

    Main m = Main.parse(System.in);
    m.well_formed();
    System.out.println(" done ");
  }
}}
}


WellFormedVis {
  {{ ClassGraph cg = new ClassGraph(true,false); }}
}

PathSpec { {{
  Boolean DJwff(ClassGraph cg){
    return (Boolean) cg.traverse(this,"from PathSpec to Simple", new Visitor(){
       Boolean wf;
       public Boolean getReturnValue() {return wf;}
       public void start() {wf = true;}
       public void after(Join j) {
         boolean b =  j.get_first().target().equals(j.get_second().source());
         wf = wf && b;
       }
       public void after(Merge m) {
         boolean source_equals =  
           m.get_first().source().equals(m.get_second().source());
         boolean target_equals =  
           m.get_first().target().equals(m.get_second().target());
           wf = wf && source_equals && target_equals;
       }

    });
  }
}} }



Main {
  void well_formed() to PathSpec (WellFormedVis);
}
WellFormedVis {
  before PathSpec {{ 
    Main.p(" input ================= ");
    host.print();
    boolean wff = host.well_formed();
    boolean wff2 = host.DemeterJwf();
    Boolean wff4 = host.DJwff(cg);
    Boolean wff3 = host.DemeterFwff();

    Main.p(" above path spec is well formed. follow-grammar: " + wff + " DemeterJ: " + wff2 + 
    " DemeterF: " + wff3 + " DJ: " + wff4);
    if ((wff != wff2) || (wff2 != wff3) || (wff3 != wff4)) 
      Main.p( "DIFFERENT RESULTS ====================!!!!!!!!! ");
  }}
}

PathSpec { {{
  Boolean DemeterFwff() {
    return new edu.neu.ccs.demeterf.Traversal(new WfCheck()).
          <Boolean> traverse(this);
  }
}} }

WfCheck { {{
  Boolean combine(Join j, Boolean fn, Boolean sn) {
    boolean b =  j.get_first().target().equals(j.get_second().source());
    return fn && sn && b;
    }
  Boolean combine(Merge m, Boolean fn, Boolean sn) {
    boolean source_equals =  
      m.get_first().source().equals(m.get_second().source());
    boolean target_equals =  
      m.get_first().target().equals(m.get_second().target());
    return fn & sn && source_equals && target_equals;
    }
  Boolean combine(Simple s, Node source, Node target) {
    return true; }
}}
}


*{ void print() to * (PrintVisitor);}
// new
PathSpec {
  boolean DemeterJwf() to Simple (WfVisitor);
}

// simulating an interposition variable with a stack
// NOT NEEDED
WfVisitor {
  {{ 
  Stack<Compound> enclosingC = new Stack<Compound>(); 
  public Compound currentEnclosingC()
     { return enclosingC.peek(); }
  }} 
  before Compound {{ enclosingC.push(host); }}
  after Compound {{ enclosingC.pop(); 
  }}
}

WfVisitor {
  Boolean get_return_val() {{ return new Boolean(wf); }}
  init {{ wf = true; }}

  after Join {{
    boolean b =  host.get_first().target().equals(host.get_second().source());
    wf = wf && b;
  }}

  after Merge {{
    boolean source_equals =  
      host.get_first().source().equals(host.get_second().source());
    boolean target_equals =  
      host.get_first().target().equals(host.get_second().target());
    boolean b = source_equals && target_equals;
    wf = wf && b;
  }}
}
// end new

//well-formed
PathSpec { {{ abstract boolean well_formed(); }} }
Simple { {{ boolean well_formed(){return true;} }} } //7
Compound { {{ // 8+9
  boolean well_formed_constituents(){
    return first.well_formed() && second.well_formed(); } }} }
Join { {{ //8
  boolean well_formed(){
    boolean b =  get_first().target().equals(get_second().source());
    Main.p(" check meeting point"); this.print(); Main.p(" result " + b);
    return b && well_formed_constituents();} }} }
Merge { {{ //9
  boolean well_formed(){
    boolean source_equals =  
      get_first().source().equals(get_second().source());
    boolean target_equals =  
      get_first().target().equals(get_second().target());
    Main.p(" check merge conditions"); this.print(); 
    Main.p(" result " + source_equals + target_equals);
    boolean both = first.well_formed() && second.well_formed();
    return source_equals && target_equals && well_formed_constituents();}
}} }

//source
PathSpec { {{ abstract Node source(); }} }
Simple { {{ Node source(){ return get_source();} }} } //1
Join { {{ Node source(){ return get_first().source();} }} } //2
Merge { {{ Node source(){ return get_first().source();} }} } //3

//target
PathSpec { {{ abstract Node target(); }} }
Simple { {{ Node target(){ return get_target();} }} } //4
Join { {{ Node target(){ return get_second().target();} }} } //5
Merge { {{ Node target(){ return get_second().target();} }} } //6

// uses equals on Node
Node { {{
   boolean equals(Node s){ 
     return this.get_v().equals(s.get_v());}
}} }