package es.upm.babel.ccjml.samples.readerswriters.java;

public abstract class AReadersWriters implements ReadersWriters {

  protected /*@ spec_public @*/ int readers = 0;
  protected /*@ spec_public @*/ int writers = 0;
  
  //@ ensures \result == (writers  + readers == 0);  
  protected /*@ spec_public pure@*/ boolean cpreBeforeWrite() {
    return readers == 0 && writers == 0 ;
  }

  //@ ensures \result == (writers == 0);
  protected /*@ spec_public pure @*/boolean cpreBeforeRead() {
    return writers == 0;
  }
  
  @Override
  public String toString(){
    return "RW = [ reader = " + readers + " | writers= " + writers + "]";
  }
  
  /*@ ensures  \result == readers >= 0 && writers >= 0 &&
    @                     (readers > 0 ==> writers == 0) &&
    @                     (writers > 0 ==> readers == 0 && writers == 1);
    @*/     
  public boolean repOk(){
    return readers >= 0 && writers >= 0 &&
           ((readers > 0 && writers == 0) ||
           (writers > 0 && readers == 0 && writers == 1));
  }

}