Commit ceb6037d authored by Michele's avatar Michele

fixed error in handleCounterexample

parent c745e85a
......@@ -45,7 +45,7 @@ import helpers.bisimulation as bi
import csv
logging.basicConfig(level=logging.INFO)
logging.basicConfig(level=logging.DEBUG)
logger = logging.getLogger(__name__)
HOST = 'localhost'
......
......@@ -63,7 +63,10 @@ class TicTacToeOutputPurpose(Purpose):
else:
# In this SUL we have many outputs (>4000)
# for this reason we use a placeholder
return 1
# It sould not be a problem later because before checking
# if a row is more specific than another, an observation query
# should be ask for all entries. (And determinism -> no problem)
return 'PLACEHOLDER'
def allOutputs(self):
return set(itertools.product('XO_', repeat=9))
......@@ -136,6 +136,14 @@ class Table:
# Check if the table is globally closed. Returns a set of rows in different
# equivalence classes
def isNotGloballyClosed(self):
newRowsMinus = self._isNotClosed()
if self.getObservableTraces() != set():
newRowsPlus = self._isNotClosed(chaos=True)
return newRowsMinus.union(newRowsPlus)
else:
return newRowsMinus
def _isNotClosed(self, chaos=False):
rows = set()
# TODO: Is there a faster way to check for global closedness
if self._closeStrategy == "First":
......@@ -143,33 +151,14 @@ class Table:
# Avoid those rows with nothing in first column
# Later, when contructing the hypothesis I send them to chaos
outputs, observation = self._entries[row]
if not outputs:
if outputs == set():
continue
found = False
# search in S for Hplus
for rowInS in self._rowsInS:
if self._moreSpecificRow(rowInS, row, True):
# Found a match, exit
found = True
break
# if not found, search in those we are adding now
# Here is the FIRST closing strategy
if not found:
for newRow in rows:
if self._moreSpecificRow(newRow, row, True):
# already added this equivalence class
found = True
break
# if not found, then add it
if not found:
# add this equivalence class
rows.add(row)
continue
found = False
# search in S for Hminus
for rowInS in self._rowsInS:
if self._moreSpecificRow(rowInS, row, False):
# search in Eq. classes
eqClasses = self.getEquivalenceClasses(chaos)
for rowInS in eqClasses:
if self._moreSpecificRow(rowInS, row, chaos):
# Found a match, exit
found = True
break
......@@ -177,14 +166,22 @@ class Table:
# Here is the FIRST closing strategy
if not found:
for newRow in rows:
if self._moreSpecificRow(newRow, row, False):
if self._moreSpecificRow(newRow, row, chaos):
# already added this equivalence class
found = True
break
# if not found, then add it
if not found:
# add this equivalence class
# first, for hPlus only, remove rows in this eq. class
if chaos:
rowsToRemove = set()
for newRow in rows:
if self._moreSpecificRow(row, newRow, chaos):
rowsToRemove.add(newRow)
rows = rows - rowsToRemove
rows.add(row)
continue
# TODO: add other closing strategies
return rows
......@@ -253,7 +250,7 @@ class Table:
newSuffixes.add(newSuffix)
# add new columns
# and add outputs to the new entry!
self._entries[ce] = self.updateEntry(ce, output)
self.updateEntry(ce, output)
return self.addColumn(newSuffixes, force=True)
def addColumn(self, columns, force=False):
......@@ -637,8 +634,6 @@ class Table:
loopState = th.flatten(row[:-1] + column, self._quiescence)
if loopState in self._entries:
self._entries[filteredEntry] = self._entries[loopState]
else:
self._entries[filteredEntry] = self._emptyEntry(filteredEntry)
# In a special case we are sure there is a quiescence loop
def _isDeltaLoop(self, row):
......@@ -689,7 +684,7 @@ class Table:
return self._possibleOutputs(trace, None)
# Update an entry in the table. If it does not exist, create it
# observation is the answer of the observation orale
# observation is the answer of the observation oracle
def updateEntry(self, trace, output=None, observation=None):
trace = th.flatten(trace, self._quiescence)
if trace in self._entries:
......@@ -703,7 +698,8 @@ class Table:
else:
if observation == None or observation == False:
self._entries[trace] = self._emptyEntry(trace)
self.updateEntry(trace, output)
if output != None:
self.updateEntry(trace, output)
else:
outputs = set()
if output != 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