diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index a3b9ea5c6c8ee581f5a4959002d1fe6c5d91bb3c..9b354cd733e1dfc51ab327548ce89e3a1abfdd0d 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -54,7 +54,7 @@ import java.util.concurrent.ThreadLocalRandom;
* Avatar Model Checker
* Creation: 31/05/2016
*
- * @author Ludovic APVRILLE
+ * @author Ludovic APVRILLE, Alessandro TEMPIA CALVINO
* @version 1.0 31/05/2016
*/
public class AvatarModelChecker implements Runnable, myutil.Graph {
@@ -93,6 +93,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private int nbOfRemainingReachabilities;
// Dealocks
+ private boolean checkNoDeadlocks;
+ private boolean deadlockStop;
private int nbOfDeadlocks;
// Liveness
@@ -101,6 +103,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private ArrayList<SpecificationLiveness> livenesses;
private SpecificationLiveness livenessInfo;
+ // Safety
+ private boolean studySafety;
+ private ArrayList<SafetyProperty> safeties;
+ private SafetyProperty safety;
+
//RG limits
private boolean stateLimitRG;
private boolean timeLimitRG;
@@ -123,6 +130,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = true;
ignoreConcurrenceBetweenInternalActions = true;
ignoreInternalStates = true;
+ checkNoDeadlocks = false;
+ deadlockStop = false;
studyReachability = false;
computeRG = false;
stateLimitRG = false; //No state limit in RG computation
@@ -190,6 +199,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
TraceManager.addDev("ignore niternal state?" + ignoreInternalStates);
ignoreInternalStates = _b;
}
+
+ public void setCheckNoDeadlocks(boolean _checkNoDeadlocks) {
+ checkNoDeadlocks = _checkNoDeadlocks;
+ deadlockStop = false;
+ }
public int setLivenessOfSelected() {
livenesses = new ArrayList<SpecificationLiveness>();
@@ -274,6 +288,18 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public int getNbOfDeadlocks() {
return nbOfDeadlocks;
}
+
+ public int setSafetyAnalysis() {
+ safeties = new ArrayList<SafetyProperty>();
+ for (String property : spec.getSafetyPragmas()) {
+ SafetyProperty sp = new SafetyProperty(property, spec);
+ if (!sp.hasError()) {
+ safeties.add(sp);
+ }
+ }
+ studySafety = safeties.size() > 0;
+ return safeties.size();
+ }
public void setComputeRG(boolean _rg) {
computeRG = _rg;
@@ -299,14 +325,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
- public boolean startModelCheckingLiveness() {
+ public boolean startModelCheckingProperties() {
boolean studyreach;
+ int deadlocks = 0;
if (spec == null) {
return false;
}
- if (livenesses == null) {
+ if ((studyLiveness && livenesses == null) || (studySafety && safeties == null)) {
return false;
}
@@ -315,16 +342,18 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyreach = studyReachability;
//then compute livenesses
- studyLiveness = true;
studyReachability = false;
computeRG = false;
livenessDone = false;
- for (SpecificationLiveness sl : livenesses) {
- livenessInfo = sl;
- startModelChecking();
- livenessDone = false;
- stoppedConditionReached = false;
+ if (studyLiveness) {
+ for (SpecificationLiveness sl : livenesses) {
+ livenessInfo = sl;
+ startModelChecking();
+ livenessDone = false;
+ stoppedConditionReached = false;
+ deadlocks += nbOfDeadlocks;
+ }
}
if (studyreach) {
@@ -333,8 +362,22 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyReachability = true;
computeRG = true;
startModelChecking();
+ deadlocks += nbOfDeadlocks;
+ }
+
+ if (checkNoDeadlocks) {
+ if (deadlocks == 0) {
+ studyLiveness = false;
+ studyReachability = false;
+ computeRG = false;
+ deadlockStop = true;
+ startModelChecking();
+ } else {
+ nbOfDeadlocks = 1;
+ }
}
studyLiveness = true;
+ studyReachability = studyreach;
return true;
}
@@ -738,6 +781,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// nbOfDeadlocks++;
}
nbOfDeadlocks++;
+ livenessDone = deadlockStop; //use this flag to stop the execution
//TraceManager.addDev("Deadlock found");
}
@@ -921,6 +965,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
+ livenessDone = deadlockStop; //use this flag to stop the execution
mustStop();
return;
}
@@ -1698,7 +1743,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public String reachabilityToStringGeneric() {
if (!studyReachability) {
- return "Reachability not activated";
+ return "Reachability not activated\n";
}
@@ -1717,13 +1762,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public String livenessToString() {
if (!studyLiveness) {
- return "Liveness not activated";
+ return "Liveness not activated\n";
}
StringBuilder ret = new StringBuilder();
if (stoppedBeforeEnd) {
- ret.append("Beware: Full study of reachability might not have been fully completed\n");
+ ret.append("Beware: Full study of liveness might not have been fully completed\n");
}
int cpt = 0;
@@ -1733,6 +1778,38 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
return ret.toString();
}
+
+ public String deadlockToString() {
+ if (!checkNoDeadlocks) {
+ return "Deadlock check not activeted\n";
+ }
+
+ String ret;
+ if (nbOfDeadlocks > 0) {
+ ret = "property is not satisfied\n";
+ } else {
+ ret = "property is satisfied\n";
+ }
+
+ return ret;
+ }
+
+ public String safetyToString() {
+ if (!studySafety) {
+ return "Safety check is not activated\n";
+ }
+
+
+ StringBuilder ret = new StringBuilder();
+ if (stoppedBeforeEnd) {
+ ret.append("Beware: Full study of safety might not have been fully completed\n");
+ }
+
+ for (SafetyProperty sp : safeties) {
+ ret.append(sp.toString() + "\n");
+ }
+ return ret.toString();
+ }
// Do not free the RG
public void freeUselessAllocations() {
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 921aa4e2ed8942fd43c0c6e1394551af5a93556e..a19407daf2332652a2d2342a958e98113618ce0a 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -42,12 +42,14 @@
package avatartranslator.modelchecker;
+import java.time.Clock;
+
import avatartranslator.*;
/**
* Class SafetyProperty
- * Coding of a ssafety property
+ * Coding of a safety property
* Creation: 22/11/2017
* @version 1.0 22/11/2017
* @author Ludovic APVRILLE
@@ -74,8 +76,12 @@ public class SafetyProperty {
private int safetyType;
private int propertyType;
private String p;
+ public boolean result;
private boolean isBlockStateProperty;
+ private AvatarBlock block;
+ private AvatarAttribute attribute;
+
private int blockIndex;
private int stateIndex;
@@ -83,55 +89,85 @@ public class SafetyProperty {
public SafetyProperty(String property, AvatarSpecification _spec) {
- rawProperty = property.trim();
- analyzeProperty(_spec);
+ rawProperty = property.trim();
+ analyzeProperty(_spec);
+ result = false;
}
public boolean analyzeProperty(AvatarSpecification _spec) {
- String tmpP = rawProperty;
-
- errorOnProperty = NO_ERROR;
-
- if (tmpP.startsWith("A[]")) {
- safetyType = ALLTRACES_ALLSTATES;
- } else if (tmpP.startsWith("A<>")) {
- safetyType = ALLTRACES_ONESTATE;
- } else if (tmpP.startsWith("E[]")) {
- safetyType = ONETRACE_ALLSTATES;
- } else if (tmpP.startsWith("E<>")) {
- safetyType = ONETRACE_ONESTATE;
- } else {
- errorOnProperty = BAD_SAFETY_TYPE;
- return false;
- }
-
- p = tmpP.substring(3, tmpP.length()).trim();
-
- if (p.length() == 0) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
- }
-
- return (errorOnProperty == NO_ERROR);
+ String tmpP = rawProperty;
+ String[] pFields;
+ String blockString, fieldString;
+
+ errorOnProperty = NO_ERROR;
+
+ if (tmpP.startsWith("A[]")) {
+ safetyType = ALLTRACES_ALLSTATES;
+ } else if (tmpP.startsWith("A<>")) {
+ safetyType = ALLTRACES_ONESTATE;
+ } else if (tmpP.startsWith("E[]")) {
+ safetyType = ONETRACE_ALLSTATES;
+ } else if (tmpP.startsWith("E<>")) {
+ safetyType = ONETRACE_ONESTATE;
+ } else {
+ errorOnProperty = BAD_SAFETY_TYPE;
+ return false;
+ }
+
+ p = tmpP.substring(3, tmpP.length()).trim();
+
+ if (p.length() == 0) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ pFields = p.split(" "); //[0] item, [1] operator, [3] value
+
+ if (pFields.length != 3 || pFields[0].split("\\.").length != 2) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ blockString = pFields[0].split("\\.")[0];
+ fieldString = pFields[0].split("\\.")[1];
+
+ block = _spec.getBlockWithName(blockString);
+
+ if (block == null) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ attribute = block.getAvatarAttributeWithName(fieldString);
+
+ if (attribute == null) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ return (errorOnProperty == NO_ERROR);
}
public boolean hasError() {
- return errorOnProperty != NO_ERROR;
+ return errorOnProperty != NO_ERROR;
}
public void setErrorOnP() {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
}
public String getP() {
- return p;
+ return p;
}
public String toString() {
- return "prop: " + rawProperty;
+ if (result) {
+ return rawProperty + " -> property is satisfied";
+ } else {
+ return rawProperty + " -> property is NOT satisfied";
+ }
}
-
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index c93d6e5bba05a836d0357fffaae764d3e2c4f9b0..b04a2f2a85d0909fb1a678c1b5db317696070650 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -678,7 +678,7 @@ public class Action extends Command {
}
TraceManager.addDev("Starting model checking");
if (livenessAnalysis) {
- amc.startModelCheckingLiveness();
+ amc.startModelCheckingProperties();
} else {
amc.startModelChecking();
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 1fd8dec95e41fd581b9a1e8a65a49ea2a3d76628..24d2e50e10cad63048b65c4c13f9c4d19586f77e 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -95,6 +95,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean generateDesignSelected = false;
protected static int reachabilitySelected = REACHABILITY_NONE;
protected static int livenessSelected = LIVENESS_NONE;
+ protected static boolean safetySelected = false;
+ protected static boolean checkNoDeadSelected = false;
protected static boolean limitStatesSelected = false;
protected static String stateLimitValue;
protected static boolean limitTimeSelected = false;
@@ -144,6 +146,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JTextField stateLimitField;
protected JCheckBox timeLimit;
protected JTextField timeLimitField;
+ protected JCheckBox noDeadlocks;
+ protected JCheckBox safety;
protected JCheckBox saveGraphAUT, saveGraphDot, ignoreEmptyTransitions, ignoreInternalStates,
ignoreConcurrenceBetweenInternalActions, generateDesign;
@@ -238,6 +242,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
ignoreInternalStatesSelected);
ignoreInternalStates.addActionListener(this);
jp01.add(ignoreInternalStates, c01);
+
+ noDeadlocks = new JCheckBox("No deadlocks?", checkNoDeadSelected);
+ noDeadlocks.addActionListener(this);
+ jp01.add(noDeadlocks, c01);
// Reachability
@@ -290,6 +298,12 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
noLiveness.setSelected(livenessSelected == LIVENESS_NONE);
livenessCheckable.setSelected(livenessSelected == LIVENESS_SELECTED);
livenessAllStates.setSelected(livenessSelected == LIVENESS_ALL);
+
+
+ //Safety pragmas
+ safety = new JCheckBox("Safety Pragmas", safetySelected);
+ safety.addActionListener(this);
+ jp01.add(safety, c01);
//Limitations
stateLimit = new JCheckBox("Limit number of states in GF", limitStatesSelected);
@@ -563,6 +577,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
+ amc.setCheckNoDeadlocks(checkNoDeadSelected);
// Reachability
int res;
@@ -617,6 +632,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
+ if (safetySelected) {
+ res = amc.setSafetyAnalysis();
+ }
+
// Limitations
if (stateLimit.isSelected()) {
amc.setStateLimit(true);
@@ -650,10 +669,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Starting model checking
testGo();
- if (livenessSelected == LIVENESS_NONE) {
+ if (livenessSelected == LIVENESS_NONE && safetySelected == false) {
amc.startModelChecking();
} else {
- amc.startModelCheckingLiveness();
+ amc.startModelCheckingProperties();
}
TraceManager.addDev("Model checking done");
@@ -673,6 +692,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jta.append("\n\nModel checking done\n");
jta.append("Nb of states:" + amc.getNbOfStates() + "\n");
jta.append("Nb of links:" + amc.getNbOfLinks() + "\n");
+ if (checkNoDeadSelected) {
+ jta.append("\nNo deadlocks?\n" + "-> " + amc.deadlockToString() + "\n");
+ }
if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
jta.append("\nReachabilities found:\n");
@@ -696,6 +718,11 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
handleLiveness(sl.ref1, sl.result);
}
}
+
+ if (safetySelected) {
+ jta.append("\nSafety Analysis:\n");
+ jta.append(amc.safetyToString());
+ }
//TraceManager.addDev(amc.toString());
//TraceManager.addDev(amc.toString());
@@ -816,6 +843,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
ignoreEmptyTransitionsSelected = ignoreEmptyTransitions.isSelected();
ignoreConcurrenceBetweenInternalActionsSelected = ignoreConcurrenceBetweenInternalActions.isSelected();
ignoreInternalStatesSelected = ignoreInternalStates.isSelected();
+ checkNoDeadSelected = noDeadlocks.isSelected();
if (noReachability.isSelected()) {
reachabilitySelected = REACHABILITY_NONE;
@@ -833,6 +861,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
livenessSelected = LIVENESS_ALL;
}
+ safetySelected = safety.isSelected();
stateLimitField.setEnabled(stateLimit.isSelected());
limitStatesSelected = stateLimit.isSelected();
timeLimitField.setEnabled(timeLimit.isSelected());