/*
 * Copyright 2007 Wishnu Prasetya.
 *
 * This file is part of T2.
 * T2 is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License (GPL) as published by the
 * Free Software Foundation; either version 3 of the License, or any
 * later version.
 * 
 * T2 is distributed in the hope that it will be useful, but WITHOUT ANY
 * WARRANTY; without even the implied warranty of MERCHANTABILITY or
 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
 * for more details.
 *
 * A copy of the GNU General Public License can be found in T2 distribution.
 * If it is missing, see http://www.gnu.org/licenses.
 */
package Sequenic.T2;
//import Sequenic.T2.Seq.* ;

import java.io.BufferedInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InvalidClassException;
import java.io.NotSerializableException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.io.OutputStream;
import java.io.Serializable;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.zip.Deflater;
import java.util.zip.DeflaterOutputStream;
import java.util.zip.Inflater;
import java.util.zip.InflaterInputStream;

import Sequenic.T2.Msg.T2Error;
import Sequenic.T2.Msg.T2Exception;
import Sequenic.T2.Seq.Trace;

/**
 * An instance of this class represents the content of a tr-file. Such a file is 
 * used to save traces for regression. To save a set of traces we first wrap them
 * as an TrFile object. Then we write the TrFile object to a file via serialization. 
 * So, indirectly, this class defines the format of a tr-file.
 */
public class TrFile implements Serializable {
		
    /**
     * Specify the name of the target class to which the traces belong to.
     */
    public String CUTname;
    /**
     * Specify the fully qualified name of the class of the pool 
     * used to produce the traces.
     */
    public String poolClassName;
    /**
     * Time stamp. Currently not used.
     */
    public String timestamp = null;
    /**
     * Serial number. Currently not used.
     */
    public String serialnr = null;
    /**
     * The name of the classes whose class invariants used during to test 
     * the traces.
     */
    public LinkedList<String> classinvariantOwners;
   	
    /**
     * The traces to be saved.
     */
    transient public Collection<Sequenic.T2.Seq.Trace> traces;

    private TrFile(){ super() ; } ;
    
    /**
     * @param C The name of the target class to which the traces belong.
     * @param p The name of the class of the pool used to create the traces.
     * @param ts The traces.
     * @param invs The class invariants used in the production of ts.
     */
    public TrFile(String C, String p, LinkedList<Sequenic.T2.Seq.Trace> ts, List<Method> invs) {
        assert C != null && p != null && ts != null && invs != null : "PRE";
        CUTname = C;
        poolClassName = p;
        traces = ts;
        classinvariantOwners = new LinkedList<String>();
        for (Method cinv : invs) {
            classinvariantOwners.add(cinv.getDeclaringClass().getName());
        }
    }

    /**
     * For saving the content of this TrFile-object.
     */
    public void save(String fname) throws T2Exception {
        try {
            ObjectOutputStream oos = initOut(fname);
            oos.writeObject(this);
            this.writeTraces(oos); //traces is transient, handle separately
            oos.close();
        } catch (NotSerializableException e) {
            throw new T2Error("A part of execution trace turns out to be unserializable.", e);
        } catch (InvalidClassException e) {
            throw new T2Error("A part of execution trace turns out to be unserializable.", e);
        } catch (Exception e) {
            throw new T2Exception("Fail to save execution traces.", e);
        }
    }
    
    static ObjectOutputStream initOut(String fname) throws IOException 
    {
    	OutputStream out;
    	if(fname==null)
    	{	
    		out = new OutputStream() {
				
				@Override
				public void write(int b) throws IOException
				{
				}
			};
    	} else {
        	out = new FileOutputStream(fname);
        	if(useCompression)
        		out = new DeflaterOutputStream(out, new Deflater(Deflater.NO_COMPRESSION),10000);
    	}
        return new ObjectOutputStream(out);
    }
    
   public  static ObjectInputStream initIn(String fname) throws IOException
    {
        InputStream ins = new FileInputStream(fname);
        if(useCompression)
        	ins = new InflaterInputStream(ins,new Inflater(),50000);
        ins = new BufferedInputStream(ins,50000);
        return new ObjectInputStream(ins);
    }

    public void save() throws T2Exception {
        save(CUTname + ".tr");
    }

    /**
     * For loading the content of a TrFile.
     */
    static public TrFile load(String fname) throws T2Exception {
        //System.out.println(">>>" + fname) ;
        TrFile tf = null;
        try {
            //System.out.println(">>>" + new File(fname).exists()) ;
            
            ObjectInputStream ois = initIn(fname);
            tf = (TrFile) ois.readObject();
            tf.readTraces(ois); //traces is transient, handle separately
            ois.close();
        } catch (Exception e) {
            //e.printStackTrace();
            throw new T2Exception("Fail to load execution traces.", e);
        }
        return tf;
    }
    
