From ef6420ba976b5af8048885a19af1415437ed375d Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Fri, 24 Apr 2020 16:48:13 +0200
Subject: [PATCH] Added non-computation state of property when not already
computed
---
.../modelchecker/AvatarModelChecker.java | 17 ++++---
.../modelchecker/SafetyProperty.java | 46 +++++++++++++++----
...e.java => SpecificationPropertyPhase.java} | 6 +--
.../SpecificationReachability.java | 12 ++---
.../ui/window/JDialogAvatarModelChecker.java | 37 +++++++++------
5 files changed, 77 insertions(+), 41 deletions(-)
rename src/main/java/avatartranslator/modelchecker/{SpecificationReachabilityType.java => SpecificationPropertyPhase.java} (94%)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 581a38e379..b50c1bba22 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -360,6 +360,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
safety = sp;
startModelChecking(nbOfThreads);
resetModelChecking();
+ safety.setComputed();
deadlocks += nbOfDeadlocks;
}
studySafety = false;
@@ -387,6 +388,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
safetyLeadStates = null;
}
+ safety.setComputed();
resetModelChecking();
deadlocks += nbOfDeadlocks;
}
@@ -542,9 +544,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public void stopModelChecking() {
emptyPendingStates();
stoppedBeforeEnd = true;
- if (studySafety) {
- safety.result = false;
- }
TraceManager.addDev("Model checking stopped");
}
@@ -615,8 +614,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Set to non reachable not computed elements
if ((studyReachability) && (!stoppedBeforeEnd)) {
for (SpecificationReachability re : reachabilities) {
- if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
- re.result = SpecificationReachabilityType.NONREACHABLE;
+ if (re.result == SpecificationPropertyPhase.NOTCOMPUTED) {
+ re.result = SpecificationPropertyPhase.NONSATISFIED;
}
}
}
@@ -665,8 +664,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Set to non reachable not computed elements
if ((studyReachability) && (!stoppedBeforeEnd)) {
for (SpecificationReachability re : reachabilities) {
- if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
- re.result = SpecificationReachabilityType.NONREACHABLE;
+ if (re.result == SpecificationPropertyPhase.NOTCOMPUTED) {
+ re.result = SpecificationPropertyPhase.NONSATISFIED;
}
}
}
@@ -1780,9 +1779,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public void checkElementReachability(AvatarStateMachineElement elt, SpecificationState _ss) {
for (SpecificationReachability re : reachabilities) {
- if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
+ if (re.result == SpecificationPropertyPhase.NOTCOMPUTED) {
if (re.ref1 == elt) {
- re.result = SpecificationReachabilityType.REACHABLE;
+ re.result = SpecificationPropertyPhase.SATISFIED;
re.state = _ss;
nbOfRemainingReachabilities--;
//TraceManager.addDev("Remaining reachabilities:" + nbOfRemainingReachabilities);
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 9f599f5554..12ab8b66c8 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -55,6 +55,7 @@ public class SafetyProperty {
private int errorOnProperty;
private AvatarExpressionSolver safetySolver;
private AvatarExpressionSolver safetySolverLead;
+ private SpecificationPropertyPhase phase;
// Error on property
public static final int NO_ERROR = 0;
@@ -86,6 +87,7 @@ public class SafetyProperty {
public SafetyProperty(String property, AvatarSpecification _spec) {
rawProperty = property.trim();
analyzeProperty(_spec);
+ phase = SpecificationPropertyPhase.NOTCOMPUTED;
}
public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state, int _safetyType) {
@@ -98,6 +100,7 @@ public class SafetyProperty {
propertyType = BLOCK_STATE;
safetyType = _safetyType;
result = true;
+ phase = SpecificationPropertyPhase.NOTCOMPUTED;
}
public boolean analyzeProperty(AvatarSpecification _spec) {
@@ -179,6 +182,10 @@ public class SafetyProperty {
public boolean getSolverLeadResult(SpecificationState _ss, AvatarStateMachineElement _asme) {
return safetySolverLead.getResult(_ss, _asme) != 0;
}
+
+ public SpecificationPropertyPhase getPhase() {
+ return phase;
+ }
public void setBlock(AvatarBlock block) {
@@ -190,23 +197,46 @@ public class SafetyProperty {
this.state = ase;
}
-
- public String toString() {
+ public void setComputed() {
if (result) {
- return rawProperty + " -> property is satisfied";
+ phase = SpecificationPropertyPhase.SATISFIED;
} else {
- return rawProperty + " -> property is NOT satisfied";
+ phase = SpecificationPropertyPhase.NONSATISFIED;
}
}
+ public String toString() {
+ String ret = "";
+ switch(phase) {
+ case NOTCOMPUTED:
+ ret = rawProperty + " -> property not computed";
+ break;
+ case SATISFIED:
+ ret = rawProperty + " -> property is satisfied";
+ break;
+ case NONSATISFIED:
+ ret = rawProperty + " -> property is NOT satisfied";
+ break;
+ }
+ return ret;
+ }
+
+
public String toLivenessString() {
String name = "Element " + state.getExtendedName() + " of block " + block.getName();
- if (result) {
- return name + " -> liveness is satisfied";
- } else {
- return name + " -> liveness is NOT satisfied";
+ switch(phase) {
+ case NOTCOMPUTED:
+ name += rawProperty + " -> liveness not computed";
+ break;
+ case SATISFIED:
+ name += rawProperty + " -> liveness is satisfied";
+ break;
+ case NONSATISFIED:
+ name += rawProperty + " -> liveness is NOT satisfied";
+ break;
}
+ return name;
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationReachabilityType.java b/src/main/java/avatartranslator/modelchecker/SpecificationPropertyPhase.java
similarity index 94%
rename from src/main/java/avatartranslator/modelchecker/SpecificationReachabilityType.java
rename to src/main/java/avatartranslator/modelchecker/SpecificationPropertyPhase.java
index 9f060efe8b..0c44918b91 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationReachabilityType.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationPropertyPhase.java
@@ -43,12 +43,12 @@
package avatartranslator.modelchecker;
/**
- * Class SpecificationReachabilityType
+ * Class SpecificationPropertyPhase
* Reachability types
* Creation: 07/06/2016
* @version 1.0 07/06/2016
* @author Ludovic APVRILLE
*/
-public enum SpecificationReachabilityType {
- NOTCOMPUTED, REACHABLE, NONREACHABLE
+public enum SpecificationPropertyPhase {
+ NOTCOMPUTED, SATISFIED, NONSATISFIED
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
index c10ed9a43c..c075ce10f9 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
@@ -54,13 +54,13 @@ import avatartranslator.AvatarStateMachineElement;
*/
public class SpecificationReachability {
public Object ref1, ref2; // ref1 must be provided, ref2 might be null
- public SpecificationReachabilityType result;
+ public SpecificationPropertyPhase result;
public SpecificationState state;
public SpecificationReachability(Object _ref1, Object _ref2) {
ref1 = _ref1;
ref2 = _ref2;
- result = SpecificationReachabilityType.NOTCOMPUTED;
+ result = SpecificationPropertyPhase.NOTCOMPUTED;
state = null;
}
@@ -81,11 +81,11 @@ public class SpecificationReachability {
}
- if (result == SpecificationReachabilityType.NOTCOMPUTED) {
+ if (result == SpecificationPropertyPhase.NOTCOMPUTED) {
return name + " -> not computed";
}
- if (result == SpecificationReachabilityType.REACHABLE) {
+ if (result == SpecificationPropertyPhase.SATISFIED) {
return name + " -> reachable in RG state " + state.id;
}
@@ -110,11 +110,11 @@ public class SpecificationReachability {
}
- if (result == SpecificationReachabilityType.NOTCOMPUTED) {
+ if (result == SpecificationPropertyPhase.NOTCOMPUTED) {
return name + " -> not computed";
}
- if (result == SpecificationReachabilityType.REACHABLE) {
+ if (result == SpecificationPropertyPhase.SATISFIED) {
return name + " -> reachable";
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 5f4907a802..16d08bf9c5 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -45,7 +45,7 @@ import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.SafetyProperty;
import avatartranslator.modelchecker.SpecificationLiveness;
import avatartranslator.modelchecker.SpecificationReachability;
-import avatartranslator.modelchecker.SpecificationReachabilityType;
+import avatartranslator.modelchecker.SpecificationPropertyPhase;
import myutil.*;
import ui.util.IconManager;
import ui.MainGUI;
@@ -621,7 +621,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jta.append("Liveness of " + res + " states activated\n");
for (SafetyProperty sp : amc.getLivenesses()) {
- handleLiveness(sp.state, false);
+ handleLiveness(sp.state, sp.getPhase());
}
}
@@ -631,12 +631,15 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jta.append("Liveness of " + res + " selected elements activated\n");
for (SafetyProperty sp : amc.getLivenesses()) {
- handleLiveness(sp.state, false);
+ handleLiveness(sp.state, sp.getPhase());
}
}
if (safetySelected) {
res = amc.setSafetyAnalysis();
+ jta.append("Analysis of " + res + " safety pragmas activated\n");
+
+ handleSafety(amc.getSafeties());
}
// Limitations
@@ -718,7 +721,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jta.append(amc.livenessToString());
for (SafetyProperty sp : amc.getLivenesses()) {
- handleLiveness(sp.state, sp.result);
+ handleLiveness(sp.state, sp.getPhase());
}
}
@@ -792,7 +795,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
//
}
- protected void handleReachability(Object _o, SpecificationReachabilityType _res) {
+ protected void handleReachability(Object _o, SpecificationPropertyPhase _res) {
if (_o instanceof AvatarStateMachineElement) {
Object o = ((AvatarStateMachineElement) _o).getReferenceObject();
if (o instanceof TGComponent) {
@@ -801,12 +804,11 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
switch (_res) {
case NOTCOMPUTED:
tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
- tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
break;
- case REACHABLE:
+ case SATISFIED:
tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
break;
- case NONREACHABLE:
+ case NONSATISFIED:
tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
break;
@@ -816,17 +818,22 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
- protected void handleLiveness(Object _o, boolean _res) {
+ protected void handleLiveness(Object _o, SpecificationPropertyPhase _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);
+ switch (_res) {
+ case NOTCOMPUTED:
+ tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
+ case SATISFIED:
+ tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
+ tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
+ break;
+ case NONSATISFIED:
+ tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
+ break;
}
tgc.getTDiagramPanel().repaint();
}
@@ -836,7 +843,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected void handleSafety(ArrayList<SafetyProperty> safeties) {
int status;
for (SafetyProperty sp : safeties) {
- if (sp.result) {
+ if (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) {
status = 1;
} else {
status = 0;
--
GitLab