Commit f2f226bb authored by Michele's avatar Michele

closedness does not work: also row function must be checked for closedness, not row+ oly

parent 79ec49b9
import random
seed = output = random.sample(range(99999999), 1)[0]
print(seed)
random.seed(81077353) # 81077353
import os, inspect, sys
# Include project dir in path
currentdir = os.path.dirname(os.path.abspath(inspect.getfile(inspect.currentframe())))
......@@ -12,6 +18,7 @@ import helpers.bisimulation as bi
from testing.randomtesting import RandomTester
from systems.iopurpose import InputPurpose, OutputPurpose
logging.basicConfig(level=logging.DEBUG)
logger = logging.getLogger(__name__)
......
......@@ -71,7 +71,7 @@ class LearningAlgorithm:
trie = th.make_trie(oTraces)
# Until we tried K times with no results
K = len(oTraces) * 150 # TODO: should not be hardcoded
K = len(oTraces) #* 5 # TODO: should not be hardcoded
found = 0
tries = 0
while tries < K:
......@@ -90,13 +90,11 @@ class LearningAlgorithm:
consecutiveInputs = () # keep track of last inputs sequence
currentTrace = () # keep track of current trace
i = 0
# We build a trace until we either
# 1 - observe an output that makes the trace not a prefix
# 2 - there is no continuation of that trace in prefixes
# We stop when we observed at least an output for each observable
while len(oTraces) > len(observations.keys()): #and i < K:
i += 1
while len(oTraces) > len(observations.keys()):
# check if trie contains no traces (but still has a child)
children = trie.keys()
......@@ -278,8 +276,11 @@ class LearningAlgorithm:
def stabilizeTable(self):
# While nothing changes, keep closing and consistent the table
print("stabilizing")
closingRows = self._table.isNotGloballyClosed()
print("found rows to close")
consistentCheck = self._table.isNotGloballyConsistent()
print("found rows to consistehnt")
while closingRows or consistentCheck:
while closingRows:
self._logger.info("Closing table")
......@@ -424,7 +425,9 @@ class LearningAlgorithm:
self._currentLoop = self._currentLoop + 1
self._logger.info("Learning loop number " + str(self._currentLoop))
# Fill the table and make it closed and consistent
self.updateTable()
print("updating table")
self.updateTable() # TODO learning sometimes stops here!
print("table updated")
self.stabilizeTable()
# Is the table quiescence reducible? If not make it so and
# then fill it again, make it closed and consitent
......
......@@ -126,7 +126,7 @@ class Table:
if not outputs:
continue
found = False
# search in S
# search in S for Hplus
for rowInS in self._rowsInS:
if self._moreSpecificRow(rowInS, row, True):
# Found a match, exit
......@@ -144,6 +144,26 @@ class Table:
if not found:
# add this equivalence class
rows.add(row)
continue
# search in S for Hminus
for rowInS in self._rowsInS:
if self._moreSpecificRow(rowInS, row, False):
# 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, False):
# already added this equivalence class
found = True
break
# if not found, then add it
if not found:
# add this equivalence class
rows.add(row)
# TODO: add other closing strategies
return rows
......@@ -318,6 +338,8 @@ class Table:
newRow1 = "chaos_quiescence"
else:
try:
# the table is closed, there should be a row
# more specific than current[0] + (label,) in S
listOfRows = list(filter(moreSpecific(current[0] + (label,)), self._rowsInS))
newRow1 = listOfRows.pop()
for row in listOfRows:
......@@ -329,14 +351,12 @@ class Table:
# the first entry is emptyEntry.
# In this case (it can only be an input) we
# send the input to chaotic_delta
# Old code, prior to _moreSpecificRow
if self._entries[current[0] + (label,)] == self._emptyEntry(current[0] + (label,)):
newRow1 = "chaos_quiescence"
else:
self._logger.error("Quiescence reducibility check: cannot obtain new pair of states. Row1: "
+ str(current[0]) + " label: " + str(label))
self.printTable(prefix="_error")
self._logger.error(self.printTable(prefix="_error"))
self._logger.error("Table printed in ./tables/_error_table.csv")
self._logger.error(error)
raise
......@@ -361,7 +381,7 @@ class Table:
else:
self._logger.error("Quiescence reducibility check: cannot obtain new pair of states."
+ " Row2: " + str(current[1]) + " label: " + str(label))
self.printTable(prefix="_error")
self._logger.error(self.printTable(prefix="_error"))
self._logger.error("Table printed in ./tables/_error_table.csv")
self._logger.error(error)
raise
......@@ -636,10 +656,10 @@ class Table:
# entry1 ⊑ entry2 => entry2.first is subset of entry1.first and entry1.second is subset of entry2.second
def _moreSpecificEntry(self, entry1, entry2, plus):
if not plus:
return entry1[0] == entry2[0]
#return entry2[0].issubset(entry1[0])
return entry1[0] == entry2[0] # equality
#return entry2[0].issubset(entry1[0]) # inclusion
else:
#return entry1 == entry2
#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
......@@ -714,3 +734,54 @@ class Table:
else:
rowRow.append(self._entries[trace])
tablewriter.writerow(rowRow)
return path
# Load a table that was printed previously, for testing Purpose
def _loadTable(self, path):
with open(path, 'r') as csvfile:
reader = csv.reader(csvfile, delimiter=',',
quoting=csv.QUOTE_MINIMAL)
columns = []
rows = []
entries = {}
rowsInS = set()
found = False
# for row in reader:
# for cell in row:
# print("new: ")
# print(cell)
rowCount = 0
for row in reader:
colCount = 0
if rowCount == 0:
# first row are elements of E
for cell in row:
if not colCount == 0:
columns.append(eval(cell))
colCount += 1
else:
# first element is an element of rows
for cell in row:
if colCount == 0:
if not found and cell == '-':
found = True
rowCount -= 1
break
if not found:
rowsInS.add(eval(cell))
rows.append(eval(cell))
else:
trace = rows[rowCount - 1] + columns[colCount - 1]
entries[th.flatten(trace, self._quiescence)] = eval(cell)
colCount += 1
rowCount += 1
self._columns = set(columns)
self._rows = set(rows)
self._rowsInS = rowsInS
self._entries = entries
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