Commit c745e85a authored by Michele's avatar Michele

fixed counterexample handling

parent f098d570
......@@ -192,33 +192,39 @@ class Table:
# Promote some rows to S
def promote(self, rows):
for row in rows:
# TODO: add check 'if row is in S'
self._rowsInS.add(th.flatten(row, self._quiescence))
if row not in self._entries.keys():
self._logger.warning("Promoting rows: "+ str(row) +" is not in the table.")
else:
self._rowsInS.add(th.flatten(row, self._quiescence))
def addOneLetterExtension(self, trace, label):
# TODO: add check 'if trace is in S'
newRow = th.flatten(trace + (label,), self._quiescence)
rows = set()
rows.add(newRow)
return self.extend(rows)
if trace not in self._entries.keys():
self._logger.warning("Add one letter extension: trace is not in the table.")
else:
newRow = th.flatten(trace + (label,), self._quiescence)
rows = set()
rows.add(newRow)
return self.extend(rows)
def addOneLetterExtensions(self, rows):
modified = False
for row in rows:
# TODO: add check 'if row is in S'
outputs, observation = self._entries[row]
for my_input in self._possibleInputs(row, outputs):
if self.addOneLetterExtension(row, my_input):
modified = True
for output in outputs:
# Do not use outputExpert here, we want only extensions
# with outputs that we have observed
if self.addOneLetterExtension(row, output):
modified = True
if row not in self._entries.keys():
self._logger.warning("Add one letter extensions: "+ str(row) +" is not in the table.")
else:
outputs, observation = self._entries[row]
for my_input in self._possibleInputs(row, outputs):
if self.addOneLetterExtension(row, my_input):
modified = True
for output in outputs:
# Do not use outputExpert here, we want only extensions
# with outputs that we have observed
if self.addOneLetterExtension(row, output):
modified = True
return modified
def handleCounterexample(self, ce, output):
# if ce is a coutnerexample, then also flatten(ce, quiescence) is.
# if ce is a counterexample, then also flatten(ce, quiescence) is.
ce = th.flatten(ce, self._quiescence)
# if ce is already in the table, then we have a new output for that
# entry
......@@ -234,7 +240,6 @@ class Table:
return False
else:
# ce is not in the table. add it to the table.
# TODO: reduce counterexample: find a way to remove cicles!
# TODO: add other ce handling techniques, for the moment
# we split ce into [existing_row + newsuffix] and add newsuffix and
# all its suffixes to the table
......@@ -248,19 +253,9 @@ class Table:
newSuffixes.add(newSuffix)
# add new columns
# and add outputs to the new entry!
outputs = set()
outputs.add(output)
self._entries[ce] = (outputs,False)
self._entries[ce] = self.updateEntry(ce, output)
return self.addColumn(newSuffixes, force=True)
# return the length of the longest suffix in columns
# def getLengthColumns(self):
# length = 0
# for item in self._columns:
# if len(item) > length:
# length = len(item)
# return length
def addColumn(self, columns, force=False):
if force:
# do not check suffix closedness
......@@ -706,12 +701,13 @@ class Table:
else:
self._entries[trace] = (outputs.copy(), outputs.copy())
else:
outputs = set()
if output != None:
outputs.add(output)
if observation == None or observation == False:
self._entries[trace] = self._emptyEntry(trace)
self.updateEntry(trace, output)
else:
outputs = set()
if output != None:
outputs.add(output)
self._entries[trace] = self._finalEntry(trace, outputs)
# given a trace, query outputPurpose for the outputs that are possibly
......
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