---

BSLObserver.java

// Environment consists of 
//  - a thread that non-deterministically adds and deletes observers 
//    for an observable
//  - a thread that repeatedly changes the observables state
//
// This environment can be scaled to vary the number of observers, NUM_O, and
// observables, NUM_S.
//
import edu.ksu.cis.bandera.abstraction.Abstraction;

public class BSLObserver {
    public static void main(String[] args) {
                Subject s = new Subject();
        new SubjectThread(s).start();

        Watcher w1 = new Watcher();
        Watcher w2 = new Watcher();
               
                Watcher w;
        while (true) {
                  if (edu.ksu.cis.bandera.abstraction.Abstraction.choose()) {
            w = w1;
                  } else {
            w = w2;
                  }
          s.addObserver(w);
          s.deleteObserver(w);
                }

    }
}

class SubjectThread extends Thread {
    Subject s;
    public SubjectThread(Subject s) {
        this.s = s;
    }
    public void run() {
          while (true) s.changeState();
    }
}

//class Subject extends Observable {
class Subject {
    public void changeState() {
        setChanged();
        notifyObservers();
    }

// copied from Observable
    protected boolean changed = false;
    protected Vector obs;
    public Subject() {
        obs = new Vector();
    }

        /**
          * @observable 
          *   RETURN end (this, Watcher watcher): watcher == o;
          */              
    public synchronized void addObserver(Watcher o) {
        if (!obs.contains(o)) {
            obs.addElement(o);
        }
    }
    protected synchronized void clearChanged() {
        changed = false;
    }
    public synchronized int countObservers() {
        return obs.size();
    }
        /**
          * @observable
          *   INVOKE begin (this, Watcher watcher): watcher == o;
          */              
    public synchronized void deleteObserver(Watcher o) {
        obs.removeElement(o);
    }
    public synchronized void deleteObservers() {
        obs.removeAllElements();
    }
    public synchronized boolean hasChanged() {
        return changed;
    }
    public void notifyObservers() {
        notifyObservers(null);
    }

            /* COMMENT FROM java.util.Observer
             *
             * We don't want the Observer doing callbacks  
             * into arbitrary code while holding its own Monitor.
             * The code where we extract each Observable from
             * the Vector and store the state of the Observer
             * needs synchronization, but notifying observers
             * does not (should not).  The worst result of any
             * potential race-condition here is that:
             * 1) a newly-added Observer will miss a
             *   notification in progress
             * 2) a recently unregistered Observer will be
             *   wrongly notified when it doesn't care
             */

        /**
          * @observable
          *   INVOKE begin (this);
          *   RETURN end (this);
          * @assert
          *   LOCATION[point] inWindow : false;
          */              
          //   LOCATION[point] inWindow (this, Watcher w): w == cw;
    public void notifyObservers(Object arg) {
                Watcher cw;
        Object[] arrLocal;
        synchronized (this) {
            if (!changed)
                return;
            arrLocal = obs.toArray();
            changed = false;
        }
        if (obs.size() != arrLocal.length) {
point:            cw = null;
                }
        for (int i = arrLocal.length - 1; i >= 0; i--) {
           cw = (Watcher) arrLocal[i];
           ((Watcher) arrLocal[i]).update(this, arg);
                }  
    }
    protected synchronized void setChanged() {
        changed = true;
        }
}

//class Watcher implements Observer {
class Watcher {
        /**
          * @observable 
          *   INVOKE begin (this, Subject subject): subject == o;
          */              
    public void update(Subject o, Object arg) { }
}

interface Observer {
        /**
          * @observable
          *   INVOKE begin (this, Observable subject): subject == o;
          */              
    public void update(Observable o, Object arg);
}

class Observable {
    protected boolean changed = false;
    protected Vector obs;
    public Observable() {
        obs = new Vector();
    }

        /**
          * @observable 
          *   RETURN end (this, Observer watcher): watcher == o;
          */              
    public synchronized void addObserver(Observer o) {
        if (!obs.contains(o)) {
            obs.addElement(o);
        }
    }
    protected synchronized void clearChanged() {
        changed = false;
    }
    public synchronized int countObservers() {
        return obs.size();
    }
        /**
          * @observable
          *   INVOKE begin (this, Observer watcher): watcher == o;
          */              
    public synchronized void deleteObserver(Observer o) {
        obs.removeElement(o);
    }
    public synchronized void deleteObservers() {
        obs.removeAllElements();
    }
    public synchronized boolean hasChanged() {
        return changed;
    }
    public void notifyObservers() {
        notifyObservers(null);
    }

            /* COMMENT FROM java.util.Observer
             *
             * We don't want the Observer doing callbacks  
             * into arbitrary code while holding its own Monitor.
             * The code where we extract each Observable from
             * the Vector and store the state of the Observer
             * needs synchronization, but notifying observers
             * does not (should not).  The worst result of any
             * potential race-condition here is that:
             * 1) a newly-added Observer will miss a
             *   notification in progress
             * 2) a recently unregistered Observer will be
             *   wrongly notified when it doesn't care
             */

        /**
          * @observable
          *   INVOKE begin (this);
          *   RETURN end (this);
          */              
    public void notifyObservers(Object arg) {
        Object[] arrLocal;
        synchronized (this) {
            if (!changed)
                return;
            arrLocal = obs.toArray();
            changed = false;
        }
        for (int i = arrLocal.length - 1; i >= 0; i--)
             ((Observer) arrLocal[i]).update(this, arg);
    }
    protected synchronized void setChanged() {
        changed = true;
    }
}

class Vector {
    Object elementData[];
    int elementCount;
    public Vector() {
        this(3);
    }
    public Vector(int n) {
        elementData = new Object[n];
        elementCount = 0;
    }
    public boolean contains(Object elem) {
        return indexOf(elem, 0) >= 0;
    }
    public int indexOf(Object elem) {
        return indexOf(elem, 0);
    }
    public synchronized int indexOf(Object elem, int index) {
        if (elem == null) {
            for (int i = index; i < elementCount; i++)
                if (elementData[i] == null)
                    return i;
        } else {
            for (int i = index; i < elementCount; i++)
                if (elem == elementData[i])
                    return i;
        }
        return -1;
    }
    public synchronized void addElement(Object obj) {
        elementData[elementCount++] = obj;
    }
    public int size() {
        return elementCount;
    }
    public synchronized boolean removeElement(Object obj) {
        int i = indexOf(obj);
        if (i >= 0) {
            removeElementAt(i);
            return true;
        }
        return false;
    }
    private void arraycopy(Object[] src, int src_position, Object[] dest, int dest_position, int length) {
        for (int i = 0; i < length; i++) {
            dest[dest_position + i] = src[src_position + i];
        }
    }
    public synchronized void removeElementAt(int index) {
        if (index >= elementCount) {
            throw new ArrayIndexOutOfBoundsException(index + " >= " + elementCount);
        } else
            if (index < 0) {
                throw new ArrayIndexOutOfBoundsException(index);
            }
        int j = elementCount - index - 1;
        if (j > 0) {
            arraycopy(elementData, index + 1, elementData, index, j);
        }
        elementCount--;
        elementData[elementCount] = null;
    }
    public synchronized void removeAllElements() {
        for (int i = 0; i < elementCount; i++)
            elementData[i] = null;
        elementCount = 0;
    }
    public synchronized Object[] toArray() {
        Object[] result = new Object[elementCount];
        arraycopy(elementData, 0, result, 0, elementCount);
        return result;
    }
}

---