sdlHandler.py 43.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
23
import sys
Maxime Perrotin's avatar
Maxime Perrotin committed
24
import ctypes
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
import vdmHandler
42
from ValueGenerator import compute_random_value, compute_combinations
Maxime Perrotin's avatar
Maxime Perrotin committed
43

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

50

Maxime Perrotin's avatar
Maxime Perrotin committed
51
52
try:
    import dataview_uniq_asn as ASN1
53
    import datamodel   # Generated by the Pyside B mapper
Maxime Perrotin's avatar
Maxime Perrotin committed
54
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
61
# 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
62
63
CleanName = lambda name: name.replace(UNICODE_SEP, '.')
UnicodeName = lambda name: name.replace('.', UNICODE_SEP)
Maxime Perrotin's avatar
Maxime Perrotin committed
64

Maxime Perrotin's avatar
Maxime Perrotin committed
65

66
67
class SendTC(QUndoCommand):
    ''' Undo command to send a message to the running system '''
68
69
    def __init__(self, handler, old_state):
        ''' Init: save the current and old states '''
70
71
        super(SendTC, self).__init__()
        self.handler = handler
72
73
74
        self.new_state = handler.current_hash
        self.old_state = old_state

75
76
77
    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 '''
78
        self.handler.restore_global_state(self.old_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
79
        self.handler.update_button_state()
80
81

    def redo(self):
82
83
84
        ''' 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
85
            self.handler.update_button_state()
86
87


88
class sdlHandler(QObject):
89
90
91
    '''
        Class managing SDL models
    '''
92
93
94
95
96
97
98
    # 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.
99
    msc = Signal(unicode, unicode, QUndoStack)
100
101
102
103
    msc_macro_start = Signal()
    msc_macro_stop = Signal()
    msc_undo = Signal()
    msc_redo = Signal()
104
    allowed_messages = Signal(list)
105
    clicker = Signal()
106

107
108
109
    def __init__(self, parent):
        ''' Startup: check if there are some SDL files in
            the directory and try to parse them and build the widget '''
110
        super(sdlHandler, self).__init__()
111
        random.seed()
112
        self.parent = parent
113
114
115
116
117
118
119
        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')
120
121
122
        # Parse the SDL model - use an ASN.1 AST compatible with C types,
        # as this is needed to access DV.enumeratedConstants in random simu
        sys.argv.append('--toC')
123
        self.ast = opengeode.parse(pr_files)
124
        sys.argv.pop()
125
126
        try:
            root_ast = self.ast[0]
Maxime Perrotin's avatar
Maxime Perrotin committed
127
            self.proc = root_ast.processes[0]
128
129
        except IndexError:
            raise IOError('SDL Handler failed to initialize')
130
        #opengeode.Helper.flatten(self.proc)
131
        graph = opengeode.Statechart.create_dot_graph(self.proc, basic=True)
132
133
134
135
        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()
136
137
138
139
140
141
        # 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 = {}
142
        self.dock_simu, self.dock_checker = self.start_simu()
Maxime Perrotin's avatar
Maxime Perrotin committed
143
        self.current_sdl_state = ''
144
145
        # Handle the state of all timers ({'timerName': 'set'/'unset'})
        self.timers = {}
146
        # Keep a state graph to allow undo/redo and state exploration
147
        self.set_of_states = {}
148
        self.current_hash = None
149
150
        # Flag set to true when a new state is created
        self.new_state_created = False
151
152
        # When checking properties, list the currently true stop conditions
        self.stop_conditions = []
153
154
        # Create a stack for handling undo/redo commands
        self.undo_stack = QUndoStack(self)
155
156
157
158
159
160
        # 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
161
162
        undo_button.clicked.connect(self.undo)
        redo_button.clicked.connect(self.redo)
Maxime Perrotin's avatar
Maxime Perrotin committed
163
        # Placeholder to keep a list of properties to be checked at runtime
164
        self.properties = {}
Maxime Perrotin's avatar
Maxime Perrotin committed
165
        self.prop_dll = None
Maxime Perrotin's avatar
Maxime Perrotin committed
166
167
        # VDM handler instance, when needed for external procedures calls
        self.vdm = None
168
169
170
171
        # 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': []}
172
173
174
175
176
177
        # 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 = []
178

179
180
181
182
    @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
183
        st = self.current_sdl_state
184
185
186
187
188
189
190
191
        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

