package Sequenic.T2;

import Sequenic.T2.*;
import org.junit.Test;

public class Main_Test_6 {

    static public class CsearchMode {

        private int status = 0 ;
        
        public CsearchMode() {}

        public void m1() { 
            assert status==0 : "PRE" ;
            status=1 ;
        }
        
        public void m2(){
            assert status==1 : "PRE" ;
            status=2 ;
        }
        
        public void m3(){
            assert status==2 : "PRE" ;
            status=3 ;            
        }

        public void m4(){
            assert status==3 : "PRE" ;
            status=4 ;            
        }
        
        public void m5(){
            assert status==4 : "PRE" ;
            assert false ;      
        }
    }
    
    /**
     * Test purpose: check if the search-mode is working.
     */
    @Test
    public void test_searchmode() {
        System.out.println("@@@ Check if the search-mode is working...");
        Class C = CsearchMode.class;
        
        // This may find the violation, but the chance is small:
        TrFile.delete(C);
        Main.main(C.getName() + " --lenexec=5") ;
        Debug.assertTrfEmpty(C);
        
        // While this one will have high probability to find the error:
        TrFile.delete(C);
        Main.main(CsearchMode.class.getName() + " --lenexec=6 --searchmode=100") ;
        Debug.assertTrfNonEmpty(C);
    }
    
    
    static public class CsearchMode_withBacktrack {

        private int i = 0 ;
        
        public CsearchMode_withBacktrack() {}

        public void m(int x) { 
            assert x==1 || x==0 : "PRE" ;
            i = i+x ;
            if (i==8) assert false ;
        }
        
    }
    
    /**
     * Test purpose: check if the backtrack feature of search-mode is working.
     * By 'backtrack' we mean that if the current step has been sufficiently
     * retried, we will backtrack further to its previous step, rather than
     * keep trying to generate a new current step.
     * 
     * In the above class, the error can only be reached if we keep calling m
     * with parameter 1.
     * 
     * Notice that the chance of accidentally creating a successful test sequence
     * that produces the error above is about 1/60000, yet the search-mode
     * can find it.
     */
    @Test
    public void test_backtrack_searchmode() {
        System.out.println("@@@ Check if the backtracking of search-mode is working...");
        Class C = CsearchMode_withBacktrack.class;
        
        // While this one will have high probability to find the error:
        TrFile.delete(C);
        Main.main(CsearchMode_withBacktrack.class.getName() + " --lenexec=10  --searchmode=7000 --nmax=10000") ;
        Debug.assertTrfNonEmpty(C);
        
        // Pure random mode will find it difficult to spot the error:
        TrFile.delete(C);
        Main.main(CsearchMode_withBacktrack.class.getName() + " --lenexec=9  --nmax=10000") ;
        Debug.assertTrfEmpty(C);
    }
    
}