package Examples;
import java.util.* ;
import java.lang.reflect.* ;

/**
 * This gives a simple demonstration of how to write an imperative application
 * model (aka trace director).
 */
public class ImperativeAppModelDemo {

   public int x = 0 ;

   public void inc() { x++ ; }
   public void dec() { x-- ; assert x>=0 ; }

   public boolean classinv(){ return x>=0 ; }
   
   static private Method INC ;
   static private Method DEC ;
   
   {
       try { 
           INC = ImperativeAppModelDemo.class.getDeclaredMethod("inc", new Class[0]) ; 
           DEC = ImperativeAppModelDemo.class.getDeclaredMethod("dec", new Class[0]) ; 
       }
       catch (Exception e) { }
   }
   
   private List<Method> aux_nextsteps = new LinkedList<Method>() ;
   private int aux_k = 0    ; // a help variable

   private List<Method> customTraceDirector() {
      aux_nextsteps.clear() ;
      if (aux_k == 0) aux_nextsteps.add(INC) ; else aux_nextsteps.add(DEC) ;
      aux_k = (aux_k+1) % 2 ;
      return aux_nextsteps ;
   }
   
   static public void main(String[] args) {
       Sequenic.T2.Main.Junit(ImperativeAppModelDemo.class.getName() + " --customtracedir") ;
   }
    
}