Commit ac26df47 authored by Michele's avatar Michele
Browse files

started finishing

parent 5823f7c1
......@@ -52,7 +52,7 @@ class Table:
# _rows also contains empty trace
self._rows = set()
for label in self._inputPurpose.getEnabled((),None):
for label in self._possibleInputs((), None):
# Define the top part of the table (for closedness)
self._rowsInS = set()
......@@ -110,15 +110,15 @@ class Table:
return True
def getEquivalenceClasses(self, plus=False):
# () is always in the equivalence classes
# for each row in S, check if it belongs to an already discovered
# equivalence class, if not, add row to equivalence classes as new
# equivalence class.
# if it is added, check if any row already representing an equivalence
# class belongs to the newly defined equivalence class. If so
# remove it.
# moreSpecific defines a PO set.
rows = set()
# for each row in S, check if there is a singleRow in equivalence classes that is
# more specific, if not, add row to equivalence classes.
# for each singleRow in equivalence classes check if row is more specific than singleRow
# if so, remove singleRow and add row.
for row in self._rowsInS - set(()):
for row in self._rowsInS:
found = False
for singleRow in rows:
if self._moreSpecificRow(singleRow, row, plus):
......@@ -192,9 +192,11 @@ 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))
def addOneLetterExtension(self, trace, label):
# TODO: add check 'if trace is in S'
newRow = th.flatten(trace + (label,), self._quiescence)
rows = set()
......@@ -203,11 +205,14 @@ class Table:
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
return modified
......@@ -261,7 +266,7 @@ class Table:
# do not check suffix closedness
return self.extend(rows=set(), columns=columns)
modified = False
tempColumns = set()
for column in columns:
if column == () or column in self._columns:
# () is already in the table
......@@ -275,9 +280,8 @@ class Table:
" suffix closedness")
return False
tempColumns = set()
modified = self.extend(rows=set(), columns=tempColumns)
modified = self.extend(rows=set(), columns=tempColumns)
return modified
def isNotQuiescenceReducible(self):
......@@ -561,6 +565,7 @@ class Table:
# is the entry final? If False, we can still observe some outputs
def _isFinal(self, entry):
# TODO: check if entries contains entry
return self._entries[entry][0] == self._entries[entry][1]
# get a final entry with given set of outputs
......@@ -616,14 +621,13 @@ class Table:
self._entries[filteredEntry] = self._emptyEntry(filteredEntry)
# In a special case we are sure there is a quiescence loop
# If False is returned, then there is no certainty that there
# is a loop or not.
def _isDeltaLoop(self, row):
# if row ends in quiescence and the state reached by
# the longest proper prefix of row enables only
# quiescence, then the entry for row is the same as the
# entry for the proper prefix [VT15]
if len(row) > 0 and row[-1] == self._quiescence:
# TODO: check that entries contains row[:-1]
(outputs, observed) = self._entries[row[:-1]]
if self._isFinal(row[:-1]) and outputs == set((self._quiescence,)):
return True
......@@ -643,7 +647,6 @@ class Table:
observableTraces = set()
for trace in self._entries.keys():
if not self._isFinal(trace):
# observed is false
return observableTraces
......@@ -652,15 +655,15 @@ class Table:
outputs = set()
if trace in self._entries:
(outputs, observed) = self._entries[trace]
return outputs
# Return the set of outputs that can be observed after trace
# TODO: not clear the purpose of this method. rename?
def getPossibleOutputs(self, trace):
if trace in self._entries and self._entries[trace][1]:
return self._entries[trace][0]
return self._outputs.union(set(self._quiescence))
return self._possibleOutputs(trace, None)
# Update an entry in the table. If it does not exist, create it
def updateEntry(self, trace, output=None, observation=None):
......@@ -703,11 +706,11 @@ class Table:
# Given two entries, check if the former is more specific than the latter
# entry1 ⊑ entry2 => entry2.first is subset of entry1.first and entry1.second is subset of entry2.second
def _moreSpecificEntry(self, entry1, entry2, plus):
# TODO: check if entry1 and entry2 are in entries
if not plus:
return entry1[0] == entry2[0] # equality
#return entry2[0].issubset(entry1[0]) # inclusion
#return entry1 == entry2 # equality
return (entry2[0].issubset(entry1[0]) and entry1[1].issubset(entry2[1]))
# Given two rows, check if the former is more specific than the latter
......@@ -717,8 +720,8 @@ class Table:
# a relation
outputs1 = self._entries[th.flatten(row1,self._quiescence)][0]
outputs2 = self._entries[th.flatten(row2,self._quiescence)][0]
inputs1 = self._possibleInputs(row1, outputs1)
inputs2 = self._possibleInputs(row2, outputs2)
inputs1 = self._possibleInputs(th.flatten(row1,self._quiescence), outputs1)
inputs2 = self._possibleInputs(th.flatten(row2,self._quiescence), outputs2)
if inputs1 != inputs2:
return False
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