\documentclass[a4paper,9pt,twoside]{article}
\usepackage{zed-cm}
\usepackage{graphicx}
%\markboth{Draft}{Draft}
\pagestyle{myheadings}
\begin{document}
\parskip 6 pt
\parindent 0 pt

\title{Regions in Virgo (v0.9)}
\author{Glyn Normington\\Steve Powell}

\maketitle
\thispagestyle{myheadings}
\pagenumbering{alph}
\setcounter{page}{0}

%=============================================================================
This document provides a formal model of how Virgo divides the OSGi framework into a directed graph
of \textit{regions}.

The model informed the work on \textbf{Bug 330776} ``Re-implement user region using
framework hooks instead of nested framework''.

The model is defined using the Z specification language. An introduction provides an informal
description of regions and how they influence framework hooks for readers who are not familiar with Z.

We are grateful to Rob Harrop for reviewing this model and raising several corrections and
points of clarification and to Dave Kemper for pointing out an inconsistency.

\clearpage
\pagenumbering{roman}
\tableofcontents

% Type checking hacks
\newcommand{\true}{true}
\newcommand{\false}{false}
\renewcommand{\emptyset}{\varnothing}
\newcommand{\ModuleDefZero}{ModuleDef_0}
\newcommand{\ModuleDefOne}{ModuleDef_1}
\newcommand{\ModuleDefTwo}{ModuleDef_2}
\newcommand{\ModuleDefThree}{ModuleDef_3}
\newcommand{\ModuleDefFour}{ModuleDef_4}

%=============================================================================
\clearpage
\pagenumbering{arabic}
\section{Introduction}
\label{cha:intro}

The Virgo kernel is isolated from applications by the use of \textit{regions}.
The kernel runs in its own region and applications run in a \textit{user region}.

Virgo 2.1.0 implemented the user region as a nested framework, but Equinox
has deprecated the nested framework support in favour of \textit{framework hooks}
which are being defined for OSGi R4.3.
\textbf{Bug 330776} re-implements the user region using the OSGi framework and service
registry hooks.

Framework hooks are used to limit which bundles can `see' particular bundles
and exported packages, and service registry hooks are used to limit which bundles
can `see' particular services. `Seeing' includes both finding and being notified via lifecycle events.

Rather than allowing arbitrary hook behaviour, we limit the hooks to operate on regions
which are connected together with filters.

A \textit{region} is then a set of bundles and a region can see bundles, exported packages, and services
from another region via a \textit{connection}. Each connection has a \textit{filter} which may limit
what can be seen across the connection.
Hence regions and connections form a directed graph decorated by filters.

For example, Figure \ref{fig:conn} shows three regions connected by three connections.
Each connection has a filter which limits what bundles, exported packages, and services
are visible across the connection.

\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.35]{connected-regions.pdf}
\caption{Connected Regions}
\end{center}
\label{fig:conn}
\end{figure}

A connection may be thought of as an import. So region C imports from region B.
The imports are filtered, so filter h may limit what region C sees from region B.
Similarly region A imports from region B through filter f and region B imports from region A through
filter g.

Unlike OSGi package imports between bundles, imports between regions are transitive.
So region C can see bundles, exported packages, and services from region A, subject to filters g and h.

We now consider visibility from the perspective of each of the framework hooks.

\subsection{Bundle Find Hook}

The bundle find hook limits the bundles that a bundle in a given region sees when listing bundles using
\texttt{BundleContext.getBundles}.

For example, Figure \ref{fig:bfind} shows a bundle W which finds bundles W, X, and Y.
It does not find Z which is filtered out. 
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{bundle-find.pdf}
\caption{Bundle Find \label{fig:bfind}}
\end{center}
\end{figure}

\subsection{Bundle Event Hook}

The bundle event hook limits the bundle events that a bundle listener in a given region receives.

For example, Figure \ref{fig:bevent} shows a bundle W which has a bundle listener.
Bundle W's bundle listener receives events for W, X, and Y. It does not receive events for bundle Z which is filtered out. 
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{bundle-event.pdf}
\caption{Bundle Event \label{fig:bevent}}
\end{center}
\end{figure}

\subsection{Service Find Hook}

The service find hook limits the services that a bundle in a given region sees when looking up services.

For example, Figure \ref{fig:sfind} shows a bundle W which can look up services s and t but not u which is filtered out.
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{service-find.pdf}
\caption{Service Find \label{fig:sfind}}
\end{center}
\end{figure}

\subsection{Service Event Hook}

The service event hook limits the service events that a service listener in a given region receives.

For example, Figure \ref{fig:sevent} shows a bundle W which has a service listener.
Bundle W's service listener receives events for s and t. It does not receive events for service u which is filtered out. 
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{service-event.pdf}
\caption{Service Event \label{fig:sevent}}
\end{center}
\end{figure}

\subsection{Resolver Hook}

The resolver hook limits the exported packages that the bundles in a given region may wire to, depending on
the region containing the bundle that exports each candidate exported package and the filters between the
regions.

For example, Figure \ref{fig:pfilt} shows a bundle Z being resolved which imports packages p and q. Bundle X
in region B exports both p and q while bundle Y in region B exports only p.

Region A is connected to region B with a filter that allows only package p to be seen by region A.
The net effect is that the import of p may be satisfied by either bundle X or Y but the import of package q may not
be satisfied by bundle X since q is filtered out.
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{package-filtering.pdf}
\caption{Package Filtering \label{fig:pfilt}}
\end{center}
\end{figure}

Another example in Figure \ref{fig:tpfilt} shows a package p transitively visible through two filters via an
intermediate region.

Bundle Z may wire to bundle X or bundle Y for package p, but not for packages q and r which are both
filtered out on the way from C to A.
\begin{figure}[h!]
\begin{center}
\includegraphics*[scale=0.4]{transitive-package-filtering.pdf}
\caption{Transitive Package Filtering \label{fig:tpfilt}}
\end{center}
\end{figure}

The remaining chapters provide a formal, albeit partial, model of bundles, regions, filters, and how
regions are connected together, via filters, into a directed graph.
The model finally defines the behaviour of framework hooks in terms of the directed graph of regions.

%=============================================================================
\clearpage
\section{Basic Types}
\label{cha:basics}

Some basic types define the primitives used in the model.

\subsection*{Bundles}

Bundles are uniquely identified in the OSGi framework by a bundle location, whose details are not
important here.
\begin{zed}
  [BLoc]
\end{zed}
Note that, as of OSGi R4.3, when the framework property \texttt{org.osgi.framework.bsnversion}
is set to \texttt{multiple}, the combination of bundle symbolic name and bundle version is no
longer guaranteed to uniquely identify a bundle in the OSGi framework.

\subsection*{Packages}

We do not need the notion of package version and the attributes associated with package imports
and exports, so we simply declare a set of package objects.
\begin{zed}
  [Package]
\end{zed}

\subsection*{Services}

Neither do we need details of services.
\begin{zed}
  [Service]
\end{zed}

%=============================================================================
\clearpage
\section{Bundle}
\label{cha:bundle}

A bundle has a location, exports zero or more packages, and publishes zero or more services.
\begin{schema}{Bundle}
  location : BLoc \\
  exportedPackages : \power Package \\
  publishedServices : \power Service \\
\end{schema}
It is unusual, and usually bad practice, to include the primary key (in this case the $location$) of
an entity in the entity's schema.
We do it here to ensure that all bundles are
distinct and use this property later when determining which region a bundle belongs to.

%=============================================================================
\clearpage
\section{Region}
\label{cha:region}

We build up to a definition of a region in several small steps.

\subsection{Proto-Region}

A proto-region is a set of bundles.
These are intended to represent the bundles installed in the framework and associated with the proto-region.
\begin{schema}{ProtoRegion}
  localBundles : \power Bundle \\
\end{schema}

\subsection{Indexed Region}

An indexed region is a proto-region with an index of a certain sort.

The index is a function identifying the bundles in the region by location.
\begin{schema}{IndexedRegion}
  ProtoRegion \\
  l : BLoc \pinj Bundle \\
\where
  l = \{ b : localBundles @ b.location \mapsto b \} \\
\end{schema}
The signature imposes the constraint of injectivity on the index.
Thus an indexed region is a set of bundles each of which is uniquely identified
by its location.
Notice that \textbf{all} the bundles in the proto-region are indexed.

\subsection{OpenRegion}

An open region is an indexed region with some derived sets of packages exported by bundles in the region
and services published by bundles in the region.

\begin{schema}{OpenRegion}
  IndexedRegion \\
  localPkg : \power Package \\
  localSvc : \power Service \\
\where
  localPkg = \bigcup \{ b : localBundles @ b.exportedPackages \} \\
  localSvc = \bigcup \{ b : localBundles @ b.publishedServices \} \\
\end{schema}
%We allow a given exported package to be associated with more than one bundle,
%which can happen if a bundle uses
%\texttt{require-bundle} with the reexport option.
%We also allow a given service to be published by more than one bundle,
%which can never happen, but which causes
%no difficulty for this model and would complicate the model if we constrained it.

\subsection{LinkedRegion}

A linked region is an open region with additional sets of imported bundles, packages, and services.

\begin{schema}{LinkedRegion}
  OpenRegion \\
  importedBundles : \power Bundle \\
  importedPkg : \power Package \\
  importedSvc : \power Service \\  
\end{schema}
The imported bundles, packages, and services come into play later when regions are filtered and combined
because it will be possible to filter out a bundle but not its exported packages or published services.
We want to represent the result as a region for simplicity, so the region needs to have a way
of recording packages and services which are `detached' from their bundle(s).

\subsection{Region}

A region is a linked region in which we derive sets of all bundles, all packages, and all services.
\begin{schema}{Region}
  LinkedRegion \\
  bundles : \power Bundle \\
  pkg : \power Package \\
  svc : \power Service \\
\where
  bundles = localBundles \cup importedBundles \\
  pkg = localPkg \cup importedPkg \\
  svc = localSvc \cup importedSvc \\
\end{schema}
The local and imported packages are not necessarily disjoint and neither are the local and imported
services. This is important as packages exported by and services published by imported bundles
are classified as both local and imported.

We define a nil region with no local or imported bundles, packages, or services.
\begin{axdef}
  NIL : Region \\
\where
 NIL.bundles = \emptyset \\
 NIL.pkg = \emptyset \\
 NIL.svc = \emptyset \\
 \end{axdef}

\subsection{Adding a Bundle to a Region}

Bundles are typically added to regions \textit{as part of} the bundle install operation
so that the bundle is associated with its region by the time the
install completes.

A bundle may also be added to a region after the bundle is installed, although this opens up a window in
which the bundle does not belong to any region.

A bundle can be added to a region provided the region does not already contain a bundle with
the given bundle's location.
\begin{schema}{RegionAddBundleOk}
  \Delta Region \\
  b? : Bundle \\
\where
  b?.location \notin \dom l \\
  bundles' = bundles \cup \{ b? \} \\
  importedPkg' = importedPkg \\
  importedSvc' = importedSvc \\
\end{schema}
Note that $l'$, $localPkg'$, $localSvc'$, $pkg'$, and $svc'$ are determined by the constraints of $Region'$.

\subsection{Combining Regions}

Although we will not support operations to combine regions, it is necessary to define how to combine
regions so we can discuss the behaviour of directed graphs of regions later.

%%inop \sqcup 3
Regions with consistent indexing may be combined to produce a composite region using the infix $\sqcup$ operator.
\begin{axdef}
 \_ \sqcup \_ : Region \cross Region \pfun Region \\
\where
 (\_ \sqcup \_) = (\lambda r1, r2 : Region @ \\
\t3 (\mu Region | \\
\t4 bundles = r1.bundles \cup r2.bundles \land \\
\t4 pkg = r1.pkg \cup r2.pkg \land \\
\t4 svc = r1.svc \cup r2.svc)) \\
\end{axdef}
The precondition of $\sqcup$ is that no bundle in one region has the same location as a bundle in the other region.

$\sqcup$ is idempotent, commutative, and associative (where defined) and $NIL$ acts as a zero.
\begin{argue}
  \shows \forall r, s,t : Region | \{ (r, s), (s, t), (t, r) \} \subseteq \dom(\_ \sqcup \_) @ \\
\t1 (r, r) \in \dom(\_ \sqcup \_) \land r \sqcup r = r \land \\
\t1 (s, r) \in \dom(\_ \sqcup \_) \land r \sqcup s = s \sqcup r \land \\
\t1 (r, s \sqcup t) \in \dom(\_ \sqcup \_) \land (r \sqcup s, t) \in \dom(\_ \sqcup \_) \land r \sqcup (s \sqcup t) = (r \sqcup s) \sqcup t \land \\
\t1 (r, NIL) \in \dom(\_ \sqcup \_) \land r \sqcup NIL = NIL \\
\end{argue}

We define the set of all pairwise consistent regions
\begin{zed}
  ConsistentRegionPairs == \dom(\_ \sqcup \_) \\
\end{zed}
and the set of all pairwise consistent finite sets of regions.
\begin{zed}
  ConsistentRegionSets == \{ f : \finset Region | \forall r, s : f @ (r, s) \in ConsistentRegionPairs \} \\
\end{zed}

Since $\sqcup$ is commutative, associative, idempotent, and has a zero, we define a distributed form.
\begin{axdef}
  \bigsqcup : \finset Region \pfun Region \\
\where
  \bigsqcup \emptyset = NIL \land \\
  (\forall r : Region; f : \finset Region | \{ r \} \cup f \in ConsistentRegionSets @ \\
\t1 \bigsqcup( \{ r \} \cup f ) = r \sqcup \bigsqcup f) \\ 
\end{axdef}
  
%=============================================================================
\clearpage
\section{Multiple Regions}
\label{cha:multiregions}

We now describe a system comprising multiple regions.

Regions are identified by a region identifier, whose details are not important here.
\begin{zed}
  [RId]
\end{zed}

The system of multiple regions has a collection of regions indexed by region identifier.
The collection is finite so that certain operations, described later, are well defined.
 
The system has convenience sets of all the bundles and of all the region identifiers in the system.
These sets are derived from the indexed collection.

The system also has a function for determining the region identifier of any bundle in the system from the
bundle's location.
\begin{schema}{Regions}
  reg : RId \ffun Region \\
  allBundles : \power Bundle \\
  rids : \power RId \\
  breg : BLoc \pfun RId \\
\where
 allBundles = \bigcup \{ r : \ran reg@ r.bundles \} \\
 rids = \dom reg \\
 breg = \{ b : Bundle; rid : rids | b \in (reg~rid).bundles @ (b.location, rid) \} \\
\end{schema}
Since $breg$ is a function, no bundle location can belong to more than one region.
Since a bundle's location uniquely identifies the bundle in its region, it follows that a bundle's location uniquely identifies the bundle in the system of multiple regions.

\subsection{Determining a Bundle's Region}

We expose the convenience function as an operation for determining a bundle's region.
\begin{schema}{GetRegionOk}
  \Xi Regions \\
  b? : Bundle \\
  r! : Region \\
\where
  b? \in allBundles \\
  r! = reg(breg~b?.location) \\
\end{schema}

\subsection{Promoting Region Operations}

We define a fairly standard schema for promoting operations on a single region into
operations on the system of multiple regions.
The region to be operated on is singled out using a region identifier and all other regions are left
unchanged.
\begin{schema}{PromoteRegion}
  \Delta Regions \\
  \Delta Region \\
  rid? : RId \\
\where
  rid? \in \dom reg \\
  \theta Region = reg~rid? \\
  reg' = reg \oplus \{ rid? \mapsto \theta Region' \} \\
\end{schema}

Then we promote the operation to add a bundle.
\begin{zed}
  RegionsAddBundleOk \defs (\exists \Delta Region @ PromoteRegion \land RegionAddBundleOk) \\
\end{zed}

This operation has the signature below, which shows that it is now an operation on the
system of multiple regions.
%%unchecked
\begin{schema}{RegionsAddBundleOk}
  \Delta Regions \\
  rid? : RId \\
  b? : Bundle \\
\where
  \ldots
\end{schema}

%=============================================================================
\clearpage
\section{Filters}
\label{cha:filters}

So far the regions in the system are independent of each other.
When we later connect the regions together, we will need to define which bundles,
packages, and services are visible across each connection from one region to another.
We'll do this using a \textit{filter}.

A filter specifies sets of bundles, packages, and services.
\begin{schema}{Filter}
  bf : \power Bundle \\
  pf : \power Package \\
  sf : \power Service \\
\end{schema}

We define some helper functions to perform filtering.

The $filterPackages$ function passes a set of exported packages through a filter.
\begin{axdef}
  filterPackages : \power Package \cross Filter \fun \power Package \\
\where
  filterPackages = \{ ps : \power Package; f : Filter @ ((ps, f), ps \cap f.pf) \}
\end{axdef}

The $filterServices$ function passes a set of published services through a filter.
\begin{axdef}
  filterServices : \power Service \cross Filter \fun \power Service \\
\where
  filterServices = \{ ss : \power Service; f : Filter @ ((ss, f), ss \cap f.sf) \}
\end{axdef}

The $bundleView$ function produces a filtered view of a bundle by applying a filter to the bundle's exported packages and published services.
\begin{axdef}
  bundleView : Bundle \cross Filter \fun Bundle
\where
  bundleView = (\lambda b: Bundle; f : Filter @ \\
\t1  (\mu Bundle | \\
\t2 location = b.location \land \\
\t2 exportedPackages = filterPackages(b.exportedPackages, f) \land \\
\t2 publishedServices = filterServices(b.publishedServices, f)))
\end{axdef}

The $filterBundles$ function passes a set of bundles through a filter.
The result is the set of filtered views of the bundles allowed by the filter.
\begin{axdef}
  filterBundles : \power Bundle \cross Filter \fun \power Bundle \\
\where
  filterBundles = (\lambda bs : \power Bundle; f : Filter @ \{ b : bs \cap f.bf @ bundleView(b, f) \}) \\
\end{axdef}

We also define the most permissive filter.
\begin{axdef}
  TOP : Filter
\where
  TOP.bf = Bundle \\
  TOP.pf = Package \\
  TOP.sf = Service \\
\end{axdef}

\subsection{Filtering Regions}

%%inop \downarrow 6
We define an infix operator $\downarrow$ to apply a filter to a region and produce another region.
\begin{axdef}
  \_ \downarrow \_ : Region \cross Filter \fun Region \\
\where
  (\_ \downarrow \_) = (\lambda r : Region;  f : Filter @ \\
\t3   (\mu Region | \\
\t4 bundles = filterBundles(r.bundles, f) \land \\
\t4 pkg = filterPackages(r.pkg, f) \land \\
\t4 svc = filterServices(r.svc, f))) \\
\end{axdef}
$\downarrow$ is total since packages and services not filtered out which are exported or published by a
bundle which \textit{is} filtered out end up
in the resultant region's imported packages and imported services sets, respectively.

The most permissive filter can be applied to any region without effect.
\begin{argue}
  \shows \forall r : Region @ r \downarrow TOP = r \\
\end{argue}

Filters can be applied in any order with the same effect.
\begin{argue}
  \shows \forall r : Region; f, g : Filter @ (r \downarrow f) \downarrow g = (r \downarrow g) \downarrow f \\
\end{argue}

$\downarrow$ distributes over $\sqcup$ (where defined).
\begin{argue}
  \shows \forall f : Filter; r, s : Region | (r, s) \in ConsistentRegionPairs @ \\
\t1 (r \downarrow f, s \downarrow f) \in ConsistentRegionPairs \land \\
\t1(r \sqcup s) \downarrow f= (r \downarrow f) \sqcup (s \downarrow f) \\
\end{argue}

%=============================================================================
\clearpage
\section{Connected Regions}
\label{cha:connregions}

We now connect up regions to form a directed graph.

Certain pairs of distinct regions are connected by filters. The net effect of connecting a region to other
regions is that the region may then be able to see bundles, exported packages, and services in other regions.
This net effect is modelled as a collection of textit{net} regions.

Every region can be considered to be connected to itself by the most permissive filter.
So the bundles in a region can see all the bundles, exported packages, and services in that region.
\begin{schema}{RegionDigraph}
  Regions \\
  filter : RId \cross RId \pfun Filter \\
  net : RId \pfun Region \\
\where
  \dom filter \subseteq (rids \cross rids) \setminus \id RId \\
  \dom net = rids \\
  (\forall rid : rids @ \\
\t1 net~rid = (reg~rid) \sqcup \bigsqcup \{ r : RId | (rid, r) \in \dom filter @ (net~r) \downarrow filter(rid, r)\})\\
\end{schema}

The $net$ function is well defined but this isn't immediately obvious.
Since there are finitely many regions, the $\bigsqcup$ expression in the constraint is well defined.
Also, we need to be sure that there is a $net$ function which satisfies the constraint.
This turns out to be the case because if we start at a given region $r$ and then form all the non-looping
paths to other regions, then we can apply all the filters along each non-looping path and then
use $\bigsqcup$ to combine the results to form $net~r$ observing that visiting the same region via
a longer, looping path does not affect the result since more filters will
be applied compared to the non-looping path to that region.

\subsection{Connecting Regions Together}

We define an operation to connect two distinct regions with a filter.
\begin{schema}{ConnectOk}
  \Delta RegionDigraph \\
  r?, s? : RId \\
  f? : Filter \\
\where
  r? \neq s? \\
  (r?, s?) \notin \dom filter \\
  \theta Regions' = \theta Regions \\
  filter' = filter \cup \{ (r?, s?) \mapsto f? \} \\
\end{schema}

\subsection{Adding a Bundle to a Region}

Adding a bundle to a region in the directed graph adds the bundle to a region in the
system of multiple regions and affects no connections or filters.
We add a constraint that the bundle being added must not 
be present in a filter associated with the region the bundle is being added to.
This is to avoid a bundle in a region clashing with a bundle from a connected region.
\begin{schema}{CRAddBundleOk}
  \Delta RegionDigraph \\
  RegionsAddBundleOk \\
\where
  filter' = filter \\
  (\forall s : RId; f : Filter | (rid?, s) \mapsto f \in filter @ \\
\t1 b? \notin f.bf) \\ 
\end{schema}

\subsection{Determining a Bundle's Region}

A bundle's region in the directed graph is the same as the bundle's
region in the syste, of multiple bundles.
This operation does not affect any connections or filters.
\begin{zed}
  CRGetRegionOk \defs \Xi RegionDigraph \land GetRegionOk \\
\end{zed}

%=============================================================================
\clearpage
\section{Framework Hooks}
\label{cha:fhooks}

We can now describe the behaviour of framework hooks in terms of our directed graph of regions.

A bundle `find' operation, such as \texttt{BundleContext.getBundles}, is returned only the
candidates in the net region of the bundle performing the operation.

That is, the bundle performing a bundle `find' operation is returned the bundles in its own region
and bundles in connected regions that are allowed by the corresponding filters.
\begin{schema}{BundleFindHook}
  \Xi RegionDigraph \\
  finder? : Bundle \\
  candidates? : \power Bundle \\
  found! : \power Bundle \\
\where
  finder? \in allBundles \\
  found! = candidates? \cap (net(breg~finder?.location)).bundles \\
\end{schema}

A bundle listener receives only events for bundles in the net region of the bundle that was used
to register the listener.

That is, the bundle listener receives events for bundles in the region used to register the listener
and for bundles in connected regions that are allowed by the corresponding filters.
\begin{schema}{BundleEventHook}
  \Xi RegionDigraph \\
  listeners? : \power Bundle \\
  eb? : Bundle \\
  fl! : \power Bundle \\
\where
  listeners? \subseteq allBundles \\
  fl! = \{ l : listeners? | eb? \in (net(breg~l.location)).bundles \} \\
\end{schema}

A bundle being resolved may wire only to exported packages and bundles in the net region of the
bundle.

That is, the bundle may wire to exported packages and bundles in its own region and to
exported packages and bundles in connected regions that are allowed by the corresponding filters.
\begin{schema}{ResolverHookFilterMatches}
  \Xi RegionDigraph \\
  requirer? : Bundle \\
  candidates? : \power Package \\
  filtered! : \power Package \\
\where
  requirer? \in allBundles \\
  filtered! = candidates? \cap (net(breg~requirer?.location)).pkg \\
\end{schema}

A service `find' operation is returned only the
candidates in the net region of the bundle performing the operation.