    static public TrFile load(Collection<Trace> set, String... fnames) throws T2Exception
    {
    	if(!useAlternativeSerialization)
    		return null;
    	TrFile res = null;
    	for(int i=0;i<fnames.length;i++)
    	{
            try {
            	System.out.println("Reading: "+fnames[i]);
    		InputStream ins = new FileInputStream(fnames[i]);
            if(useCompression)
            	ins = new InflaterInputStream(ins);
            ObjectInputStream ois = new ObjectInputStream(ins);
            if(i==0) {
            	res = (TrFile) ois.readObject();
            	res.traces = set;
            }
            else
            	res.compatible((TrFile) ois.readObject());
            res.readTraces(ois); //traces is transient, handle separately
            ois.close();
            } catch(Exception e) {
                throw new T2Exception("Fail to load execution traces.", e);
            }
    	}
    	return res;
    }

    /**
     * Deleting a TrFile.
     */
    static public void delete(Class C) {
        //System.out.println("*** " + C.getName() + ".tr") ;
        (new File(C.getName() + ".tr")).delete();
    }
    
    /**
     * Return a new TrFile that merges this TrFile and tf2. Both TrFile
     * should have the same CUTname, classinv-owners, and pool.
     * 
     * The method leaves the serialnr and timestamp fields null.
     */
    public TrFile merge(TrFile tf2) {
    	TrFile tfout = new TrFile() ;
    	tfout.CUTname = CUTname ;
    	tfout.classinvariantOwners = classinvariantOwners ;
    	tfout.poolClassName = poolClassName ;
    	tfout.traces = traces ;
    	tfout.traces.addAll(tf2.traces) ;
    	return tfout ;
    }

    //=============================
    // (De)serialization of traces 
    //=============================

    private void writeTraces(java.io.ObjectOutputStream out)
    throws IOException
    {	
    	if(useAlternativeSerialization) 
    	{
        	int size = traces == null ? -1 : traces.size();
        	out.writeInt(size);
        	if(size > 0)
        		for(Trace t : traces)
        			t.alternativeSerializationWrite(out);    		
    	} else 
    		out.writeObject(traces);
    }

    private void readTraces(java.io.ObjectInputStream in)
    throws IOException, ClassNotFoundException
    {
    	if(useAlternativeSerialization)
    	{
        	int size = in.readInt();
        	if(traces==null && size>=0)
        	{	
        		traces = new ArrayList<Trace>(size+5);
            	while(size-->0)
            	{
            		traces.add(Trace.alternativeSerializationRead(in));	
            	}
        	} else if (size==-2) 
        	{
        		traces = new ArrayList<Trace>();
        		while(true) 
        		{
            		Trace t = Trace.alternativeSerializationRead(in);
            		if(t==null)
            			return;
            		traces.add(t);
        		}
        	}
    	} else
    		traces = (LinkedList<Trace>) in.readObject();
    }
    
	// Use alternative serialization of traces.
	// Ensure that traces is marked transient!
    //Will save 10-20% storage space (excl. compression), and should be faster too.
	static final boolean useAlternativeSerialization = true;
    
	//use compression
	private static final boolean useCompression = true;
    
	private static final long serialVersionUID; 
    
    static {
    	//In order to distinguish different serialization methods, vary the UID
    	long base = 24535245791224L;
    	if(useAlternativeSerialization)
    		base += 81982484L;
    	if(useCompression)
    		base += 466274L;
    	serialVersionUID = base;
    }

    

    /** Checks whether TrFil n can be merged with this TrFile
     * 
     * @param n
     * @throws T2Exception
     */
    public void compatible(TrFile n) throws T2Exception {
		if(!CUTname.equals(n.CUTname))
			throw new T2Exception("CUT is not the same: "+CUTname+" vs. "+n.CUTname);
		if(!poolClassName.equals(n.poolClassName))
			throw new T2Exception("Pool is not the same: "+poolClassName+" vs. "+n.poolClassName);
		HashSet<String> s = new HashSet<String>(classinvariantOwners);
		
		for(String i : n.classinvariantOwners)
			if(!s.contains(i))
				throw new T2Exception("New classinvariant: "+i);
		s.removeAll(n.classinvariantOwners);
		if(!s.isEmpty())
			throw new T2Exception("Missing classinvariant(s): "+s);
	}
    
}