diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 076c789cf39a32749a0b057ca72febb753b0890d..7085d1bda9b51531e447df4c6da5fa436a9f78eb 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -43,10 +43,10 @@ import avatartranslator.*;
/**
* Class SafetyProperty
- * Coding of a safety property
+ * Coding of a safety or liveness property
* Creation: 22/11/2017
- * @version 1.0 22/11/2017
- * @author Ludovic APVRILLE
+ * @version 1.0 24/08/2020
+ * @author Ludovic APVRILLE, Alessandro TEMPIA CALVINO
*/
public class SafetyProperty {
@@ -77,10 +77,11 @@ public class SafetyProperty {
public int propertyType;
public int leadType;
public boolean result;
-
+ public boolean expectedResult;
public SafetyProperty(String property) {
rawProperty = property;
+ expectedResult = true;
phase = SpecificationPropertyPhase.NOTCOMPUTED;
/* to manually analyze after the AvatarSpecification is ready
for model-checking in order to build correct expression solvers */
@@ -94,6 +95,7 @@ public class SafetyProperty {
propertyType = BLOCK_STATE;
safetyType = _safetyType;
result = true;
+ expectedResult = true;
phase = SpecificationPropertyPhase.NOTCOMPUTED;
rawProperty = "Element " + state.getExtendedName() + " of block " + block.getName();
this.state = state;
@@ -103,6 +105,8 @@ public class SafetyProperty {
String tmpP = rawProperty.trim();
String p;
+ tmpP = checkExpectedResult(tmpP);
+
if (!initType(tmpP)) {
return false;
}
@@ -124,6 +128,8 @@ public class SafetyProperty {
String tmpP = rawProperty.trim();
String p;
+ tmpP = checkExpectedResult(tmpP);
+
if (!initType(tmpP)) {
return false;
}
@@ -205,13 +211,14 @@ public class SafetyProperty {
public void setComputed() {
- if (result) {
+ if (result == expectedResult) {
phase = SpecificationPropertyPhase.SATISFIED;
} else {
phase = SpecificationPropertyPhase.NONSATISFIED;
}
}
+
public AvatarStateMachineElement getState() {
return state;
}
@@ -261,6 +268,18 @@ public class SafetyProperty {
return name;
}
+ private String checkExpectedResult(String tmpP) {
+ if (tmpP.startsWith("T") || tmpP.startsWith("t")) {
+ expectedResult = true;
+ return tmpP.substring(1).trim();
+ } else if (tmpP.startsWith("F") || tmpP.startsWith("f")) {
+ expectedResult = false;
+ return tmpP.substring(1).trim();
+ }
+
+ return tmpP;
+ }
+
private boolean initType(String tmpP) {
errorOnProperty = NO_ERROR;
diff --git a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
index da00c618df0abdb040c3057eb490ac5458b9ef75..23618c6f408ab4e3f7252a23a71e5f794cc3e398 100644
--- a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
+++ b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
@@ -177,7 +177,7 @@ public class ModelCheckerValidator {
if (dStudy) {
System.out.println("Deadlock Study");
- uResult = workQuery(gtm, rshc, "A[] not deadlock", fn);
+ uResult = workQuery(gtm, rshc, "A[] not deadlock", fn, true);
if (!((uResult == 0 && amc.getNbOfDeadlocks() > 0) || (uResult == 1 && amc.getNbOfDeadlocks() == 0))) {
diff.append("No Deadlock: amc = " + (amc.getNbOfDeadlocks() == 0) + "; uppaal = " + (uResult == 1) + "\n");
equal = false;
@@ -193,7 +193,7 @@ public class ModelCheckerValidator {
index = s.indexOf('$');
if ((index != -1)) {
query = s.substring(0, index);
- uResult = workQuery(gtm, rshc, "E<> " + query, fn);
+ uResult = workQuery(gtm, rshc, "E<> " + query, fn, true);
match = false;
for (SpecificationReachability sr : reachabilities) {
if (sr.ref1 instanceof AvatarStateMachineElement) {
@@ -228,7 +228,7 @@ public class ModelCheckerValidator {
index = s.indexOf('$');
if ((index != -1)) {
query = s.substring(0, index);
- uResult = workQuery(gtm, rshc, "A<> " + query, fn);
+ uResult = workQuery(gtm, rshc, "A<> " + query, fn, true);
match = false;
for (SafetyProperty sp : livenesses) {
Object o = sp.getState().getReferenceObject();
@@ -255,8 +255,8 @@ public class ModelCheckerValidator {
if (sStudy) {
ArrayList<SafetyProperty> safeties = amc.getSafeties();
for (SafetyProperty sp : safeties) {
- query = translateCustomQuery(gtm, spec, sp.getRawProperty());
- uResult = workQuery(gtm, rshc, query, fn);
+ query = translateCustomQuery(gtm, spec, removeExpectedResult(sp.getRawProperty()));
+ uResult = workQuery(gtm, rshc, query, fn, sp.expectedResult);
if (!(uResult == 1 && sp.getPhase() == SpecificationPropertyPhase.SATISFIED ||
uResult == 0 && sp.getPhase() == SpecificationPropertyPhase.NONSATISFIED)) {
diff.append("Safety " + sp.getRawProperty() + ": amc = " + (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) + "; uppaal = " + (uResult == 1) + "\n");
@@ -285,10 +285,19 @@ public class ModelCheckerValidator {
}
+ private static String removeExpectedResult(String query) {
+ if (query.matches("^[TtFf].*")) {
+ return query.substring(1).trim();
+ } else {
+ return query;
+ }
+ }
+
+
// return: -1: error
// return: 0: property is NOt satisfied
// return: 1: property is satisfied
- private static int workQuery(GTURTLEModeling gtm, RshClient rshc, String query, String fn) throws LauncherException {
+ private static int workQuery(GTURTLEModeling gtm, RshClient rshc, String query, String fn, boolean expectedResult) throws LauncherException {
int ret;
//TraceManager.addDev("Working on query: " + query);
@@ -307,11 +316,19 @@ public class ModelCheckerValidator {
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_VERIFIED_LABELS)) {
- ret = 1;
+ if (expectedResult) {
+ ret = 1;
+ } else {
+ ret = 0;
+ }
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_NOT_VERIFIED_LABELS)) {
- ret = 0;
+ if (!expectedResult) {
+ ret = 1;
+ } else {
+ ret = 0;
+ }
} else {
ret = -1;
}
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index aa9fa01e6e292819e104a6806714829aaad17cf5..47567278d2944adc37b98d3f9d12989acb8624c5 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -423,6 +423,11 @@ public class AvatarDesignPanelTranslator {
//Todo: check types
//Todo: handle complex types
_pragma = _pragma.trim();
+
+ //remove expected result letter from the start if present
+ if (_pragma.matches("^[TtFf].*")) {
+ _pragma = _pragma.substring(1).trim();
+ }
if (_pragma.contains("=") && !(_pragma.contains("==") || _pragma.contains("<=") || _pragma.contains(">=") || _pragma.contains("!="))) {
//not a query
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index aee111931558b0132fb3ad5e5fc03fe5ed6f3f9b..baa855e6e576860a959dc98faa2a72b6e7cb2e87 100644
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -152,6 +152,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected java.util.List<String> customQueries;
public Map<String, Integer> verifMap;
protected int status = -1;
+ private boolean expectedResult;
/*
* Creates new form
@@ -619,6 +620,9 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
rshc = new RshClient(host);
RshClient rshctmp = rshc;
+
+ expectedResult = true;
+
try {
// checking UPPAAL installation
@@ -795,7 +799,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
for (JCheckBox j : customChecks) {
if (j.isSelected()) {
jta.append(j.getText() + "\n");
- String translation = translateCustomQuery(j.getText());
+ String translation = checkExpectedResult(j.getText());
+ translation = translateCustomQuery(translation);
jta.append(translation);
status = -1;
workQuery(translation, fn, trace_id, rshc);
@@ -859,6 +864,20 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
mode = NOT_STARTED;
setButtons();
}
+
+ private String checkExpectedResult(String query) {
+ query = query.trim();
+ expectedResult = true;
+
+ if (query.startsWith("T") || query.startsWith("t")) {
+ return query.substring(1).trim();
+ } else if (query.startsWith("F") || query.startsWith("f")) {
+ expectedResult = false;
+ return query.substring(1).trim();
+ }
+
+ return query;
+ }
private String translateCustomQuery(String query) {
@@ -979,16 +998,26 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_VERIFIED_LABELS)) {
// else if (data.indexOf("Property is satisfied") >-1){
- jta.append("-> property is satisfied\n");
- status = 1;
+ if (expectedResult) {
+ jta.append("-> property is satisfied\n");
+ status = 1;
+ } else {
+ jta.append("-> property is NOT satisfied\n");
+ status = 0;
+ }
ret = 1;
}
// Issue #35: Different labels for UPPAAL 4.1.19
else if (checkAnalysisResult(data, PROP_NOT_VERIFIED_LABELS)) {
// else if (data.indexOf("Property is NOT satisfied") > -1) {
- jta.append("-> property is NOT satisfied\n");
- status = 0;
- ret = 0;
+ if (!expectedResult) {
+ jta.append("-> property is satisfied\n");
+ status = 1;
+ } else {
+ jta.append("-> property is NOT satisfied\n");
+ status = 0;
+ }
+ ret = 1;
} else {
jta.append("ERROR -> property could not be studied\n");
status = 2;