[Javapathfinder-svn] SF.net SVN: javapathfinder:[1909] branches/mango/Mango

[<fra...@us...>]

Revision: 1909
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1909&view=rev
Author:   frankrimlinger
Date:     2009-09-16 20:50:57 +0000 (Wed, 16 Sep 2009)

Log Message:
-----------
To write the choice logic for methods and blowups, first need the notion of the *strong attractor* and the *weak attractor* of a vertex.  The strong attractor  S(v) of v is the maximal subgraph of G with unique sink v.  Clearly the strong attractor is unique, and for vertices v and w, either S(v) and S(w) are disjoint, or one of these graphs is included in the other.  The weak attractor W(v) of v is the union of all paths which terminate at v.  Clearly W(v) contains S(v).  The attraction is weak because when you are in W(v)-S(v) you still have the chance to escape v altogether.

Let G be the graph of all components together with superCpnConnection and subCpnConnection connections.  We are interested in S(omega) and W(omega) for omega vertices of G.

Computation for S(v):
0) v is in S(v)
1) if w is a vertex of S(v), then every inbound edge to w is in S(v).
2) a vertex w is in S(v) if and only if every outbound edge of w is in S(v).

Computation for W(v)
0) S(V) is in W(v)
1) if w is a vertex of W(v), then every inbound edge to w is in W(v).
2) a vertex w is in W(v) if and only if there exists an outbound edge of w in S(V).

MethodChoiceGenerator trail logic: Let Omega be the set of all omega vertices. The the trail state set is {open,attracted,repelled} x Omega.  The trail starts out in the open state for each omega.  If it enters S(omega) for some omega, the state transitions to attracted for that omega.  The trail must now hit omega, when it does, it jumps to the corresponding alpha, and changes its state to repelled with respect to omega.  The trail must now remain in the repelled state with respect to omega, which means either stopping at alpha (i.e. stuck in infinite loop) or traveling along a path in G-V(omega) to a sink of G.  Notice that by infinite loop we mean a *structurally* infinite loop, i.e., no exit branch, like while(true){}.  This doesn't happen very often, but a driver could have this structure.

Strictly speaking the attracted state is unnecessary, but good feedback.

BlowupChoiceGenerator trail logic: Start at alpha and remain in W(omega). End at omega.

Observe that there is ample opportunity for exponential growth in the number of trails.  But for now, we punt on case filtering and case consolidation.  The point here is that the computation of S(v) and W(v) is linear in the size of G, so there is no problem computing the branching logic as such.

To implement, after you get the choice vector, you can enumerate the relevant omega vertices, then use computation logic above to radiate away from each omega, updating

HashMap<Object,HashSet<Vertex>> strongMap
HashMap<Object, HashSet <Vertex>> weakMap

Given any edge, relevant GraphicConnection, or vertex x, strongMap.get(x) contains omega for x in S(omega).  Mutatis mutandis for weak map.

The following gets added to the MangoAnnotation to manage the trail state:

enum TrailState {ATTRACTED,REPELLED}
HashMap<Vertex,TrailState> trailState

The trail state is assumed to be open for each omega, unless otherwise indicated. Now just update trailState everytime there is a state change as described above.

Introduce TrailManager object to compute strongMap and weakMap.  The ComponentChoiceGenerator constructor instantiates and initializes the TrailManager.

Modified Paths:
--------------
    branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
    branches/mango/Mango/src/mango/intro/LoginDialog.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.