#!/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())