adding deadlock and reacha info

src/avatartranslator/modelchecker/AvatarModelChecker.java

@@ -87,6 +87,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     private ArrayList<SpecificationReachability> reachabilities;
     private int nbOfRemainingReachabilities;
 
+    // Dealocks
+    private int nbOfDeadlocks;
+
     public AvatarModelChecker(AvatarSpecification _spec) {
         spec = _spec;
         ignoreEmptyTransitions = true;
@@ -177,6 +180,17 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         return nbOfRemainingReachabilities;
     }
 
+    public int getNbOfReachabilities() {
+	if (reachabilities == null) {
+	    return -1;
+	}
+        return reachabilities.size() - nbOfRemainingReachabilities;
+    }
+
+    public int getNbOfDeadlocks() {
+	return nbOfDeadlocks;
+    }
+
     public void setComputeRG(boolean _rg) {
         computeRG = _rg;
     }
@@ -185,6 +199,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     public void startModelChecking() {
         stoppedBeforeEnd = false;
         stateID = 0;
+	nbOfDeadlocks = 0;
 
         // Remove timers, composite states, randoms
         TraceManager.addDev("Reworking Avatar specification");
@@ -454,6 +469,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             }
         }
 
+	if (transitions.size() == 0) {
+	    nbOfDeadlocks ++;
+	}
+
         //TraceManager.addDev("Possible transitions 4:" + transitions.size());
         // For each realizable transition
         //   Make it, reset clock of the involved blocks to 0, increase clockmin/clockhmax of each block

src/ui/window/JDialogAvatarModelChecker.java

@@ -116,7 +116,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
     protected JScrollPane jsp;
 
     // Information
-    protected JLabel nbOfStates, nbOfLinks, nbOfPendingStates, elapsedTime, nbOfStatesPerSecond, info;
+    protected JLabel nbOfStates, nbOfLinks, nbOfPendingStates, elapsedTime, nbOfStatesPerSecond, nbOfDeadlocks, nbOfReachabilities, info;
 
 
     private Thread t;
@@ -270,6 +270,19 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
 	nbOfLinks = new JLabel("-");
 	jpinfo.add(nbOfLinks, c02);
 
+	c02.gridwidth = 1;
+	jpinfo.add(new JLabel("Reachability found:"), c02);
+	//c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+	nbOfReachabilities = new JLabel("-");
+	jpinfo.add(nbOfReachabilities, c02);
+	
+
+	c02.gridwidth = 1;
+	jpinfo.add(new JLabel("Nb of deadlock states:"), c02);
+	c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+	nbOfDeadlocks = new JLabel("-");
+	jpinfo.add(nbOfDeadlocks, c02);
+
 	c02.gridwidth = 1;
 	jpinfo.add(new JLabel("Nb of pending states:"), c02);
 	//c02.gridwidth = GridBagConstraints.REMAINDER; //end row
@@ -516,6 +529,17 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
 		int nbOfStatess = amc.getNbOfStates();
 		nbOfStates.setText(""+nbOfStatess);
 		nbOfLinks.setText(""+amc.getNbOfLinks());
+
+		// Reachability and deadlocks
+		int nb = amc.getNbOfReachabilities();
+		if (nb == -1) {
+		    //nbOfReachabilities.setText("-");
+		} else {
+		    nbOfReachabilities.setText("" + nb);
+		}
+		nbOfDeadlocks.setText(""+amc.getNbOfDeadlocks());
+
+		
 		nbOfPendingStates.setText(""+amc.getNbOfPendingStates());
 		Date d;
 		previousDate = new Date();
@@ -541,6 +565,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
 
 		nbOfStatesPerSecond.setText(""+1000*diff/duration);
 
+		
+
 		updateInfo();
 			//}
 	    }