sdlHandler.py 46.8 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
45
46
47
try:
    import opengeode
except ImportError:
    print 'OpenGEODE module is not available'

48
49
import opengeode.undoCommands as undo

Maxime Perrotin's avatar
Maxime Perrotin committed
50
51
52
try:
    import dataview_uniq_asn as ASN1
except ImportError:
Maxime Perrotin's avatar
Maxime Perrotin committed
53
    #print 'No Python A mapper generated dataview, SDL handler cannot be used'
Maxime Perrotin's avatar
Maxime Perrotin committed
54
    ASN1 = None
55

56
57
58
# 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
59
60
61
CleanName = lambda name: name.replace(UNICODE_SEP, '->')
UnicodeName = lambda name: name.replace('->', UNICODE_SEP)

Maxime Perrotin's avatar
Maxime Perrotin committed
62

63
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
# 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))


117
118
119
120
121
122
123
124
125
126
127
# 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
128
    elif basic.kind == 'BooleanType':
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
        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
148
def compute_integer_combinations(asn1_ty, max_iter=0):
149
150
151
152
153
    ''' 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
154
        if each > max_iter:
155
            break
156
157
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
        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 '''
187
188
189
190
    # 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
191
192
193
194
195
196
197
198
199
    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
200
    for size in xrange(int(asn1_ty.Min), int(asn1_ty.Max) + 1):
201
202
203
204
205
        elems = []
        for _ in xrange(size):
            elems.append(compute_combinations(asn1_ty, pool))
        for each in itertools.product(*elems):
            yield  '{{ {} }}'.format(', '.join(each))
206
207


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

217
218
219
    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 '''
220
        self.handler.restore_global_state(self.old_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
221
        self.handler.update_button_state()
222
223

    def redo(self):
224
225
226
        ''' 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
227
            self.handler.update_button_state()
228
229


230
class sdlHandler(QObject):
231
232
233
    '''
        Class managing SDL models
    '''
234
235
236
237
238
239
240
    # 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.
241
    msc = Signal(unicode, unicode, QUndoStack)
242
243
244
245
    msc_macro_start = Signal()
    msc_macro_stop = Signal()
    msc_undo = Signal()
    msc_redo = Signal()
246
    allowed_messages = Signal(list)
247

248
249
250
    def __init__(self, parent):
        ''' Startup: check if there are some SDL files in
            the directory and try to parse them and build the widget '''
251
        super(sdlHandler, self).__init__()
252
        random.seed()
253
        self.parent = parent
254
255
256
257
258
259
260
261
262
263
        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
264
            self.proc = root_ast.processes[0]
265
266
        except IndexError:
            raise IOError('SDL Handler failed to initialize')
Maxime Perrotin's avatar
Maxime Perrotin committed
267
        opengeode.Helper.flatten(self.proc)
268
        graph = opengeode.Statechart.create_dot_graph(self.proc, basic=True)
269
270
271
272
        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()
273
274
275
276
277
278
        # 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 = {}
279
        self.dock_simu, self.dock_checker = self.start_simu()
Maxime Perrotin's avatar
Maxime Perrotin committed
280
        self.current_sdl_state = ''
281
282
        # Handle the state of all timers ({'timerName': 'set'/'unset'})
        self.timers = {}
283
        # Keep a state graph to allow undo/redo and state exploration
284
        self.set_of_states = {}
285
        self.current_hash = None
286
287
        # Flag set to true when a new state is created
        self.new_state_created = False
288
289
        # When checking properties, list the currently true stop conditions
        self.stop_conditions = []
290
291
        # Create a stack for handling undo/redo commands
        self.undo_stack = QUndoStack(self)
292
293
294
295
296
297
        # 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
298
299
        undo_button.clicked.connect(self.undo)
        redo_button.clicked.connect(self.redo)
Maxime Perrotin's avatar
Maxime Perrotin committed
300
        # Placeholder to keep a list of properties to be checked at runtime