192
193
194
195
196
197
198
199
200
    @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)
201
        self.dock.setFloating(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
202
        self.dock.resize(400, 400)
203
        self.dock.setObjectName('SDLViewer')
204
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock)
205
206
207
208
209
        self.dock.setAllowedAreas(Qt.NoDockWidgetArea)
        self.sdl_view.show()
        self.dock.setWidget(self.sdl_view)
        self.running = False
        self.dock.hide()
210
        # Dock widget to display the internal state
211
212
213
214
215
        ui = QFile(':/internalState.ui')
        loader = QUiLoader()
        widgets = loader.load(ui, parent=self.parent)
        self.asn1_editor = widgets.findChild(asn1_value_editor.asn1Editor,
                                             'ASN1EDITOR')
216
        self.asn1_editor.hideExtraColumns()
217
218
        apply_button = widgets.findChild(QToolButton, 'applyButton')
        apply_button.pressed.connect(self.change_internal_state)
219
        self.dock_state = QDockWidget('Internal state', self.parent)
220
221
        self.dock_state.setFloating(False)
        #self.dock_state.resize(400, 400)
222
223
        self.dock_state.setObjectName('InternalStateViewer')
        self.parent.addDockWidget(Qt.RightDockWidgetArea, self.dock_state)
224
        #self.dock_state.setAllowedAreas(Qt.NoDockWidgetArea)
225
        self.dock_state.setWidget(widgets)
226
227
        self.dock_state.show()
        self.parent.tabifyDockWidget(self.dock_state, self.dock_simu)
228
        self.parent.tabifyDockWidget(self.dock_simu, self.dock_checker)
Maxime Perrotin's avatar
Maxime Perrotin committed
229
        # Add the state list to the ASN.1 Editor (at row 0)
230
        row = 0
231
232
233

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

237
238
        stnames = list(opengeode.Helper.statenames(context, sep=UNICODE_SEP))
        stnames.extend(list(opengeode.Helper.rec_findstates(context)))
239

Maxime Perrotin's avatar
Maxime Perrotin committed
240
241
242
243
        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
244
        self.tree_items['_states'] = self.asn1_editor.setAsn1Model(states, row)
245

246
        # Add state variables for parallel states in aggregations
247
248
249
        for agg, substates in aggregates.viewitems():
            for each in substates:
                row += 1
250
251
                subst = ['not in state']
                subst.extend(list(opengeode.Helper.statenames(each)))
252
253
254
                states = {'id': 'Substate {}.{}'.format(CleanName(agg),
                                                        each.statename),
                          'type': 'ENUMERATED',
Maxime Perrotin's avatar
Maxime Perrotin committed
255
256
                          'values': subst,
                          'valuesInt': {a: b for b, a in enumerate(subst)}}
257
258
259
                self.tree_items['substate_{}'.format(each.statename)] = \
                        self.asn1_editor.setAsn1Model(states, row)

Maxime Perrotin's avatar
Maxime Perrotin committed
260
        # Add the SDL variables to the ASN.1 editor
261
        row += 1
262
        for var, (sort, _) in self.proc.variables.viewitems():
Maxime Perrotin's avatar
Maxime Perrotin committed
263
264
            sortName = sort.ReferencedTypeName
            item = asn1sccToasn1ValueEditorTypes(self.proc.dataview,
265
                                                 var, sort)
266
267
            self.tree_items[var] = self.asn1_editor.setAsn1Model(item, row)
            row += 1
268
269
        # In the simulation panel, set the buttons to send paramless TC/timers
        self.set_paramless_tc()
Maxime Perrotin's avatar
Maxime Perrotin committed
270
        self.set_paramless_tm()
271
        # Fill in data in the checker panel
272
        self.checker_table = self.set_dock_checker()
273
274
        # Add handler to callback functions for SDL external procedure calls
        self.register_external_procedures()
275
276
277
278
        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
279
        self.current_sdl_state = u''
280
        self.init_timers()
281
282
        # Call the start transition of the SDL model
        getattr(value, '{}_startup'.format(self.proc.processName))()
283
        self.check_state()
284
285
286
287
288
289
290
291
292
        try:
            self.init_state = self.current_hash = self.on_event()
        except ValueError as err:
            # Exception raised when some SDL variables are not initialized
            # (in that case impossible to read a proper state)
            box = QMessageBox(QMessageBox.Critical,
                              'SDL Variable not initialized', str(err))
            box.exec_()
            raise
