package Examples;
import java.util.* ;

/**
 * Demonstrating how we can check a property <>!open. The property is first
 * encoded as a Buhci automaton. We need to implement cycle detection.
 * 
 * Hash values will be used, rather than storing images of states.
 */
public class SimpleTemporalSpecDemo2 {

    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 
    private List<Integer> aux_history = new LinkedList<Integer>() ;
    private int aux_state = 0 ;
    static private final int ERROR_STATE = 0 ;

    /**
     * A check to temporal spec is encoded in the class invariant.
     */
    private boolean classinv() {
        boolean violation = false ;
        if (aux_state == ERROR_STATE) violation = aux_history.contains(hashCode()) ;
        // Update Buchi state:
        if (aux_state==0 && !open) aux_state=1 ;
        // Update history:
        if (aux_state == ERROR_STATE) aux_history.add(hashCode()) ;
        // Returning the result of checking:
        return !violation ;
    }
    
    static public void main(String[] args) {
        // Calling T2 from here:
        Sequenic.T2.Main.Junit(SimpleTemporalSpecDemo2.class.getName());
     }
    
}