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

Add function that yields neighbor states

parent 896f78c0
......@@ -664,9 +664,39 @@ class sdlHandler(QObject):
# Send a message every 100 ms.. Should be configurable
QTimer().singleShot(100, self.random_step)
def children_states(self):
''' Call all available interfaces with all possible values and yield
the resulting state hash plus the transition that caused it
This function does not filter out the states that were already
visited - it is exhaustive. '''
def exhaust_interface(name, asn1_ty):
''' For all combinations of a given interface parameter, execute
the PI, save the resulting state, undo, and yield the state '''
if asn1_ty:
for arg in compute_combinations(asn1_ty, self.proc.dataview):
self.click_tc(name, arg)
new_hash = self.current_hash
yield new_hash, (name, arg)
new_hash = self.current_hash
yield new_hash, (name, None)
for name in self.active_tc:
# Start from the current state
asn1_ty = None
for inp in self.proc.input_signals:
if inp['name'].lower() == name.lower():
sort = inp.get('type', None)
if sort:
asn1_ty = self.proc.dataview[sort.ReferencedTypeName]
exhaust_interface(name, ty)
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'
Supports Markdown
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