properties.py 3.46 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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
    # Parse the stop conditions (property file)
    stop_conditions = []
    with open(ppty_file, 'r') as ppties:
        for line in ppties.readlines():
            if not line.strip():
                continue
            expr, syntax, semantic, warnings, term = \
               opengeode.ogParser.parseSingleElement('stop_if', line, process)
            if syntax or semantic or warnings:
                log.error('Error in expression: {}'.format(line))
            else:
                stop_conditions.append(expr)

    # Set the context in the Ada generator
    if stop_conditions:
        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)

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
107
108
109
110
111
112
113
114

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

    parse_input_files(options.models, options.spec)

    return 0

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