Maxime Perrotin's avatar
Maxime Perrotin committed
293

294
    def load_properties(self, prop_file=None):
Maxime Perrotin's avatar
Maxime Perrotin committed
295
296
297
298
        ''' 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
299
300
301
        them all without a priori knowledge of their content
        External API function (called by gui.py when called with -p prop_file)
        '''
302
303
        if not prop_file:
            return
Maxime Perrotin's avatar
Maxime Perrotin committed
304
        try:
Maxime Perrotin's avatar
Maxime Perrotin committed
305
306
            # Property file must be in the current directory
            self.prop_dll = ctypes.CDLL('./lib{}_stop_conditions.so'
Maxime Perrotin's avatar
Maxime Perrotin committed
307
308
                                   .format(self.proc.processName))
        except OSError as err:
Maxime Perrotin's avatar
Maxime Perrotin committed
309
310
311
            self.log_area.addItem('lib{}_stop_conditions.so could not be '
                                  'loaded - {}'
                                  .format(self.proc.processName, str(err)))
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
            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
340
341
        self.properties = {ppty.inputString: ptr
                           for ppty, ptr in zip(props, properties)}
Maxime Perrotin's avatar
Maxime Perrotin committed
342

343
    def check_properties(self, statehash):
Maxime Perrotin's avatar
Maxime Perrotin committed
344
345
346
347
348
        ''' 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
349
        self.restore_global_state(statehash, dll=self.prop_dll)
350
        self.stop_conditions = []
351
        for text, check in self.properties.viewitems():
352
            if check():
353
354
                msg = 'Property "{}" is true'.format(text)
                self.log_area.addItem(msg)
355
                self.stop_conditions.append(text)
356
357
358
359
360
                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
361

362
363
364
365
366
367
368
369
    @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()
370

371
    def check_state(self):
372
        ''' Highlight the current state on the statechart diagram
