First easy implementation of counterexamples for safety pragmas

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");
+            }
         }
     }
 

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();
+    }
 
 }

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());