Patch, exaustive loop search inserted for non trivial counterexamples

src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java

@@ -959,7 +959,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     
     private void generateCounterexample() {
         if (counterexample && counterTrace.hasCounterexample()) {
-            counterTrace.buildTrace();
+            counterTrace.buildTrace(states, traceStates);
             if (studySafety) {
                 counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
                 counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");

src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java

@@ -2,9 +2,13 @@ package avatartranslator.modelchecker;
 
 import java.util.ArrayList;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
+
+import com.sun.net.httpserver.Authenticator.Result;
 
 import avatartranslator.AvatarBlock;
 import avatartranslator.AvatarSpecification;
@@ -78,6 +82,70 @@ public class CounterexampleTrace {
     }
     
     
+    public boolean buildTrace(Map<Integer, SpecificationState> states, Map<Integer, CounterexampleTraceState> counterstates) {
+        if (counterexampleState == null) {
+            return false;
+        }
+
+        trace = new LinkedList<CounterexampleTraceState>();
+
+        CounterexampleTraceState cs = counterexampleState;
+        CounterexampleTraceState loopPoint = counterstates.get(counterexampleState.hash);
+        
+        if (loopPoint != null) {
+            //search for a loop
+            boolean loop = false;
+            while (cs.father != null) {
+                cs = cs.father;
+                if (cs == loopPoint) {
+                    loop = true;
+                }
+            }
+            if (loop == true) {
+                //registered path contains a loop
+                cs = counterexampleState;
+                trace.add(cs);
+                while (cs.father != null) {
+                    cs = cs.father;
+                    trace.add(0, cs);
+                }
+            } else {
+                //registered path does not contain a loop
+                cs = loopPoint;
+                trace.add(cs);
+                while (cs.father != null) {
+                    cs = cs.father;
+                    trace.add(0, cs);
+                }
+                List<SpecificationState> loopTrace = findLoopTrace(states.get(loopPoint.hash));
+                if (loopTrace != null) {
+                    //integrate
+                    for (SpecificationState ss : loopTrace) {
+                        trace.add(counterstates.get(ss.hashValue));
+                    }
+                } else {
+                    //continue normally
+                    int pos = trace.size();
+                    cs = counterexampleState;
+                    while (cs.father != loopPoint) {
+                        cs = cs.father;
+                        trace.add(pos, cs);
+                    }
+                }
+            }
+        } else {
+            //normal trace
+            trace.add(cs);
+            while (cs.father != null) {
+                cs = cs.father;
+                trace.add(0, cs);
+            }
+        }
+
+        return true;
+    }
+    
+    
     public String toString() {
         if (trace == null) {
             return "";
@@ -138,7 +206,7 @@ public class CounterexampleTrace {
         int id = 0;
         SpecificationState state = null;
         for (CounterexampleTraceState cs : trace) {
-            if (state != null) {
+            if (state != null && state.nexts != null) {
                 for (SpecificationLink sl : state.nexts) {
                     if (sl.destinationState.hashValue == cs.hash) {
                         s.append("Transition " + sl.action + "\n");
@@ -203,5 +271,39 @@ public class CounterexampleTrace {
         CounterexampleQueryReport cr = new CounterexampleQueryReport(null, query, s.toString());
         autTraces.add(cr);
     }
+    
+    private List<SpecificationState> findLoopTrace(SpecificationState start) {
+        Set<Long> visited= new HashSet<Long>();
+        List<SpecificationState> loopTrace = new ArrayList<>();
+        
+        if (!(start.getNextsSize() == 0 || visited.contains(start.id))) {
+            for (SpecificationLink i : start.nexts) {
+                if(findLoopTraceRec(i.destinationState, start, visited, loopTrace, 0)) {
+                    return loopTrace;
+                }
+            }
+        }
+
+        return null;
+    }
+    
+    private boolean findLoopTraceRec(SpecificationState start, SpecificationState arrival, Set<Long> visited, List<SpecificationState> loopTrace, int depth) {
+        loopTrace.add(depth, start);
+        
+        if (start == arrival) {
+            return true;
+        } else if (start.getNextsSize() == 0 || visited.contains(start.id)) {
+            return false;
+        }
+        
+        visited.add(start.id);
+        for (SpecificationLink i : start.nexts) {
+            if (findLoopTraceRec(i.destinationState, arrival, visited, loopTrace, depth + 1)) {
+                return true;
+            }
+        }
+        loopTrace.remove(depth);
+        return false;
+    }
 
 }

src/main/java/cli/Action.java

@@ -41,6 +41,7 @@ package cli;
 
 import avatartranslator.AvatarSpecification;
 import avatartranslator.modelchecker.AvatarModelChecker;
+import avatartranslator.modelchecker.CounterexampleQueryReport;
 import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
 import common.ConfigurationTTool;
 import common.SpecConfigTTool;
@@ -854,7 +855,8 @@ public class Action extends Command {
                     + "-n NUM\tmaximum states created (Only for a non verification study)\n"
                     + "-t NUM\tmaximum time (ms) (Only for a non verification study)\n"
                     + "-c\tconsider full concurrency between actions\n"
-                    + "-v FILE\tsave counterexample traces for pragmas in FILE";
+                    + "-v FILE\tsave counterexample traces for pragmas in FILE"
+                    + "-va FILE\tsave counterexample traces and AUT graph for pragmas in FILE";
             }
 
             public String getExample() {
@@ -889,6 +891,7 @@ public class Action extends Command {
                 amc.setComputeRG(false);
                 boolean rgGraph = false;
                 boolean counterTraces = false;
+                boolean counterTracesAUT = false;
                 boolean reachabilityAnalysis = false;
                 boolean livenessAnalysis = false;
                 boolean safetyAnalysis = false;
@@ -997,6 +1000,16 @@ public class Action extends Command {
                                 return Interpreter.BAD;
                             }
                             break;
+                        case "-va":
+                            if (i != commands.length - 1) {
+                                counterPath = commands[++i];
+                                amc.setCounterExampleTrace(true, true);
+                                counterTraces = true;
+                                counterTracesAUT = true;
+                            } else {
+                                return Interpreter.BAD;
+                            }
+                            break;
                         default:
                             return Interpreter.BAD;
                     }
@@ -1031,17 +1044,40 @@ public class Action extends Command {
                 if (counterTraces) {
                     String trace = amc.getCounterTrace();
                     
-                    String autfile;
+                    String file;
                     if (counterPath.indexOf("$") != -1) {
-                        autfile = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
+                        file = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
                     } else {
-                        autfile = counterPath;
+                        file = counterPath;
                     }
                     try {
-                        FileUtils.saveFile(autfile, trace);
-                        System.out.println("\nCounterexample trace saved in " + autfile + "\n");
+                        File f = new File(file);
+                        FileUtils.saveFile(file, trace);
+                        System.out.println("\nCounterexample trace saved in " + file + "\n");
                     } catch (Exception e) {
-                        System.out.println("\nCounterexample trace could not be saved in " + autfile + "\n");
+                        System.out.println("\nCounterexample trace could not be saved in " + file + "\n");
+                    }
+                    
+                    List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
+                    if (autTraces != null) {
+                        int i = 0;
+                        String autfile = FileUtils.removeFileExtension(file);
+                        for (CounterexampleQueryReport tr : autTraces) {
+                            String filename = autfile + "_" + i + ".aut";
+                            try {
+                                RG rg = new RG(file);
+                                rg.data = tr.getReport();
+                                rg.fileName = filename;
+                                rg.name = tr.getQuery();
+                                interpreter.mgui.addRG(rg);
+                                File f = new File(filename);
+                                FileUtils.saveFile(filename, tr.getReport());
+                                System.out.println("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
+                            } catch (Exception e) {
+                                System.out.println("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
+                            }
+                            i++;
+                        }
                     }
                 }