package Sequenic.T2;

import Sequenic.T2.*;
import Sequenic.T2.Msg.*;
import java.io.*;
import java.util.*;
import org.junit.Test;

public class Main_Test_5 {

    static public class C1 {

        private int x = 0;
        public C1 next = null;

        public C1(int x0) {
            x = x0;
        }

        public C1 m(C1 c) {  next = c ;
            return next ;
        }

        public void ouch(Integer y) {
            y = x ;
            assert false;
        }
    }

    /**
     * Test purpose: check if the regression tool can reproduce exact the same execution.
     */
    @Test
    public void test_regress() {
        System.out.println("@@@ Check if the regression tool can reproduce exact the same execution...");
        File log1 = new File("test1.log") ;
        File log2 = new File("test2.log") ;
        log1.delete() ;
        log2.delete() ;
        Main.main(C1.class.getName() + " --violmax=3 --savegoodtr=1 --outfile=test1.log");
        Main.main("-R " + C1.class.getName() + ".tr --onlyviol --outfile=test2.log");
        String report1 = Debug.getT2ReportContent("test1.log");
        String report2 = Debug.getT2ReportContent("test2.log");
        //System.out.println("XXX" + report2) ;
        assert report1.equals(report2) ;
    }
    
    @Test
    public void test_GenAndReplayFunction() {
    	
    	new File("blatrfile.tr") . delete() ;
    	
    	File log = new File("test3.log") ;
    	log.delete() ;
    	PrintStream out_ = null ;
    	try {	
    		out_ = new PrintStream(log) ;
    	}
    	catch (Exception e) {
    		assert false ;
    	}
    	
    	PrintStream orgOut = System.out ;
    	
    	System.setOut(out_) ;
    	try {
    		Main.GenAndReplayJunit(C1.class,
    			"blatrfile",
    			" --violmax=3 --savegoodtr=1",
    			"") ;
    		assert false ;
    	}
    	catch (Violation e) { ; }
    	finally { 
    		out_.flush() ; 
    		System.setOut(orgOut) ;
    	}
    	
    	String report1 = Debug.getT2ReportWholeContent(log.getName()) ;
   
    	assert report1.contains("TESTS GENERATOR") ;
    	
    	log.delete() ;
    	
    	System.setOut(out_) ;
    	try {
    		Main.GenAndReplayJunit(C1.class,
    			"blatrfile",
    			" --violmax=3 --savegoodtr=1",
    			"") ;
    		assert false ;
    	}
    	catch (Violation e) { ; }
    	finally { 
    		out_.flush() ; 
    		System.setOut(orgOut) ;
    	}
    	
       	report1 = Debug.getT2ReportWholeContent(log.getName()) ;
        
    	assert report1.contains("REPLAY") ;
    }
}