Hi Carole and Boaz and Mitch: enclosed is an application of AI FR techniques to software development, using powerful tools like the Boyer-Moore theorem prover. Is this a good way to go or are direct graph algorithms more effective? Boaz had a proposal for an algorithm which checks whether X is always before Y when traversing paths specified by some strategy. -- Karl >From dta@organon.com Tue Sep 2 18:55:23 1997 >From: Dean T Allemang >To: lieber@ccs.neu.edu >Subject: Applying ZD to Demeter (or vice versa?) >Status: R > >Hello Karl, > >I have been working on the problem you set on the plane, when we came >back from Seattle. It turns out to have been quite interesting for a >number of reasons. > >There seem to be a number of ways to approach the problem from a ZD >perspective, but only one of them seems to show any promise of a >solution. Before I talk about these various approaches, I need to >talk a bit about how ZD works, and what it means to cast a problem >into ZD. > >ZD talks about decomposing a system (or "device") into "subdevices". >Then the modeler tells a story about how the subdevices cooperate to >provide the functionality of the device. The story is told via an >"annotated finite state automaton" diagram. The basic FSA diagram in >ZD is a sequence of states, with transitions annotated by mentions of >functions of other devices, thus: > > i=3 & s=6 > | > | Using increment of index > | > V > i=4 & s=6 > | > | > | Using sum of total (i) > | > V > i=4 & s=10 > > >This FSA fragment shows how the functions (called "increment" and >"sum" here) of two subdevices (called "index" and "total" >respectively) work together (in this case, by using increment and then >sum). The annotations are the references to the subdevices (using the >keyword "Using"). > >There are a number of extensions to basic FSAs that ZD uses, but for >this discussion, we will concentrate on the "recursive FSA". A >recursive transition in a FSA is drawn with two arcs in the graph, as >follows: > > >Function 0: > > state A > | > | > | Using fun1 > | > V > state B > | > | > | Using fun2 > | > V > state C > | | > | | > Using fun4 | | Using function 0 > | | > V V > state D > > Figure 0 > > >Notice that one of the arcs on the double link refers recursively to >the function that is described in this diagram. > >The interpretation of such a recursive FSA diagram is as follows: > > > state A > | > | > | > | > V > state B > | > | > | > | > V > state C == state A' > | > | > | > | > V > state B' > | > | > | > | > V > state C' == state A'' > | > | > | > | > V > state B'' > | > | > | > | > V > state C'' == state A''' > | > | > | > | > V > state B''' > | > | > | > | > V > state C''' > | > | > | Using fun4 > | > V > state D == state D' == state D'' == state D''' > > > (figure 1) > > >That is, the recursive FSA expands to a large FSA consisting of >several nested copies of the original FSA as shown. The primes ('') >have to do with the level of recursive reference; state C'' is not the >same as state C, but is described by the same node in the recursive >diagram. The number of 's needed will depend on the particular run of >the program described by the diagram; the recursive diagram is a >fixed-size representation of an indeterminate sized underlying >diagram. In order for this to be meaningful, there must be a way to >map the initial state of the recursive FSA (state A) to the state >description just before the recursive reference (state C). This >corresponds to a loop invariant in program verification. Similarly, >the final state of the recursive FSA (state D) must be made to >correspond to the state after the recursive references (also state D). > >The following example is a typical use of recursive FSAs. Notice that >the initial state (corresponding to state A) can be mapped to the >state before the recursive call by substituting the (current) value x >for the new value x+1. > > >Function Count: > > i=x & P(i) > | > | > | Using increment of index > | > V > i=x+1 & P(i-1) > | > | > | Using visit of element (i) > | > V > i=x+1 & P(i) > | | > | | > Using null | | Using Count > | | > V V > i=x+1 & P(i) & i=N > > > > >Proviso Propagation >~~~~~~~~~~~~~~~~~~~ > >ZD provides a number of mechanisms for determining the consistency of >a functional representation. The one which is relevant in this >example is called "Proviso Propagation". The basic idea is that, in >addition to the specification of a subdevice, you can provide certain >information about the dynamic context in which the subdevice can be >used. We will see an example of this in the Demeter problem below. > >The simplest form of proviso propagation can be shown even for >non-recursive FSA diagrams. Consider the following (non-recursive) >diagram: > > >Function 0: > > State A > | > | > | Using fun1 > | > V > State B > | > | > | Using fun2 > | > | > V > State C > | > | > | Using fun3 > | > | > V > State D > >Suppose that fun3 has a proviso attached to it, say P. This means, >that for fun3 to work (to "fulfill its function") in this diagram, P >has to hold in state C. If we can prove P given C, then we can prove >that this will be the case. If, however, P cannot be proven given C, >then we will have to say that the entire function Function 0 can only >fulfill its function, provided P holds in its context. The "proviso" >P can thus be propagated to higher and higher levels. > >There is another way in which P can be satisfied. Suppose that fun2 >provides additional results, say Q, which are not integrated into the >state description state C. These results could be used to show that P >is satisfied. If we can prove P given Q, then we need not propagate >it to a higher level (i.e., function 0). > >Similar comments hold for fun1; if fun1 provides Q', and Q' can prove >P, then P need not be propagated further. > >Thus, for non-recursive diagrams, the proviso propagation algorithm is >a simple graph search, which determines matches of P's and Q's in this >fashion, and propagates whatever is left over to the next level up. > > >Proviso Propagation gets interesting when the FSA is recursive. >Returning to figure 1, we have more opportunities for a proviso to be >satisfied. > >Suppose that fun2 has a proviso P, and fun1 an additional result Q, >such that given Q, we can prove P. Then we can use the simple proviso >propagation mechanism above to determine that we need not propagate P >to a higher level. This is shown in figure 2. > > state A > | > | > | Using fun1 Q > | | > V v > state B > | ^ > | | > | Using fun2 P > | > V > state C > > figure 2. > > >Suppose instead, that fun1 has a proviso P, and fun2 an additional >result Q. > > state A > | ^ > | | > | Using fun1 P > | > V > state B > | > | > | Using fun2 Q > | | > V v > state C > > figure 3 > >In a non-recursive FSA, this would mean that P and Q would be >propagated as proviso and additional result to the higher level. But >in the context of the recursive expansion, this becomes even more >problematic: > > state A > | ^ > | | > | Using fun1 P > | > V > state B > | > | Using fun2 Q > | | > | v > V > state C == state A' > | ^ > | | > | Using fun1 P' > | > V > state B' > | > | > | Using fun2 Q' > | | > V v > state C' > > > > figure 4 > >Now the propagated proviso has to be P & P' & P'' & P''' & ..., and the >propagated additional result has to be Q & Q' & Q'' & Q''' & .... >Since the details of how many levels of 's depends on the particular >run, we cannot propagate these terms, unless we find a way to make a >closed form for them. > >This can happen if we can show that Q can guarantee P', Q' can >guarantee P'', etc, with Q(j) guaranteeing P(j+1) as the general >case (where Q(k) indicates Q with k primes (') after it). > >ZD checks for this case, and issues P and Q(n) as the proviso and >additional result respectively from this case. Often these >expressions, as boundary conditions, reduce to trivialities. >Sometimes they reflect a profound summary of what is going on in the >recursive situation. > >While it might be possible to consider arbitrary matches between P(j) >and Q(k) in determining what expressions to propagate, ZD only does >the one specified above (which corresponds to an inductive proof). >The reason for this is that the method used by ZD allows a local >decision (e.g., Q(j) -> P(j+1)) to be leveraged into a global property >(P and Q(n) being propagated). Determination of arbitrary >interactions of Q's and P's would require generation of the entire >expanded FSA, thus losing any advantage to having the "closed form" of >the recursive definition. > > >Application to Demeter >~~~~~~~~~~~~~~~~~~~~~~ > >Now we are in a position to apply ZD to Demeter. The following is >based on a sample problem set by Karl, as a means of showing how ZD >might be applied to adaptive programming. > >In the following, I view Demeter's actions as taking a class graph, >with two nodes designated as "source" and "destination", along with >some rules about which nodes/links may/may not be visited, and >producing a set of paths from the source to the destination, >respecting these restrictions. This is based on the behavior of >dem.lisp, the Common Lisp implementation of a restricted version of >Demeter. > >The problem, as it was stated, was to determine whether the paths >produced in this way have a certain interesting property, namely that >each visit to a particular node (say, Y) is preceded by a visit to >another particular node (say X). > >On the face of it, this does not seem like a ZD problem, since ZD >deals with decomposition of a system into subsystems, and the >interaction of these systems. However, it can easily be transformed >into such a problem, as follows. We consider the "visit" method of >node Y having a condition that the "visit" method of node X has >already been called (in ZD terms, the visit method of Y has a >"proviso" - it will work "provided" some statement holds, while the >visit method of X has an "additional result", which happens to be the >same statement). ZD can then determine whether the combination of >these visitors with the original graph is consistent. > >The problem with representing this in ZD is to make the FSA diagram, >which calls upon "functions" of these two subdevices, namely the >visitor and the class graph. We could imagine something like the >following: > >Function ADAPTIVE-CALL-METHOD > > > Call made to next node, and > methods processed for all previous nodes > | > | > | Using function NEXT of graph > | > V > call made to current node, and > methods processed for all previous nodes > | > | > | Using function VISIT of visit method > | > | > V > call made to current node, and > methods processed for all previous nodes and current node > | | > | | > Using NULL | | Using ADAPTIVE-CALL-METHOD (recursive call) > | | > | | > V V > methods processed for all nodes > > >The problem with this approach is that the function "next" of the >graph is basically the Demeter specification; we need to be able to >determine from a graph, which node Demeter will recommend as the next >method dispatch. > >This problem can be solved easily enough by modifying the Demeter >code to produce a description, in the language of the theorem prover >underlying ZD (at present, this is the NQTHM language of Boyer and >Moore), which describes the NEXT function. In fact, I have done this >(creating thereby a sort of DEM-NQ). > >Let's create an example to discuss this further. Consider the >following class graph (there are no subclass links in this graph) > > > --- X -------- B ---- > / \ > S ---- A < Y------ E > \ / > --- C --------------- > > figure 5 > > >So, the definition of NEXT in NQTH looks something like this: > > (DCL NEXT (ARG)) > > (ADD-AXIOM G448 (REWRITE) (MEMBER (E) (NEXT (Y)))) > (ADD-AXIOM G449 (REWRITE) (MEMBER (Y) (NEXT (B)))) > (ADD-AXIOM G450 (REWRITE) (MEMBER (B) (NEXT (X)))) > (ADD-AXIOM G451 (REWRITE) (MEMBER (X) (NEXT (A)))) > (ADD-AXIOM G452 (REWRITE) (MEMBER (A) (NEXT (S)))) > (ADD-AXIOM G453 (REWRITE) (MEMBER (E) (NEXT (Y)))) > (ADD-AXIOM G454 (REWRITE) (MEMBER (Y) (NEXT (C)))) > (ADD-AXIOM G455 (REWRITE) (MEMBER (C) (NEXT (A)))) > (ADD-AXIOM G456 (REWRITE) (MEMBER (A) (NEXT (S)))) > >The add-axiom construct is a way in NQTHM to specify things about a >function, without necessarily defining it totally. These axioms say >things like "node E is one of the nodes which follows node Y". Notice >that the two followers of node A each have separate axioms. Had the >Demeter event specified, say, that node C should be omitted from >consideration, then only the axioms relating to the path S-A-X-B-Y-E >would have been generated. > >So, to cast the problem into the proviso propagation mold of ZD, we >say that the visit method for Y has a proviso, say R, and that the >visit method for X has R as an additional result. If every path from >S to E contains an X and a Y (in that order), then no proviso will be >propagated onwards. If, as is the case in figure 5, there is a path >with a Y and without an X, then the proviso (R) will be propagated, >indicating that the system will only work in a context where R is >already guaranteed, outside the system. > > >Can we use the ZD PP mechanism to determine this? To find out, we >have to consult figure 4. We have to determine what P, P', P'', >... and Q, Q', Q'', etc. refer to. > >As we have seen above, Q(n) is just R, whenever the node visited at >level (n) is X, and P(n) is R, whenever the node visited at level (n) >is Y. This presents a problem for the proviso propagation method >described in figure 4; namely, we cannot show that Q(j) guarantees >P(j+1). This means that there is no way to collapse the sequence of >Qs and Ps into a simple proviso and additional result made up of P and >Q(n) respectively. > >Now, it is possible to state axioms which, in addition to the DEM-NQ >axioms above, will allow the theorem prover to perform the appropriate >search to produce the right proviso. We could provide another proviso >propagation mechanism in ZD to generate these axioms. However, this >would leave the search strategy up to the theorem prover; if we use a >different theorem prover, then this proviso propagation method would >have to change. > > > >Using the current PPP mechanism to resolve the problem >~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > >The real problem here is one of graph searching; namely, is there a >path from S to Y that leaves out X? We can set up the theorem prover >to do this search, but since the proviso propagation method is already >searching the graph, why not instead figure out a way to get ZD to do >the search directly? > >This solution turns out to be fairly straightforward - we simply >translate the output of Demeter (i.e., the allowed paths) into ZD >FSAs. There are a number of ways to do this, each of which uses a ZD >construct similar to the recursive link shown in figure 0. I have >implemented one of these, in which a class graph is translated into a >ZD graph. > >The solution uses the dem.lisp code to generate all the valid paths >from the class graph and the constraints. Each path is then used to >create a ZD device, which connects the start node to the finish node. >A high-level device is then created, which > > >The solution is probably best illustrated by using the example shown >in figure 5, for which dem.lisp generates two paths, namely >S-A-X-B-Y-E and S-A-C-Y-E. Given the graph in figure 5, the following >ZD structure are generated with the event call > >(zd-event zorch (((S) (E) () ())) > ( > (X :provided () :addres (something 1)) > (Y :provided (something 1) :addres ())) > ((something :type FUN))) > > > >First, dem-zd creates one device per path, thus: > >Device path1 > >Function traverse1 > > T > | > | Using Visit of S > | > | > V > T > | > | Using Visit of A > | > | > V > T > | > | Using Visit of X > | > | > V > T > | > | Using Visit of B > | > | > V > T > | > | Using Visit of Y > | > | > V > T > | > | Using Visit of E > | > | > V > T > > >Device path2 > >Function path2 > > T > | > | Using Visit of S > | > | > V > T > | > | Using Visit of A > | > | > V > T > | > | Using Visit of C > | > | > V > T > | > | Using Visit of Y > | > | > V > T > | > | Using Visit of E > | > | > V > T > > >Notice that all the state descriptions are simply "T"; this is because >we don't have any information on the state that should hold in the >system, when, say, the method has been dispatched to S and A, but not >yet to X. One could imagine information of this sort being provided >by some other aspect, being woven in by Demeter. > >Notice also that the state-transition graph in each of these devices >is the /dual/ graph of the path generated by dem.lisp; i.e., for each >node in the path, there is an edge in the state-transition graph, and >vice versa. This is because each node in the class graph corresponds >to an action in the FSA. > >Finally, another device is created, which refers to both of these >devices, in a simple FSA that demonstrates that either of them can be >used to achieve the connection from start to end, i.e., from S to E. > >Device zorch > >Function zorch > > T > > | | > | | > | | > Using traverse1 of path1 | | Using traverse2 of path2 > | | > | | > V V > > T > >Again, the states are both simply "T", because we have no information >about the state of the system during the call. > > >We then attach provisos to the links in traverse1 and traverse2 as >indicated in the event call, namely for X.visit, addres is (something >1), for X.visit, provided is (something 1). > >The (non-recursive) version of PPP can determine whether Y is always >preceded by X; in this case, the answer is NO, (since path2 has a >path in which Y appears, but X does not). In this case, ZD propagates >(something 1) as a proviso for zorch, since this statement must hold >in order for Y to function, and therefor for zorch to function. > >If, on the other hand, we generate the ZD graph using the event >description > >(zd-event zorch (((S) (E) () ((C * *)))) > ( > (X :provided () :addres (something 1)) > (Y :provided (something 1) :addres ())) > ((something :type FUN))) > >then only path1 is generated, and (something 1) is not propagated as a >proviso (but it is propagated as an additional result. The rationale >for this is that while an additional result can guarantee a proviso, >thereby relieving the system of the burden of requiring it. However, >just because an additional result was used to prove some proviso, does >not make it stop being true; it could be used further to guarantee >more provisos. Thus, we continue to propagate additional results, >even after they have been used). > > > >More interesting applications of ZD to Demeter >~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > >The application of ZD to Demeter above is somehow boring; all the >recursion is left to the dem-zd module; the ZD diagrams are completely >uninteresting. > >It would be nice to use the recursive tracing powers of the PPP >mechanism to do something a little bit more powerful. I think this is >possible; I would like to conclude by discussing the possibilities, and >see what might already exist in Demeter to make these things happen. > >It is possible, by appropriate assignments of provisos and addreses, >to make ZD ignore certain paths. For example, when we had Demeter >generate both paths from figure 5, I was able to make ZD ignore the >path with the C in it (i.e., as if I had asked Demeter to include (C * >*) in its exclude list). I believe that the current search techniques >in ZD would be able to do a lot of Demeter-like stuff, if only we >could represent the graphs in it. > >This is not a problem for non-cyclic graphs; even though ZD wants to >have all the graphs of the form made from links of the form > > >A -------> B > > >or > > >A =======> B > > >for some kind of double link, this can be used to represent arbitrary >acyclic graphs. The problem comes with the cycles. For example: > > ----------------- > / \ > | | > | -----> C -----> E > V/ \ >S -----> A ----> B \ > ^ \ F > \ -----> D > \ | > --------------/ > > >There are two loops here, one A-B-D and one B-C-E. It is possible to >represent this with a sequence of splits and recursive graphs in ZD. >Is this true in general? Does Demeter already face some form of >"cycle linearization" to do what it does? I noticed that dem.lisp >doesn't pay any attention to the cycles at all. What is the full >Demeter policy on this? > >If it were possible to linearize a graph like this into ZD FSAs (or if >it isn't necessary, because Demeter does not handle cycles anyway), >then it should be possible to specify a lot of Demeter conditions as >provisos on the corresponding visitors. It would be interesting to >see if this provides a different level of expressiveness for the >allowable paths. > >Dean > >