public class ProofNode
    {
        EntityExpression  roleExp;    // What EntityExpression this node is about
        SolutionManager forwardMgr = new SolutionManager(); 
        SolutionManager backwardMgr = new SolutionManager();

        ProofNode (EntityExpression re) {
            debugInfo("A new node is created for " + re);
            roleExp = re;
            forwardMgr.solutionAdded(this, roleExp);
            backwardMgr.solutionAdded(this, roleExp);
        }

        // The method that does the work when we visit a node
        void forwardProcess() {
            // first go over all credentials that have this as subject
            Iterator  credIt = findCredentialsBySubject(roleExp);
            while (credIt.hasNext()) { 
                StaticCredential credential = (StaticCredential) credIt.next();
                ProofNode node = addForwardNode(credential.getDefinedRole());
                addProofEdge(this, node, credential);
            }
        }

        void backwardProcess() {
        }

        /**
         * Class SolutionManager implements listener management and solution 
         * management.
         */
       class SolutionManager implements SolutionListener
       {
            private HashMap    solutions = new HashMap();
            private LinkedList listeners = new LinkedList();

            public void solutionAdded(ProofNode s, ProofSolution r) {
                debugInfo("Solution added: " + roleExp + "; " + s.roleExp + "; " + r);
                if (! solutions.containsKey(r)) {   // when solution r is new
                    solutions.put(r, new SmallSet(s));  // add solution together with source
                    Object[] lisArray = listeners.toArray();    // inform all listeners
                    for (int i=0; i<lisArray.length; i++) {
                        ((SolutionListener)lisArray[i]).solutionAdded(ProofNode.this, r);
                    }
                } else if (trackAll) {
                    ((SmallSet)solutions.get(r)).add(s);
                }
            }

            void addListener(SolutionListener sl) {
                listeners.add(sl);
                // inform the listener of existing solutions
                Object[] sols = solutions.keySet().toArray();  
                for (int i=0; i<sols.length; i++) {
                     sl.solutionAdded(ProofNode.this, (EntityExpression)(sols[i]));
                }
            }

            Set getSolutions()     {  return solutions.keySet();     }
        } // End of class SolutionManager
    } // End of class ProofNode