diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java index 8c4efb953d105ee93efdc4ef17a8cdb3cb1b6064..81ae1e14ebabc11c6559d0358ff46302efdca171 100644 --- a/src/avatartranslator/modelchecker/AvatarModelChecker.java +++ b/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 diff --git a/src/ui/window/JDialogAvatarModelChecker.java b/src/ui/window/JDialogAvatarModelChecker.java index 9712ad131bd5d42803512829957aceec13705fce..fa10d4640d58ec6c9c155672b278f9dabd848e53 100644 --- a/src/ui/window/JDialogAvatarModelChecker.java +++ b/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(); //} }