Commit c57a21db authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

First level of exhaustive simulation

parent 2646e4c7
......@@ -28,7 +28,8 @@ from itertools import chain
from PySide.QtGui import (QDockWidget, QPushButton, QGridLayout, QListWidget,
QUndoStack, QUndoCommand, QToolButton, QTableWidget,
QTableWidgetItem, QComboBox, QMessageBox)
QTableWidgetItem, QComboBox, QMessageBox,
QApplication)
from PySide.QtCore import QObject, Signal, Slot, Qt, QFile, QTimer
from PySide.QtUiTools import QUiLoader
......@@ -284,6 +285,8 @@ class sdlHandler(QObject):
self.current_hash = None
# Flag set to true when a new state is created
self.new_state_created = False
# When checking properties, list the currently true stop conditions
self.stop_conditions = []
# Create a stack for handling undo/redo commands
self.undo_stack = QUndoStack(self)
# Associate the Undo, Redo, Reset buttons with an action
......@@ -443,10 +446,12 @@ class sdlHandler(QObject):
if not self.prop_dll:
return
self.restore_global_state(statehash, dll=self.prop_dll)
self.stop_conditions = []
for text, check in self.properties.viewitems():
if check():
msg = 'Property "{}" is true'.format(text)
self.log_area.addItem(msg)
self.stop_conditions.append(text)
if self.sim_param['state'] != 'exhaustive':
box = QMessageBox(QMessageBox.Information,
'Stop condition', msg)
......@@ -694,6 +699,52 @@ class sdlHandler(QObject):
QTimer().singleShot(1000, self.random_step)
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
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
......@@ -717,17 +768,6 @@ class sdlHandler(QObject):
print 'End of simulation'
self.sim_param['state'] = 'manual'
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 '
def exhaust_interface(name, asn1_ty):
''' Send all combinations of an input signal and return
a list of new states '''
for each in compute_combinations(asn1_ty, self.proc.dataview):
pass
@Slot()
def add_to_msc(self, direction, msg):
''' Create an undo command and display message on the MSC diagram '''
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment