diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java index 6d2c668cdc8737ba4b5d1d4bd0a2721a0b1aace8..4117d60278662ecff8ae4dfcad3c90c1f817da71 100644 --- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java +++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java @@ -47,8 +47,6 @@ import myutil.TraceManager; import java.util.*; -import org.apache.commons.io.filefilter.FalseFileFilter; - /** * Class AvatarModelChecker @@ -197,10 +195,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { for (AvatarBlock block : spec.getListOfBlocks()) { for (AvatarStateMachineElement elt : block.getStateMachine().getListOfElements()) { //TraceManager.addDev("null elt in state machine of block=" + block.getName()); - if (elt.canBeVerified() && elt.isChecked()) { + //if (elt.canBeVerified() && elt.isChecked()) { + if (elt.isChecked()) { livenessInfo = new SpecificationLiveness(elt, block); states++; - break; + //break; } } } @@ -1265,8 +1264,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { return getNextState(e, _newState, maxNbOfIterations); } - private AvatarStateElement getNextStateNoCheck(AvatarStateMachineElement e, int maxNbOfIterations) { + private AvatarStateMachineElement getNextStateLivenessCheck(AvatarStateMachineElement e, int maxNbOfIterations) { + //Returns an element if there is a liveness checked element else it returns a state e = e.getNext(0); + if (e == livenessInfo.ref1) { + //liveness element found + return e; + } if (e instanceof AvatarStateElement) { return (AvatarStateElement) e; } @@ -1274,7 +1278,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { if (maxNbOfIterations == 0) { return null; } - return getNextStateNoCheck(e, maxNbOfIterations); + return getNextStateLivenessCheck(e, maxNbOfIterations); } // Execute the actions of a transition, and correspondingly impact the variables of the @@ -1468,7 +1472,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { } private boolean checkFalseLivenessFromCurrentState(SpecificationState _ss, ArrayList<SpecificationTransition> transitions) { - AvatarStateElement ase; + AvatarStateMachineElement asme; boolean livenessState = false; int livenessAlternatives = 0; @@ -1476,10 +1480,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { for (int i = 0; i < tr.transitions.length; i++) { if (tr.transitions[i].getBlock() == livenessInfo.ref2) { //transition on same state machine to check - ase = getNextStateNoCheck(tr.transitions[i], 10); - if (ase != null) { + asme = getNextStateLivenessCheck(tr.transitions[i], 10); + if (asme != null) { livenessAlternatives++; - if (livenessInfo.ref1 == ase) { + if (livenessInfo.ref1 == asme) { TraceManager.addDev("Liveness found on a path"); livenessState = true; } @@ -1497,14 +1501,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { } private boolean setLivenessofState(SpecificationState newState, SpecificationTransition tr, boolean livenessStateCuncurrent, boolean precLiveness) { - AvatarStateElement ase; + AvatarStateMachineElement asme; boolean found = false; // Find if newState carries the transition to a liveness check state for (int i = 0; i < tr.transitions.length; i++) { - ase = getNextStateNoCheck(tr.transitions[i], 10); - if (ase != null) { - if (livenessInfo.ref1 == ase) { + asme = getNextStateLivenessCheck(tr.transitions[i], 10); + if (asme != null) { + if (livenessInfo.ref1 == asme) { newState.liveness = livenessStateCuncurrent; found = true; } diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java index 7ef97e16265b087c6808fd2ace3f89d099554e14..0ff5b266d662fa628e4560c2022606488065d5a0 100644 --- a/src/main/java/ui/window/JDialogAvatarModelChecker.java +++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java @@ -601,6 +601,12 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act mgui.resetLiveness(); res = amc.setLivenessofState(); jta.append("Liveness of " + res + " selected elements activated\n"); + + SpecificationLiveness sl = amc.getLivenessResult(); + handleLiveness(sl.ref1, false); +// if (sl.ref2 != sl.ref1) { +// handleLiveness(sl.ref2, sl.result); +// } } // Limitations @@ -677,6 +683,12 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act if (livenessSelected != LIVENESS_NONE) { jta.append("\nLiveness Analysis:\n"); jta.append(amc.getLivenessResult().toString()); + + SpecificationLiveness sl = amc.getLivenessResult(); + handleLiveness(sl.ref1, sl.result); +// if (sl.ref2 != sl.ref1) { +// handleLiveness(sl.ref2, sl.result); +// } } //TraceManager.addDev(amc.toString()); @@ -764,6 +776,23 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act } } } + + protected void handleLiveness(Object _o, boolean _res) { + if (_o instanceof AvatarStateMachineElement) { + Object o = ((AvatarStateMachineElement) _o).getReferenceObject(); + if (o instanceof TGComponent) { + TGComponent tgc = (TGComponent) (o); + //TraceManager.addDev("Reachability of tgc=" + tgc + " value=" + tgc.getValue() + " class=" + tgc.getClass()); + if (_res) { + tgc.setReachability(TGComponent.ACCESSIBILITY_OK); + tgc.setLiveness(TGComponent.ACCESSIBILITY_OK); + } else { + tgc.setLiveness(TGComponent.ACCESSIBILITY_KO); + } + tgc.getTDiagramPanel().repaint(); + } + } + } protected void checkMode() { mode = NOT_STARTED;