301
        self.properties = {}
Maxime Perrotin's avatar
Maxime Perrotin committed
302
        self.prop_dll = None
Maxime Perrotin's avatar
Maxime Perrotin committed
303
304
        # VDM handler instance, when needed for external procedures calls
        self.vdm = None
305
306
307
308
        # 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': []}
309
310
311
312
313
314
        # 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 = []
315

316
317
318
319
320
321
322
323
324
325
326
327
328
    @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
        st = unicode(self.current_sdl_state.decode('latin1'))
        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

329
330
331
332
333
334
335
336
337
    @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)
338
        self.dock.setFloating(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
339
        self.dock.resize(400, 400)
340
        self.dock.setObjectName('SDLViewer')
341
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock)
342
343
344
345
346
        self.dock.setAllowedAreas(Qt.NoDockWidgetArea)
        self.sdl_view.show()
        self.dock.setWidget(self.sdl_view)
        self.running = False
        self.dock.hide()
347
        # Dock widget to display the internal state
348
349
350
351
352
        ui = QFile(':/internalState.ui')
        loader = QUiLoader()
        widgets = loader.load(ui, parent=self.parent)
        self.asn1_editor = widgets.findChild(asn1_value_editor.asn1Editor,
                                             'ASN1EDITOR')
353
        self.asn1_editor.hideExtraColumns()
354
355
        apply_button = widgets.findChild(QToolButton, 'applyButton')
        apply_button.pressed.connect(self.change_internal_state)
356
        self.dock_state = QDockWidget('Internal state', self.parent)
357
358
        self.dock_state.setFloating(False)
        #self.dock_state.resize(400, 400)
359
360
        self.dock_state.setObjectName('InternalStateViewer')
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock_state)
361
        #self.dock_state.setAllowedAreas(Qt.NoDockWidgetArea)
362
        self.dock_state.setWidget(widgets)
363
364
        self.dock_state.show()
        self.parent.tabifyDockWidget(self.dock_state, self.dock_simu)
365
        self.parent.tabifyDockWidget(self.dock_simu, self.dock_checker)
Maxime Perrotin's avatar
Maxime Perrotin committed
366
        # Add the state list to the ASN.1 Editor (at row 0)
367
        row = 0
Maxime Perrotin's avatar
Maxime Perrotin committed
368
369
370
371
372
373
374
        statenames = [CleanName(s) for s in self.proc.mapping.viewkeys()
                      if not s.endswith(u'START')]
        states = {'id': 'Current SDL state', 'type': 'ENUMERATED',
                  'values': statenames}
        self.tree_items['_states'] = self.asn1_editor.setAsn1Model(states, row)
        # Add the SDL variables to the ASN.1 editor
        row = 1
375
        for var, (sort, _) in self.proc.variables.viewitems():
376
            item = asn1sccToasn1ValueEditorTypes(self.proc.dataview, var, sort)
377
378
            self.tree_items[var] = self.asn1_editor.setAsn1Model(item, row)
            row += 1
379
380
        # In the simulation panel, set the buttons to send paramless TC/timers
        self.set_paramless_tc()
Maxime Perrotin's avatar
Maxime Perrotin committed
381
        self.set_paramless_tm()
382
        # Fill in data in the checker panel
383
        self.checker_table = self.set_dock_checker()
384
385
        # Add handler to callback functions for SDL external procedure calls
        self.register_external_procedures()
386
387
388
389
        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
Maxime Perrotin's avatar
Maxime Perrotin committed
390
        self.current_sdl_state = ''
391
        self.check_state()
392
        self.init_timers()
393
        self.init_state = self.current_hash = self.on_event()
Maxime Perrotin's avatar
Maxime Perrotin committed
394

395
    def load_properties(self, prop_file=None):
