Added re-initialization check property in avatar model-checker

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

@@ -135,6 +135,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         checkNoDeadlocks = false;
         deadlockStop = false;
         studyReachability = false;
+        studyReinit = false;
         computeRG = false;
         stateLimitRG = false; //No state limit in RG computation
         timeLimitRG = false;
@@ -326,13 +327,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     }
     
 
-    public void setReinitAnalyzis(boolean studyReinit) {
+    public void setReinitAnalysis(boolean studyReinit) {
         this.studyReinit = studyReinit;
     }
     
     
     public boolean getReinitResult() {
-        if (initState != null) {
+        if (studyReinit && initState != null) {
             return initState.getResult();
         }
         return false;
@@ -363,7 +364,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
       }*/
 
     public boolean startModelCheckingProperties() {
-        boolean studyS, studyL, studyR, genRG;
+        boolean studyS, studyL, studyR, studyRI, genRG;
         long deadlocks = 0;
         
         if (spec == null) {
@@ -382,6 +383,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         studyR = studyReachability;
         studyL = studyLiveness;
         studyS = studySafety;
+        studyRI = studyReinit;
         genRG = computeRG;
         
         //then compute livenesses
@@ -390,15 +392,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         studySafety = false;
         studyLiveness = false;
         studyReachability = false;
+        studyReinit = false;
 
         if (studyL) {
             studySafety = true;
             for (SafetyProperty sp : livenesses) {
                 safety = sp;
                 startModelChecking(nbOfThreads);
+                deadlocks += nbOfDeadlocks;
                 resetModelChecking();
                 safety.setComputed();
-                deadlocks += nbOfDeadlocks;
             }
             studySafety = false;
         }
@@ -426,12 +429,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                     safetyLeadStates = null;
                 }
                 safety.setComputed();
-                resetModelChecking();
                 deadlocks += nbOfDeadlocks;
+                resetModelChecking();
             }
             studySafety = false;
         }
         
+        if (studyRI) {
+            studyReinit = true;
+            startModelChecking(nbOfThreads);
+            deadlocks += nbOfDeadlocks;
+            resetModelChecking();
+            studyReinit = false;
+        }
+        
         if (studyR || genRG) {
             if (genRG) {
                 deadlocks = 0;
@@ -462,6 +473,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         studyLiveness = studyL;
         studySafety = studyS;
         studyReachability = studyR;
+        studyReinit = studyRI;
         
         TraceManager.addDev("Model checking done");
         return true;
@@ -538,6 +550,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         } else {
             pendingStates.add(initialState);
         }
+        
+        if (studyReinit) {
+            initState = new SpecificationReinit(initialState);
+        }
+
         //states.put(initialState.hashValue, initialState);
         //statesByID.put(initialState.id, initialState);
         nbOfCurrentComputations = 0;
@@ -1858,18 +1875,29 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 }
             }
         }
+
+        if (studyReinit && similar != null) {
+            if (similar != initState.initState && stateIsReachableFromState(similar, _ss)) {
+                propertyDone = true;
+                initState.setResult(false);
+            }
+        }
     }
     
     private void checkPropertyOnDeadlock(SpecificationState ss) {
         if (studySafety) {
             if (safety.safetyType == SafetyProperty.ALLTRACES_ONESTATE && ss.property == false) {
-                safety.result = false;
                 propertyDone = true;
+                safety.result = false;
             } else if (safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES && ss.property == false) {
-                safety.result = true;
                 propertyDone = true;
+                safety.result = true;
             }
         }
+        if (studyReinit) {
+            propertyDone = true;
+            initState.setResult(false);
+        }
     }
 
 
@@ -2092,6 +2120,23 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         }
         return ret.toString();
     }
+    
+    
+    public String reinitToString() {
+        if (!studyReinit || initState == null) {
+            return "Reinitialization check not activeted\n";
+        }
+        
+        String ret;
+        if (initState.getResult()) {
+            ret = "property is satisfied\n";
+        } else {
+            ret = "property is NOT satisfied\n";
+        }
+        
+        return ret;
+    }
+    
 
     // Do not free the RG
     public void freeUselessAllocations() {

src/main/java/ui/window/JDialogAvatarModelChecker.java

@@ -101,6 +101,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
     protected static int livenessSelected = LIVENESS_NONE;
     protected static boolean safetySelected = false;
     protected static boolean checkNoDeadSelected = false;
+    protected static boolean checkReinitSelected = false;
     protected static boolean limitStatesSelected = false;
     protected static String stateLimitValue;
     protected static boolean limitTimeSelected = false;
@@ -151,6 +152,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
     protected JCheckBox timeLimit;
     protected JTextField timeLimitField;
     protected JCheckBox noDeadlocks;
+    protected JCheckBox reinit;
     protected JCheckBox safety;
     protected JButton checkUncheckAllPragmas;
     protected java.util.List<JCheckBox> customChecks;
@@ -302,9 +304,17 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
         
         
         // Deadlocks
+        cbasic.gridwidth = 1;
         noDeadlocks = new JCheckBox("No deadlocks?", checkNoDeadSelected);
         noDeadlocks.addActionListener(this);
         jpbasic.add(noDeadlocks, cbasic);
+        
+        
+        // Reinit
+        cbasic.gridwidth = GridBagConstraints.REMAINDER;
+        reinit = new JCheckBox("Reinitialization?", checkReinitSelected);
+        reinit.addActionListener(this);
+        jpbasic.add(reinit, cbasic);
 
         
         // Reachability
@@ -699,6 +709,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
             amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
             amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
             amc.setCheckNoDeadlocks(checkNoDeadSelected);
+            amc.setReinitAnalysis(checkReinitSelected);
 
             // Reachability
             int res;
@@ -824,9 +835,14 @@ 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 (checkReinitSelected) {
+                jta.append("\nReinitialization?\n" + "-> " + amc.reinitToString() + "\n");
+            }
 
             if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
                 jta.append("\nReachabilities found:\n");
@@ -1002,6 +1018,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
         ignoreConcurrenceBetweenInternalActionsSelected = ignoreConcurrenceBetweenInternalActions.isSelected();
         ignoreInternalStatesSelected = ignoreInternalStates.isSelected();
         checkNoDeadSelected = noDeadlocks.isSelected();
+        checkReinitSelected = reinit.isSelected();
 
         if (noReachability.isSelected()) {
             reachabilitySelected = REACHABILITY_NONE;
@@ -1034,7 +1051,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
 
         switch (mode) {
             case NOT_STARTED:
-                if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || graphSelected || graphSelectedDot) {
+                if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || checkReinitSelected || graphSelected || graphSelectedDot) {
                     start.setEnabled(true);
                 } else {
                     if (safetySelected) {