That is, the bundle performing a service `find' operation is returned the services in its own region
and services in connected regions that are allowed by the corresponding filters.
\begin{schema}{ServiceFindHook}
  \Xi RegionDigraph \\
  finder? : Bundle \\
  candidates? : \power Service \\
  found! : \power Service \\
\where
  finder? \in allBundles \\
  found! = candidates? \cap (net(breg~finder?.location)).svc \\
\end{schema}

A service listener receives only events for services in the net region of the bundle that was used
to register the listener.

That is, the service listener receives events for services in the region used to register the listener
and for services in connected regions that are allowed by the corresponding filters.
\begin{schema}{ServiceEventHook}
  \Xi RegionDigraph \\
  listeners? : \power Bundle \\
  es? : Service \\
  fl! : \power Bundle \\
\where
  listeners? \subseteq allBundles \\
  fl! = \{ l : listeners? | es? \in (net(breg~l.location)).svc \} \\
\end{schema}

%=============================================================================
\newpage
\section{Z Notation}
\label{cha:znot}

\makeatletter % the following code is taken from Mike Spivey's zed.tex

\def\symtab{\setbox0=\vbox\bgroup \def\\{\cr}
        \halign\bgroup\strut$##$\hfil&\quad##\hfil\cr}
\def\endsymtab{\crcr\egroup\egroup
        \dimen0=\ht0 \divide\dimen0 by2 \advance\dimen0 by\ht\strutbox
        \splittopskip=\ht\strutbox \vbadness=10000
        \predisplaypenalty=0
        $$\halign{##\cr\hbox to\linewidth{% 
                \valign{##\vfil\cr
                        \setbox1=\vsplit0 to\dimen0 \unvbox1\cr 
                        \noalign{\hfil}\unvbox0\cr
                        \noalign{\hfil}}}\cr 
                \noalign{\prevdepth=\dp\strutbox}}$$
        \global\@ignoretrue}

\makeatother 

Numbers:
\begin{symtab}
        \nat & \verb/Natural numbers/ \{\verb/0,1,.../\} \\
%       \num & \verb/Integers (...,-1,0,1,...)/ \\
%       \nat_1 & \verb/Positive natural numbers/ \\
%       \upto & \verb/integral range/ \\
%       + & \verb/Addition/\quad\hfill 3 \\
%       - & \verb/Subtraction/\quad\hfill 3 \\
%       * & \verb/Multiply/\quad\hfill 4 \\
%       \div & \verb/Remainder/\quad\hfill 4 \\
%       \mod & \verb/Modulus/\quad\hfill 4 \\
%       < & \verb/Less than/ \\
%       > & \verb/Greater than/ \\
%       \leq & \verb/Less than or equal/ \\
%       \geq & \verb/Greater than or equal/ \\
%       \neq & \verb/Inequality/ \\
\end{symtab}
Propositional logic and the schema calculus:
\begin{symtab}
%       \lnot & \verb/Not/ \\
        \ldots\land\ldots & \verb/And/ \\
        \ldots\lor\ldots & \verb/Or/ \\
        \ldots\implies\ldots & \verb/Implies/ \\
%       \iff & \verb/If and only if/ \\
        \forall..\mid..\spot.. & \verb/For all/ \\
        \exists..\mid..\spot.. & \verb/There exists/ \\
%       \exists_1..\mid..\spot.. & \verb/There exists unique/ \\
        \ldots\hide\ldots & \verb/Hiding/ \\
%       \project & \verb/\project/ \\
%       \pre & \verb/\pre/ \\
%       \semi & \verb/\semi/
        \ldots\defs\ldots & \verb/Schema definition/ \\
        \ldots==\ldots & \verb/Abbreviation/ \\
        \ldots::=\ldots\mid\ldots & \verb/Free type definition/ \\
        \ldata\ldots\rdata & \verb/Free type injection/ \\
        [\ldots] & \verb/Given sets/ \\
        ',?,!,_0\ldots_9 & \verb/Schema decorations/ \\
        \ldots\shows\ldots & \verb/theorem/ \\
        \theta\ldots & \verb/Binding formation/ \\
        \lambda\ldots & \verb/Function definition/ \\
        \mu\ldots & \verb/Mu-expression/ \\
        \Delta\ldots & \verb/State change/ \\
        \Xi\ldots & \verb/Invariant state change/ \\
\end{symtab}
Sets and sequences:
%and bags:
\begin{symtab}
        \{\ldots\} & \verb/Set/ \\
        \{..\mid..\spot..\} & \verb/Set comprehension/ \\
        \power\ldots & \verb/Set of subsets of/ \\
%       \power_1 & \verb/Non-empty subsets of/ \\
%       \finset & \verb/Finite sets/ \\
%       \finset_1 & \verb/Non-empty finite sets/ \\
        \emptyset & \verb/Empty set/ \\
        \ldots\cross\ldots & \verb/Cartesian product/ \\
        \ldots\in\ldots & \verb/Set membership/ \\
        \ldots\notin\ldots & \verb/Set non-membership/ \\
        \ldots\cup\ldots & \verb/Union/ \\
        \ldots\cap\ldots & \verb/Intersection/ \\
        \ldots\setminus\ldots & \verb/Set difference/ \\
        \bigcup\ldots & \verb/Distributed union/ \\
%       \bigcap & \verb/Distributed intersection/ \\
        \#\ldots & \verb/Cardinality/ \\
%       \dcat & \verb/Distributed sequence concatenation/
        \ldots\subseteq\ldots & \verb/Subset/ \\
        \ldots\subset\ldots & \verb/Proper subset/ \\
        \ldots\partition\ldots & \verb/Set partition/ \\
        \seq & \verb/Sequences/ \\
%       \seq_1 & \verb/Non-empty sequences/ \\
%       \iseq & \verb/Injective sequences/ \\
        \langle\ldots\rangle & \verb/Sequence/ \\
%       \cat & \verb/Sequence concatenation/ \\
        \disjoint\ldots & \verb/Disjoint sequence of sets/ \\
%       \bag & \verb/Bags/ \\
%       \lbag\ldots\rbag & \verb/Bag/ \\
%       \inbag & \verb/Bag membership/ \\
\end{symtab}
%Here are the infix function symbols. Each symbol is
%shown with its priority:
%\begin{symtab}
%       \uplus & \verb/\uplus/ \\
%       \filter & \verb/Schema projection/ \\
%       \uminus & \verb/\uminus/
%\end{symtab}
Functions and relations:
\begin{symtab}
        \ldots\rel\ldots  & \verb/Relation/ \\
        \ldots\pfun\ldots & \verb/Partial function/ \\
        \ldots\fun\ldots  & \verb/Total function/ \\
        \ldots\pinj\ldots & \verb/Partial injection/ \\
        \ldots\inj\ldots  & \verb/Injection/ \\
%       \psurj & \verb/Partial surjection/ \\
%       \surj & \verb/Surjection/ \\
%       \bij  & \verb/Bijection/ \\
%       \ffun & \verb/Finite partial function/ \\
%       \finj & \verb/Finite partial injection/ \\
        \dom\ldots & \verb/Domain/ \\
        \ran\ldots & \verb/Range/ \\
        \ldots\mapsto\ldots & \verb/maplet/ \\
        \ldots\inv & \verb/Relational inverse/ \\
%       \ldots\plus & \verb/Transitive closure/ \\
        \ldots\star & \verb/Reflexive-transitive closure/ \\
%       \ldots\bsup n \esup & \verb/Relational iteration/ \\
        \ldots\limg\ldots\rimg & \verb/Relational image/ \\
%       \comp & \verb/Forward relational composition/ \\
%       \circ & \verb/Relational composition/ \\
        \ldots\oplus\ldots & \verb/Functional overriding/ \\
        \ldots\dres\ldots & \verb/Domain restriction/ \\
%       \ldots\rres\ldots & \verb/Range restriction/ \\
        \ldots\ndres\ldots & \verb/Domain subtraction/ \\
%       \ldots\nrres\ldots & \verb/Range subtraction/ \\
%       \id & \verb/Identity relation/ \\
\end{symtab}
Axiomatic descriptions:
%%unchecked
\begin{axdef}
  Declarations
\where
  Predicates
\end{axdef}
Schema definitions:
%%unchecked
\begin{schema}{SchemaName}
  Declaration
\where
  Predicates
\end{schema}
\end{document}