package Examples;

/**
 * A simple class where we demonstrate how to write a predicative application
 * model. The model will impose alternating sequences of inc,dec,inc...
 */
public class PredicativeAppModelDemo {

   public int x = 0 ;

   public void inc() { x++ ; }
   public void dec() { x-- ; }

   private String aux_laststep ; // declaring a slot variable
   private int    aux_k = 0    ; // an auxilliary variable

   private boolean classinv() {
      if (aux_k == 1) assert aux_laststep.equals("inc") : "APPMODEL" ;
      if (aux_k == 2) assert aux_laststep.equals("dec") : "APPMODEL" ;
      if (aux_k < 2) aux_k++ ; else aux_k-- ;
      return x>=0 ;
   }
   
   static public void main(String[] args) {
       Sequenic.T2.Main.Junit(PredicativeAppModelDemo.class.getName()) ;
   }
   
}