Aliasing and disjointness, with ASAP

In the ASAP method, linkage information in a structure is expressed via a series of axioms. The axioms come in two basic types, either describing when nodes are equal (aliased) or unequal (disjoint). To incorporate this information into the AG description we augment it with two further FSAs, $\mathcal{F}_a$ to hold the aliasing information and $\mathcal{F}_d$ to hold the disjointness information. We can then add to the information provided by the bare AG structure by combining with $\mathcal{F}_a$ and $\mathcal{F}_d$ at appropriate points in the analysis.

There are three kinds of axiom in the ASAP framework.

$$\begin{eqnarray*}1) && \quad \forall p \quad p.RE1 \neq p.RE2 \\ 2) && \quad \f... ... p.RE1 \neq q.RE2 \\ 3) && \quad \forall p \quad p.RE1 = p.RE2 \end{eqnarray*}$$

Where p,q are any path names and RE1,RE2 are regular expressions over A^* . Given a regular expression RE1 it is trivial to convert it to a two variable `appended' FSA denoted Ap_RE1, that accepts (p.RE1, p) for all p, . Additionally, using $\mathcal{F}_{\neq}$ the FSA that accepts a pair of paths if they are not equal, we can give expressions that convert axioms of each type to FSAs that accept the equivalent pairs of words. The required equations are as follows.

$$\begin{eqnarray*}1) && \quad \textrm{Ap}_{RE1} . (\textrm{Ap}_{RE2}^{-1}) \\ 2)... ...}) \\ 3) && \quad \textrm{Ap}_{RE1} . (\textrm{Ap}_{RE2}^{-1}) \end{eqnarray*}$$

We then build $\mathcal{F}_d$ by ORing together all the FSAs produced from axioms 1 and 2, and $\mathcal{F}_a$ by ORing the ones from axiom 3. We can thus automatically generate $\mathcal{F}_a$ and $\mathcal{F}_d$ from ASAP axioms, and thus combine these descriptions with the bare AG ones.

It should be noted that the FSAs for some sets of axioms can get quite large, for example the axioms for a sparse matrix produce a $\mathcal{F}_d$ of approximately 150 states. This may be too large for much further analysis of the structure to be completed.