properties.py 3.5 KB
Newer Older
Maxime Perrotin's avatar
Maxime Perrotin committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
#!/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

32
# Set up the logging facilities
Maxime Perrotin's avatar
Maxime Perrotin committed
33
log = logging.getLogger(__name__)
34
35
36
console = logging.StreamHandler(sys.__stdout__)
console.setFormatter(ColorFormatter())
log.addHandler(console)
Maxime Perrotin's avatar
Maxime Perrotin committed
37
38
39
40
41


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) '''
42
43

    # Parse the SDL model
Maxime Perrotin's avatar
Maxime Perrotin committed
44
45
46
47
48
49
50
    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')

51
    # Parse the stop conditions (property file)
Maxime Perrotin's avatar
Maxime Perrotin committed
52
53
54
55
56
57
58
59
60
61
62
63
    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')
64
65

    # Set the context in the Ada generator
Maxime Perrotin's avatar
Maxime Perrotin committed
66
67
68
69
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals
70
71
72
73
74
75

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)

Maxime Perrotin's avatar
Maxime Perrotin committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

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))

Maxime Perrotin's avatar
Maxime Perrotin committed
107
108
109
110
    try:
        parse_input_files(options.models, options.spec)
    except IOError as err:
        log.error(str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
111
112
113
114
115
116
117

    return 0

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