Maxime Perrotin's avatar
Maxime Perrotin committed
373
        Return True if the state has changed '''
374
        state = self.get_sdl_state().decode('latin1')
375
376
377
        if state != self.current_sdl_state:
            self.current_sdl_state = state
            self.sdl_scene.clear_highlight()
378
379
380
381
            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)
382
            self.log_area.addItem('New state: {}'.format(CleanName(state)))
Maxime Perrotin's avatar
Maxime Perrotin committed
383
384
            return True
        return False
385

386
    def reset_simulation(self):
387
388
389
390
        ''' Jump back to the first step of simulation '''
        while self.undo_stack.canUndo():
            self.undo()
        self.log_area.clear()
391

Maxime Perrotin's avatar
Maxime Perrotin committed
392
393
394
395
    def undo(self):
        ''' Called when the undo button is pressed '''
        self.undo_stack.undo()
        self.check_state()
396
        self.current_hash = self.on_event(check_ppty=False)
397
        self.msc_undo.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
398
399
400
401
402
403

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

Maxime Perrotin's avatar
Maxime Perrotin committed
406
    def restore_global_state(self, statehash, dll=None):
407
408
        ''' From a hashcode, restore a global state in the DLL (state +
            all internal variables '''
Maxime Perrotin's avatar
Maxime Perrotin committed
409
        target = dll or self.dll
410
        target_state = self.set_of_states[statehash]
411
        for idx, (var, (sort, _)) in enumerate(self.proc.variables.viewitems()):
412
            # get internal variables, translate them to swig, and print them
Maxime Perrotin's avatar
Maxime Perrotin committed
413
            setter_ptr = getattr(target, "_set_{}".format(var))
414
415
416
417
            #value_asn1 = target_state[idx]
            value_uper = target_state[idx]
            typename = sort.ReferencedTypeName.replace('-', '_')
            value_asn1 = self.decode_from_uper(value_uper, typename)
418
            setter_ptr(value_asn1._ptr)
419
        state_value = target_state[idx+1]
Maxime Perrotin's avatar
Maxime Perrotin committed
420
        set_state = getattr(target, "_set_state")
Maxime Perrotin's avatar
Maxime Perrotin committed
421
        set_state(ctypes.c_char_p(state_value.encode('latin1')))
Maxime Perrotin's avatar
Maxime Perrotin committed
422
423
        if target is self.dll:
            self.check_state()
424

425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
    def check_asn1_constraints(self, instance, typename_c):
        ''' ASN1SCC provides functions to check ASN.1 constraints '''
        is_valid, err_code = instance.IsConstraintValid()
        if not is_valid:
            msg = ("Type {}: constraint error - {}"
                    .format(datamodel.errCodes[err_code]['name'],
                            datamodel.errCodes[err_code]['constraint']))
            raise ValueError(msg)

    def encode_uper(self, instance, typename_c):
        ''' Encode an ASN.1 value to unaligned PER using ASN1SCC '''
        assert '-' not in typename_c
        size = getattr(ASN1.DV, "{}_REQUIRED_BYTES_FOR_ENCODING"
                                .format(typename_c))
        buf = ASN1.DataStream(size)
        instance.Encode(buf)
        return buf.GetPyString()

    def decode_from_uper(self, uper_buf, typename_c, to_inst=None):
        ''' Decode an ASN.1 uPER-encoded value to a ctype instance
            to_inst is an optional instance to put the value in '''
        assert '-' not in typename_c
        to_inst = to_inst or getattr(ASN1, typename_c)()
        size = getattr(ASN1.DV, "{}_REQUIRED_BYTES_FOR_ENCODING"
449
                                .format(typename_c))
450
451
452
453
454
        buf = ASN1.DataStream(size)
        buf.SetFromPyString(uper_buf)
        to_inst.Decode(buf)
        return to_inst

455
456
    def change_internal_state(self):
        ''' When user press the "Apply" button to change the model's internal
Maxime Perrotin's avatar
Maxime Perrotin committed
457
458
            state (variables of the SDL model, or state of the automaton)
            Create an undo action that applies the change.
459
        '''
Maxime Perrotin's avatar
Maxime Perrotin committed
460
461
        # Create a new global state
        new_state = []
462
463
        # 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
464
465
466
            typename = sort.ReferencedTypeName.replace('-', '_')
            asn1_type = self.proc.dataview[sort.ReferencedTypeName]
            asn1_instance = getattr(ASN1, typename)()
467
            # Fill up the ASN.1 instance
468
469
            self.asn1_editor.getVariable(root=self.tree_items[var],
                                         dest=asn1_instance)
470
471
472
            uper_encoded = self.encode_uper(asn1_instance, typename)
            #new_state.append(asn1_instance)
            new_state.append(uper_encoded)
Maxime Perrotin's avatar
Maxime Perrotin committed
473
        # Add the SDL state to the new global state, create a new hash, save it
474
475
        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
476
        new_state.append(UnicodeName(new_sdl_state))
Maxime Perrotin's avatar
Maxime Perrotin committed
477
478
479
480
481
        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)
482
        self.current_hash = new_hash
Maxime Perrotin's avatar
Maxime Perrotin committed
483
484
        undo_cmd = SendTC(self, old_state)
        self.undo_stack.push(undo_cmd)
485

486
    def on_event(self, tc_name=None, param=None, check_ppty=True):
Maxime Perrotin's avatar
Maxime Perrotin committed
487
488
489
        ''' 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.
490
            This function does not trigger any undoable action '''
491
        complete_state = []
492
        # Read in the DLL the list of internal variables
Maxime Perrotin's avatar
Maxime Perrotin committed
493
        for var, (sort, _) in self.proc.variables.viewitems():
494
            typename = sort.ReferencedTypeName.replace('-', '_')
Maxime Perrotin's avatar
Maxime Perrotin committed
495
            get_size = getattr(self.dll, "{}_size".format(var))
496
            get_size.restype = ctypes.c_uint
Maxime Perrotin's avatar
Maxime Perrotin committed
497
            size = get_size()
498
499
            # 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
500
            get_value.restype = ctypes.c_void_p
501
            value = get_value()
Maxime Perrotin's avatar
Maxime Perrotin committed
502
503
504
505
            asn1_instance = getattr(ASN1, typename)()
            asn1_instance.SetData(value)
            self.asn1_editor.updateVariable(root=self.tree_items[var],
                                            asn1Var=asn1_instance)
506
507
508
509
510
511
512
513
            try:
                self.check_asn1_constraints(asn1_instance, typename)
            except ValueError as err:
                err_msg = (u"Variable {} has a value out of range - {}"
                           .format(var, str(err)))
                raise ValueError(err_msg)
            else:
                uper_encoded = self.encode_uper(asn1_instance, typename)
514
515
516
            #complete_state.append(asn1_instance)
            # a state contains a compact version of the data
            complete_state.append(uper_encoded)
517
        # Add the SDL state to the new global state
518
        complete_state.append(self.current_sdl_state)
Maxime Perrotin's avatar
Maxime Perrotin committed
519
        # Update the SDL state in the global state panel
520
521
522
        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)
523
        # And save this new state in the graph, if it was not there yet
524
        new_hash = hash(frozenset(complete_state))
525
526
527
528
529
        # 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
530
        self.set_of_states[new_hash] = complete_state
Maxime Perrotin's avatar
Maxime Perrotin committed
531
532
533
534
535
536
        # 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 ''))
537
538
539
        if check_ppty:
            # When doing undo, dont check propertis again
            self.check_properties(new_hash)
540
        #self.check_properties(new_hash)
Maxime Perrotin's avatar
Maxime Perrotin committed
541
542
543
544
545
        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 '''
546
        # Find the list of allowed TC based on the current state
547
        st = self.current_sdl_state.split(UNICODE_SEP)
548
549
550
551
        st_iter = st.pop(0)
        context = self.proc

        def find_allowed_tc(context, statename):
552
553
554
555
556
557
558
559
            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))
