#!/usr/bin/env python3

import os
import glob
import csv
import re
import sys


def get_time(experiment, tool):
    """Returns the elapsed time of the experiment

    Parameters
    ----------
    experiment : str
        Path of the file containing the output of the experiment
    tool : str
        Name of the tool

    Returns
    -------
    dict of str
        Dictionary with collected data
    """
    regex_true = r''
    regex_false = r''
    regex_time = r''
    regex_explored = re.compile(r'Explored (\d+) states')
    regex_error = re.compile(r'Error')
    filename = ""

    name, extension = os.path.splitext(experiment)

    if (tool == 'pmc-sog'):
        filename = "{}.{}".format(name, 'out')

        regex_true = re.compile(r'Property is verified')
        regex_false = re.compile(r'Property is violated')
        regex_time = re.compile(r'Verification duration : (\d+(\.\d+)?)')
    elif (tool == 'pnml2lts-mc'):
        filename = "{}.{}".format(name, 'err')

        regex_true = re.compile(r'Empty product with LTL')
        regex_false = re.compile(r'Accepting cycle FOUND|Non-progress cycle FOUND')
        regex_time = re.compile(r'Total exploration time (\d+(\.\d+)?)')
    else:
        print('{} does not exists'.format(tool))
        sys.exit()

    with open(filename, mode='r') as output_file:
        file_content = output_file.read()

        match_error = False if (tool == 'pmc-sog') else regex_error.search(file_content)
        match_true = regex_true.search(file_content)
        match_false = regex_false.search(file_content)
        match_time = regex_time.search(file_content)
        match_explored = regex_explored.search(file_content)

        explored_states = None
        verification = None
        time_s = None

        if not match_error:
            # property verification
            if match_true:
                verification = 'T'
            elif match_false:
                verification = 'F'

            # get time
            if match_time:
                time = float(match_time.group(1))
                time_s = time / 1000. if (tool == 'pmc-sog') else time

        # get explored states
        if match_explored:
            explored_states = match_explored.group(1)

        output = {
            "elapsed_time": time_s,
            "property_check": verification,
            "explored_states": explored_states
        }

        return output


def check_error(experiment):
    """Returns the error returned in the experiment

    Parameters
    ----------
    experiment: str
        Path of the file containing the output of the experiment

    Returns
    -------
    str
        Error code
    """
    regex = re.compile(
        r'(TIME LIMIT|Segmentation fault|terminate|Aborted|MDD|Invalid identifier|table full)'
    )
    name, extension = os.path.splitext(experiment)
    error_file = '{}.err'.format(name)

    with open(error_file, mode='r') as output_file:
        file_content = output_file.read()
        match_error = regex.search(file_content)

        output = match_error.group(1).upper() if match_error else 'UNKNOWN'
        return output


def get_data(experiments):
    """Returns a list with all the experiments' results

    Parameters
    ----------
    experiments: list of str
        List with all the experiments paths

    Returns
    -------
    list of dict
        List of dictionaries with keys: "model", "tool", "strategy",
        "num_nodes", "num_threads", "formula", "time", "property",
        "explored_states", and "error"
    """
    results = []

    # Regex to find the # nodes, # threads and the formula id
    regex = re.compile(r'-n(\d+).*-th(\d+).*-f(\d+)')

    for experiment in experiments:
        tool, strategy, model_folder, model, out_file = experiment.split(
            '/')[-5:]
        strategy = '_'.join(strategy.split('_')[1:])

        num_nodes, num_threads, formula = regex.findall(out_file)[0]

        data = get_time(experiment, tool)
        elapsed_time, property_check, explored_states = map(
            data.get, ('elapsed_time', 'property_check', 'explored_states'))

        error = "OK"
        if ((elapsed_time is None) and (property_check is None)):
            error = check_error(experiment)

        results.append({
            "model": model,
            "formula": int(formula),
            "tool": tool,
            "strategy": strategy,
            "num_nodes": int(num_nodes),
            "num_threads": int(num_threads),
            "time": elapsed_time,
            "property": property_check,
            "explored_states": explored_states,
            "error": error
        })

    return results


def write2csv(filename, header, values):
    """Writes results in a csv file

    Parameters
    ----------
    filename: str
        Filename of the csv output
    header: list of str
        fields of the csv header. Possible fields are "model", "tool",
        "strategy" "num_nodes", "num_threads", "formula", "time", "property",
        and "error"
    values: list of dict
        Values to be saved. Keys: "model", "tool", "strategy", "num_nodes",
        "num_threads", "formula", "time", "property", and "error"
    """
    with open(filename, mode='w') as csv_file:
        writer = csv.DictWriter(csv_file, fieldnames=header)
        writer.writeheader()

        # write to csv file
        writer.writerows(results)


if __name__ == '__main__':

    # Root folder
    PROJECT_FOLDER = os.path.abspath(
        os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))

    # Folder where are stored the results
    BASE_FOLDER = os.path.join(PROJECT_FOLDER, "results")

    # Get file containing the output of experiments
    EXPERIMENTS = glob.glob(os.path.join(BASE_FOLDER, '**/*.out'),
                            recursive=True)

    # csv file gathering all the results
    OUTPUT_CSV_FILE = os.path.join(BASE_FOLDER, 'output.csv')

    # structure of the csv file
    CSV_FIELDNAMES = [
        'model', 'formula', 'tool', 'strategy', 'num_nodes', 'num_threads',
        'time', 'property', 'explored_states', 'error'
    ]

    # experiments' results
    results = sorted(get_data(EXPERIMENTS),
                     key=lambda k: (k['model'], k['formula'], k['tool'], k[
                         'strategy'], k['num_nodes'], k['num_threads']))

    # write results to csv file
    write2csv(OUTPUT_CSV_FILE, CSV_FIELDNAMES, results)