Maxime Perrotin's avatar
Maxime Perrotin committed
396
397
398
399
        ''' 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
400
401
402
        them all without a priori knowledge of their content
        External API function (called by gui.py when called with -p prop_file)
        '''
403
404
        if not prop_file:
            return
Maxime Perrotin's avatar
Maxime Perrotin committed
405
        try:
Maxime Perrotin's avatar
Maxime Perrotin committed
406
407
            # Property file must be in the current directory
            self.prop_dll = ctypes.CDLL('./lib{}_stop_conditions.so'
Maxime Perrotin's avatar
Maxime Perrotin committed
408
409
                                   .format(self.proc.processName))
        except OSError as err:
Maxime Perrotin's avatar
Maxime Perrotin committed
410
411
            self.log_area.addItem('lib{}_stop_conditions.so not found '
                                  'in current directory'
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
                                  .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
441
442
        self.properties = {ppty.inputString: ptr
                           for ppty, ptr in zip(props, properties)}
Maxime Perrotin's avatar
Maxime Perrotin committed
443

444
    def check_properties(self, statehash):
Maxime Perrotin's avatar
Maxime Perrotin committed
445
446
447
448
449
        ''' 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
450
        self.restore_global_state(statehash, dll=self.prop_dll)
451
        self.stop_conditions = []
452
        for text, check in self.properties.viewitems():
453
            if check():
454
455
                msg = 'Property "{}" is true'.format(text)
                self.log_area.addItem(msg)
456
                self.stop_conditions.append(text)
457
458
459
460
461
                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
462

463
464
465
466
467
468
469
470
    @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()
471

472
    def check_state(self):
473
        ''' Highlight the current state on the statechart diagram
Maxime Perrotin's avatar
Maxime Perrotin committed
474
        Return True if the state has changed '''
475
476
477
478
        state = self.get_sdl_state()
        if state != self.current_sdl_state:
            self.current_sdl_state = state
            self.sdl_scene.clear_highlight()
479
            state = state.decode('latin1') # Recover the unicode chars
480
481
            for each in self.sdl_scene.find_text(u'\\b{}\\b'.format(state)):
                self.sdl_scene.highlight(each)
482
            self.log_area.addItem('New state: {}'.format(CleanName(state)))
Maxime Perrotin's avatar
Maxime Perrotin committed
483
484
            return True
        return False
485

486
    def reset_simulation(self):
487
488
489
490
        ''' Jump back to the first step of simulation '''
        while self.undo_stack.canUndo():
            self.undo()
        self.log_area.clear()
491

Maxime Perrotin's avatar
Maxime Perrotin committed
492
493
494
495
496
    def undo(self):
        ''' Called when the undo button is pressed '''
        self.undo_stack.undo()
        self.check_state()
        self.current_hash = self.on_event()
497
        self.msc_undo.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
498
499
500
501
502
503

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

Maxime Perrotin's avatar
Maxime Perrotin committed
506
    def restore_global_state(self, statehash, dll=None):
507
508
        ''' From a hashcode, restore a global state in the DLL (state +
            all internal variables '''
Maxime Perrotin's avatar
Maxime Perrotin committed
509
        target = dll or self.dll
510
        target_state = self.set_of_states[statehash]
511
        for idx, (var, (sort, _)) in enumerate(self.proc.variables.viewitems()):
512
            # get internal variables, translate them to swig, and print them
Maxime Perrotin's avatar
Maxime Perrotin committed
513
            setter_ptr = getattr(target, "_set_{}".format(var))
514
            value_asn1 = target_state[idx]
515
516
517
518
519
520
521
            try:
                value_swig_ptr = int(value_asn1._ptr)
            except TypeError:
                # for some types, swig uses a proxy class, in which case the
                # pointer is not in _ptr but in _ptr.this
                value_swig_ptr = int(value_asn1._ptr.this)
            value_ptr = ctypes.cast(value_swig_ptr,
522
523
524
                                    ctypes.POINTER(ctypes.c_uint32))
            setter_ptr(value_ptr)
        state_value = target_state[idx+1]
Maxime Perrotin's avatar
Maxime Perrotin committed
525
        set_state = getattr(target, "_set_state")
526
        set_state(ctypes.c_char_p(state_value))
Maxime Perrotin's avatar
Maxime Perrotin committed
527
528
        if target is self.dll:
            self.check_state()
529
530
531

    def change_internal_state(self):
        ''' When user press the "Apply" button to change the model's internal
Maxime Perrotin's avatar
Maxime Perrotin committed
532
533
            state (variables of the SDL model, or state of the automaton)
            Create an undo action that applies the change.
534
        '''
Maxime Perrotin's avatar
Maxime Perrotin committed
535
536
        # Create a new global state
        new_state = []
537
538
        # 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
539
540
541
542
543
544
545
546
547
            typename = sort.ReferencedTypeName.replace('-', '_')
            asn1_type = self.proc.dataview[sort.ReferencedTypeName]
            asn1_instance = getattr(ASN1, typename)()
            # Fill up the SWIG ASN.1 instance
            self.asn1_editor.to_asn1scc_swig(root=self.tree_items[var],
                                             dest=asn1_instance, ASN1Swig=ASN1,
                                             sort=sort,
                                             ASN1_AST=self.proc.dataview)
            new_state.append(asn1_instance)
Maxime Perrotin's avatar
Maxime Perrotin committed
548
        # Add the SDL state to the new global state, create a new hash, save it
Maxime Perrotin's avatar
Maxime Perrotin committed
549
550
551
        sdl_state = self.asn1_editor.getVariable(self.tree_items['_states'])
        new_sdl_state = sdl_state['Current SDL state']['Enum']
        new_state.append(UnicodeName(new_sdl_state))
Maxime Perrotin's avatar
Maxime Perrotin committed
552
553
554
555
556
        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)
557
        self.current_hash = new_hash
Maxime Perrotin's avatar
Maxime Perrotin committed
558
559
        undo_cmd = SendTC(self, old_state)
        self.undo_stack.push(undo_cmd)
560

561
    def on_event(self, tc_name=None, param=None):
Maxime Perrotin's avatar
Maxime Perrotin committed
562
563
564
        ''' 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.
565
            This function does not trigger any undoable action '''
566
        complete_state = []
567
        # Read in the DLL the list of internal variables
Maxime Perrotin's avatar
Maxime Perrotin committed
568
        for var, (sort, _) in self.proc.variables.viewitems():
569
            typename = sort.ReferencedTypeName.replace('-', '_')
Maxime Perrotin's avatar
Maxime Perrotin committed
570
            get_size = getattr(self.dll, "{}_size".format(var))
571
            get_size.restype = ctypes.c_uint
Maxime Perrotin's avatar
Maxime Perrotin committed
572
            size = get_size()
573
574
575
            # ctypes hint: don't use c_char_p except for text strings
            get_value = getattr(self.dll, "{}_value".format(var))
            get_value.restype = ctypes.POINTER(ctypes.c_char)
576
577
578
579
580
            value = get_value()
            swig_ptr = ASN1.DV.new_byte_SWIG_PTR(size)
            for idx in xrange(size):
                ASN1.DV.byte_SWIG_PTR_setitem(swig_ptr,
                                              idx,
581
582
                                              ord(value[idx])
                                                if value[idx] else 0)
583
584
585
586
            asn1_instance = getattr(ASN1, typename)()
            setter = getattr(ASN1.DV, "SetDataFor_{}".format(typename))
            setter(asn1_instance._ptr, swig_ptr)
            gser = asn1_instance.GSER()
Maxime Perrotin's avatar
Maxime Perrotin committed
587
            as_pyside = vn.fromValueNotationToPySide(var, gser)
588
589
            self.asn1_editor.updateVariable(as_pyside,
                                            root=self.tree_items[var])
590
            complete_state.append(asn1_instance)   # not gser
591
        # Add the SDL state to the new global state
592
        complete_state.append(self.current_sdl_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
593
594
595
596
597
        # Update the SDL state in the global state panel
        state_as_pyside = vn.fromValueNotationToPySide('Current SDL state',
                 '{}'.format(self.current_sdl_state.lower().replace('_', '-')))
        self.asn1_editor.updateVariable(state_as_pyside,
                                        root=self.tree_items['_states'])
598
        # And save this new state in the graph, if it was not there yet
599
        new_hash = hash(frozenset(complete_state))
600
601
602
603
604
        # 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
605
        self.set_of_states[new_hash] = complete_state
Maxime Perrotin's avatar
Maxime Perrotin committed
606
607
608
609
610
611
        # 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 ''))
612
        self.check_properties(new_hash)
613
        # TEMP TO TEST
614
#       for name, typedef in self.proc.dataview.viewitems():
615
#           if name != 'MySeq': continue
616
617
618
#           print 'All combinations of ', name
#           for combi in compute_combinations(typedef, self.proc.dataview):
#               print combi
619
        # END TEMP
Maxime Perrotin's avatar
Maxime Perrotin committed
620
621
622
623
624
        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 '''
625
        # Find the list of allowed TC based on the current state
626
627
        st = unicode(self.current_sdl_state.decode('latin1'))
        inputs = self.proc.mapping[st.replace(UNICODE_SEP, '_').lower()]
628
629
630
631
632
633
634
635
        allowed_tc = []
        for each in inputs:
            allowed_tc.extend(each.inputlist)
        # 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:
636
                # Ignore timers, they are handled differently, below
637
                continue
638
            button.setEnabled(tc in allowed_tc)
639
        if tc_name in self.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
640
            self.buttons[tc_name].setEnabled(False)
641
642
        # Emit the list of allowed TC for the GUI to update other buttons
        self.allowed_messages.emit(allowed_tc)
643
644
645

    def start_simu(self):
        '''
646
           Set up the simulation and checker bays, from UI files
647
           This panel handles parameterless signals and
648
649
           the simulation console
        '''
650
651
652
653
654
655
656
657
658
659
660
661
        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
662

663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
    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:
                    argpy = vn.fromValueNotationToPySide(name, arg)
                    vals['editor'].updateVariable(argpy)
                    vals['send_btn'].click()

681
682
    def random_step(self):
        ''' One step of random simulation '''
683
684
        if self.sim_param['state'] != 'random':
            return
685
        arg = None
686
        for name, asn1_ty in self.sim_param['periodic']:
687
688
689
            if asn1_ty:
                arg = compute_random_value(asn1_ty, self.proc.dataview)
            self.click_tc(name, arg)
690
        # Select randomly an active TC and call it
Maxime Perrotin's avatar
Maxime Perrotin committed
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
        #random_tc = random.choice(list(self.active_tc))
        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)
706

707
        QTimer().singleShot(1000, self.random_step)
708

709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
    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'

        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)
            next_level.extend(next_states)
        print 'length of next level: ', len(next_level)

        print 'Number of stop conditions reached:', error_count

