sdlHandler.py 46.5 KB
Newer Older
1
2
3
4
5
#!/usr/bin/env python
# -*- coding: utf-8 -*-

# pylint: disable=C0302
"""
6
    ASN.1 Value Editor - SDL Statechart handler
7

8
9
10
11
12
13
    Connect to OpenGEODE to drive a simulation using the ASN.1 Editor
    Display the statechart during the simulation
    View and allow user to modify any SDL internal variable
    Send events to the MSC handler in order to display messages and timers
    Manage context - enable buttons for sending TCs only if the SDL model is
    in a state where they are expected.
14
15
16
17
18
19
20
21
22

    Copyright (c) 2012-2015 European Space Agency

    Designed and implemented by Maxime Perrotin

    Contact: maxime.perrotin@esa.int
"""

import os
Maxime Perrotin's avatar
Maxime Perrotin committed
23
import ctypes
24
import itertools
25
import random
Maxime Perrotin's avatar
Maxime Perrotin committed
26
from functools import partial
27
from itertools import chain
28

29
from PySide.QtGui import (QDockWidget, QPushButton, QGridLayout, QListWidget,
30
                          QUndoStack, QUndoCommand, QToolButton, QTableWidget,
31
32
                          QTableWidgetItem, QComboBox, QMessageBox,
                          QApplication)
33
from PySide.QtCore import QObject, Signal, Slot, Qt, QFile, QTimer
34
from PySide.QtUiTools import QUiLoader
35

36
37
import asn1_value_editor
from standalone_editor import asn1sccToasn1ValueEditorTypes
Maxime Perrotin's avatar
Maxime Perrotin committed
38
import vn
Maxime Perrotin's avatar
Maxime Perrotin committed
39
import vdm_vn
40
import resources
Maxime Perrotin's avatar
Maxime Perrotin committed
41
42
import vdmHandler

43
44
try:
    import opengeode
45
    import opengeode.undoCommands as undo
46
47
48
except ImportError:
    print 'OpenGEODE module is not available'

49

Maxime Perrotin's avatar
Maxime Perrotin committed
50
try:
51
52
    # Not correct, this assumes that the dataview is always named
    # "dataview-uniq.asn" ! the actual name shall be parsed in the SDL model
Maxime Perrotin's avatar
Maxime Perrotin committed
53
54
    import dataview_uniq_asn as ASN1
except ImportError:
Maxime Perrotin's avatar
Maxime Perrotin committed
55
    #print 'No Python A mapper generated dataview, SDL handler cannot be used'
Maxime Perrotin's avatar
Maxime Perrotin committed
56
    ASN1 = None
57

58
59
60
# Unicode separator used by Opengeode in the Ada backend
# to build unambiguous names, in particular when using nested states
UNICODE_SEP = u'\u00dc'
Maxime Perrotin's avatar
Maxime Perrotin committed
61
62
CleanName = lambda name: name.replace(UNICODE_SEP, '.')
UnicodeName = lambda name: name.replace('.', UNICODE_SEP)
Maxime Perrotin's avatar
Maxime Perrotin committed
63

Maxime Perrotin's avatar
Maxime Perrotin committed
64

65
66
67
68
69
70
71
72
73
74
75
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
115
116
117
118
# Set of functions used by the simulator to compute a random value for
# a given ASN.1 type, return a Value Notation string
def compute_random_value(asn1_ty, pool):
    ''' Top-level, type-dispatching function
    pool is the set of types from process.dataview attribute '''
    basic = opengeode.ogParser.find_basic_type(asn1_ty.type, pool)
    if basic.kind.startswith('Integer'):
        return rand_int(basic)
    elif basic.kind == 'BooleanType':
        return rand_bool(basic)
    elif basic.kind.startswith('Real'):
        return rand_real(basic)
    elif basic.kind == 'EnumeratedType':
        return rand_enum(basic)
    elif basic.kind == 'ChoiceType':
        return compute_random_choice(basic, pool)
    elif basic.kind in ('SequenceType', 'SetType'):
        return compute_random_sequence(basic, pool)
    elif basic.kind in ('SequenceOfType', 'SetOfType'):
        return compute_random_sequenceof(basic, pool)


# Random values for basic types
rand_int = lambda ty: str(random.randint(long(ty.Min), long(ty.Max)))
rand_real = lambda ty: str(random.uniform(float(ty.Min), float(ty.Max)))
rand_bool = lambda _: random.choice(['TRUE', 'FALSE'])
rand_enum = lambda ty: random.choice(ty.EnumValues.keys())


def compute_random_choice(asn1_ty, pool):
    ''' Select randomly a choice item and set a random value '''
    choice = random.choice(asn1_ty.Children.keys())
    value_ty = asn1_ty.Children[choice]
    value = compute_random_value(value_ty, pool)
    return '{}: {}'.format(choice, value)


def compute_random_sequence(asn1_ty, pool):
    ''' Compute randomly the values of SEQUENCE fields '''
    res = []
    for name, ty in asn1_ty.Children.viewitems():
        res.append('{} {}'.format(name, compute_random_value(ty, pool)))
    return '{{ {} }}'.format(', '.join(res))


def compute_random_sequenceof(asn1_ty, pool):
    ''' Compute a list of a random size and random values '''
    size = random.randint(int(asn1_ty.Min), int(asn1_ty.Max))
    elems = []
    for _ in xrange(size):
        elems.append(compute_random_value(asn1_ty, pool))
    return  '{{ {} }}'.format(', '.join(elems))


119
120
121
122
123
124
125
126
127
128
129
# Set of functions used by the simulator to compute the combination input
# parameters for each ASN.1 data type. Yield ASN.1 Value Notation strings
# ASN.1 types must be in the format generated by ASN1SCC Python backend
def compute_combinations(asn1_ty, pool):
    ''' Top-level, type-dispatching function
    "pool" is the set of types, found in the process.dataview attribute '''
    basic = opengeode.ogParser.find_basic_type(asn1_ty.type, pool)
    # Python2 has no "yield from"...
    if basic.kind.startswith('Integer'):
        for each in compute_integer_combinations(basic):
            yield each