560
561
562
563

        allowed_tc = list(find_allowed_tc(context, st_iter))

        while len(st):
564
            # Handle state composition
565
566
567
568
569
570
            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)))
571
            st_iter = next_st
572

573
574
575
576
577
        # 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:
578
                # Ignore timers, they are handled differently, below
579
                continue
580
            button.setEnabled(tc in allowed_tc)
581
        if tc_name in self.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
582
            self.buttons[tc_name].setEnabled(False)
583
584
        # Emit the list of allowed TC for the GUI to update other buttons
        self.allowed_messages.emit(allowed_tc)
585
586
587

    def start_simu(self):
        '''
588
           Set up the simulation and checker bays, from UI files
589
           This panel handles parameterless signals and
590
591
           the simulation console
        '''
592
593
594
595
596
597
598
599
600
601
602
603
        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
604

605
606
607
608
609
610
611
612
613
614
615
616
617
618
    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
619
620
621
622
623
624
625
626
627
628
                    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
Maxime Perrotin's avatar
Maxime Perrotin committed
629
630
631
632
633
634
635
636
                    try:
                        # Remove all previously connected buttons to avoid
                        # clicking them all
                        self.clicker.disconnect()
                    except RuntimeError:
                        # Ignore - will trigger the first time only if no
                        # signal is currently connected.
                        pass
637
638
                    self.clicker.connect(vals['send_btn'].click)
                    self.clicker.emit()
639

640
641
    def random_step(self):
        ''' One step of random simulation '''
642
643
        if self.sim_param['state'] != 'random':
            return
644
        arg = None
645
        for name, asn1_ty in self.sim_param['periodic']:
646
647
            if asn1_ty:
                arg = compute_random_value(asn1_ty, self.proc.dataview)
648
        # Select randomly an active TC and call it
Maxime Perrotin's avatar
Maxime Perrotin committed
649
650
651
652
653
654
655
656
657
658
659
660
661
662
        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)
663

664
        # Send a message every 100 ms.. Should be configurable
Maxime Perrotin's avatar
Maxime Perrotin committed
665
        QTimer().singleShot(100, self.random_step)
666

667
668
669
670
671
672
    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
673
        total_err = 0
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708

        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
709
            total_err += error_count
710
711
712
            next_level.extend(next_states)
        print 'length of next level: ', len(next_level)

Maxime Perrotin's avatar
Maxime Perrotin committed
713
        print 'Number of stop conditions reached:', total_err
714

715
716
717
718
719
    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'
720
721
722
        self.sim_param['random'] = []
        self.sim_param['periodic'] = []
        for row_nb in xrange(self.checker_table.rowCount()):
723
724
725
            item = self.checker_table.item(row_nb, 0)
            name = item.text()
            asn1_ty = item.data(Qt.UserRole)
726
727
            cond = self.checker_table.cellWidget(row_nb, 1).currentText()
            if cond == 'Random':
728
                self.sim_param['random'].append((name, asn1_ty))
729
            elif cond == 'Periodic':
730
                self.sim_param['periodic'].append((name, asn1_ty))
731
        self.random_step()
