Commit 955fa303 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

first commit

parents
all: install
install:
@python setup.py install --record install.record
clean:
@rm -rf build dist *.egg-info properties/*.pyc
.PHONY: all install clean
This directory contains the code for the TASTE Property Parser and code generator
Install by typing, as root:
$ make install
This command will call: python setup.py install --record
You can install in a virtualenv instead
You must first install opengeode, which is a required dependency
(c) European Space Agency, 2015
Author: Maxime Perrotin
#!/usr/bin/env python2
# -*- coding:Utf-8 -*-
''' Custom logging color formatter
When logging, use the following format
[criticality] file - message
the color of [criticality] (warning, info, etc.) is different for each value
Adapted by ESA from examples found on StackOverflow
'''
import logging
class ColorFormatter(logging.Formatter):
''' Custom color formatter for shell logging '''
COLORS = {'WARNING' : 33, # yellow
'INFO' : 32, # green
'DEBUG' : 37, # white
'CRITICAL' : 31, # red
'ERROR' : 31}
def __init__(self):
''' Create a custom format for the logging messages '''
fmt = "[%(levelname)-19s] \033[1m%(filename)-20s\033[0m%(message)s"
super(ColorFormatter, self).__init__(fmt)
def format(self, record):
''' When formatting, set the color of the criticality level text '''
col = self.COLORS[record.levelname]
record.levelname = '\033[1m\033[{}m {}\033[0m'.format(col,
record.levelname)
return super(ColorFormatter, self).format(record)
#!/usr/bin/env python
# -*- coding: utf-8 -*-
"""
Taste Properties parses "stop if" conditions, check semantics against
an opengeode model, and generate Ada code to verify the stop conditions,
for use in a model checker or simulator.
"""
import properties
__version__ = properties.__version__
#!/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
log = logging.getLogger(__name__)
terminal_formatter = logging.Formatter(
fmt="%(levelname)s - %(name)s: %(message)s")
handler_console = logging.StreamHandler()
handler_console.setLevel(logging.DEBUG)
handler_console.setFormatter(terminal_formatter)
log.addHandler(handler_console)
# Make sure the gui can import modules in the current directory
sys.path.insert(0, '.')
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) '''
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')
def cli():
''' Application entry point, when used from the command line '''
version = 'Taste Properties version {}'.format(__version__)
# Set up the logging facilities
log = logging.getLogger("properties")
console = logging.StreamHandler(sys.__stdout__)
console.setFormatter(ColorFormatter())
log.addHandler(console)
# 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())
#!/usr/bin/env python
# -*- coding: utf-8 -*-
'''
Setup file for Linux distribution
Usage: python setup.py sdist --> to create a tarball
python setup.py install --> to install in python directory
'''
# from distutils.core import setup
from setuptools import setup, find_packages
import properties
setup(
name='properties',
version=properties.__version__,
packages=find_packages(),
author='Maxime Perrotin',
author_email='maxime.perrotin@esa.int',
description='Parser/Code generator for model checker properties',
long_description=open('README.md').read(),
include_package_data=True,
url='http://taste.tuxfamily.org',
classifiers=[
'Programming Language :: Python',
'License :: OSI Approved :: GNU Lesser General Public License v3 (LGPLv3)',
'Operating System :: OS Independent',
'Programming Language :: Python :: 2.7'
],
entry_points={
'console_scripts': [
'taste-properties = properties:cli'
]
}
)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment