diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 4feb36dabd4e2eee529c806d3a8e1a30d3b88b49..1dc764ece04c67ed40050024021fc3e3a3fe6db1 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -300,6 +300,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = safeties.size() > 0;
return safeties.size();
}
+
+ public ArrayList<SafetyProperty> getSafeties() {
+ return safeties;
+ }
public void setComputeRG(boolean _rg) {
computeRG = _rg;
@@ -326,8 +330,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
public boolean startModelCheckingProperties() {
- boolean studyreach;
- int deadlocks = 0;
+ boolean studyS, studyL, studyR;
+ long deadlocks = 0;
if (spec == null) {
return false;
@@ -339,14 +343,19 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
stateLimitRG = false;
timeLimitRG = false;
- studyreach = studyReachability;
+ studyR = studyReachability;
+ studyL = studyLiveness;
+ studyS = studySafety;
//then compute livenesses
- studyReachability = false;
computeRG = false;
propertyDone = false;
+ studySafety = false;
+ studyLiveness = false;
+ studyReachability = false;
- if (studyLiveness) {
+ if (studyL) {
+ studyLiveness = true;
for (SpecificationLiveness sl : livenesses) {
livenessInfo = sl;
startModelChecking();
@@ -354,30 +363,40 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
stoppedConditionReached = false;
deadlocks += nbOfDeadlocks;
}
+ studyLiveness = false;
}
- if (studyreach) {
- //do a run to compute reachabilities
- studyLiveness = false;
+ if (studyS) {
+ studySafety = true;
+ for (SafetyProperty sp : safeties) {
+ safety = sp;
+ startModelChecking();
+ propertyDone = false;
+ stoppedConditionReached = false;
+ deadlocks += nbOfDeadlocks;
+ }
+ studySafety = false;
+ }
+
+ if (studyR) {
studyReachability = true;
- computeRG = true;
+ //computeRG = true;
startModelChecking();
deadlocks += nbOfDeadlocks;
+ studyReachability = false;
}
if (checkNoDeadlocks) {
if (deadlocks == 0) {
- studyLiveness = false;
- studyReachability = false;
- computeRG = false;
deadlockStop = true;
startModelChecking();
} else {
nbOfDeadlocks = 1;
}
}
- studyLiveness = true;
- studyReachability = studyreach;
+ studyLiveness = studyL;
+ studySafety = studyS;
+ studyReachability = studyR;
return true;
}
@@ -451,10 +470,17 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (ignoreEmptyTransitions) {
handleNonEmptyUniqueTransition(initialState);
}
+
if (studyLiveness && initialState.property == true) {
//property on initial states
return;
}
+
+ if (studySafety) {
+ initialState.property = evaluateSafetyProperty(initialState, false);
+ actionOnProperty(initialState, 0, null, null);
+ }
+
prepareTransitionsOfState(initialState);
blockValues = initialState.getBlockValues();
initialState.distance = 0;
@@ -774,12 +800,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//TraceManager.addDev("Possible transitions 4:" + transitions.size());
if (transitions.size() == 0) {
- if (studyLiveness && _ss.property == false) {
- livenessInfo.result = false;
- propertyDone = true;
- //} else {
- // nbOfDeadlocks++;
- }
+ checkPropertyOnDeadlock(_ss);
nbOfDeadlocks++;
propertyDone = deadlockStop; //use this flag to stop the execution
//TraceManager.addDev("Deadlock found");
@@ -860,7 +881,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (!studyLiveness && !studySafety) {
pendingStates.add(newState);
} else {
- actionOnProperty(newState, i, null, _ss);
+ actionOnProperty(newState, i, similar, _ss);
}
//newState.id = getStateID();
//TraceManager.addDev("Creating new state for newState=" + newState);
@@ -913,6 +934,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
setLivenessofState(newState, st, previousState.property);
}
+ if (studySafety) {
+ newState.property = evaluateSafetyProperty(newState, previousState.property);
+ }
+
if (ignoreEmptyTransitions) {
handleNonEmptyUniqueTransition(newState);
}
@@ -930,17 +955,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
link.destinationState = similar;
nbOfLinks++;
_ss.addNext(link);
- if (studyLiveness && newState.property == false) {
- if (similar.property) {
- //found a branch with false liveness
- propertyDone = true;
- livenessInfo.result = false;
- } else if (stateIsReachableFromState(similar, _ss)) {
- //found a loop with false liveness
- propertyDone = true;
- livenessInfo.result = false;
- }
- }
+ actionOnProperty(newState, 0, similar, _ss);
break;
}
@@ -1024,24 +1039,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (similar != null) {
// check if it has been created by another thread in the meanwhile
link.destinationState = similar;
- if (studyLiveness && newState.property == false) {
- if (similar.property) {
- //found a branch with false liveness
- propertyDone = true;
- livenessInfo.result = false;
- } else if (stateIsReachableFromState(similar, _ss)) {
- //found a loop with false liveness
- propertyDone = true;
- livenessInfo.result = false;
- }
- }
+ actionOnProperty(newState, 0, similar, _ss);
} else {
link.destinationState = newState;
newState.distance = _ss.distance + 1;
- if (!studyLiveness) {
+ if (!studyLiveness && !studySafety) {
pendingStates.add(newState);
- } else if (!newState.property) {
- pendingStates.add(0, newState);
+ } else {
+ actionOnProperty(newState, 0, similar, _ss);
}
}
nbOfLinks++;
@@ -1587,10 +1592,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
result = !result;
}
- return result |! precProperty;
+ return result || precProperty;
}
- private boolean actionOnProperty(SpecificationState newState, int i, SpecificationState similar, SpecificationState _ss) {
+ private void actionOnProperty(SpecificationState newState, int i, SpecificationState similar, SpecificationState _ss) {
if (studyLiveness) {
if (similar == null && !newState.property) {
if (i == 0) {
@@ -1600,24 +1605,83 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//Not priority for parallel BFS on the other transitions
pendingStates.add(newState);
}
- } else if (similar != null) {
- if (newState.property == false) {
- if (similar.property) {
- //found a branch with false liveness
+ } else if (similar != null && newState.property == false) {
+ if (similar.property) {
+ //found a branch with false liveness
+ propertyDone = true;
+ livenessInfo.result = false;
+ } else if (stateIsReachableFromState(similar, _ss)) {
+ //found a loop with false liveness
+ propertyDone = true;
+ livenessInfo.result = false;
+ }
+ }
+ } else if (studySafety) {
+ if (safety.safetyType == SafetyProperty.ALLTRACES_ALLSTATES) {
+ if (newState.property) {
+ propertyDone = true;
+ safety.result = false;
+ } else if (similar == null){
+ pendingStates.add(newState);
+ }
+ } else if (safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES) {
+ if (similar == null && !newState.property) {
+ if (i == 0) {
+ //Priority for parallel DFS on the first transition
+ pendingStates.add(0, newState);
+ } else {
+ //Not priority for parallel BFS on the other transitions
+ pendingStates.add(newState);
+ }
+ } else if (similar != null && !newState.property) {
+ if (!similar.property && stateIsReachableFromState(similar, _ss)) {
+ //found a loop with true property
propertyDone = true;
- livenessInfo.result = false;
- } else if (stateIsReachableFromState(similar, _ss)) {
- //found a loop with false liveness
+ safety.result = true;
+ }
+ }
+ } else if (safety.safetyType == SafetyProperty.ALLTRACES_ONESTATE) {
+ if (similar == null && !newState.property) {
+ if (i == 0) {
+ //Priority for parallel DFS on the first transition
+ pendingStates.add(0, newState);
+ } else {
+ //Not priority for parallel BFS on the other transitions
+ pendingStates.add(newState);
+ }
+ } else if (similar != null && newState.property == false) {
+ if (!similar.property && stateIsReachableFromState(similar, _ss)) {
+ //found a loop with false property
propertyDone = true;
- livenessInfo.result = false;
+ safety.result = false;
}
}
+ } else if (safety.safetyType == SafetyProperty.ONETRACE_ONESTATE) {
+ if (newState.property) {
+ propertyDone = true;
+ safety.result = true;
+ } else if (similar == null) {
+ pendingStates.add(newState);
+ }
+ }
+ }
+ }
+
+ private void checkPropertyOnDeadlock(SpecificationState ss) {
+ if (studyLiveness) {
+ if (ss.property == false) {
+ livenessInfo.result = false;
+ propertyDone = true;
}
} else if (studySafety) {
-
+ if (safety.safetyType == SafetyProperty.ALLTRACES_ONESTATE && ss.property == false) {
+ safety.result = false;
+ propertyDone = true;
+ } else if (safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES && ss.property == false) {
+ safety.result = true;
+ propertyDone = true;
+ }
}
-
- return true;
}
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index fe51b1ecfbe6416f27987f64ef0c3b92c865a7a4..cc3235178c3494265b71cf57a45083a5d7383af3 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -91,7 +91,6 @@ public class SafetyProperty {
public SafetyProperty(String property, AvatarSpecification _spec) {
rawProperty = property.trim();
analyzeProperty(_spec);
- result = false;
}
public boolean analyzeProperty(AvatarSpecification _spec) {
@@ -103,14 +102,19 @@ public class SafetyProperty {
if (tmpP.startsWith("A[]")) {
safetyType = ALLTRACES_ALLSTATES;
+ result = true;
} else if (tmpP.startsWith("A<>")) {
safetyType = ALLTRACES_ONESTATE;
+ result = true;
} else if (tmpP.startsWith("E[]")) {
safetyType = ONETRACE_ALLSTATES;
+ result = false;
} else if (tmpP.startsWith("E<>")) {
safetyType = ONETRACE_ONESTATE;
+ result = false;
} else {
errorOnProperty = BAD_SAFETY_TYPE;
+ result = false;
return false;
}
@@ -146,6 +150,8 @@ public class SafetyProperty {
return false;
}
+ p = fieldString + " " + pFields[1] + " " + pFields[2];
+
return (errorOnProperty == NO_ERROR);
}
@@ -162,6 +168,10 @@ public class SafetyProperty {
return p;
}
+ public String getRawProperty() {
+ return rawProperty;
+ }
+
public String toString() {
if (result) {
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 24d2e50e10cad63048b65c4c13f9c4d19586f77e..7427aa3b4f09e42d6819d82bd16202789858aaa1 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -42,6 +42,7 @@ package ui.window;
import avatartranslator.AvatarSpecification;
import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
+import avatartranslator.modelchecker.SafetyProperty;
import avatartranslator.modelchecker.SpecificationLiveness;
import avatartranslator.modelchecker.SpecificationReachability;
import avatartranslator.modelchecker.SpecificationReachabilityType;
@@ -49,6 +50,7 @@ import myutil.*;
import ui.util.IconManager;
import ui.MainGUI;
import ui.TGComponent;
+import ui.TURTLEPanel;
import graph.RG;
import graph.AUTGraph;
@@ -59,7 +61,10 @@ import java.awt.event.ActionListener;
import java.io.File;
import java.text.DateFormat;
import java.text.SimpleDateFormat;
+import java.util.ArrayList;
import java.util.Date;
+import java.util.HashMap;
+import java.util.Map;
import java.util.TimerTask;
import java.util.concurrent.TimeUnit;
@@ -164,7 +169,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// private boolean hasError = false;
private java.util.Timer timer;
//protected boolean startProcess = false;
-
+ protected Map<String, Integer> verifMap;
/*
* Creates new form
@@ -188,6 +193,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
initComponents();
myInitComponents();
pack();
+
+ verifMap = new HashMap<String, Integer>();
/*if ((mgui != null) && (spec != null)) {
mgui.drawAvatarSpecification(spec);
@@ -722,6 +729,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (safetySelected) {
jta.append("\nSafety Analysis:\n");
jta.append(amc.safetyToString());
+ handleSafety(amc.getSafeties());
}
//TraceManager.addDev(amc.toString());
@@ -826,6 +834,19 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
}
+
+ protected void handleSafety(ArrayList<SafetyProperty> safeties) {
+ int status;
+ for (SafetyProperty sp : safeties) {
+ if (sp.result) {
+ status = 1;
+ } else {
+ status = 0;
+ }
+ verifMap.put(sp.getRawProperty(), status);
+ }
+ mgui.modelBacktracingUPPAAL(verifMap);
+ }
protected void checkMode() {
mode = NOT_STARTED;
@@ -869,7 +890,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
switch (mode) {
case NOT_STARTED:
- if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL)|| graphSelected || graphSelectedDot) {
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || safetySelected|| graphSelected || graphSelectedDot) {
start.setEnabled(true);
} else {
start.setEnabled(false);