732
733
734
735
736
737

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

738
739
740
741
742
    @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)

743
744
745
746
    @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 '''
747
        self.msc_macro_start.emit()
748
        with undo.UndoMacro(self.undo_stack, 'Send TC'):
Maxime Perrotin's avatar
Maxime Perrotin committed
749
750
751
752
753
754
            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 '')
755
756
                self.add_to_msc('out', msg.replace('  ', ' ')
                                          .replace(' ,', ','))
757
758
759
760
            old_state = self.current_hash

            # Send the TC
            if param:
761
                tc_func_ptr(param._ptr)
762
763
764
            else:
                tc_func_ptr()

Maxime Perrotin's avatar
Maxime Perrotin committed
765
766
            if self.check_state():
                # If state changed, update the MSC
Maxime Perrotin's avatar
Maxime Perrotin committed
767
                self.add_to_msc('condition', CleanName(self.current_sdl_state))
768
769
770
771
            # Update windows, highlight state, enable/disable buttons, etc.
            self.current_hash = self.on_event(tc_name=name,
                                              param=param.GSER() if param
                                                                 else None)
772

773
774
775
            # Create the Undo command to restore the previous state
            undo_cmd = SendTC(self, old_state)
            self.undo_stack.push(undo_cmd)
776
        self.msc_macro_stop.emit()
Maxime Perrotin's avatar
Maxime Perrotin committed
777

Maxime Perrotin's avatar
Maxime Perrotin committed
778
    def receive_tm(self, tm_name):
779
        ''' Callback function when a paramless TM is received '''
780
        self.add_to_msc('in', tm_name)
Maxime Perrotin's avatar
Maxime Perrotin committed
781
        self.log_area.addItem('Received event "{}"'.format(tm_name))
Maxime Perrotin's avatar
Maxime Perrotin committed
782

783
    def external_proc_handler(self, name, *args):
784
        ''' Callback function when an external procedure is invoked
785
786
787
788
            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"
789
        interface = {'in' : [], 'out': []}
790
791
792
793
        # 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]
794
        # Decode all input and output parameters and create native ASN.1 values
795
        for spec, (val, size) in zip(procedure.fpar, params):
796
            # Create native ASN.1 type
797
            typename = spec['type'].ReferencedTypeName.replace('-', '_')
798
            asn1_instance = getattr(ASN1, typename)(ptr=val)
799
800
801
802
            # Input parameters: copy the content in the ASN.1 Swig type
            if spec['direction'] == 'in':
                interface['in'].append((spec, asn1_instance))
            else:
803
                interface['out'].append((spec, val, asn1_instance))
Maxime Perrotin's avatar
Maxime Perrotin committed
804
        # make the function call
Maxime Perrotin's avatar
Maxime Perrotin committed
805
806
        vdm_cls = getattr(procedure, "vdm_instance", None)
        if vdm_cls:
Maxime Perrotin's avatar
Maxime Perrotin committed
807
            # convert input parameters to VDM value notation
Maxime Perrotin's avatar
Maxime Perrotin committed
808
            inp_as_vdm = []
Maxime Perrotin's avatar
Maxime Perrotin committed
809
810
811
812
813
814
815
            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
816
817
818
819
            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
820
            # assuming 1 return parameter
821
822
823
824
825
            vdm_vn.vdm_to_ctypes(vdm=outp,
                                 dest=out_asn1_inst,
                                 sort=spec['type'],
                                 ASN1_AST=self.proc.dataview,
                                 ASN1Mod=ASN1)
826
827
        # Display the call on the MSC
        inp, outp = [], []
828
        for _, asn1_instance in interface['in']:
829
830
            inp.append(asn1_instance.GSER())
            del asn1_instance
831
        for _, _, asn1_instance in interface['out']:
832
            outp.append(asn1_instance.GSER())
833
            del(asn1_instance)
834
835
836
837
        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))
838

Maxime Perrotin's avatar
Maxime Perrotin committed
839
840
    def set_timer(self, name, duration):
        ''' Callback function when the SDL model sets a timer '''
841
        self.add_to_msc('set', 'SET_{}_{}'.format(name, duration))
Maxime Perrotin's avatar
Maxime Perrotin committed
842
843
        self.log_area.addItem('Received event "SET_{}({})"'
                              .format(name, duration))
844
        self.buttons[name].setEnabled(True)
