class Counter {
  var value: int;

  invariant acc(value) && old(value)<=value;
}

class Program {

  method main1(){
    var counter := new Counter;
    counter.value := 0;
    share counter;

    acquire counter;
    var tmp1 := counter.value;
    release counter;
    
    acquire counter;
    var tmp2 := counter.value;
    release counter;

    assert tmp1 <= tmp2;
  }

  method main2(){
    var counter := new Counter;
    counter.value := 0;
    share counter;

    acquire counter;
    release counter;

    call bar(counter);
  }

  method bar(c: Counter)
    requires c!=null && acc(c.mu) && waitlevel << c.mu;
    requires eval(c.release, acc(c.value) && 0<=c.value);
  {
    lock (c) {
      assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
    }
  }

  method main3() returns (counter: Counter)
    lockchange counter;
  {
    counter := new Counter;
    counter.value := 0;
    share counter;
    acquire counter;
    call doRelease(counter, counter.value);
  }

  method doRelease(c: Counter, i: int)
    requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
    lockchange c;
  {
    release c; // ok, because of atAcquire conjunct in the precondition
  }

  method main4(){
    var counter := new Counter;
    counter.value := 0;
    share counter;

    acquire counter;
    counter.value := counter.value - 1;
    release counter;  // error: should fail
  }

  method main5(){
    var counter := new Counter;
    counter.value := 10;
    share counter;

    call foo(counter);

    unshare counter;
    assert 10<=counter.value; // error: should fail
  }

  method foo(c: Counter)
    requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);
    ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);
    lockchange c;
  {
    acquire c;
    unshare c;
    c.value := 5;
    share c;
    acquire c;
  }

  method nestedGood0(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    lock (c) {
      release c
      acquire c
    }
  }

  method nestedGood1(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    var t: Counter := c
    lock (t) {
      t := new Counter
      share t
      acquire t
    }  // this line releases the original value for t
    release t
  }

  method nestedBad0(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    lock (c) {
      release c
    }  // error: no longer holds c
  }

  method nestedBad1(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    lock (c) {
      acquire c  // error: already holds c
    }
  }

  method nestedBad2(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    lock (c) {
      lock (c) {  // error: already holds c
      }
    }
  }

  method nestedBad3(c: Counter)
    requires c != null && acc(c.mu) && waitlevel << c.mu;
  {
    var t: Counter := c
    lock (t) {
      release t
      t := new Counter
      share t
      acquire t
    }  // error: this line attempts to release the original t
  }
}