#!/usr/bin/python

''' Property parser for SDL systems

Parse expressions such as:
    "stop if state=toto and x = 3"

and generate code to verify the property

(c) European Space Agency, 2015

Author: Maxime.Perrotin@esa.int
'''

__author__ = "Maxime Perrotin"
__license__ = "ESA Community (compatible with LGPLv3)"
__version__ = "1.0"
__url__ = "http://taste.tuxfamily.org"

import os
import traceback
import signal
import sys
import platform
import re
import logging
import argparse

from ColorFormatter import ColorFormatter
import opengeode

# Set up the logging facilities
log = logging.getLogger(__name__)
console = logging.StreamHandler(sys.__stdout__)
console.setFormatter(ColorFormatter())
log.addHandler(console)


def parse_input_files(pr_files, ppty_file):
    ''' Invoke opengeode to parse the SDL models and use the expression
    parser to analyse the properties (stop conditions) '''

    # Parse the SDL model
    try:
        ast = opengeode.parse(pr_files)
        process = ast[0].processes[0]
    except (IndexError, IOError) as err:
        raise IOError('SDL Parser failed - {}'.format(err))
    log.info('SDL parser OK')

    # Parse the stop conditions (property file)
    with open(ppty_file, 'r') as pt:
        stop_conditions, syntax, semantic, warnings, term = \
           opengeode.ogParser.parseSingleElement('stop_if', pt.read(), process)
        for each in syntax:
            log.error(each)
        for each in semantic:
            log.error(each[0])
        for each in warnings:
            log.warning(each[0])

    if syntax or semantic or warnings or not stop_conditions:
        raise IOError('Error parsing stop conditions - Aborting')

    # Set the context in the Ada generator
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
    # For each stop condition create a new Procedure with a boolean return type
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
    process.mapping = {}
    idx = 0
    for each in stop_conditions:
        proc = opengeode.ogAST.Procedure()
        proc.return_type = opengeode.ogParser.BOOLEAN
        proc.inputString = 'property_{}'.format(idx)
        proc.global_variables = process.variables
        proc.global_timers = process.timers
        proc.input_signals = process.input_signals
        proc.output_signals = process.output_signals
        proc.procedures = process.procedures
        proc.operators = process.operators
        proc.content.parent = process
        start = opengeode.ogAST.Start()
        start.transition = opengeode.ogAST.Transition()
        proc.content.start = start
        decision = opengeode.ogAST.Terminator()
        decision.kind = 'return'
        decision.return_expr = each
        proc.content.start.transition.terminator = decision
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1
    opengeode.AdaGenerator.generate(process)

def cli():
    ''' Application entry point, when used from the command line '''

    version = 'Taste Properties version {}'.format(__version__)

    # Parse the command line
    parser = argparse.ArgumentParser(version=version)
    parser.add_argument('-g', '--verbose', action='store_true', default=False,
                      help='Display debug information')
    parser.add_argument('-s', '--spec', dest='spec', default='./spec',
                  help='Path and filename of the property list (one per line)')
    parser.add_argument('models', metavar='file.pr', type=str, nargs='*',
                         help='SDL model(s)')
    options = parser.parse_args()
    if options.verbose:
        log.setLevel(logging.DEBUG)
    else:
        log.setLevel(logging.INFO)
    log.info(version)

    log.debug('{version} using Python {pyVersion}'.format(
                        version=version, pyVersion=platform.python_version()))

    if not options.models or not options.spec:
        log.error('You must specify SDL and property files')
        return 1

    log.debug('SDL files: {}'.format(', '.join(options.models)))
    log.debug('Property file: {}'.format(options.spec))

    try:
        parse_input_files(options.models, options.spec)
    except IOError as err:
        log.error(str(err))

    return 0

if __name__ == '__main__':
    # Exit app on Ctrl-C
    signal.signal(signal.SIGINT, signal.SIG_DFL)
    sys.exit(cli())