/**
 *
 */

package de.renew.lola2.analysis;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Arrays;

import de.renew.lola2.LolaPlugin;


/**
 * This is the main class for analyzing nets with LoLA. So far it offers the
 * capabilities to check if places are bounded and if transitions are dead.
 *
 * @author hewelt, wagner
 *
 */
public class LolaAnalyzer {
    private static org.apache.log4j.Logger _logger =
        org.apache.log4j.Logger.getLogger(LolaAnalyzer.class);

    /**
     * The timeout for the LoLA call in seconds.
     */
    public static final int TIMEOUT = 5;

    /**
     * Points to the location, where the lola binaries reside
     */
    protected String _lolaPath;

    /**
     * Default constructor. Uses the lola path defined in the LolaPlugin.
     */
    public LolaAnalyzer() {
        _lolaPath = LolaPlugin.getLolaPath();
    }

    /**
     * Constructor that allows to specify a custom path for the LoLA binaries.
     *
     * @param lolaPath The path to the directory containing the LoLA binaries.
     */
    public LolaAnalyzer(String lolaPath) {
        this._lolaPath = lolaPath;
    }

    /**
     * Calls the lola binaries for a given netFile and formula.
     * Returns the output of the call (maybe an error) capsulated in a
     * LolaResult object
     *
     * @param formula The formula to be checked by LoLA.
     * @param netFile The net in LoLA file format.
     *
     * @return a DirectLolaResult object containing the result of the LoLA call.
     */
    public DirectLolaResult callLola(String formula, File netFile) {
        return callLola(formula, netFile, new String[] { });
    }

    /**
     * Calls the lola binaries for a given netFile, taskFile and lolaCommand.
     * Returns the output of the call (maybe an error) capsulated in a
     * LolaResult object
     *
     * @param formula The formula to be checked by LoLA.
     * @param netFile The net in LoLA file format.
     * @param parameter Additional parameters for the LoLA command.
     *
     * @return a DirectLolaResult object containing the result of the LoLA call.
     */
    public DirectLolaResult callLola(String formula, File netFile, String[] parameter) {
        Runtime myrun = Runtime.getRuntime();
        /*
         * construct lola call
         */
        File lolaBin = new File(_lolaPath, LolaHelper.LOLA_COMMAND);
        if (_logger.isDebugEnabled()) {
            _logger.debug(
                "LolaAnalyzer.callLola: lolaBin, netFile, formula, parameter are " + lolaBin + " "
                    + netFile + " " + formula + " " + parameter);
        }

        // json file for output
        File jsonFile = null;
        try {
            jsonFile = File.createTempFile("lolaoutput", ".json", LolaHelper.findTmpDir());
        } catch (IOException ioe) {
            _logger.error("[Lola] Could not create temporary file for JSON output");
        }

        ArrayList<String> argList = new ArrayList<String>();
        argList.add(lolaBin.toString());
        argList.add(netFile.toString());
        argList.add("--timelimit=" + TIMEOUT);
        argList.add("--json=" + jsonFile.getAbsolutePath());
        if (formula != null) {
            argList.add("--formula=" + formula);
        }
        argList.addAll(Arrays.asList(parameter));
        String[] args = new String[argList.size()];
        args = argList.toArray(args);

        if (_logger.isInfoEnabled()) {
            _logger.info("[Lola] Executing " + renderCommand(args));
        }

        // lola puts output runtime information on standard error ("This output 
        // is purely informational and may change in future versions.") and json 
        // output on standard out.  
        StringBuilder outputBuilder = new StringBuilder();
        StringBuilder errorBuilder = new StringBuilder();

        int lolaRetVal = 1;
        try {
            Process lolproc = myrun.exec(args);
            lolaRetVal = lolproc.waitFor();

            BufferedReader outputReader = new BufferedReader(new FileReader(jsonFile));

            //            BufferedReader outputReader = new BufferedReader(new InputStreamReader(lolproc.getInputStream()));
            BufferedReader errorReader =
                new BufferedReader(new InputStreamReader(lolproc.getErrorStream()));

            String line = "";
            while ((line = outputReader.readLine()) != null) {
                outputBuilder.append(line);
                outputBuilder.append(System.lineSeparator());
                _logger.debug("[callLola OUTPUT]" + line);
            }
            while ((line = errorReader.readLine()) != null) {
                errorBuilder.append(line);
                errorBuilder.append(System.lineSeparator());
                _logger.debug("[callLola ERROR]" + line);
            }

            _logger.debug("[Lola] Call returned exit value " + lolaRetVal);
            outputReader.close();
            errorReader.close();
        } catch (IOException e) {
            _logger.error("[Lola] Execution failed");
            e.printStackTrace();
        } catch (InterruptedException e) {
            _logger.error("[Lola] Execution interrupted");
            e.printStackTrace();
        }

        DirectLolaResult lolaResult =
            new DirectLolaResult(lolaRetVal, outputBuilder.toString(), errorBuilder.toString());
        return lolaResult;
    }

    private String renderCommand(String[] args) {
        String cmd = "";
        for (int i = 0; i < args.length; i++) {
            String arg = args[i];
            if (arg.contains(" ")) {
                arg = "\"" + arg + "\"";
            }
            cmd += arg;
            if (i < args.length - 1) {
                cmd += " ";
            }
        }
        return cmd;
    }
}