properties.py 4.89 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

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
75
76
77
78
79
    # For each stop condition create a new Procedure with a boolean return type
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
80
    process.mapping = {state:[] for state in process.mapping.keys()}
Maxime Perrotin's avatar
Maxime Perrotin committed
81
    process.processName = '{}_stop_conditions'.format(process.processName)
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
    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
100
        proc.content.start.transition.terminator = decision
101
102
103
104
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1
105
    opengeode.AdaGenerator.generate(process, simu=True)
Maxime Perrotin's avatar
Maxime Perrotin committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

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
137
138
139
140
    try:
        parse_input_files(options.models, options.spec)
    except IOError as err:
        log.error(str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
141
142
143
144
145
146
147

    return 0

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