Bug on invariants partially resolved

src/myutil/IntMatrix.java

@@ -285,8 +285,8 @@ public class IntMatrix {
    }
    
    
-   
-   public void Farkas() {
+   // noMultiplier indicates whether names of lines may contain the "*" sign, or not.
+   public void Farkas(boolean noMultiplier) {
    	   int sizeColumBeforeConcat = sizeColumn;
    	   IntMatrix idMat = new IntMatrix(sizeRow, sizeRow);
    	   idMat.makeID();
@@ -297,6 +297,7 @@ public class IntMatrix {
    	   int l, i;
    	   String s0, s1;
    	   String nameOfNewLine;
+   	   int cpt;
    	   
    	   for(int j=0; j<sizeColumBeforeConcat; j++) {
    	   	   // Loop on lines to add line combinations
@@ -314,14 +315,28 @@ public class IntMatrix {
    	   	   	   	   	   if (Math.abs(lined2[j]) == 1) {
    	   	   	   	   	   	   s0 =  nameOfRows[i] + " + ";
    	   	   	   	   	   } else {
-   	   	   	   	   	   	   s0 = "" + Math.abs(lined2[j]) + "*("  + nameOfRows[i] + ") + ";
+   	   	   	   	   	   	   if (noMultiplier) {
+   	   	   	   	   	   	   	   s0 = nameOfRows[i] + " + ";
+   	   	   	   	   	   	   	   for(cpt=Math.abs(lined2[j]); cpt>1; cpt--) {
+   	   	   	   	   	   	   	   	   s0 += nameOfRows[i] + " + " ;
+   	   	   	   	   	   	   	   }
+   	   	   	   	   	   	   } else {
+   	   	   	   	   	   	   	   s0 = "" + Math.abs(lined2[j]) + "*("  + nameOfRows[i] + ") + ";
+   	   	   	   	   	   	   }
    	   	   	   	   	   }
    	   	   	   	   	   
-   	   	   	   	   	   if (Math.abs(lined2[j]) == 1) {
-   	   	   	   	   	   	   s1 =  nameOfRows[k];
+   	   	   	   	   	   if (Math.abs(lined1[j]) == 1) {
+   	   	   	   	   	   	    s1 =  nameOfRows[k];
    	   	   	   	   	   } else {
-   	   	   	   	   	   	   s1 = "" + Math.abs(lined1[j]) + "*(" + nameOfRows[k] + ")";
-   	   	   	   	   	   }
+   	   	   	   	   	   	   if (noMultiplier) {
+   	   	   	   	   	   	   	    s1 =  nameOfRows[k];
+   	   	   	   	   	   	   	   for(cpt=Math.abs(lined1[j]); cpt>1; cpt--) {
+   	   	   	   	   	   	   	   	   s1 += " +" + nameOfRows[k];
+   	   	   	   	   	   	   	   }
+   	   	   	   	   	   	   } else {
+   	   	   	   	   	   	   	   s1 = "" + Math.abs(lined1[j]) + "*("  + nameOfRows[k] + ") + ";
+   	   	   	   	   	   	   }
+   	   	   	   	   	   } 
    	   	   	   	   	   
    	   	   	   	   	   nameOfNewLine = s0 + s1;
    	   	   	   	   	   gcd = MyMath.gcd(lined);
@@ -343,7 +358,7 @@ public class IntMatrix {
    	   	   for(i=0;i<sizeRow; i++) {
    	   	   	   if (matrice[i][j] != 0) {
    	   	   	   	   removeLine(i);
-   	   	   	   	   System.out.println("matafterremove " + i + "=\n" + toString() + "\n\n");
+   	   	   	   	   //System.out.println("matafterremove " + i + "=\n" + toString() + "\n\n");
    	   	   	   	   i--;
    	   	   	   }
    	   	   }

src/ui/Invariant.java

@@ -73,12 +73,16 @@ public class Invariant implements GenericTree {
 	}
 	
 	public void addComponent(TGComponent _tgc) {
+		if (_tgc == null) {
+			TraceManager.addDev("NULL Component added to invariant -> IGNORING");
+			return;
+		}
 		components.add(_tgc);
 	}
 	
     
 	public String toString() {
-        return name;
+        return "(" + value + ") " + name;
     }
     
     public int getChildCount() {

src/ui/avatarcd/AvatarCDBlock.java

@@ -186,7 +186,7 @@ public class AvatarCDBlock extends TGCScalableWithInternalComponent implements S
 		Color avat = ColorManager.AVATAR_BLOCK;
 		int h;
 		h = 2* (currentFontSize + (int)(textY1 * tdp.getZoom())) + 2;
-		g.setColor(new Color(avat.getRed(), avat.getGreen(), avat.getBlue() + (getMyDepth() * 10)));
+		g.setColor(new Color(avat.getRed(), avat.getGreen(), Math.min(255, avat.getBlue() + (getMyDepth() * 10))));
 		g.fill3DRect(x+1, y+1, width-1, Math.min(h, height)-1, true);
 		g.setColor(c);
         
@@ -219,7 +219,7 @@ public class AvatarCDBlock extends TGCScalableWithInternalComponent implements S
 		h = h +2;
 		if (h < height) {
 			//g.drawLine(x, y+h, x+width, y+h);
-			g.setColor(new Color(avat.getRed(), avat.getGreen(), avat.getBlue() + (getMyDepth() * 10)));
+			g.setColor(new Color(avat.getRed(), avat.getGreen(), Math.min(255, avat.getBlue() + (getMyDepth() * 10))));
 			g.fill3DRect(x+1, y+h, width-1, height-1-h, true);
 			g.setColor(c);
 		}

src/ui/tree/InvariantDataTree.java

@@ -76,7 +76,7 @@ public class InvariantDataTree implements GenericTree {
     public Object getChild(int index) {
     	LinkedList<Invariant> invs = mgui.getInvariants();
     	if (invs.size() == 0) {
-    		return "Not yet performed";
+    		return "No invariant";
     	}
     	return mgui.getInvariants().get(index);
     }

src/ui/window/JDialogInvariantAnalysis.java

@@ -253,8 +253,8 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
              testGo();
              
              jta.append("Computing invariants\n");
-            im.Farkas();
-            jtainvariants.append("Invariants:\n" + im.namesOfRowToString() + "\n\n");
+            im.Farkas(true);
+            //jtainvariants.append("All invariants:\n" + im.namesOfRowToString() + "\n\n");
             
             mgui.gtm.clearInvariants();
             
@@ -274,6 +274,8 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
             AvatarBlock prevBlock;
             int ignored = 0;
             
+            jtainvariants.append("Computed invariants:\n-----------------\n");
+            
             for(int i=0; i<im.getNbOfLines(); i++) {
             	name =  im.getNameOfLine(i);
             	prevBlock = null;
@@ -287,7 +289,7 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
             	state = 0;
             	for(int j=0; j<elts.length; j++) {
             		tmp = elts[j].trim();
-            		TraceManager.addDev("#" + j + "=" + elts[j]);
+            		//TraceManager.addDev("#" + j + "=" + elts[j]);
             		tmp = Conversion.replaceAllString(tmp, "__", "&");
             		tmps = tmp.split("&");
             		if (tmps.length > 2) {
@@ -303,14 +305,14 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
             			try {
             					myid = Integer.decode(tmps[2]).intValue();
             					o = ab.getStateMachine().getReferenceObjectFromID(myid);
-            					TraceManager.addDev("Adding component to inv   block=" + ab.getName() + " id=" + myid + " object=" + o);
+            					//TraceManager.addDev("Adding component to inv   block=" + ab.getName() + " id=" + myid + " object=" + o);
             					inv.addComponent((TGComponent)o);
-            					TraceManager.addDev("Component added:" + o);
+            					//TraceManager.addDev("Component added:" + o);
             					if (o instanceof AvatarSMDStartState) {
             						valToken ++;
             					}
             				} catch (Exception e) {
-            					TraceManager.addDev("Exception invariants:" + e.getMessage());
+            					TraceManager.addDev("Exception invariants:" + e.getMessage() + "tmps[2]=" + tmps[2] + "inv=" + name);
             				}
             		}
             	}
@@ -318,8 +320,10 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
             	
             	if (!(ignoreInvariants.isSelected() && sameBlock)) {
             		mgui.gtm.addInvariant(inv);
+            		jtainvariants.append(inv + "\n");
             	} else {
-            		TraceManager.addDev("Invariant ignored " + inv);
+            		//TraceManager.addDev("Invariant ignored " + inv);
+            		jtainvariants.append("Ignored invariant: " + inv + "\n");
             		ignored ++;
             	}