// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

class Node {
  var left: Node;
  var right: Node;
  var parent: Node;
  var anc: set<Node>;
  var desc: set<Node>;
  var sense: bool;
  var pc: int;


  function validDown(): bool
    reads this, desc;    
  {
    this !in desc &&
    null !in desc &&
    left != right &&  // not needed, but speeds up verification

    (right != null ==> right in desc && left !in right.desc) &&

    (left != null ==> 
      left in desc && 
      (right != null ==> desc == {left,right} + left.desc + right.desc)  &&
      (right == null ==> desc == {left} + left.desc)  &&
      left.validDown()) &&
    (left == null ==> 
      (right != null ==> desc == {right} + right.desc)  &&
      (right == null ==> desc == {})) &&

    (right != null ==> right.validDown()) &&

    (blocked() ==> forall m :: m in desc ==> m.blocked()) &&
    (after() ==> forall m :: m in desc ==> m.blocked() || m.after())
//    (left != null && right != null ==> left.desc !! right.desc)  // not needed
  }




  function  validUp(): bool
    reads this, anc;    
  {
    this !in anc &&
    null !in anc &&
    (parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) &&
    (parent == null ==> anc == {}) &&
    (after() ==> forall m :: m in anc ==> m.after())
  }

  function valid(): bool
    reads this, desc, anc;
  { validUp() && validDown() && desc !! anc }

  function before(): bool
    reads this;
  { !sense && pc <= 2 }

  function blocked(): bool
    reads this;
  { sense }

  function after(): bool
    reads this;
  { !sense && 3 <= pc }


  method barrier()
    requires valid();
    requires before();
    modifies this, left, right;
    decreases *;  // allow the method to not terminate
  {
//A
    pc := 1;
    if(left != null) {
      while(!left.sense) 
        modifies left;
        invariant validDown(); // this seems necessary to get the necessary unfolding of functions
        invariant valid();
        decreases *;  // to by-pass termination checking for this loop
      {
        // this loop body is supposed to model what the "left" thread
        // might do to its node. This body models a transition from
        // "before" to "blocked" by setting sense to true. A transition
        // all the way to "after" is not permitted; this would require
        // a change of pc.
        // We assume that "left" preserves the validity of its subtree,
        // which means in particular that it goes to "blocked" only if
        // all its descendants are already blocked.
        left.sense := *; 
        assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked();
      }  
    }
    if(right != null) {
      while(!right.sense) 
        modifies right;
        invariant validDown(); // this seems necessary to get the necessary unfolding of functions
        invariant valid();
        decreases *;  // to by-pass termination checking for this loop
      {
        // analogous to the previous loop
        right.sense := *; 
        assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked();
      }  
    }

//B
    pc := 2;
    if(parent != null) {
      sense := true; 
    }
//C
    pc := 3;
    while(sense)
        modifies this;
        invariant validUp(); // this seems necessary to get the necessary unfolding of functions
        invariant valid();
        invariant left == old(left);
        invariant right == old(right);
        invariant sense ==> parent != null;
        decreases *;  // to by-pass termination checking for this loop
    {
      // this loop body is supposed to model what the "parent" thread
      // might do to its node. The body models a transition from
      // "blocked" to "after" by setting sense to false.
      // We assume that "parent" initiates this transition only
      // after it went to state "after" itself.
      sense := *;
      assume !sense ==> parent.after();
    }
//D
    pc := 4;
    if(left != null) {
      left.sense := false;
    }
//E
    pc := 5;
    if(right != null) {
      right.sense := false;
    }
//F
    pc := 6;
  }
}