755
756
757
758
759
    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'
760
761
762
        self.sim_param['random'] = []
        self.sim_param['periodic'] = []
        for row_nb in xrange(self.checker_table.rowCount()):
763
764
765
            item = self.checker_table.item(row_nb, 0)
            name = item.text()
            asn1_ty = item.data(Qt.UserRole)
766
767
            cond = self.checker_table.cellWidget(row_nb, 1).currentText()
            if cond == 'Random':
768
                self.sim_param['random'].append((name, asn1_ty))
769
            elif cond == 'Periodic':
770
                self.sim_param['periodic'].append((name, asn1_ty))
771
        self.random_step()
772
773
774
775
776
777

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

778
779
780
781
782
    @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)

783
784
785
786
    @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 '''
787
        self.msc_macro_start.emit()
788
        with undo.UndoMacro(self.undo_stack, 'Send TC'):
Maxime Perrotin's avatar
Maxime Perrotin committed
789
790
791
792
793
794
795
            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 '')
                self.add_to_msc('out', msg)
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
            old_state = self.current_hash

            # Send the TC
            if param:
                # Cast the SWIG type (ASN.1 Native format) to a ctypes pointer
                try:
                    swig_ptr = int(param._ptr)
                except TypeError:
                    # when swig uses a proxy class, pointer is in _ptr.this
                    swig_ptr = int(param._ptr.this)
                param_ptr = ctypes.cast(swig_ptr,
                                        ctypes.POINTER(ctypes.c_uint32))
                tc_func_ptr(param_ptr)
            else:
                tc_func_ptr()

Maxime Perrotin's avatar
Maxime Perrotin committed
812
813
            if self.check_state():
                # If state changed, update the MSC
Maxime Perrotin's avatar
Maxime Perrotin committed
814
                self.add_to_msc('condition', CleanName(self.current_sdl_state))
815
816
817
818
            # Update windows, highlight state, enable/disable buttons, etc.
            self.current_hash = self.on_event(tc_name=name,
                                              param=param.GSER() if param
                                                                 else None)
819

820
821
822
            # Create the Undo command to restore the previous state
            undo_cmd = SendTC(self, old_state)
            self.undo_stack.push(undo_cmd)
823
        self.msc_macro_stop.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
824

Maxime Perrotin's avatar
Maxime Perrotin committed
825
    def receive_tm(self, tm_name):
826
        ''' Callback function when a paramless TM is received '''
827
        self.add_to_msc('in', tm_name)
Maxime Perrotin's avatar
Maxime Perrotin committed
828
        self.log_area.addItem('Received event "{}"'.format(tm_name))
Maxime Perrotin's avatar
Maxime Perrotin committed
829

830
    def external_proc_handler(self, name, *args):
831
        ''' Callback function when an external procedure is invoked
