properties.py 5.87 KB
Newer Older
Maxime Perrotin's avatar
Maxime Perrotin committed
1
2
3
4
5
6
7
8
9
#!/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

10
11
This shall be used in combination with the OpenGEODE simulator

12
(c) European Space Agency, 2015-2016
Maxime Perrotin's avatar
Maxime Perrotin committed
13
14
15
16
17

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

__author__ = "Maxime Perrotin"
18
19
__license__ = "LGPL v3"
__version__ = "1.0.2"
Maxime Perrotin's avatar
Maxime Perrotin committed
20
21
22
23
24
25
26
27
28
29
30
31
32
33
__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

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

40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
MAKEFILE_TEMPLATE = '''all: build

clean:
	@rm -rf *.o *.ad? *.ali bin examiner *.idx *_simu.sh *_interface.aadl *.wrn *.gpr gnat.cfg runSpark.sh lib{name}.so

build:
	asn1.exe -Ada {asn1} -typePrefix asn1Scc -equal
	gnatmake -gnat2012 -c {name}.adb
	gnatbind -n -Llib{name} {name}
	gnatmake -c -gnat2012 b~{name}.adb
	gcc -shared -fPIC -o lib{name}.so b~{name}.o {name}.o {modules} adaasn1rtl.o -lgnat


.PHONY: all clean build
'''
Maxime Perrotin's avatar
Maxime Perrotin committed
55
56
57
58

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) '''
59
60

    # Parse the SDL model
Maxime Perrotin's avatar
Maxime Perrotin committed
61
62
63
64
65
66
67
    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')

68
    # Parse the stop conditions (property file)
Maxime Perrotin's avatar
Maxime Perrotin committed
69
70
71
72
73
74
75
76
77
78
79
80
    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')
81
82

    # Set the context in the Ada generator
Maxime Perrotin's avatar
Maxime Perrotin committed
83
84
85
86
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals
87
88
89
90
91

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
92
93
94
95
96
    # For each stop condition create a new Procedure with a boolean return type
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
97
    process.mapping = {state:[] for state in process.mapping.keys()}
Maxime Perrotin's avatar
Maxime Perrotin committed
98
    process.processName = '{}_stop_conditions'.format(process.processName)
99
100
101
102
103
104
105
106
107
108
109
110
    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
111
        proc.exported = True
112
113
114
115
116
117
        start = opengeode.ogAST.Start()
        start.transition = opengeode.ogAST.Transition()
        proc.content.start = start
        decision = opengeode.ogAST.Terminator()
        decision.kind = 'return'
        decision.return_expr = each
118
        proc.content.start.transition.terminator = decision
119
120
121
122
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1
123
    opengeode.AdaGenerator.generate(process, simu=True)
Maxime Perrotin's avatar
Maxime Perrotin committed
124

125
126
127
128
129
130
131
132
133
    # gather asn.1 files and modules
    asn1_files = ' '.join(ast[0].asn1_filenames) #'dataview-uniq.asn'
    asn1_modules = ' '.join(name.lower().replace('-', '_') + '.o'
                            for name in ast[0].asn1Modules)
    with open('Makefile.properties', 'w') as Makefile:
        Makefile.write(MAKEFILE_TEMPLATE.format(name=process.processName,
                                                asn1=asn1_files,
                                                modules=asn1_modules))

Maxime Perrotin's avatar
Maxime Perrotin committed
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
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
164
165
166
167
    try:
        parse_input_files(options.models, options.spec)
    except IOError as err:
        log.error(str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
168
169
170
171
172
173
174

    return 0

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