130
    elif basic.kind == 'BooleanType':
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
        for each in compute_boolean_combinations(basic):
            yield each
    elif basic.kind.startswith('Real'):
        for each in compute_real_combinations(basic):
            yield each
    elif basic.kind == 'EnumeratedType':
        for each in compute_enumerated_combinations(basic):
            yield each
    elif basic.kind == 'ChoiceType':
        for each in compute_choice_combinations(basic, pool):
            yield each
    elif basic.kind in ('SequenceType', 'SetType'):
        for each in compute_sequence_combinations(basic, pool):
            yield each
    elif basic.kind in ('SequenceOfType', 'SetOfType'):
        for each in compute_sequenceof_combinations(basic, pool):
            yield each


Maxime Perrotin's avatar
Maxime Perrotin committed
150
def compute_integer_combinations(asn1_ty, max_iter=0):
151
152
153
154
155
    ''' Generator returning all integer values, with optional limit '''
    # Do not use xrange, it needs a value that fits in a C long
    max_iter = (long(asn1_ty.Min)
                + max_iter) if max_iter != 0 else long(asn1_ty.Max)
    for each in itertools.count(long(asn1_ty.Min)):
Maxime Perrotin's avatar
Maxime Perrotin committed
156
        if each > max_iter:
157
            break
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
        yield str(each)


def compute_real_combinations(asn1_ty):
    ''' Generator returning three real values only (set is infinite) '''
    yield asn1_ty.Min
    yield str((float(asn1_ty.Max) + float(asn1_ty.Min)) / 2.0)
    yield asn1_ty.Max


def compute_boolean_combinations(asn1_ty):
    ''' Generator returning all combinations of boolean '''
    yield 'TRUE'
    yield 'FALSE'


def compute_enumerated_combinations(asn1_ty):
    ''' Generator returning all combinations of enumerated '''
    for each in asn1_ty.EnumValues.viewkeys():
        yield each


def compute_choice_combinations(asn1_ty, pool):
    ''' Generator returning all combinations of choice components '''
    for discr, value_ty in asn1_ty.Children.viewitems():
        for each in compute_combinations(value_ty, pool):
            yield '{}: {}'.format(discr, each)


def compute_sequence_combinations(asn1_ty, pool):
    ''' Generator returning all combinations of SEQUENCE types '''
189
190
191
192
    # Prepare generators to compute combinations of each field
    elems = (compute_combinations(sort, pool)
             for sort in asn1_ty.Children.viewvalues())
    # Combine all field generators to get the complete set of values
193
194
195
196
197
198
199
200
201
    for each in itertools.product(*elems):
        # each is a tuple with values for the sequence, join with fieldnames
        pairs = itertools.izip(asn1_ty.Children.viewkeys(), each)
        res = ('{} {}'.format(name, value) for name, value in pairs)
        yield '{{ {} }}'.format(', '.join(res))


def compute_sequenceof_combinations(asn1_ty, pool):
    ''' Generator returning all combinations of arrays '''
Maxime Perrotin's avatar
Maxime Perrotin committed
202
    for size in xrange(int(asn1_ty.Min), int(asn1_ty.Max) + 1):
203
204
205
206
207
        elems = []
        for _ in xrange(size):
            elems.append(compute_combinations(asn1_ty, pool))
        for each in itertools.product(*elems):
            yield  '{{ {} }}'.format(', '.join(each))
208
209


210
211
class SendTC(QUndoCommand):
    ''' Undo command to send a message to the running system '''
212
213
    def __init__(self, handler, old_state):
        ''' Init: save the current and old states '''
214
215
        super(SendTC, self).__init__()
        self.handler = handler
216
217
218
        self.new_state = handler.current_hash
        self.old_state = old_state

219
220
221
    def undo(self):
        ''' Undo a send TC: Restore the system state as it was before the TC
        was sent - setting back all global variables and internal state '''