832
833
834
835
            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"
836
        interface = {'in' : [], 'out': []}
837
838
839
840
        # 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]
841
        # Decode all input and output parameters and create native ASN.1 values
842
843
844
        for spec, (val, size) in zip(procedure.fpar, params):
            # Cast the void* to an array of unsigned bytes, knowing the size:
            as_bytes = ctypes.cast(val,
845
846
                                 ctypes.POINTER((ctypes.c_ubyte * (size / 8))))
            # Create native ASN.1 type
847
848
            typename = spec['type'].ReferencedTypeName.replace('-', '_')
            asn1_instance = getattr(ASN1, typename)()
849
850
851
852
853
854
855
856
857
858
859
860
861
862
            # Input parameters: copy the content in the ASN.1 Swig type
            if spec['direction'] == 'in':
                # Create a SWIG buffer of the same size:
                swig_ptr = ASN1.DV.new_byte_SWIG_PTR(size / 8)
                # Copy the content of the input buffer to the SWIG buffer:
                for idx in xrange(size / 8):
                    ASN1.DV.byte_SWIG_PTR_setitem(swig_ptr,
                                                  idx,
                                                  as_bytes.contents[idx])
                setter = getattr(ASN1.DV, "SetDataFor_{}".format(typename))
                setter(asn1_instance._ptr, swig_ptr)
                interface['in'].append((spec, asn1_instance))
            else:
                interface['out'].append((spec, as_bytes, asn1_instance))
