AUTGraph.java

	Map<Integer, AUTBlock> allBlocks = Collections.synchronizedMap(new HashMap<Integer, AUTBlock>());
	
	// Create the first block that contains all states
	AUTBlock b0 = new AUTBlock();
	for(AUTState st: states) {
	    b0.addState(st);
	}
	b0.computeHash();
	allBlocks.put(new Integer(b0.hashValue), b0);

	
	AUTBlock b0Test = new AUTBlock();
	for(AUTState st: states) {
	    b0Test.addState(st);
	}
	b0Test.computeHash();

	AUTBlock B0Ret = allBlocks.get(new Integer(b0Test.hashValue));
	if (B0Ret == null) {
	    TraceManager.addDev("ERROR: hash not working for blocks");
	} else {
	    TraceManager.addDev("Hash working for blocks");
	}
	
	

	// Create the first partition containing only block B0
	AUTPartition partition = new AUTPartition();
	partition.addBlock(b0);

	// Create the splitter that contains partitions
	
	AUTPartition partitionForSplitter = new AUTPartition();
	partitionForSplitter.addBlock(b0);
	AUTSplitter w = new AUTSplitter();
	w.addPartition(partitionForSplitter);

	printConfiguration(partition, w);

	int maxIte = 1000;

	AUTPartition currentP;
	while((w.size()>0) && (maxIte >0)) {
	    maxIte --;
	    currentP = w.partitions.get(0);
	    w.partitions.remove(0);

	    // Simple splitter?
	    if (currentP.blocks.size() == 1) {
		TraceManager.addDev("Simple splitter = " + currentP);
		AUTBlock currentBlock = currentP.blocks.get(0);
		//List<AUTElement> sortedAlphabet = new ArrayList<AUTElement>(alphabet.values());
		//Collections.sort(sortedAlphabet);
		for(AUTElement elt: sortedAlphabet) {
		    TraceManager.addDev("\n*** Considering alphabet element = " + elt.value); 
		    printConfiguration(partition, w);
		    // Look for states of the leading to another state by a = T
		    // Construct I = all blocks of P that have at least an element in T
		    AUTBlock T_minus1_elt_B = currentBlock.getMinus1(elt, states);

		    TraceManager.addDev("T_minus1_elt_B=" + T_minus1_elt_B);
		    
		    LinkedList<AUTBlock> I = partition.getI(elt, T_minus1_elt_B);
		    printI(I);
		    for(AUTBlock blockX: I) {
			AUTBlock blockX1 = blockX.getStateIntersectWith(T_minus1_elt_B);
			blockX1.computeHash();
			AUTBlock blockX2 = blockX.getStateDifferenceWith(T_minus1_elt_B);
			blockX2.computeHash();
			TraceManager.addDev("X1=" + blockX1);
			TraceManager.addDev("X2=" + blockX2);

			if (blockX1.isEmpty() || blockX2.isEmpty()) {
			    TraceManager.addDev("Nothing to do");
			    // Nothing to do!
			} else {
			    boolean b = partition.removeBlock(blockX);
			    if (!b) {
				TraceManager.addDev("Block " + blockX + " could not be removed from partition");
			    }
			    partition.addBlock(blockX1);
			    partition.addBlock(blockX2);
			    AUTPartition X_X1_X2 = new AUTPartition();
			    X_X1_X2.addBlock(blockX);
			    X_X1_X2.addBlock(blockX1);
			    X_X1_X2.addBlock(blockX2);
			    w.addPartition( X_X1_X2);
			    TraceManager.addDev("Modifying P and W:");
			    printConfiguration(partition, w);
			    TraceManager.addDev("-----------------\n");
			}
			
		    }
<<<<<<< Upstream, based on aa363fe017f226394c627b60189e75002e6b1199
=======
		    TraceManager.addDev("-----------------\n");
>>>>>>> d0df681 Update on algo management
		    
		}
		
	    }
	    
	    // Compound splitter
	    else if (currentP.blocks.size() == 3){
		TraceManager.addDev("Complexe splitter (b, bi, bii) =" + currentP);
		AUTBlock b = currentP.blocks.get(0);
		AUTBlock bi = currentP.blocks.get(1);
		AUTBlock bii = currentP.blocks.get(2);

		if (bi.size() > bii.size()) {
		    bi = currentP.blocks.get(2);
		    bii = currentP.blocks.get(1);
		}

		TraceManager.addDev("B= " + b +  " bi=" + bi + " bii=" + bii);

		for(AUTElement elt: sortedAlphabet) {
		    TraceManager.addDev("\n*** Considering alphabet element = " + elt.value);
		    printConfiguration(partition, w);
		    AUTBlock T_minus1_elt_B = b.getMinus1(elt, states);
		    TraceManager.addDev("T_minus1_elt_B=" + T_minus1_elt_B);
		    LinkedList<AUTBlock> I = partition.getI(elt, T_minus1_elt_B);
		    printI(I);
		    for(AUTBlock blockX: I) {
			// Compute block X1 = set of states in blockX that goes to Bi, but not to Bii
			// with current action
			AUTBlock blockX1 = new AUTBlock();
			
			// Compute block X2 = set of states in blockX that goes to Bii, but not to Bi
			// with current action
			AUTBlock blockX2 = new AUTBlock();

			// Compute block X3 = set of states in blockX that goes to both Bi and Bii
			// with current action
			boolean b1, b2;
			AUTBlock blockX3 = new AUTBlock();
			for(AUTState st: blockX.states) {
			    b1 = blockX.leadsTo(bi, elt);
			    b2 = blockX.leadsTo(bii, elt);
			    if (b1 && !b2) {
				blockX1.addState(st);
			    } else if (!b1 && b2) {
				blockX2.addState(st);
			    } else {
				blockX3.addState(st);
			    }
			}
			TraceManager.addDev("Block1,2,3 computed\n\tX1 = " + blockX1 + "\n\tX2 = " + blockX2 + "\n\tX3 = " + blockX3); 
			
		    }
		    
		}

	    }
	}
	    
 
	
       
	
	
    }

    private void printConfiguration(AUTPartition _part, AUTSplitter _w) {
	TraceManager.addDev("P={" + _part.toString() + "}");
	TraceManager.addDev("W={" + _w.toString() + "}");
    }

    private void printI(LinkedList<AUTBlock> I) {
	StringBuffer sb = new StringBuffer("I:");
	for(AUTBlock b: I) {
	    sb.append(" " + b);
	}
	TraceManager.addDev(sb.toString());
	
    }
    



}