diff --git a/Main.py b/Main.py new file mode 100644 index 0000000..18b67c6 --- /dev/null +++ b/Main.py @@ -0,0 +1,41 @@ + +from VeriFlow.Network import Network + +ROUTE_VIEW = 1; +BIT_BUCKET = 2; + + +def main(): + print("Enter network configuration file name (eg.: file.txt):"); + # filename = input("> "); + filename = "Topo1.txt" + network = Network(); + network.parseNetworkFromFile(filename); + generatedECs = network.getECsFromTrie(); + network.checkWellformedness(); + network.log(generatedECs); + while True: + print(" "); + print("Add rule by entering A#switchIP-rulePrefix-nextHopIP (eg.A#127.0.0.1-128.0.0.0/2-127.0.0.2)"); + print("Remove rule by entering R#switchIP-rulePrefix-nextHopIP (eg.R#127.0.0.1-128.0.0.0/2-127.0.0.2)"); + print("To exit type exit"); + + affectedEcs = set() + inputline = input('> ') + if (inputline.startswith("A")): + affectedEcs = network.addRuleFromString(inputline[2:]); + network.checkWellformedness(affectedEcs); + elif (inputline.startswith("R")): + affectedEcs = network.deleteRuleFromString(inputline[2:]); + network.checkWellformedness(affectedEcs); + elif ("exit" in inputline): + break; + else: + print("Wrong input format!"); + continue; + + print(""); + network.log(affectedEcs); + +if __name__ == '__main__': + main() \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..ad43dbe --- /dev/null +++ b/README.md @@ -0,0 +1,45 @@ +# VeriFlow + +## Requirements + - Python 3 + +## Running + + +```bash +$ python Main.py +``` + +## Sample Run + +```bash +$ python Main.py + Enter network configuration file name (eg.: file.txt): + > Topo1.txt + + Number of ECs: 9 + Number of affected ECs: 9 + Network is well-formed (No property violations) + + Add rule by entering A#switchIP-rulePrefix-nextHopIP (eg.A#127.0.0.1-128.0.0.0/2-127.0.0.2) + Remove rule by entering R#switchIP-rulePrefix-nextHopIP (eg.R#127.0.0.1-128.0.0.0/2-127.0.0.2) + To exit type exit + > A#127.0.0.1-128.0.0.0/2-127.0.0.2 + + Number of ECs: 9 + Number of affected ECs: 2 + Network is well-formed (No property violations) + + Add rule by entering A#switchIP-rulePrefix-nextHopIP (eg.A#127.0.0.1-128.0.0.0/2-127.0.0.2) + Remove rule by entering R#switchIP-rulePrefix-nextHopIP (eg.R#127.0.0.1-128.0.0.0/2-127.0.0.2) + To exit type exit + > exit + ``` + + + + + + + + diff --git a/Topo1.txt b/Topo1.txt new file mode 100644 index 0000000..e8878fb --- /dev/null +++ b/Topo1.txt @@ -0,0 +1,54 @@ +S# +127.0.0.1:127.0.0.11 +127.0.0.2:127.0.0.11,127.0.0.3 +127.0.0.3:127.0.0.5,127.0.0.4,127.0.0.2,127.0.0.11,127.0.0.7,127.0.0.6 +127.0.0.4:127.0.0.3,127.0.0.7,127.0.0.6,127.0.0.11 +127.0.0.5:127.0.0.3 +127.0.0.6:127.0.0.3,127.0.0.4 +127.0.0.7:127.0.0.3,127.0.0.4,127.0.0.9 +127.0.0.8:127.0.0.11 +127.0.0.9:127.0.0.7,127.0.0.11 +127.0.0.10:127.0.0.11 +127.0.0.11:127.0.0.1,127.0.0.2,127.0.0.3,127.0.0.4,127.0.0.8,127.0.0.9,127.0.0.10 +H# +127.0.0.101:127.0.0.5 +127.0.0.102:127.0.0.1 +127.0.0.103:127.0.0.10 +127.0.0.104:127.0.0.9 +127.0.0.105:127.0.0.8 +127.0.0.106:127.0.0.7 +127.0.0.107:127.0.0.6 +127.0.0.108:127.0.0.4 +R# +127.0.0.10-0.0.0.0/2-127.0.0.11 +127.0.0.11-0.0.0.0/2-127.0.0.2 +127.0.0.2-0.0.0.0/2-127.0.0.3 +127.0.0.3-0.0.0.0/2-127.0.0.5 +127.0.0.10-96.0.0.0/4-127.0.0.11 +127.0.0.11-96.0.0.0/4-127.0.0.3 +127.0.0.3-96.0.0.0/4-127.0.0.4 +127.0.0.4-128.0.0.0/3-127.0.0.6 +127.0.0.9-144.0.0.0/4-127.0.0.11 +127.0.0.11-144.0.0.0/4-127.0.0.3 +127.0.0.3-144.0.0.0/4-127.0.0.7 +127.0.0.4-192.0.0.0/3-127.0.0.7 +127.0.0.7-192.0.0.0/3-127.0.0.9 +127.0.0.4-64.0.0.0/3-127.0.0.11 +127.0.0.11-64.0.0.0/3-127.0.0.8 +127.0.0.1-128.0.0.0/3-127.0.0.11 +127.0.0.11-128.0.0.0/3-127.0.0.3 +127.0.0.3-128.0.0.0/3-127.0.0.6 +E! + + + +-0.0.0.0/2- 00* +-96.0.0.0/4- 0110* +-128.0.0.0/3- 100* +-144.0.0.0/4- 1001* +-192.0.0.0/3- 110* +-64.0.0.0/3- 010* + + + + diff --git a/Topo2.txt b/Topo2.txt new file mode 100644 index 0000000..1683005 --- /dev/null +++ b/Topo2.txt @@ -0,0 +1,54 @@ +S# +127.0.0.1:127.0.0.11 +127.0.0.2:127.0.0.11,127.0.0.3 +127.0.0.3:127.0.0.5,127.0.0.4,127.0.0.2,127.0.0.11,127.0.0.7,127.0.0.6 +127.0.0.4:127.0.0.3,127.0.0.7,127.0.0.6,127.0.0.11 +127.0.0.5:127.0.0.3 +127.0.0.6:127.0.0.3,127.0.0.4 +127.0.0.7:127.0.0.3,127.0.0.4,127.0.0.9 +127.0.0.8:127.0.0.11 +127.0.0.9:127.0.0.7,127.0.0.11 +127.0.0.10:127.0.0.11 +127.0.0.11:127.0.0.1,127.0.0.2,127.0.0.3,127.0.0.4,127.0.0.8,127.0.0.9,127.0.0.10 +H# +127.0.0.101:127.0.0.5 +127.0.0.102:127.0.0.1 +127.0.0.103:127.0.0.10 +127.0.0.104:127.0.0.9 +127.0.0.105:127.0.0.8 +127.0.0.106:127.0.0.7 +127.0.0.107:127.0.0.6 +127.0.0.108:127.0.0.4 +R# +127.0.0.10-0.0.0.0/2-127.0.0.11 +127.0.0.11-0.0.0.0/2-127.0.0.2 +127.0.0.2-0.0.0.0/2-127.0.0.3 +127.0.0.3-0.0.0.0/2-127.0.0.11 +127.0.0.10-96.0.0.0/4-127.0.0.11 +127.0.0.11-96.0.0.0/4-127.0.0.3 +127.0.0.3-96.0.0.0/4-127.0.0.4 +127.0.0.4-128.0.0.0/3-127.0.0.6 +127.0.0.9-144.0.0.0/4-127.0.0.11 +127.0.0.11-144.0.0.0/4-127.0.0.3 +127.0.0.3-144.0.0.0/4-127.0.0.7 +127.0.0.4-192.0.0.0/3-127.0.0.7 +127.0.0.7-192.0.0.0/3-127.0.0.9 +127.0.0.4-64.0.0.0/3-127.0.0.11 +127.0.0.11-64.0.0.0/3-127.0.0.8 +127.0.0.1-128.0.0.0/3-127.0.0.11 +127.0.0.11-128.0.0.0/3-127.0.0.3 +127.0.0.3-128.0.0.0/3-127.0.0.6 +E! + + + +-0.0.0.0/2- 00* +-96.0.0.0/4- 0110* +-128.0.0.0/3- 100* +-144.0.0.0/4- 1001* +-192.0.0.0/3- 110* +-64.0.0.0/3- 010* + + + + diff --git a/VeriFlow/ErrorType.py b/VeriFlow/ErrorType.py new file mode 100644 index 0000000..7e86077 --- /dev/null +++ b/VeriFlow/ErrorType.py @@ -0,0 +1,2 @@ +LOOP = 0 +BLACK_HOLE = 1 \ No newline at end of file diff --git a/VeriFlow/ForwardingGraph.py b/VeriFlow/ForwardingGraph.py new file mode 100644 index 0000000..cd42a30 --- /dev/null +++ b/VeriFlow/ForwardingGraph.py @@ -0,0 +1,18 @@ +class ForwardingGraph(object): + """docstring for ForwardingGraph""" + def __init__(self): + super(ForwardingGraph, self).__init__() + self.forwardingGraph = set() + + def addToGraph(self, nextHopId): + self.forwardingGraph.add(nextHopId) + + def getForwardingGraph(self): + return self.forwardingGraph + + def setForwardingGraph(self, forwardingGraph): + self.forwardingGraph = forwardingGraph + + def contains(self, id): + return id in self.forwardingGraph + \ No newline at end of file diff --git a/VeriFlow/Host.py b/VeriFlow/Host.py new file mode 100644 index 0000000..dc4ee8d --- /dev/null +++ b/VeriFlow/Host.py @@ -0,0 +1,19 @@ +class Host(object): + """docstring for Host""" + def __init__(self): + super(Host, self).__init__() + self.id = None + self.switchId = None + + def getId(self): + return self.id + + def setId(self, id): + self.id = id + + def getSwitchId(self): + return self.switchId + + def setSwitchId(self, switchId): + self.switchId = switchId + \ No newline at end of file diff --git a/VeriFlow/Interval.py b/VeriFlow/Interval.py new file mode 100644 index 0000000..c6d5350 --- /dev/null +++ b/VeriFlow/Interval.py @@ -0,0 +1,34 @@ +class Interval(object): + """docstring for Interval""" + def __init__(self, left, right): + super(Interval, self).__init__() + self.left = left + self.right = right + + def getRight(self): + return self.right + + def setRight(self, right): + self.right = right + + def getLeft(self): + return self.left + + def setLeft(self, left): + self.left = left + + + def hashCode(self): + return Objects.hash(left, right) + + def equals(self, obj) : + if obj is None: + return False + try: + eq = self.left == obj.left and self.right == obj.right + except Exception as e: + eq = False + return eq + + def toString(self): + return "[" + left + "," + right + ")" diff --git a/VeriFlow/Network.py b/VeriFlow/Network.py new file mode 100644 index 0000000..11fd5dc --- /dev/null +++ b/VeriFlow/Network.py @@ -0,0 +1,203 @@ +from VeriFlow.ForwardingGraph import ForwardingGraph +from VeriFlow.Interval import Interval +from VeriFlow.Trie import Trie +from VeriFlow.Switch import Switch +from VeriFlow.Host import Host +from VeriFlow.Rule import Rule +from VeriFlow.TrieNode import TrieNode + + +class Network(object): + """docstring for Network""" + def __init__(self): + super(Network, self).__init__() + self.trie = Trie() + self.switches, self.hosts, self.rulePrefixes = {}, {}, {} + self.ecs, self.networkErrors = [], [] + + def parseNetworkFromFile(self, fileName): + f = open(fileName, 'r') + try: + f.readline(); + self.addSwitchesFromFileFormat(f); + self.addHostsFromFileFormat(f); + self.addRulesFromFileFormat(f); + f.close(); + except Exception as e: + print(e); + f.close(); + + def getNumberOfECs(self): + return self.trie.numberOfECs(); + + def addRulesFromFileFormat(self, f): + currentLine = f.readline(); + while (not currentLine.startswith("E")): + currentLine = currentLine.strip('\n') + ecs = self.addRuleFromString(currentLine); + currentLine = f.readline(); + + def addRuleFromString(self, ruleString): + split1 = ruleString.split("-"); + rule = Rule(); + rule.setSwitchId(split1[0]); + rule.setPrefix(split1[1]); + rule.setNextHopId(split1[2]); + return self.addRule(rule); + + def addHostsFromFileFormat(self, fh): + currentLine = fh.readline(); + while (not currentLine.startswith("R")): + ts = Host(); + currentLine = currentLine.strip('\n') + split1 = currentLine.split(":"); + ts.setId(split1[0]); + ts.setSwitchId(split1[1]); + switch1 = self.switches.get(ts.getSwitchId()); + switch1.addConnectedHost(ts.getId()); + self.hosts[ts.getId()] = ts; + currentLine = fh.readline(); + + def addSwitchesFromFileFormat(self, fs): + currentLine = fs.readline(); + while (not currentLine.startswith("H")): + ts = Switch(); + currentLine = currentLine.strip('\n') + split1 = currentLine.split(":"); + ts.setId(split1[0]); + nhops = split1[1].split(","); + for nh in nhops: + ts.addNextHop(nh) + self.switches[ts.getId()] = ts; + currentLine = fs.readline(); + + + def getSwitches(self): + return self.switches; + + def getHostWithId(self, id): + return self.hosts.get(id); + + def getHosts(self): + return self.hosts; + + def addEc(self, ec): + self.getEcs().add(ec); + + + def checkWellformedness(self, ecs = None): + if(ecs is None): + ecs = self.getECsFromTrie() + self.getNetworkErrors().clear(); + for ec in self.ecs: + for host in hosts.values(): + connectedSwitchId = host.getSwitchId(); + currentSwitch = self.switches.get(connectedSwitchId); + forwardingGraph = ForwardingGraph(); + forwardingGraph.addToGraph(connectedSwitchId); + while (True): + associatedRule = currentSwitch.getAssociatedRule(ec.getLeft()); + if (associatedRule == None) : + # networkError = NetworkError(); + # networkError.setErrorType(ErrorType.BLACK_HOLE); + # networkError.setEc(ec); + # networkError.setStartingPoint(self.switches.get(connectedSwitchId)); + # getNetworkErrors().add(networkError); + break; + + nextHopId = associatedRule.getNextHopId(); + if (hosts.containsKey(nextHopId)): + break; + if (forwardingGraph.contains(nextHopId)): + networkError = NetworkError(); + networkError.setErrorType(ErrorType.LOOP); + networkError.setEc(ec); + networkError.setStartingPoint(self.switches.get(connectedSwitchId)); + getNetworkErrors().add(networkError); + break; + currentSwitch = self.switches.get(nextHopId); + forwardingGraph.addToGraph(nextHopId); + + def getEcs(self): + return ecs; + + def setEcs(self, ecs): + self.ecs = ecs; + + + def getNetworkErrors(self): + return self.networkErrors; + + + def setNetworkErrors(self, networkErrors): + self.networkErrors = networkErrors; + + + def getTrie(self): + return self.trie; + + + def setTrie(self, trie): + self.trie = trie; + + + def addRule(self, rule): + switch1 = self.switches.get(rule.getSwitchId()); + switch1.addRule(rule); + + if (rule.getPrefix() not in self.rulePrefixes.keys()): + updateEcs = self.getTrie().addRule(rule); + self.rulePrefixes[rule.getPrefix()]=1 + return updateEcs; + else: + self.rulePrefixes[rule.getPrefix()] = self.rulePrefixes.get(rule.getPrefix()) + 1 + return set() + + + + + def deleteRule(self, rule): + switchId = rule.getSwitchId(); + count = self.rulePrefixes.get(rule.getPrefix()); + try: + self.rulePrefixes.pop(rule.getPrefix()); + affectedECs = self.trie.deleteFromTrie(rule.getPrefix() + "*"); + if (count != 1): + self.rulePrefixes.put(rule.getPrefix(), count - 1); + switch1 = self.switches.get(switchId); + rules = switch1.getRules(); + for r in rules: + if r.equals(rule): + rules.remove(r) + + self.switches[switchId].setRules(rules) + return affectedECs; + + except Exception as e: + return set() + + + def log(self, affectedEcs): + print("Number of ECs: " ,self.getNumberOfECs()); + print("Number of affected ECs: " ,len(affectedEcs)); + if (len(self.getNetworkErrors()) == 0): + print("Network is well-formed (No property violations)"); + else: + for netErr in self.getNetworkErrors(): + if (netErr.getErrorType() == ErrorType.LOOP): + print("There is a loop starting from switch " + netErr.getStartingPoint().getId() + " for EC " + netErr.getEc() + "!"); + + def deleteRuleFromString(self, ruleString): + split1 = ruleString.split("-"); + rule = Rule(); + rule.setSwitchId(split1[0]); + rule.setPrefix(split1[1]); + rule.setNextHopId(split1[2]); + return self.deleteRule(rule); + + def generateECs(self): + return self.trie.generateECs(); + + def getECsFromTrie(self): + return self.trie.getECListFromTrie(); + diff --git a/VeriFlow/NetworkError.py b/VeriFlow/NetworkError.py new file mode 100644 index 0000000..31ef2ed --- /dev/null +++ b/VeriFlow/NetworkError.py @@ -0,0 +1,27 @@ +class NetworkError(object): + """docstring for NetworkError""" + def __init__(self, arg): + super(NetworkError, self).__init__() + self.errorType = None + self.ec = None + self.startingPoint = None + + def getErrorType(self): + return self.errorType; + + def setErrorType(self, errorType): + self.errorType = errorType; + + def getEc(self): + return self.ec; + + def setEc(self, ec): + self.ec = ec; + + def getStartingPoint(self): + return self.startingPoint; + + def setStartingPoint(self, startingPoint): + self.startingPoint = startingPoint; + + \ No newline at end of file diff --git a/VeriFlow/Rule.py b/VeriFlow/Rule.py new file mode 100644 index 0000000..962f00d --- /dev/null +++ b/VeriFlow/Rule.py @@ -0,0 +1,52 @@ + +class Rule(object): + """docstring for Rule""" + def __init__(self, prefix = None, switchId = None, nextHopId = None): + super(Rule, self).__init__() + self.prefix = prefix; + self.switchId = switchId; + self.nextHopId = nextHopId; + + + def equals(self, obj): + if obj is None: + return False + + return obj.prefix == self.prefix and obj.switchId == self.switchId and obj.nextHopId == self.nextHopId + + def decodeIpMask(self, ipMask): + splitMask = ipMask.split("/"); + splitIp = splitMask[0].split("."); + output = ""; + for s in splitIp: + intValue = int(s) + output += self.toEightBitBinary(intValue) + return output[:int(splitMask[1])] + + def toEightBitBinary(self, intValue): + binaryString = bin(intValue)[2:]; + length = len(binaryString); + for i in range(length, 8): + binaryString = "0" + binaryString + return binaryString + + def getPrefix(self): + return self.prefix + + def setPrefix(self, prefix): + self.prefix = self.decodeIpMask(prefix) + + def getSwitchId(self): + return self.switchId + + def setSwitchId(self, switchId): + self.switchId = switchId + + def getNextHopId(self): + return self.nextHopId + + def setNextHopId(self, nextHopId): + self.nextHopId = nextHopId + + def matches(self, rulePrefix): + return rulePrefix.startsWith(prefix) diff --git a/VeriFlow/Switch.py b/VeriFlow/Switch.py new file mode 100644 index 0000000..ff157b2 --- /dev/null +++ b/VeriFlow/Switch.py @@ -0,0 +1,50 @@ +class Switch(object): + """docstring for Switch""" + def __init__(self): + super(Switch, self).__init__() + self.id = None + self.nextHops = [] + self.connectedHosts = [] + self.rules = [] + + def getAssociatedRule(self, rulePrefix): + for r in self.rules: + if r.matches(rulePrefix): + return r + return None + + def getId(self): + return self.id; + + def setId(self, id): + self.id = id; + + def addNextHop(self, nextHop): + self.nextHops.append(nextHop); + + def addConnectedHost(self, id): + self.connectedHosts.append(id); + + + def getNextHops(self): + return self.nextHops; + + def setNextHops(self, nextHops): + self.nextHops = nextHops; + + def addRule(self, newRule): + self.rules.insert(0, newRule); + + def setRules(self, rules): + self.rules = rules + + def getRules(self): + return self.rules; + + + def getConnectedHosts(self): + return self.connectedHosts; + + def setConnectedHosts(self, connectedHosts): + self.connectedHosts = connectedHosts; + diff --git a/VeriFlow/Trie.py b/VeriFlow/Trie.py new file mode 100644 index 0000000..cb469d8 --- /dev/null +++ b/VeriFlow/Trie.py @@ -0,0 +1,275 @@ +from VeriFlow.TrieNode import TrieNode +from VeriFlow.Interval import Interval + +class Trie(object): + """docstring for Trie""" + def __init__(self): + super(Trie, self).__init__() + self.root = TrieNode() + self.root.setStarChild(TrieNode()) + self.ecs = set() + + def getRoot(self): + return self.root + + def setRoot(self, root): + self.root = root + + # def deleteFromTrie(self, prefix): + # return self.deleteFromTrie(prefix + "*", root, "") + + def deleteFromTrie(self, ip, node = None, path = ""): + if (node is None): + node = self.root + generatedEcs = [] + currentChar = ip[0]; + if (currentChar == '*'): + if (node.getStarChild() == None): + print("No such rule to be deleted!"); + return set() + + node.setStarChild(None); + if (node.numberOfNonStarChildren() == 0): + node.setNodeValue(0); + return set() + + nodeValue = 0; + if (node.numberOfNonStarChildren() == 2): + nodeValue = node.getRightChild().getNodeValue() + node.getLeftChild().getNodeValue(); + if (node.getLeftChild().isOpenRight() or node.getRightChild().isOpenLeft()): + nodeValue+=1; + + elif (node.getLeftChild() != None): + node.setOpenLeft(node.getLeftChild().isOpenLeft()); + nodeValue = node.getLeftChild().getNodeValue(); + else: + node.setOpenRight(node.getRightChild().isOpenRight()); + nodeValue = node.getRightChild().getNodeValue(); + node.setNodeValue(nodeValue); + + elif (currentChar == '0'): + isNew = node.getLeftChild() == None; + if (isNew): + print("No such rule to be deleted!"); + return set(); + + ecLeft = self.deleteFromTrie(ip[1:], node.getLeftChild(), path + "0"); + generatedEcs.extend(list(ecLeft)); + else: + isNew = node.getRightChild() == None; + if (isNew): + print("No such rule to be deleted!"); + return set(); + + ecRight = self.deleteFromTrie(ip[1:], node.getRightChild(), path + "1"); + generatedEcs.extend(list(ecRight)); + + generatedEcs.extend(list(self.updateNode(node, path))); + return set(generatedEcs); + + + def insertIntoTrie(self, ip, node = None, path = ""): + if(node is None): + node = self.root + + ecSet = []; + currentChar = ip[0]; + if (currentChar == '*'): + node.setStarChild(TrieNode()); + node.setOpenLeft(False); + node.setOpenRight(False); + + elif (currentChar == '0'): + isNew = node.getLeftChild() == None; + if (isNew): + node.setLeftChild(TrieNode()); + ecS1 = self.insertIntoTrie(ip[1:], node.getLeftChild(), path + "0"); + ecSet.extend(list(ecS1)); + else: + isNew = node.getRightChild() == None; + if (isNew): + node.setRightChild(TrieNode()); + ecS2 = self.insertIntoTrie(ip[1:], node.getRightChild(), path + "1"); + ecSet.extend(list(ecS2)); + + upn = self.updateNode(node, path) + ecSet.extend(upn) + return set(ecSet); + + def updateNode(self, node, path): + nodeValue = 0; + + newEcs, generatedEcs = set(), set() + oldECs = node.getEcs(); + + if (node.getLeftChild() != None): + if (node.getLeftChild().getNodeValue() == 0): + node.setLeftChild(None); + if (node.getRightChild() != None): + if (node.getRightChild().getNodeValue() == 0): + node.setRightChild(None); + + if(node.numberOfNonStarChildren() == 2): + if (node.getLeftChild().isOpenRight() or node.getRightChild().isOpenLeft()): + generatedEcs.add(Interval(node.getLeftChild().getAdvertisedInterval().getRight(), node.getRightChild().getAdvertisedInterval().getLeft())); + + nodeValue = node.getLeftChild().getNodeValue() + node.getRightChild().getNodeValue(); + if (node.getStarChild() != None): + if (node.getLeftChild().isOpenLeft()): + generatedEcs.add(Interval(path, node.getLeftChild().getAdvertisedInterval().getLeft())); + nodeValue+=1; + if (node.getRightChild().isOpenRight()): + generatedEcs.add(Interval(node.getRightChild().getAdvertisedInterval().getRight(), self.binaryAdd(path, 1))); + nodeValue+=1; + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + + else: + node.setAdvertisedInterval(Interval(node.getLeftChild().getAdvertisedInterval().getLeft(), node.getRightChild().getAdvertisedInterval().getRight())); + node.setOpenLeft(node.getLeftChild().isOpenLeft()); + node.setOpenRight(node.getRightChild().isOpenRight()); + + if (node.getRightChild().isOpenLeft() or node.getLeftChild().isOpenRight()): + nodeValue+=1; + + elif(node.numberOfNonStarChildren() == 1): + if (node.getLeftChild() != None): + nodeValue = node.getLeftChild().getNodeValue(); + node.setOpenLeft(node.getLeftChild().isOpenLeft()); + node.setOpenRight(True); + if (node.getStarChild() != None): + generatedEcs.add(Interval(node.getLeftChild().getAdvertisedInterval().getRight(), self.binaryAdd(path, 1))); + nodeValue += 1; + if (node.isOpenLeft()): + generatedEcs.add(Interval(path, node.getLeftChild().getAdvertisedInterval().getLeft())); + nodeValue+=1; + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + node.setOpenLeft(False); + node.setOpenRight(False); + else: + node.setAdvertisedInterval(node.getLeftChild().getAdvertisedInterval()); + else: + nodeValue = node.getRightChild().getNodeValue(); + node.setOpenRight(node.getRightChild().isOpenRight()); + node.setOpenLeft(True); + if (node.getStarChild() != None) : + generatedEcs.add(Interval(path, node.getRightChild().getAdvertisedInterval().getLeft())); + nodeValue+=1; + if (node.isOpenRight()): + generatedEcs.add(Interval(node.getRightChild().getAdvertisedInterval().getRight(), self.binaryAdd(path, 1))); + nodeValue+=1; + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + node.setOpenLeft(False); + node.setOpenRight(False); + else: + node.setAdvertisedInterval(node.getRightChild().getAdvertisedInterval()); + elif(node.numberOfNonStarChildren() == 0): + nodeValue = 1; + node.setOpenLeft(False); + node.setOpenRight(False); + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + generatedEcs.add(node.getAdvertisedInterval()); + + + for i in generatedEcs: + if (i not in oldECs): + newEcs.add(i); + node.setEcs(generatedEcs); + node.setNodeValue(nodeValue); + return newEcs; + + def getECListFromTrie(self, node = None): + if(node is None): + node = self.root + ecs = []; + if (node.getRightChild() != None): + ecs.extend(list(self.getECListFromTrie(node.getRightChild()))); + if (node.getLeftChild() != None): + ecs.extend(list(self.getECListFromTrie(node.getLeftChild()))); + ecs.extend(list(node.getEcs())); + return set(ecs); + + + def numberOfECs(self): + return self.root.getNodeValue(); + + def addRule(self, rule): + return self.insertIntoTrie(rule.getPrefix() + "*", self.root, ""); + + def getEcs(self): + return ecs; + + def setEcs(self, ecs): + self.ecs = ecs; + + + def generateECs(self): + self.ecs.clear(); + generateECs(root, ""); + return ecs; + + + def generateECs(self, node, path): + + if(node.numberOfNonStarChildren() == 2): + ecLeft = generateECs(node.getLeftChild(), path + "0"); + ecRight = generateECs(node.getRightChild(), path + "1"); + if (node.getLeftChild().isOpenRight() or node.getRightChild().isOpenLeft()): + ecs.add(Interval(ecLeft.getRight(), ecRight.getLeft())); + if (node.getStarChild() != None): + if (node.getLeftChild().isOpenLeft()): + ecs.add(Interval(path, ecLeft.getLeft())); + if (node.getRightChild().isOpenRight()): + ecs.add(Interval(ecRight.getRight(), self.binaryAdd(path, 1))); + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + return node.getAdvertisedInterval(); + else: + node.setAdvertisedInterval(Interval(ecLeft.getLeft(), ecRight.getRight())); + return node.getAdvertisedInterval(); + + elif(node.numberOfNonStarChildren() == 1): + if (node.getLeftChild() != None): + ecLeft = generateECs(node.getLeftChild(), path + "0"); + if (node.getStarChild() != None): + ecs.add(Interval(ecLeft.getRight(), self.binaryAdd(path, 1))); + if (node.getLeftChild().isOpenLeft()): + ecs.add(Interval(path, ecLeft.getLeft())); + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + return node.getAdvertisedInterval(); + + node.setAdvertisedInterval(ecLeft); + return node.getAdvertisedInterval(); + + else: + ecRight = generateECs(node.getRightChild(), path + "1"); + if (node.getStarChild() != None): + ecs.add(Interval(path, ecRight.getLeft())); + if (node.getRightChild().isOpenRight()): + ecs.add(Interval(ecRight.getRight(), self.binaryAdd(path, 1))); + node.setAdvertisedInterval(Interval(path, self.binaryAdd(path, 1))); + return node.getAdvertisedInterval(); + node.setAdvertisedInterval(ecRight); + return ecRight; + elif(node.numberOfNonStarChildren() == 0): + e = Interval(path, self.binaryAdd(path, 1)); + ecs.add(e); + node.setAdvertisedInterval(e); + return e; + + assert (False); + return None; + + + def intToBinaryString(self, intValue, numDigits): + binaryString = bin(intValue)[2:]; + length = len(binaryString); + for i in range(length, numDigits): + binaryString = "0" + binaryString + return binaryString + + def binaryAdd(self, path, i): + if (path == ""): + return "End"; + decimal = int(path, 2); + decimal += i; + return self.intToBinaryString(decimal, len(path)); + diff --git a/VeriFlow/TrieNode.py b/VeriFlow/TrieNode.py new file mode 100644 index 0000000..ca2bc8c --- /dev/null +++ b/VeriFlow/TrieNode.py @@ -0,0 +1,89 @@ +class TrieNode(object): + """docstring for TrieNode""" + def __init__(self): + super(TrieNode, self).__init__() + self.ecs = set() + self.leftChild = self.rightChild = self.starChild = None + self.openLeft = self.openRight = False + self.possibleLeftEC = self.possibleRightEC = None + self.nodeValue = None + self.advertisedInterval = None + + def getLeftChild(self): + return self.leftChild; + + def setLeftChild(self, leftChild): + self.leftChild = leftChild; + + def getRightChild(self): + return self.rightChild; + + def setRightChild(self, rightChild): + self.rightChild = rightChild; + + def isOpenLeft(self): + return self.openLeft; + + def setOpenLeft(self, openLeft): + self.openLeft = openLeft; + + def isOpenRight(self): + return self.openRight; + + def setOpenRight(self, openRight): + self.openRight = openRight; + + def getStarChild(self): + return self.starChild; + + def setStarChild(self, starChild): + self.starChild = starChild; + + + def numberOfNonStarChildren(self): + num = 0; + if (self.rightChild): + num+=1 + if (self.leftChild): + num+=1 + return num + + + def getPath(self): + return self.getPossibleLeftEC(); + + def setPath(self, path): + self.setPossibleLeftEC(path); + + def getPossibleRightEC(self): + return self.possibleRightEC; + + def setPossibleRightEC(self, possibleRighttEC): + self.possibleRightEC = possibleRighttEC; + + def getPossibleLeftEC(self): + return self.possibleLeftEC; + + def setPossibleLeftEC(self, possibleLeftEC): + self.possibleLeftEC = possibleLeftEC; + + def getNodeValue(self): + return self.nodeValue; + + def setNodeValue(self, nodeValue): + self.nodeValue = nodeValue; + + def getEcs(self): + return self.ecs; + + def setEcs(self, ecs): + self.ecs = ecs; + + def addEC (self, ec): + self.ecs.add(ec); + + def getAdvertisedInterval(self): + return self.advertisedInterval; + + def setAdvertisedInterval(self, advertisedInterval): + self.advertisedInterval = advertisedInterval;