Maxime Perrotin's avatar
Maxime Perrotin committed
863
        # make the function call
Maxime Perrotin's avatar
Maxime Perrotin committed
864
865
        vdm_cls = getattr(procedure, "vdm_instance", None)
        if vdm_cls:
Maxime Perrotin's avatar
Maxime Perrotin committed
866
            # convert input parameters to VDM value notation
Maxime Perrotin's avatar
Maxime Perrotin committed
867
            inp_as_vdm = []
Maxime Perrotin's avatar
Maxime Perrotin committed
868
869
870
871
872
873
874
            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
875
876
877
            outp = self.vdm.call_function(vdm_cls, name,
                                          ','.join(inp_as_vdm))
            print "CALLED VDM. Result =", outp
Maxime Perrotin's avatar
Maxime Perrotin committed
878
            #outp = outp.replace('[', '{').replace(']', '}')
Maxime Perrotin's avatar
Maxime Perrotin committed
879
            spec, _, out_asn1_inst = interface['out'][0]
Maxime Perrotin's avatar
Maxime Perrotin committed
880
881
882
883
884
885
            # assuming 1 return parameter
            vdm_vn.vdm_to_swig(vdm=outp,
                               dest=out_asn1_inst,
                               sort=spec['type'],
                               ASN1_AST=self.proc.dataview,
                               ASN1Swig=ASN1)
