package Examples;

/**
 * An simple example demonstrating a test pattern of how T2 can be used to check 
 * a temporal property of a class. This class maintains an int variable 'x' and
 * a boolean variable 'open'. Methods are provided to increase and
 * decrease x. The method 'close' will switch 'open' to false, and once this
 * happens, all methods will have no effect. We want to express this property
 * as a specification. Using LTL temporal operators we can express it like this:
 *
 * <blockquote>
 * For all X:
 * <pre>
 *   [](!open /\ x=X --&gt O(x=X && !open))
 * </pre>
 * </blockquote>
 * 
 * However this specification quantifies over X, which is a bit problematic to
 * test directly. If we introduce auxilliary variables recording the 'old' value
 * of x and open (that is, their values in the previous state), then the 
 * specification above can also be expressed like this:
 *  
 * <blockquote>
 * <pre>
 * [](!open_old --&gt (x=x_old && !open))
 * </pre>
 * </blockquote>
 * 
 * provided open_old is innitialized to true. A property of this form can be
 * encoded as a class invariant. The only thing extra we need to do is to
 * add a mechanism to maintain the correct value of x_old and 
 * open_old. 
 */
public class SimpleTemporalSpecDemo {

    private int x = 0;
    private boolean open = true;

    /**
     * Will increase x.
     */
    public void inc() {
        if (open) {
            x++;
        }
    }

    /**
     * Will decrease x.
     */
    public void dec() {
        if (open) {
            x--;
        }
    }

    /**
     * After this is called, increase and decrease is supposed to have no
     * effect.
     */
    public void close() {
        open = false;
    }
    // Defining auxiliary variables 
    // Old-value of open and x:
    private boolean aux_open_old = true ;
    private int aux_x_old;

    /**
     * A check to temporal spec is encoded in the class invariant.
     */
    private boolean classinv() {

        boolean ok = true;
        // Checking the temporal property:
        ok = aux_open_old || ((x == aux_x_old) && !open);
        // Updating the old-vars:
        aux_open_old = open;
        aux_x_old = x;
        // Returning the result of checking:
        return ok;
    }

    static public void main(String[] args) {
        // Calling T2 from here:
        Sequenic.T2.Main.main(SimpleTemporalSpecDemo.class.getName());
    }
}