222
        self.handler.restore_global_state(self.old_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
223
        self.handler.update_button_state()
224
225

    def redo(self):
226
227
228
        ''' Set the internal variables to the new state '''
        if self.new_state != self.handler.current_hash:
            self.handler.restore_global_state(self.new_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
229
            self.handler.update_button_state()
230
231


232
class sdlHandler(QObject):
233
234
235
    '''
        Class managing SDL models
    '''
236
237
238
239
240
241
242
    # Qt signals:
    #    - msc is used to display an item on the MSC diagram
    #    - msc_macro_start/top are used to control the undo stack macros
    #    - allowed_messages is used to activate/deactivate GUI buttons
    #      depending on the context, driven by the SDL model internal state
    #    - msc undo/redo are used to request an undo stack action to the MSC
    #      handler, which lives in a different thread.
243
    msc = Signal(unicode, unicode, QUndoStack)
244
245
246
247
    msc_macro_start = Signal()
    msc_macro_stop = Signal()
    msc_undo = Signal()
    msc_redo = Signal()
248
    allowed_messages = Signal(list)
249
    clicker = Signal()
250

251
252
253
    def __init__(self, parent):
        ''' Startup: check if there are some SDL files in
            the directory and try to parse them and build the widget '''
254
        super(sdlHandler, self).__init__()
255
        random.seed()
256
        self.parent = parent
257
258
259
260
261
262
263
264
265
266
        all_files = os.listdir('.')
        pr_files = []
        for each in all_files:
            if each.endswith('.pr'):
                pr_files.append(each)
        if not pr_files:
            raise IOError('SDL Handler failed to initialize')
        self.ast = opengeode.parse(pr_files)
        try:
            root_ast = self.ast[0]
Maxime Perrotin's avatar
Maxime Perrotin committed
267
            self.proc = root_ast.processes[0]
268
269
        except IndexError:
            raise IOError('SDL Handler failed to initialize')
270
        #opengeode.Helper.flatten(self.proc)
271
        graph = opengeode.Statechart.create_dot_graph(self.proc, basic=True)
272
273
274
275
        self.sdl_scene = opengeode.SDL_Scene('statechart')
        self.sdl_view = opengeode.SDL_View(self.sdl_scene)
        opengeode.Statechart.render_statechart(self.sdl_scene, graph)
        self.sdl_view.refresh()
276
277
278
279
280
281
        # Pointer to the shared library, set by gui.py
        self._dll = None
        self.dock = None
        self.dock_state = None
        self.asn1_editor = None
        self.tree_items = {}
282
        self.dock_simu, self.dock_checker = self.start_simu()
Maxime Perrotin's avatar
Maxime Perrotin committed
283
        self.current_sdl_state = ''
284
285
        # Handle the state of all timers ({'timerName': 'set'/'unset'})
        self.timers = {}
286
        # Keep a state graph to allow undo/redo and state exploration
287
        self.set_of_states = {}
288
        self.current_hash = None
289
290
        # Flag set to true when a new state is created
        self.new_state_created = False
291
292
        # When checking properties, list the currently true stop conditions
        self.stop_conditions = []
293
294
        # Create a stack for handling undo/redo commands
        self.undo_stack = QUndoStack(self)
295
296
297
298
299
300
        # Associate the Undo, Redo, Reset buttons with an action
        widget = self.dock_simu.widget()
        undo_button = widget.findChild(QToolButton, 'undoButton')
        redo_button = widget.findChild(QToolButton, 'redoButton')
        reset_button = widget.findChild(QToolButton, 'resetButton')
        reset_button.clicked.connect(self.reset_simulation)
Maxime Perrotin's avatar
Maxime Perrotin committed
301
302
        undo_button.clicked.connect(self.undo)
        redo_button.clicked.connect(self.redo)
Maxime Perrotin's avatar
Maxime Perrotin committed
303
        # Placeholder to keep a list of properties to be checked at runtime
304
        self.properties = {}
Maxime Perrotin's avatar
Maxime Perrotin committed
305
        self.prop_dll = None
Maxime Perrotin's avatar
Maxime Perrotin committed
306
307
        # VDM handler instance, when needed for external procedures calls
        self.vdm = None
308
309
310
311
        # Reference to the random simulator/checker table (set with DLL)
        self.checker_table = None
        # Parameter when using automatic simulation (random/exhaustive)
        self.sim_param = {'state': 'manual', 'periodic': [], 'random': []}
312
313
314
315
316
317
        # self.buttons: paramless TC buttons (set when loading dll)
        self.buttons = {}
        # ASN.1 editors and send buttons of TC with parameters
        # list of {'name': str, 'editor': asn1Editor, 'send_btn': QPushButton}
        # set by gui.py
        self.param_tc_editors = []
318

319
320
321
322
    @property
    def active_tc(self):
        ''' Yield list of TCs that can be sent (including timeouts) '''
        # Find the list of allowed TC based on the current state
323
        st = self.current_sdl_state
324
325
326
327
328
329
330
331
        inputs = self.proc.mapping[st.replace(UNICODE_SEP, '_').lower()]
        allowed_tc = (tc for each in inputs for tc in each.inputlist)
        for each in allowed_tc:
            if each in self.timers and not self.buttons[each].isEnabled():
                # Timers: check if button is active
                continue
            yield each

332
333
334
335
336
337
338
339
340
    @property
    def dll(self):
        return self._dll

    @dll.setter
    def dll(self, value):
        ''' Set the DLL - initialize the docks '''
        self._dll = value
        self.dock = QDockWidget('SDL/Statechart Viewer', self.parent)
341
        self.dock.setFloating(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
342
        self.dock.resize(400, 400)
343
        self.dock.setObjectName('SDLViewer')
344
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock)
345
346
347
348
349
        self.dock.setAllowedAreas(Qt.NoDockWidgetArea)
        self.sdl_view.show()
        self.dock.setWidget(self.sdl_view)
        self.running = False
        self.dock.hide()
350
        # Dock widget to display the internal state
351
352
353
354
355
        ui = QFile(':/internalState.ui')
        loader = QUiLoader()
        widgets = loader.load(ui, parent=self.parent)
        self.asn1_editor = widgets.findChild(asn1_value_editor.asn1Editor,
                                             'ASN1EDITOR')
356
        self.asn1_editor.hideExtraColumns()
357
358
        apply_button = widgets.findChild(QToolButton, 'applyButton')
        apply_button.pressed.connect(self.change_internal_state)
359
        self.dock_state = QDockWidget('Internal state', self.parent)
360
361
        self.dock_state.setFloating(False)
        #self.dock_state.resize(400, 400)
362
363
        self.dock_state.setObjectName('InternalStateViewer')
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock_state)
364
        #self.dock_state.setAllowedAreas(Qt.NoDockWidgetArea)
365
        self.dock_state.setWidget(widgets)
366
367
        self.dock_state.show()
        self.parent.tabifyDockWidget(self.dock_state, self.dock_simu)
368
        self.parent.tabifyDockWidget(self.dock_simu, self.dock_checker)
Maxime Perrotin's avatar
Maxime Perrotin committed
369
        # Add the state list to the ASN.1 Editor (at row 0)
370
        row = 0
371
372
373

        # Build up the list of states, including state compositions
        context = self.proc
374
375
        # get the list of state aggregations
        aggregates = opengeode.Helper.state_aggregations(context)
376

377
378
        stnames = list(opengeode.Helper.statenames(context, sep=UNICODE_SEP))
        stnames.extend(list(opengeode.Helper.rec_findstates(context)))
379

Maxime Perrotin's avatar
Maxime Perrotin committed
380
381
382
383
        states = {'id': 'Current SDL state',
                  'type': 'ENUMERATED',
                  'values': stnames,
                  'valuesInt': {a: b for b, a in enumerate(stnames)}}
Maxime Perrotin's avatar
Maxime Perrotin committed
384
        self.tree_items['_states'] = self.asn1_editor.setAsn1Model(states, row)
385

386
        # Add state variables for parallel states in aggregations
387
388
389
        for agg, substates in aggregates.viewitems():
            for each in substates:
                row += 1
390
391
                subst = ['not in state']
                subst.extend(list(opengeode.Helper.statenames(each)))
392
393
394
                states = {'id': 'Substate {}.{}'.format(CleanName(agg),
                                                        each.statename),
                          'type': 'ENUMERATED',
Maxime Perrotin's avatar
Maxime Perrotin committed
395
396
                          'values': subst,
                          'valuesInt': {a: b for b, a in enumerate(subst)}}
397
398
399
                self.tree_items['substate_{}'.format(each.statename)] = \
                        self.asn1_editor.setAsn1Model(states, row)

Maxime Perrotin's avatar
Maxime Perrotin committed
400
        # Add the SDL variables to the ASN.1 editor
401
        row += 1
402
        for var, (sort, _) in self.proc.variables.viewitems():
Maxime Perrotin's avatar
Maxime Perrotin committed
403
404
405
            sortName = sort.ReferencedTypeName
            item = asn1sccToasn1ValueEditorTypes(self.proc.dataview,
                                                 sortName, sort)
406
407
            self.tree_items[var] = self.asn1_editor.setAsn1Model(item, row)
            row += 1
408
409
        # In the simulation panel, set the buttons to send paramless TC/timers
        self.set_paramless_tc()
Maxime Perrotin's avatar
Maxime Perrotin committed
410
        self.set_paramless_tm()
411
        # Fill in data in the checker panel
412
        self.checker_table = self.set_dock_checker()
413
414
        # Add handler to callback functions for SDL external procedure calls
        self.register_external_procedures()
415
416
417
418
        self.get_sdl_state = getattr(value,
                                     '{}_state'.format(self.proc.processName))
        self.get_sdl_state.restype = ctypes.c_char_p
        # Initialization: set current state and internal variables
419
        self.current_sdl_state = u''
420
        self.init_timers()
421
422
        # Call the start transition of the SDL model
        getattr(value, '{}_startup'.format(self.proc.processName))()
423
        self.check_state()
424
        self.init_state = self.current_hash = self.on_event()
Maxime Perrotin's avatar
Maxime Perrotin committed
425

426
    def load_properties(self, prop_file=None):
Maxime Perrotin's avatar
Maxime Perrotin committed
427
428
429
430
        ''' Try loading a shared object with properties to verify
        Properties are e.g. stop conditions, processed by the "properties.py"
        module, and transformed to Ada code compiled as a dynamic library.
        There may be several properties, this function tries to retrieve
Maxime Perrotin's avatar
Maxime Perrotin committed
431
432
433
        them all without a priori knowledge of their content
        External API function (called by gui.py when called with -p prop_file)
        '''
434
435
        if not prop_file:
            return
Maxime Perrotin's avatar
Maxime Perrotin committed
436
        try:
Maxime Perrotin's avatar
Maxime Perrotin committed
437
438
            # Property file must be in the current directory
            self.prop_dll = ctypes.CDLL('./lib{}_stop_conditions.so'
Maxime Perrotin's avatar
Maxime Perrotin committed
439
440
                                   .format(self.proc.processName))
        except OSError as err:
Maxime Perrotin's avatar
Maxime Perrotin committed
441
442
            self.log_area.addItem('lib{}_stop_conditions.so not found '
                                  'in current directory'
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
                                  .format(self.proc.processName))
            return
        properties = []
        idx = 0
        while True:
            try:
                prop = getattr(self.prop_dll, '_property_{}'.format(idx))
                prop.restype = ctypes.c_uint
                properties.append(prop)
            except AttributeError:
                break
            else:
                idx +=1
        self.log_area.addItem('Loaded {} properties'.format(idx))
        self.log_area.addItem('Property file: {}'.format(prop_file))
        try:
            with open(prop_file, 'r') as pt:
                props, syntax, semantic, warnings, term = \
                   opengeode.ogParser.parseSingleElement('stop_if',
                                                         pt.read(),
                                                         self.proc)
                if syntax or semantic:
                    raise IOError('Properties parsing error')
        except IOError as err:
            self.log_area.addItem('Could not open property file!')
            return
        if idx != len(props):
            self.log_area.addItem('Wrong number of properties found!')
            return
472
473
        self.properties = {ppty.inputString: ptr
                           for ppty, ptr in zip(props, properties)}
Maxime Perrotin's avatar
Maxime Perrotin committed
474

475
    def check_properties(self, statehash):
Maxime Perrotin's avatar
Maxime Perrotin committed
476
477
478
479
480
        ''' Check the properties at runtime
        First copy the running system state to the property system state,
        then execute each property and check the return value '''
        if not self.prop_dll:
            return
481
        self.restore_global_state(statehash, dll=self.prop_dll)
482
        self.stop_conditions = []
483
        for text, check in self.properties.viewitems():
484
            if check():
485
486
                msg = 'Property "{}" is true'.format(text)
                self.log_area.addItem(msg)
487
                self.stop_conditions.append(text)
488
489
490
491
492
                if self.sim_param['state'] != 'exhaustive':
                    box = QMessageBox(QMessageBox.Information,
                                'Stop condition', msg)
                    box.exec_()
                    self.sim_param['state'] = 'manual'
Maxime Perrotin's avatar
Maxime Perrotin committed
493

494
495
496
497
498
499
500
501
    @Slot()
    def startStop(self):
        ''' Trigger or stop the SDL display '''
        self.running = not self.running
        if self.running:
            self.dock.show()
        else:
            self.dock.hide()
502

503
    def check_state(self):
504
        ''' Highlight the current state on the statechart diagram
Maxime Perrotin's avatar
Maxime Perrotin committed
505
        Return True if the state has changed '''
506
        state = self.get_sdl_state().decode('latin1')
507
508
509
        if state != self.current_sdl_state:
            self.current_sdl_state = state
            self.sdl_scene.clear_highlight()
510
511
512
513
            composition = state.split(UNICODE_SEP)
            for each in composition:
                for symb in self.sdl_scene.find_text(u'\\b{}\\b'.format(each)):
                    self.sdl_scene.highlight(symb)
514
            self.log_area.addItem('New state: {}'.format(CleanName(state)))
Maxime Perrotin's avatar
Maxime Perrotin committed
515
516
            return True
        return False
517

518
    def reset_simulation(self):
519
520
521
522
        ''' Jump back to the first step of simulation '''
        while self.undo_stack.canUndo():
            self.undo()
        self.log_area.clear()
523

Maxime Perrotin's avatar
Maxime Perrotin committed
524
525
526
527
    def undo(self):
        ''' Called when the undo button is pressed '''
        self.undo_stack.undo()
        self.check_state()
528
        self.current_hash = self.on_event(check_ppty=False)
529
        self.msc_undo.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
530
531
532
533
534
535

    def redo(self):
        ''' Called when the redo button is pressed '''
        self.undo_stack.redo()
        self.check_state()
        self.current_hash = self.on_event()
536
        self.msc_redo.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
537

Maxime Perrotin's avatar
Maxime Perrotin committed
538
    def restore_global_state(self, statehash, dll=None):
539
540
        ''' From a hashcode, restore a global state in the DLL (state +
            all internal variables '''
Maxime Perrotin's avatar
Maxime Perrotin committed
541
        target = dll or self.dll
542
        target_state = self.set_of_states[statehash]
543
        for idx, (var, (sort, _)) in enumerate(self.proc.variables.viewitems()):
544
            # get internal variables, translate them to swig, and print them
Maxime Perrotin's avatar
Maxime Perrotin committed
545
            setter_ptr = getattr(target, "_set_{}".format(var))
546
            value_asn1 = target_state[idx]
547
            setter_ptr(value_asn1._ptr)
548
        state_value = target_state[idx+1]
Maxime Perrotin's avatar
Maxime Perrotin committed
549
        set_state = getattr(target, "_set_state")
Maxime Perrotin's avatar
Maxime Perrotin committed
550
        set_state(ctypes.c_char_p(state_value.encode('latin1')))
Maxime Perrotin's avatar
Maxime Perrotin committed
551
552
        if target is self.dll:
            self.check_state()
553
554
555

    def change_internal_state(self):
        ''' When user press the "Apply" button to change the model's internal
Maxime Perrotin's avatar
Maxime Perrotin committed
556
557
            state (variables of the SDL model, or state of the automaton)
            Create an undo action that applies the change.
558
        '''
Maxime Perrotin's avatar
Maxime Perrotin committed
559
560
        # Create a new global state
        new_state = []
561
562
        # Get the variables values from the asn1_value_editor window
        for var, (sort, _) in self.proc.variables.viewitems():
Maxime Perrotin's avatar
Maxime Perrotin committed
563
564
565
            typename = sort.ReferencedTypeName.replace('-', '_')
            asn1_type = self.proc.dataview[sort.ReferencedTypeName]
            asn1_instance = getattr(ASN1, typename)()
566
            # Fill up the ASN.1 instance
567
568
            self.asn1_editor.getVariable(root=self.tree_items[var],
                                         dest=asn1_instance)
Maxime Perrotin's avatar
Maxime Perrotin committed
569
            new_state.append(asn1_instance)
Maxime Perrotin's avatar
Maxime Perrotin committed
570
        # Add the SDL state to the new global state, create a new hash, save it
571
572
        state_row = self.tree_items['_states'].row()
        new_sdl_state = self.asn1_editor.model.item(state_row, 3).text()
Maxime Perrotin's avatar
Maxime Perrotin committed
573
        new_state.append(UnicodeName(new_sdl_state))
Maxime Perrotin's avatar
Maxime Perrotin committed
574
575
576
577
578
        new_hash = hash(frozenset(new_state))
        self.set_of_states[new_hash] = new_state
        # Apply the change and create Undo command to restore previous state
        old_state = self.current_hash
        self.restore_global_state(new_hash)
579
        self.current_hash = new_hash
Maxime Perrotin's avatar
Maxime Perrotin committed
580
581
        undo_cmd = SendTC(self, old_state)
        self.undo_stack.push(undo_cmd)
582

583
    def on_event(self, tc_name=None, param=None, check_ppty=True):
Maxime Perrotin's avatar
Maxime Perrotin committed
584
585
586
        ''' Read the values of internal variables in the dll, update the gui
            accordingly (in the "global state" panel), and depending on the
            current SDL state, enable/disable the buttons for sending TCs.
587
            This function does not trigger any undoable action '''
588
        complete_state = []
589
        # Read in the DLL the list of internal variables
Maxime Perrotin's avatar
Maxime Perrotin committed
590
        for var, (sort, _) in self.proc.variables.viewitems():
591
            typename = sort.ReferencedTypeName.replace('-', '_')
Maxime Perrotin's avatar
Maxime Perrotin committed
592
            get_size = getattr(self.dll, "{}_size".format(var))
593
            get_size.restype = ctypes.c_uint
Maxime Perrotin's avatar
Maxime Perrotin committed
594
            size = get_size()
595
596
            # ctypes hint: don't use c_char_p except for text strings
            get_value = getattr(self.dll, "{}_value".format(var))
Maxime Perrotin's avatar
Maxime Perrotin committed
597
            get_value.restype = ctypes.c_void_p
598
            value = get_value()
Maxime Perrotin's avatar
Maxime Perrotin committed
599
600
601
602
603
            asn1_instance = getattr(ASN1, typename)()
            asn1_instance.SetData(value)
            self.asn1_editor.updateVariable(root=self.tree_items[var],
                                            asn1Var=asn1_instance)
            complete_state.append(asn1_instance)
604
        # Add the SDL state to the new global state
605
        complete_state.append(self.current_sdl_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
606
        # Update the SDL state in the global state panel
607
608
609
        readable_state = CleanName(self.current_sdl_state)
        state_row = self.tree_items['_states'].row()
        self.asn1_editor.model.item(state_row, 3).setText(readable_state)
610
        # And save this new state in the graph, if it was not there yet
611
        new_hash = hash(frozenset(complete_state))
612
613
614
615
616
        # Set a flag indicating a new state was added
        if new_hash not in self.set_of_states:
            self.new_state_created = True
        else:
            self.new_state_created = False
617
        self.set_of_states[new_hash] = complete_state
Maxime Perrotin's avatar
Maxime Perrotin committed
618
619
620
621
622
623
        # Disable the TC buttons the current state does does allow
        self.update_button_state(tc_name)
        if tc_name:
            # Log all TC sent
            self.log_area.addItem('Sent {}({})'.format(tc_name,
                                                       param or ''))
624
625
626
        if check_ppty:
            # When doing undo, dont check propertis again
            self.check_properties(new_hash)
627
        self.check_properties(new_hash)
Maxime Perrotin's avatar
Maxime Perrotin committed
628
629
630
631
632
        return new_hash

    def update_button_state(self, tc_name=None):
        ''' Depending on the current SDL state, enable or disable the buttons
            for sending TCs '''
633
        # Find the list of allowed TC based on the current state
634
        st = self.current_sdl_state.split(UNICODE_SEP)
635
636
637
638
        st_iter = st.pop(0)
        context = self.proc

        def find_allowed_tc(context, statename):
639
640
641
642
643
644
645
646
            try:
                inputs = context.mapping[statename.lower()]
                for each in inputs:
                    for inp in each.inputlist:
                        yield inp
            except KeyError as err:
                # FIXME: State Aggregations are not in context.mapping
                print('State {} not supported/found'.format(statename))
647
648
649
650

        allowed_tc = list(find_allowed_tc(context, st_iter))

        while len(st):
651
            # Handle state composition
652
653
654
655
656
657
            next_st = st.pop(0)
            for each in context.composite_states:
                if each.statename.lower() == st_iter.lower():
                    context = each
                    break
            allowed_tc.extend(list(find_allowed_tc(context, next_st)))
658
            st_iter = next_st
659

660
661
662
663
664
        # Remove timers from the list
        allowed_tc = set(allowed_tc) - set(self.proc.timers)
        # Enable/disable the parameterless TC buttons accordingly
        for tc, button in self.buttons.viewitems():
            if tc in self.proc.timers:
665
                # Ignore timers, they are handled differently, below
666
                continue
667
            button.setEnabled(tc in allowed_tc)
668
        if tc_name in self.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
669
            self.buttons[tc_name].setEnabled(False)
670
671
        # Emit the list of allowed TC for the GUI to update other buttons
        self.allowed_messages.emit(allowed_tc)
672
673
674

    def start_simu(self):
        '''
675
           Set up the simulation and checker bays, from UI files
676
           This panel handles parameterless signals and
677
678
           the simulation console
        '''
679
680
681
682
683
684
685
686
687
688
689
690
        docks = []
        for each in ('Simulation', 'Checker'):
            widgets = QUiLoader().load(QFile(':/{}.ui'.format(each.lower())),
                                       parent=self.parent)
            dock = QDockWidget('{} bay'.format(each), self.parent)
            dock.setFloating(False)
            dock.setObjectName(each)
            self.parent.addDockWidget(Qt.RightDockWidgetArea, dock)
            dock.setWidget(widgets)
            dock.show()
            docks.append(dock)
        return docks
691

692
693
694
695
696
697
698
699
700
701
702
703
704
705
    def click_tc(self, name, arg=None):
        ''' Send a TC by clicking on the Send button automatically
            Inputs: name of Input,
                    arg: parameter in GSER format (ASN.1 Value Notation)
            Doing so enables Undo/Redo, MSC Trace, etc. '''
        if name not in self.active_tc:
            return
        if name in self.buttons:
            # paramless TC
            self.buttons[name].click()
        else:
            # tc with a param, use the Send button
            for vals in self.param_tc_editors:
                if vals['name'] == name:
Maxime Perrotin's avatar
Maxime Perrotin committed
706
707
708
709
710
711
712
713
714
715
                    asn1Instance = vals['editor'].asn1Instance
                    ASN1_AST=self.proc.dataview
                    sort=ASN1_AST[vals['editor'].item['nodeTypename']].type
                    vn.valueNotationToCTypes(gser=arg,
                                             dest=asn1Instance,
                                             sort=sort,
                                             ASN1Mod=ASN1,
                                             ASN1_AST=ASN1_AST)
                    vals['editor'].updateVariable()
                    # Send a signal to click on the button
716
717
                    self.clicker.connect(vals['send_btn'].click)
                    self.clicker.emit()
718

719
720
    def random_step(self):
        ''' One step of random simulation '''
721
722
        if self.sim_param['state'] != 'random':
            return
723
        arg = None
724
        for name, asn1_ty in self.sim_param['periodic']:
725
726
727
            if asn1_ty:
                arg = compute_random_value(asn1_ty, self.proc.dataview)
            self.click_tc(name, arg)
728
        # Select randomly an active TC and call it
Maxime Perrotin's avatar
Maxime Perrotin committed
729
730
731
732
733
734
735
736
737
738
739
740
741
742
        try:
            random_tc, asn1_ty = random.choice(list(self.sim_param['random']))
        except IndexError:
            pass
        else:
            for inp in self.proc.input_signals:
                if inp['name'].lower() == random_tc.lower():
                    sort = inp.get('type', None)
                    if sort:
                        typename = sort.ReferencedTypeName.replace('-', '_')
                        ty = self.proc.dataview[sort.ReferencedTypeName]
                        arg = compute_random_value(ty, self.proc.dataview)
                    break
            self.click_tc(random_tc, arg)
743

744
745
        # Send a message every 100 ms.. Should be configurable
        QTimer().singleShot(100, self.random_step)
746

747
748
749
750
751
752
    def exhaustive_simulation(self):
        ''' Model checker - try all combinations of all inputs in all
        possible states, and verify properties on the fly '''
        print 'Exhaustive simulation (Breadth first)'
        next_level = []
        self.sim_param['state'] = 'exhaustive'
Maxime Perrotin's avatar
Maxime Perrotin committed
753
        total_err = 0
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788

        def exhaust_interface(name, asn1_ty):
            ''' Send all combinations of an input signal and return
            a list of new states (should be doing this in a worker thread) '''
            error = 0
            new_hashes = []
            if asn1_ty:
                for arg in compute_combinations(asn1_ty, self.proc.dataview):
                    QApplication.processEvents()
                    if self.sim_param['state'] != 'exhaustive':
                        return new_hashes, error
                    self.click_tc(name, arg)
                    if self.new_state_created:
                        # Create new state only if no stop conditions
                        if not self.stop_conditions:
                            new_hashes.append((name, arg, self.current_hash))
                        else:
                            # TODO: generate scenario
                            error += 1
                    self.undo()
            else:
                self.click_tc(name)
                if self.new_state_created:
                    new_hashes.append((name, None, self.current_hash))
                self.undo()
            return new_hashes, error
        for name in self.active_tc:
            ty = None
            for inp in self.proc.input_signals:
                if inp['name'].lower() == name.lower():
                    sort = inp.get('type', None)
                    if sort:
                        typename = sort.ReferencedTypeName.replace('-', '_')
                        ty = self.proc.dataview[sort.ReferencedTypeName]
            next_states, error_count = exhaust_interface(name, ty)
Maxime Perrotin's avatar
Maxime Perrotin committed
789
            total_err += error_count
790
791
792
            next_level.extend(next_states)
        print 'length of next level: ', len(next_level)

Maxime Perrotin's avatar
Maxime Perrotin committed
793
        print 'Number of stop conditions reached:', total_err
794

795
796
797
798
799
    def random_simulation(self):
        ''' Random simulator - read the config from the checker_table and
        call TC either randomly or periodically, until the stop button is
        pressed '''
        self.sim_param['state'] = 'random'
800
801
802
        self.sim_param['random'] = []
        self.sim_param['periodic'] = []
        for row_nb in xrange(self.checker_table.rowCount()):
803
804
805
            item = self.checker_table.item(row_nb, 0)
            name = item.text()
            asn1_ty = item.data(Qt.UserRole)
806
807
            cond = self.checker_table.cellWidget(row_nb, 1).currentText()
            if cond == 'Random':
808
                self.sim_param['random'].append((name, asn1_ty))
809
            elif cond == 'Periodic':
810
                self.sim_param['periodic'].append((name, asn1_ty))
811
        self.random_step()
812
813
814
815
816
817

    def stop_simulation(self):
        ''' Stop a random or exhaustive simulation '''
        print 'End of simulation'
        self.sim_param['state'] = 'manual'

818
819
820
821
822
    @Slot()
    def add_to_msc(self, direction, msg):
        ''' Create an undo command and display message on the MSC diagram '''
        self.msc.emit(direction, msg, self.undo_stack)

823
824
825
826
    @Slot()
    def send_tc(self, name, tc_func_ptr, param=None):
        ''' Send a TC - Used either locally (parameterless TCs) or via
        a signal sent by the B-mapper-generated backends '''
827
        self.msc_macro_start.emit()
828
        with undo.UndoMacro(self.undo_stack, 'Send TC'):
Maxime Perrotin's avatar
Maxime Perrotin committed
829
830
831
832
833
834
            if name in self.timers:
                self.add_to_msc('timeout', name)
            else:
                msg = '{tc}{arg}'.format(tc=name,
                                         arg='({})'.format(param.GSER())
                                             if param else '')
835
836
                self.add_to_msc('out', msg.replace('  ', ' ')
                                          .replace(' ,', ','))
837
838
839
840
            old_state = self.current_hash

            # Send the TC
            if param:
841
                tc_func_ptr(param._ptr)
842
843
844
            else:
                tc_func_ptr()

Maxime Perrotin's avatar
Maxime Perrotin committed
845
846
            if self.check_state():
                # If state changed, update the MSC
Maxime Perrotin's avatar
Maxime Perrotin committed
847
                self.add_to_msc('condition', CleanName(self.current_sdl_state))
848
849
850
851
            # Update windows, highlight state, enable/disable buttons, etc.
            self.current_hash = self.on_event(tc_name=name,
                                              param=param.GSER() if param
                                                                 else None)
852

853
854
855
            # Create the Undo command to restore the previous state
            undo_cmd = SendTC(self, old_state)
            self.undo_stack.push(undo_cmd)
856
        self.msc_macro_stop.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
857

Maxime Perrotin's avatar
Maxime Perrotin committed
858
    def receive_tm(self, tm_name):
859
        ''' Callback function when a paramless TM is received '''
860
        self.add_to_msc('in', tm_name)
Maxime Perrotin's avatar
Maxime Perrotin committed
861
        self.log_area.addItem('Received event "{}"'.format(tm_name))
Maxime Perrotin's avatar
Maxime Perrotin committed
862

863
    def external_proc_handler(self, name, *args):
864
        ''' Callback function when an external procedure is invoked
865
866
867
868
            Parameters: name is the name of the external procedure, and
            args is the list of arguments: (void*, size) for each in/out fpar
        '''
        assert len(args) % 2 is 0, "Invalid number of arguments"
869
        interface = {'in' : [], 'out': []}
870
871
872
873
        # Cut the params into tuples of (void *, size)
        params = ((args[i], args[i+1]) for i in xrange(0, len(args), 2))
        # Retrieve the AST of the procedure to get the list of FPARs
        procedure = self.proc_handlers[name.lower()][1]
874
        # Decode all input and output parameters and create native ASN.1 values
875
        for spec, (val, size) in zip(procedure.fpar, params):
876
            # Create native ASN.1 type
877
            typename = spec['type'].ReferencedTypeName.replace('-', '_')
878
            asn1_instance = getattr(ASN1, typename)(ptr=val)
879
880
881
882
            # Input parameters: copy the content in the ASN.1 Swig type
            if spec['direction'] == 'in':
                interface['in'].append((spec, asn1_instance))
            else:
883
                interface['out'].append((spec, val, asn1_instance))
Maxime Perrotin's avatar
Maxime Perrotin committed
884
        # make the function call
Maxime Perrotin's avatar
Maxime Perrotin committed
885
886
        vdm_cls = getattr(procedure, "vdm_instance", None)
        if vdm_cls:
Maxime Perrotin's avatar
Maxime Perrotin committed
887
            # convert input parameters to VDM value notation
Maxime Perrotin's avatar
Maxime Perrotin committed
888
            inp_as_vdm = []
Maxime Perrotin's avatar
Maxime Perrotin committed
889
890
891
892
893
894
895
            for spec, asn1_instance in interface['in']:
                as_pyside = vn.fromValueNotationToPySide('var',
                                                         asn1_instance.GSER())
                as_vdm = vdm_vn.pyside_to_vdm(as_pyside.popitem()[1],
                                              spec['type'], self.proc.dataview)
                inp_as_vdm.append(as_vdm)
            # Actual function call with input parameters in VDM format:
Maxime Perrotin's avatar
Maxime Perrotin committed
896
897
898
899
            outp = self.vdm.call_function(vdm_cls, name,
                                          ','.join(inp_as_vdm))
            print "CALLED VDM. Result =", outp
            spec, _, out_asn1_inst = interface['out'][0]
Maxime Perrotin's avatar
Maxime Perrotin committed
900
            # assuming 1 return parameter
901
902
903
904
905
            vdm_vn.vdm_to_ctypes(vdm=outp,
                                 dest=out_asn1_inst,
                                 sort=spec['type'],
                                 ASN1_AST=self.proc.dataview,
                                 ASN1Mod=ASN1)
906
907
        # Display the call on the MSC
        inp, outp = [], []
908
        for _, asn1_instance in interface['in']:
909
910
            inp.append(asn1_instance.GSER())
            del asn1_instance
911
        for _, _, asn1_instance in interface['out']:
912
            outp.append(asn1_instance.GSER())
913
            del(asn1_instance)
914
915
916
917
        call_str = u'{}({})'.format(name,
                                            ', '.join(chain(inp, outp)))
        self.add_to_msc('procedure_call', call_str)
        self.log_area.addItem('Call to {}'.format(call_str))
918

Maxime Perrotin's avatar
Maxime Perrotin committed
919
920
    def set_timer(self, name, duration):
        ''' Callback function when the SDL model sets a timer '''
921
        self.add_to_msc('set', 'SET_{}_{}'.format(name, duration))
Maxime Perrotin's avatar
Maxime Perrotin committed
922
923
        self.log_area.addItem('Received event "SET_{}({})"'
                              .format(name, duration))
924
        self.buttons[name].setEnabled(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
925
926
927

    def reset_timer(self, name):
        ''' Callback function when the SDL model resets a timer '''
928
        self.add_to_msc('reset', 'RESET_{}'.format(name))
Maxime Perrotin's avatar
Maxime Perrotin committed
929
930
        self.log_area.addItem('Received event "RESET_{}"'
                              .format(name))
931
        self.buttons[name].setEnabled(False)
Maxime Perrotin's avatar
Maxime Perrotin committed
932

933
    def set_dock_checker(self):
934
935
936
937
938
939
940
        ''' Once the DLL is loaded, fill in the checker tab with the list of
        TCs to allow user configuring the behaviour of the random and
        exhaustive simulators. Each TC trigger can be configured as periodic,
        random, or manual. If the TC has parameters, the feedlist can be
        customised to limit the range of values used in the simulator
        (this feature is not implemented yet) '''
        widget = self.dock_checker.widget()
941
942
        checker_table = widget.findChild(QTableWidget, 'tableWidget')
        checker_table.setRowCount(len(self.proc.input_signals))
943
944
        for idx, inp in enumerate(self.proc.input_signals):
            name = inp['name']
945
946
947
948
            sort = inp.get('type', None)
            if sort:
                typename = sort.ReferencedTypeName.replace('-', '_')
                ty = self.proc.dataview[sort.ReferencedTypeName]
Maxime Perrotin's avatar
Maxime Perrotin committed
949
950
            else:
                ty = None
951
952
            item = QTableWidgetItem(name)
            item.setFlags(Qt.ItemIsEnabled)
953
954
            # Associate the ASN.1 data type as hidden data
            item.setData(Qt.UserRole, ty)
955
956
            combo = QComboBox()
            combo.addItems(('Manual', 'Random', 'Periodic'))
957
958
959
960
961
            checker_table.setItem(idx, 0, item)
            checker_table.setCellWidget(idx, 1, combo)
        # Plug the "Random" button to the function handling random simulation
        random_btn = widget.findChild(QToolButton, 'randomButton')
        random_btn.pressed.connect(self.random_simulation)
962
963
        exhaust_btn = widget.findChild(QToolButton, 'exhaustButton')
        exhaust_btn.pressed.connect(self.exhaustive_simulation)
964
965
966
        stop_btn = widget.findChild(QToolButton, 'stopButton')
        stop_btn.pressed.connect(self.stop_simulation)
        return checker_table
967

968
969
    def set_paramless_tc(self):
        ''' Once the DLL is loaded set the buttons to send paramless TC '''
Maxime Perrotin's avatar
Maxime Perrotin committed
970
        # tc_area and buttons have to be in self because of known pyside bug
971
        widget = self.dock_simu.widget()
Maxime Perrotin's avatar
Maxime Perrotin committed
972
        self.tc_area = widget.findChild(QGridLayout, 'tc_grid')
973
974
975
        # Find parameterless input signals and create buttons
        for each in self.proc.input_signals:
            if 'type' not in each:
Maxime Perrotin's avatar
Maxime Perrotin committed
976
                self.buttons[each['name']] = QPushButton(each['name'])
977
        for each in self.proc.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
978
            self.buttons[each] = QPushButton(each+' timeout')
979
        col, row = 0, 0
Maxime Perrotin's avatar
Maxime Perrotin committed
980
        for name, button in self.buttons.viewitems():
981
982
983
984
            self.tc_area.addWidget(button, row, col)
            if col:
                row += 1
            col = (col + 1) % 2
985
986
            tc = getattr(self.dll, '{}_{}'.format(self.proc.processName,
                                                  name))
987
            button.pressed.connect(partial(self.send_tc, name, tc))
988

Maxime Perrotin's avatar
Maxime Perrotin committed
989
990
991
992
993
994
995
996
997
998
999
1000
1001
    def set_paramless_tm(self):
        ''' Once the DLL is loaded register the paramless TM to log them '''
        widget = self.dock_simu.widget()
        self.log_area = widget.findChild(QListWidget, 'log_tm')
        # Define a single function to handle all parameterless TM
        func = ctypes.CFUNCTYPE(None, ctypes.c_char_p)
        self.tm_func = func(self.receive_tm)
        for each in self.proc.output_signals:
            if 'type' not in each:
                register_func = getattr(self.dll, 'register_{}'
                                                   .format(each['name']))
                register_func(self.tm_func)

1002
1003
1004
1005
1006
    def register_external_procedures(self):
        ''' Once the DLL is loaded, register the external procedures
        specified in the SDL model and connect them to handling function '''
        # External procedures have a non-fixed number of parameters
        # but the first one is always a char string (name of procedure)
1007
        self.proc_handlers = {}
1008
1009
1010
        for each in self.proc.procedures:
            if not each.external:
                continue
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
            if each.comment:
                cmt = each.comment.inputString.lower()
            else:
                print(u"Unspecified language for procedure {} - default is C"
                      .format(each.inputString))
                cmt = '#c'
            # external procedure code has to be provided. Supported options
            # are VDM (Overture tool), and C/Ada (in .so)
            if "#vdm" in cmt:
                print(u'Procedure {} in VDM... Connecting to Overture'
                      .format(each.inputString))
Maxime Perrotin's avatar
Maxime Perrotin committed
1022
                if not self.vdm:
1023
1024
1025
1026
1027
1028
                    try:
                        self.vdm = vdmHandler.vdmHandler()
                    except IOError as err:
                        print("Socket connection error: " + str(err))
                        self.log_area.addItem('ERROR: could not connect to '
                                              'Overture')
Maxime Perrotin's avatar
Maxime Perrotin committed
1029
1030
1031
1032
1033
1034
                tokens = each.comment.inputString.split("#")
                classname = None
                for tok in tokens:
                    if tok.startswith("classname"):
                        #TODO: catch exception
                        classname = tok.split("=")[1]
1035
1036
1037
1038
1039
1040
                if self.vdm:
                    try:
                        inst = self.vdm.instanciate_class(classname)
                        each.vdm_instance = inst
                    except (IOError, AttributeError) as err:
                        print("VDM class creation error: " + str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
1041

1042
            elif "#c" in cmt:
Maxime Perrotin's avatar
Maxime Perrotin committed
1043
                print(u'Procedure {} in C... UNSUPPORTED'