Standalone computational specification

def adjacency(self, include_latent=False): adj = v: set() for v in self.regions() for _, u, v in self.active: adj[u].add(v) if include_latent: for _, ends in self.latent: u, v = tuple(ends) adj[u].add(v) adj[v].add(u) return adj

def acyclic(self): adj = self.adjacency() colour = v: 0 for v in adj

def visit(v): if colour[v] == 1: return False if colour[v] == 2: return True colour[v] = 1 for w in adj[v]: if not visit(w): return False colour[v] = 2 return True

return all(visit(v) for v in adj)

def has_path(self, source, target): seen = set() todo = [source] adj = self.adjacency() while todo: v = todo.pop() if v == target: return True if v not in seen: seen.add(v) todo.extend(adj[v] - seen) return False

def potential_relation(self): adj = self.adjacency(include_latent=True) out = set() for source in adj: seen = set() todo = [source] while todo: v = todo.pop() if v not in seen: seen.add(v) out.add((source, v)) todo.extend(adj[v] - seen) return frozenset(out)

def mu(self): return (sum(c for _, c in self.cap) + len(self.active) + len(self.latent))

def cut_mu(self, X): X = frozenset(X) require(X <= self.regions(), "cut contains unknown region") Y = self.regions() - X cap_x = sum(c for v, c in self.cap if v in X) latent_x = sum(len(ends & X) == 1 for _, ends in self.latent) active_xy = sum(u in X and v in Y for _, u, v in self.active) return cap_x + latent_x + active_xy

def sigma(self, X): X = frozenset(X) require(X <= self.regions(), "cut contains unknown region") return ( sum(len(ends & X) == 1 for _, ends in self.latent) + sum((u in X) != (v in X) for _, u, v in self.active) )

def all_cuts(g): V = sorted(g.regions()) for k in range(len(V) + 1): for members in combinations(V, k): yield frozenset(members)

def owned(cell, frame): if cell not in set(frame): raise GuardFailure("missing ownership permission")

def finish(g, g2, expected_mu_delta): require(g2.mu() - g.mu() == expected_mu_delta, "incorrect scalar ledger") for X in all_cuts(g): require(g2.cut_mu(X) <= g.cut_mu(X), "cut_mu increased") require(g2.sigma(X) <= g.sigma(X), "sigma increased") require(g2.potential_relation() <= g.potential_relation(), "potential reachability increased") return g2