Commit 371d434f authored by Michele's avatar Michele

adapted consistency check to new row relation, not tested!

parent 2573e7f7
......@@ -12,7 +12,7 @@ import helpers.bisimulation as bi
from testing.randomtesting import RandomTester
from systems.iopurpose import InputPurpose, OutputPurpose
logging.basicConfig(level=logging.INFO)
logging.basicConfig(level=logging.DEBUG)
logger = logging.getLogger(__name__)
inputs = set(['a','b'])
......
import csv
import os, inspect
from itertools import combinations, product
from itertools import permutations, product
import logging
import helpers.traces as th
import helpers.deprecator as d
......@@ -360,44 +360,69 @@ class Table:
def _isNotConsistent(self, chaos=False):
# get all labels in a set
labels = self._inputs.union(self._outputs)
labels.add(self._quiescence)
# get all combinations of rows in S, without repetitions
combi = combinations(self._rowsInS, 2)
# get all combinations of rows in S, with repetitions
combi = permutations(self._rowsInS, 2)
newColumns = set()
for row1, row2 in combi:
# If the rows are in the same equivalence class
if self._moreSpecificRow(row1, row2, chaos):
#row2 is in the equivalence class defined by row1
# get all possible (enabled) labels
inputs = self._possibleInputs(row1)
outputs = self._entries[row1][0]
labels = inputs.union(outputs)
for label in labels:
rowExt1 = row1 + (label,)
rowExt2 = row2 + (label,)
if rowExt1 in self._rows and rowExt2 in self._rows:
# I could call self._moreSpecificRow() but then
# I need to iterate again to find the suffix.
# It is better to do it directly.
for column in self._columns:
entry1 = th.flatten(rowExt1 + column, self._quiescence)
entry2 = th.flatten(rowExt2 + column, self._quiescence)
if (entry1 not in self._entries and
entry2 not in self._entries):
continue
elif (entry1 not in self._entries or
entry2 not in self._entries):
newColumns.add((label,) + column)
break
if chaos:
if (not self._entries[entry1] ==
self._entries[entry2]):
newColumns.add((label,) + column)
break
else:
outputs1, obs1 = self._entries[entry1]
outputs2, obs2 = self._entries[entry2]
if not outputs1 == outputs2:
newColumns.add((label,) + column)
break
# rowExt1 must be in Rows, because label is either an
# enabled input after row, or an observed output.
if rowExt1 not in self._rows:
self._logger.error("Error while checking consistency: the prefix "+str(rowExt1)+" should be a row, but it is not.")
self.printTable(prefix="_error")
self._logger.error("Table printed in ./tables/_error_table.csv")
self._logger.error(error)
raise
if not rowExt2 in self._rows:
# rowExt2 is not in rows. If label is an input then
# row2 does not enable it: row1 should not be more
# specific than row2
if label in inputs:
self._logger.error("Error while checking consistency: the prefix "+str(rowExt2)+" should be a row, but it is not.")
self.printTable(prefix="_error")
self._logger.error("Table printed in ./tables/_error_table.csv")
self._logger.error(error)
raise
# If label is an output, then ok (being less specific,
# this is allowed)
else:
continue
# rowExt1 in self._rows and rowExt2 in self._rows
# I could call self._moreSpecificRow() but then
# I need to iterate again to find the suffix.
# If they enable the same inputs, check each entry.
# It is better to do it directly.
for column in self._columns:
entry1 = th.flatten(rowExt1 + column, self._quiescence)
entry2 = th.flatten(rowExt2 + column, self._quiescence)
if (entry1 not in self._entries and
entry2 not in self._entries):
# for some reason both entry do not exist.
self._logger.warning("Checking relation between rows in Consistency check: some entries are not defined.")
continue
elif (entry1 not in self._entries or
entry2 not in self._entries):
self._logger.warning("Checking relation between rows in Consistency check: one entry is not defined.")
newColumns.add((label,) + column)
break
if not self._moreSpecificEntry(self._entries[entry1], self._entries[entry2], chaos):
newColumns.add((label,) + column)
break
if newColumns:
# TODO: only one suffix per round, ok?
break
......@@ -595,12 +620,23 @@ class Table:
# Given two rows, check if the former is more specific than the latter
def _moreSpecificRow(self, row1, row2, plus=False):
# First: if they do not enable the same inputs, they are not in such
# a relation
inputs1 = self._possibleInputs(row1)
inputs2 = self._possibleInputs(row2)
if inputs1 != inputs2:
return False
# If they enable the same inputs, check each entry.
for column in self._columns:
entry1 = th.flatten(row1 + column, self._quiescence)
entry2 = th.flatten(row2 + column, self._quiescence)
if entry1 not in self._entries and entry2 not in self._entries:
return True
# for some reason both entry do not exist.
self._logger.warning("Checking relation between rows: both entries are not defined.")
continue
elif entry1 not in self._entries or entry2 not in self._entries:
self._logger.warning("Checking relation between rows: one entry is not defined.")
return False
if not self._moreSpecificEntry(self._entries[entry1],
self._entries[entry2], plus):
......
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