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

Add placeholder for new model checker run in a separate thread
parent 3984b00b
#!/usr/bin/env python2
# -*- coding: utf-8 -*-
# pylint: disable=C0302
ASN.1 Value Editor - Exhaustive Simulator
Simplest algorithm (pseudo code)
(1) current_state = read_state
(2) resulting_state = next_transition()
store the transition (signal name and parameter)
if hash(resulting_state) not in total_state_list:
if depth_first:
recurse (go back to (1))
restore "current_state"
go back to (2)
Copyright (c) 2016 European Space Agency
Author: Maxime Perrotin / contact
from ValueGenerator import compute_combinations
from PySide.QtCore import QThread, Signal
class ExhaustiveSimulator(QThread):
''' This class implements a basic model checker for SDL systems '''
statesVisited = Signal(int)
def __init__(self, parent=None):
super(self, ExhaustiveSimulator).__init__(parent)
self.stop_requested = False
self.numberOfStates = 0
def run(self):
print("Starting exhaustive simulation")
while True:
if self.stop_requested:
return self.numberOfStates
def stop(self):
''' Request the simulator to stop '''
self.stop_requested = True
if __name__ == 'main':
print("The CLI interface for the model checker is not implemented yet")
......@@ -484,7 +484,7 @@ class sdlHandler(QObject):
if check_ppty:
# When doing undo, dont check propertis again
return new_hash
def update_button_state(self, tc_name=None):
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