886
887
888
889
890
891
892
893
894
895
        # Copy the OUT parameters back from SWIG to ctypes
        for spec, as_bytes, asn1_instance in interface['out']:
            # Create new SWIG byte array
            swig_ptr = ASN1.DV.new_byte_SWIG_PTR(len(as_bytes.contents))
            typename = spec['type'].ReferencedTypeName.replace('-', '_')
            setter = getattr(ASN1.DV, "SetDataFor_{}".format(typename))
            setter(swig_ptr, asn1_instance._ptr)
            for idx in xrange(len(as_bytes.contents)):
                as_bytes.contents[idx] = \
                        ASN1.DV.byte_SWIG_PTR_getitem(swig_ptr, idx)
896
897
        # Display the call on the MSC
        inp, outp = [], []
898
        for _, asn1_instance in interface['in']:
899
900
            inp.append(asn1_instance.GSER())
            del asn1_instance
901
        for _, _, asn1_instance in interface['out']:
902
            outp.append(asn1_instance.GSER())
903
            del(asn1_instance)
904
905
906
907
        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))
908

Maxime Perrotin's avatar
Maxime Perrotin committed
909
910
    def set_timer(self, name, duration):
        ''' Callback function when the SDL model sets a timer '''
911
        self.add_to_msc('set', 'SET_{}_{}'.format(name, duration))
Maxime Perrotin's avatar
Maxime Perrotin committed
912
913
        self.log_area.addItem('Received event "SET_{}({})"'
                              .format(name, duration))