Maxime Perrotin's avatar
Maxime Perrotin committed
845
846
847

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

853
    def set_dock_checker(self):
854
855
856
857
858
859
860
        ''' 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()
861
862
        checker_table = widget.findChild(QTableWidget, 'tableWidget')
        checker_table.setRowCount(len(self.proc.input_signals))
863
864
        for idx, inp in enumerate(self.proc.input_signals):
            name = inp['name']
865
866
867
868
            sort = inp.get('type', None)
            if sort:
                typename = sort.ReferencedTypeName.replace('-', '_')
                ty = self.proc.dataview[sort.ReferencedTypeName]
Maxime Perrotin's avatar
Maxime Perrotin committed
869
870
            else:
                ty = None
871
872
            item = QTableWidgetItem(name)
            item.setFlags(Qt.ItemIsEnabled)
873
874
            # Associate the ASN.1 data type as hidden data
            item.setData(Qt.UserRole, ty)
875
876
            combo = QComboBox()
            combo.addItems(('Manual', 'Random', 'Periodic'))
877
878
879
880
881
            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)
882
883
        exhaust_btn = widget.findChild(QToolButton, 'exhaustButton')
        exhaust_btn.pressed.connect(self.exhaustive_simulation)
884
885
886
        stop_btn = widget.findChild(QToolButton, 'stopButton')
        stop_btn.pressed.connect(self.stop_simulation)
        return checker_table
887

888
889
    def set_paramless_tc(self):
        ''' Once the DLL is loaded set the buttons to send paramless TC '''
Maxime Perrotin's avatar
Maxime Perrotin committed
890
        # tc_area and buttons have to be in self because of known pyside bug
891
        widget = self.dock_simu.widget()
Maxime Perrotin's avatar
Maxime Perrotin committed
892
        self.tc_area = widget.findChild(QGridLayout, 'tc_grid')
893
894
895
        # 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
896
                self.buttons[each['name']] = QPushButton(each['name'])
897
        for each in self.proc.timers:
Maxime Perrotin's avatar
Maxime Perrotin committed
898
            self.buttons[each] = QPushButton(each+' timeout')
899
        col, row = 0, 0
Maxime Perrotin's avatar
Maxime Perrotin committed
900
        for name, button in self.buttons.viewitems():
901
902
903
904
            self.tc_area.addWidget(button, row, col)
            if col:
                row += 1
            col = (col + 1) % 2
905
906
            tc = getattr(self.dll, '{}_{}'.format(self.proc.processName,
                                                  name))
907
            button.pressed.connect(partial(self.send_tc, name, tc))
908

Maxime Perrotin's avatar
Maxime Perrotin committed
909
910
911
912
913
914
915
916
917
918
919
920
921
    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)

922
923
924
925
926
    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)
927
        self.proc_handlers = {}
928
929
930
        for each in self.proc.procedures:
            if not each.external:
                continue
931
932
933
934
935
936
937
938
939
940
941
            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
942
                if not self.vdm:
943
944
945
946
947
948
                    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
949
950
951
952
953
954
                tokens = each.comment.inputString.split("#")
                classname = None
                for tok in tokens:
                    if tok.startswith("classname"):
                        #TODO: catch exception
                        classname = tok.split("=")[1]
955
956
957
958
959
960
                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
961

962
            elif "#c" in cmt:
Maxime Perrotin's avatar
Maxime Perrotin committed
963
                print(u'Procedure {} in C... UNSUPPORTED'
964
965
                      .format(each.inputString))
            elif "#ada" in cmt:
Maxime Perrotin's avatar
Maxime Perrotin committed
966
                print(u'Procedure {} in Ada... UNSUPPORTED'
967
                      .format(each.inputString))
968
969
970
971
972
973
            # 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)
974
975
            register_func = getattr(self.dll, "register_{}"
                                              .format(each.inputString))
976
            register_func(self.proc_handlers[each.inputString.lower()][0])
977
978


979
980
    def init_timers(self):
        ''' When loading the DLL, initialize timers/set callbacks, etc '''
Maxime Perrotin's avatar
Maxime Perrotin committed
981
982
983
984
985
        # 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)
986
987
988
        for each in self.proc.timers:
            self.timers[each] = 'unset'
            self.buttons[each].setEnabled(False)
Maxime Perrotin's avatar
Maxime Perrotin committed
989
990
991
992
993
994
            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))