diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 152c2217f50bf9fdb877db67114d02f01d47f723..76af8022964d816583229c0b5a7b78608b8086f1 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -114,6 +114,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean counterexample;
private CounterexampleTrace counterTrace;
public Map<Integer, CounterexampleTraceState> traceStates;
+ private StringBuilder counterTraceReport;
//RG limits
private boolean stateLimitRG;
@@ -344,6 +345,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
return false;
}
+
+ public void setCounterExampleTrace(boolean counterexample) {
+ this.counterexample = counterexample;
+ if (counterexample) {
+ counterTraceReport = new StringBuilder();
+ }
+ }
+
+ public String getCounterTrace() {
+ if (counterTraceReport == null) {
+ return "";
+ }
+ return counterTraceReport.toString();
+ }
public void setComputeRG(boolean _rg) {
computeRG = _rg;
@@ -383,9 +398,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
initModelChecking();
-
- counterexample = true; //TODO: delete
-
+
stateLimitRG = false;
timeLimitRG = false;
emptyTr = ignoreEmptyTransitions;
@@ -411,9 +424,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = true;
for (SafetyProperty sp : livenesses) {
safety = sp;
- initCounterexample();
+// initCounterexample();
startModelChecking(nbOfThreads);
- generateCounterexample();
+// generateCounterexample();
deadlocks += nbOfDeadlocks;
resetModelChecking();
if (!stoppedBeforeEnd) {
@@ -447,8 +460,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (SpecificationState state : safetyLeadStates.values()) {
deadlocks += nbOfDeadlocks;
resetModelChecking();
+ initCounterexample();
startModelChecking(state, nbOfThreads);
if (safety.result == false) {
+ generateCounterexample();
break;
}
}
@@ -898,15 +913,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private void initCounterexample() {
- counterTrace = new CounterexampleTrace(spec);
- traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ if (counterexample) {
+ counterTrace = new CounterexampleTrace(spec);
+ traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ }
}
private void generateCounterexample() {
if (counterexample && counterTrace.hasCounterexample()) {
counterTrace.buildTrace();
- System.out.println(counterTrace.generateSimpleTrace());
+ if (studySafety) {
+ counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
+ counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n");
+ }
}
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index ba7048f59824b5de91d3de8a1034d27a190285ab..aad9fadbd34068c75a2611824b690c9ad86f00e5 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -2,6 +2,7 @@ package avatartranslator.modelchecker;
import java.util.LinkedList;
import java.util.List;
+import java.util.Map;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
@@ -69,6 +70,7 @@ public class CounterexampleTrace {
return s.toString();
}
+
public String generateSimpleTrace() {
if (trace == null) {
return "";
@@ -95,5 +97,43 @@ public class CounterexampleTrace {
}
return s.toString();
}
+
+
+ public String generateSimpleTrace(Map<Integer, SpecificationState> states) {
+ if (trace == null) {
+ return "";
+ }
+
+ StringBuilder s = new StringBuilder();
+ List<AvatarBlock> blocks = spec.getListOfBlocks();
+
+ for (AvatarBlock block : blocks) {
+ if (block.getStateMachine().allStates == null) {
+ return "";
+ }
+ }
+
+ int id = 0;
+ SpecificationState state = null;
+ for (CounterexampleTraceState cs : trace) {
+ if (state != null) {
+ for (SpecificationLink sl : state.nexts) {
+ if (sl.destinationState.hashValue == cs.hash) {
+ s.append("Transition " + sl.action + "\n");
+ break;
+ }
+ }
+ }
+ s.append("State " + id + ":\t");
+ int j = 0;
+ for (AvatarBlock block : blocks) {
+ s.append("\t" + block.getName() + "." + block.getStateMachine().allStates[cs.blocksStates[j++]].getName());
+ }
+ s.append("\n");
+ state = states.get(cs.hash);
+ id++;
+ }
+ return s.toString();
+ }
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index bb9327efbd3eebb6bcfa67b8345231619997b3c4..b3ccbac29ac0767789a92bb8ee4b8f6790432e52 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -104,6 +104,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean checkNoDeadSelected = false;
protected static boolean checkReinitSelected = false;
protected static boolean limitStatesSelected = false;
+ protected static boolean generateCountertraceSelected = false;
+ protected static String countertracePath;
protected static String stateLimitValue;
protected static boolean limitTimeSelected = false;
protected static String timeLimitValue;
@@ -155,6 +157,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JCheckBox noDeadlocks;
protected JCheckBox reinit;
protected JCheckBox safety;
+ protected JCheckBox countertrace;
+ protected JTextField countertraceField;
protected JButton checkUncheckAllPragmas;
protected java.util.List<JCheckBox> customChecks;
@@ -191,6 +195,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
graphDirDot = _graphDir + File.separator + "rgavatar$.dot";
}
+ countertracePath = "trace$.txt";
stateLimitValue = "100";
timeLimitValue = "5000";
@@ -443,7 +448,18 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
cadvanced.gridwidth = GridBagConstraints.REMAINDER; //end row
jpadvanced.add(jsp, cadvanced);
}
+ cadvanced.gridwidth = GridBagConstraints.REMAINDER;
+ //Countertrace
+ cadvanced.gridwidth = 1;
+ countertrace = new JCheckBox("Generate counterexample traces", generateCountertraceSelected);
+ countertrace.addActionListener(this);
+ jpadvanced.add(countertrace, cadvanced);
+ cadvanced.gridwidth = GridBagConstraints.REMAINDER;
+ countertraceField = new JTextField(countertracePath);
+ jpadvanced.add(countertraceField, cadvanced);
+
+
jpopt.add(jp01, c01);
jpopt.add(jpbasic, cbasic);
jpopt.add(jpadvanced, cadvanced);
@@ -711,6 +727,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
+ amc.setCounterExampleTrace(generateCountertraceSelected);
// Reachability
int res;
@@ -879,6 +896,23 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
Date date = new Date();
String dateAndTime = dateFormat.format(date);
+
+ if (generateCountertraceSelected) {
+ String trace = amc.getCounterTrace();
+
+ String autfile;
+ if (countertraceField.getText().indexOf("$") != -1) {
+ autfile = Conversion.replaceAllChar(countertraceField.getText(), '$', dateAndTime);
+ } else {
+ autfile = countertraceField.getText();
+ }
+ try {
+ FileUtils.saveFile(autfile, trace);
+ jta.append("\nCounterexample trace saved in " + autfile + "\n");
+ } catch (Exception e) {
+ jta.append("\nCounterexample trace could not be saved in " + autfile + "\n");
+ }
+ }
if (saveGraphAUT.isSelected()) {
graphAUT = amc.toAUT();
@@ -1047,6 +1081,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
+ countertrace.setEnabled(safety.isSelected());
+ countertraceField.setEnabled(countertrace.isSelected());
+ generateCountertraceSelected = countertrace.isSelected();
+
stateLimitField.setEnabled(stateLimit.isSelected());
limitStatesSelected = stateLimit.isSelected();
timeLimitField.setEnabled(timeLimit.isSelected());