914
        self.buttons[name].setEnabled(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
915
916
917

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

923
    def set_dock_checker(self):
924
925
926
927
928
929
930
        ''' 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()
931
932
        checker_table = widget.findChild(QTableWidget, 'tableWidget')
        checker_table.setRowCount(len(self.proc.input_signals))
933
934
        for idx, inp in enumerate(self.proc.input_signals):
            name = inp['name']
935
936
937
938
            sort = inp.get('type', None)
            if sort:
                typename = sort.ReferencedTypeName.replace('-', '_')
                ty = self.proc.dataview[sort.ReferencedTypeName]
Maxime Perrotin's avatar
Maxime Perrotin committed
939
940
            else:
                ty = None
941
942
            item = QTableWidgetItem(name)
            item.setFlags(Qt.ItemIsEnabled)
943
944
            # Associate the ASN.1 data type as hidden data
            item.setData(Qt.UserRole, ty)
945
946
            combo = QComboBox()
            combo.addItems(('Manual', 'Random', 'Periodic'))
947
948
949
950
951
            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)
952
953
        exhaust_btn = widget.findChild(QToolButton, 'exhaustButton')
        exhaust_btn.pressed.connect(self.exhaustive_simulation)
954
955
956
        stop_btn = widget.findChild(QToolButton, 'stopButton')
        stop_btn.pressed.connect(self.stop_simulation)
        return checker_table
957

958
959
    def set_paramless_tc(self):
        ''' Once the DLL is loaded set the buttons to send paramless TC '''
Maxime Perrotin's avatar
Maxime Perrotin committed
960
        # tc_area and buttons have to be in self because of known pyside bug
961
        widget = self.dock_simu.widget()
Maxime Perrotin's avatar
Maxime Perrotin committed
962
        self.tc_area = widget.findChild(QGridLayout, 'tc_grid')
963
964
965
        # 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
966
                self.buttons[each['name']] = QPushButton(each['name'])
967
        for each in self.proc.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
968
            self.buttons[each] = QPushButton(each+' timeout')
969
        col, row = 0, 0
Maxime Perrotin's avatar
Maxime Perrotin committed
970
        for name, button in self.buttons.viewitems():
971
972
973
974
            self.tc_area.addWidget(button, row, col)
            if col:
                row += 1
            col = (col + 1) % 2
975
976
            tc = getattr(self.dll, '{}_{}'.format(self.proc.processName,
                                                  name))
977
            button.pressed.connect(partial(self.send_tc, name, tc))
978

Maxime Perrotin's avatar
Maxime Perrotin committed
979
980
981
982
983
984
985
986
987
988
989
990
991
    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)

992
993
994
995
996
    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)
997
        self.proc_handlers = {}
998
999
1000
        for each in self.proc.procedures:
            if not each.external:
                continue
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
            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
1012
                if not self.vdm:
1013
1014
1015
1016
1017
1018
                    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
1019
1020
1021
1022
1023
1024
                tokens = each.comment.inputString.split("#")
                classname = None
                for tok in tokens:
                    if tok.startswith("classname"):
                        #TODO: catch exception
                        classname = tok.split("=")[1]
1025
1026
1027
1028
1029
1030
                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
1031

1032
1033
1034
1035
1036
1037
            elif "#c" in cmt:
                print(u'Procedure {} in C... Loading DLL'
                      .format(each.inputString))
            elif "#ada" in cmt:
                print(u'Procedure {} in Ada... Loading DLL'
                      .format(each.inputString))
1038
1039
1040
1041
1042
1043
            # Variable number of parameters of type (void *, size)
            params = (ctypes.c_char_p,) + \
                    (ctypes.c_void_p, ctypes.c_long) * len(each.fpar)
            func = ctypes.CFUNCTYPE(None, *params)
            self.proc_handlers[each.inputString.lower()] = \
                    (func(self.external_proc_handler), each)
1044
1045
            register_func = getattr(self.dll, "register_{}"
                                              .format(each.inputString))
1046
            register_func(self.proc_handlers[each.inputString.lower()][0])
1047
1048


1049
1050
    def init_timers(self):
        ''' When loading the DLL, initialize timers/set callbacks, etc '''
Maxime Perrotin's avatar
Maxime Perrotin committed
1051
1052
1053
1054
1055
        # Define a single function to handle all timer SET functions
        set_func = ctypes.CFUNCTYPE(None, ctypes.c_char_p, ctypes.c_int)
        reset_func = ctypes.CFUNCTYPE(None, ctypes.c_char_p)
        self.set_timer_wrap = set_func(self.set_timer)
        self.reset_timer_wrap = reset_func(self.reset_timer)
1056
1057
1058
        for each in self.proc.timers:
            self.timers[each] = 'unset'
            self.buttons[each].setEnabled(False)
Maxime Perrotin's avatar
Maxime Perrotin committed
1059
1060
1061
1062
1063
1064
            register_set_func = getattr(self.dll, 'register_SET_{}'
                                                  .format(each))
            register_set_func(self.set_timer_wrap)
            register_reset_func = getattr(self.dll, 'register_RESET_{}'
                                                    .format(each))
            register_reset_func(self.reset_timer_wrap)