Model-checker: improved heap memory footprint of about 60%

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

@@ -209,7 +209,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 //TraceManager.addDev("null elt in state machine of block=" + block.getName());
                 //if (elt.canBeVerified() && elt.isChecked()) {
                 if (elt.isChecked()) {
-                    SafetyProperty sp = new SafetyProperty(block, elt);
+                    SafetyProperty sp = new SafetyProperty(block, elt, SafetyProperty.ALLTRACES_ONESTATE);
                     livenesses.add(sp);
                 }
             }
@@ -223,7 +223,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         for (AvatarBlock block : spec.getListOfBlocks()) {
             for (AvatarStateMachineElement elt : block.getStateMachine().getListOfElements()) {
                 if (((elt instanceof AvatarStateElement) && (elt.canBeVerified())) || (elt.isCheckable())) {
-                    SafetyProperty sp = new SafetyProperty(block, elt);
+                    SafetyProperty sp = new SafetyProperty(block, elt, SafetyProperty.ALLTRACES_ONESTATE);
                     livenesses.add(sp);
                 }
             }
@@ -549,7 +549,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     public void stopModelChecking() {
         emptyPendingStates();
         stoppedBeforeEnd = true;
-        safety.result = false;
+        if (studySafety) {
+            safety.result = false;
+        }
         TraceManager.addDev("Model checking stopped");
     }
     
@@ -770,7 +772,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                             ((AvatarActionAssignment) aa).buildActionSolver(block);
                         }
                     }
-                }else if (elt instanceof AvatarActionOnSignal) {
+                } else if (elt instanceof AvatarActionOnSignal) {
                     ((AvatarActionOnSignal) elt).buildActionSolver(block);
                 }
             }
@@ -1423,7 +1425,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             ase = getNextState(_st.transitions[i], _newState, 10);
             if (ase != null) {
                 checkElement(ase, _newState);
-                int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
+                //int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
+                int index = _st.transitions[i].getBlock().getStateMachine().getIndexOfState(ase);
                 if (index > -1) {
                     _newState.blocks[_st.blocksInt[i]].values[SpecificationBlock.STATE_INDEX] = index;
                 }
@@ -1507,7 +1510,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             retAction = "";
         }
 
-        return "i(" + _st.blocks[0].getName() + "/" + retAction + ")";
+        //return "i(" + _st.blocks[0].getName() + "/" + retAction + ")";
+        return "i(" + _st.transitions[0].getBlock().getName() + "/" + retAction + ")";
+
     }
 
     private String executeSyncTransition(SpecificationState _previousState, SpecificationState _newState, SpecificationTransition _st) {

src/main/java/avatartranslator/modelchecker/SafetyProperty.java

@@ -88,7 +88,7 @@ public class SafetyProperty  {
         analyzeProperty(_spec);
     }
     
-    public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state) {
+    public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state, int _safetyType) {
         //create liveness safety
         this.block = block;
         this.state = state;
@@ -96,7 +96,7 @@ public class SafetyProperty  {
         safetySolver = new AvatarExpressionSolver();
         safetySolver.builExpression(attribute);
         propertyType = BLOCK_STATE;
-        safetyType = ALLTRACES_ONESTATE;
+        safetyType = _safetyType;
         result = true;
     }
 

src/main/java/avatartranslator/modelchecker/SpecificationTransition.java

@@ -57,8 +57,6 @@ public class SpecificationTransition  {
 
     public boolean fromStateWithMoreThanOneTransition;
     
-    public AvatarBlock[] blocks;
-    public SpecificationBlock[] specBlocks;
     public int[] blocksInt;
 
     public AvatarTransition[] transitions;
@@ -71,13 +69,7 @@ public class SpecificationTransition  {
 
     public void init(int _nbOfElements, AvatarTransition _at, AvatarBlock _ab, SpecificationBlock _sb, int _blockIndex) {
         transitions = new AvatarTransition[_nbOfElements];
-        transitions[0] = _at;
-
-        blocks = new AvatarBlock[_nbOfElements];
-        blocks[0] = _ab;
-
-        specBlocks = new SpecificationBlock[_nbOfElements];
-        specBlocks[0] = _sb;
+        transitions[0] = _at;        
 
         blocksInt = new int[_nbOfElements];
         blocksInt[0] = _blockIndex;
@@ -97,14 +89,6 @@ public class SpecificationTransition  {
         transitions[0] = _tr1.transitions[0];
         transitions[1] = _tr2.transitions[0];
 
-        blocks = new AvatarBlock[nbOfElements];
-        blocks[0] = _tr1.blocks[0];
-        blocks[1] = _tr2.blocks[0];
-
-        specBlocks = new SpecificationBlock[nbOfElements];
-        specBlocks[0] = _tr1.specBlocks[0];
-        specBlocks[1] = _tr2.specBlocks[0];
-
         blocksInt = new int[nbOfElements];
         blocksInt[0] = _tr1.blocksInt[0];
         blocksInt[1] = _tr2.blocksInt[0];
@@ -115,17 +99,17 @@ public class SpecificationTransition  {
     }
 
     public boolean hasBlockOf(SpecificationTransition _tr) {
-        if (blocks == null) {
+        if (transitions == null) {
             return false;
         }
 
-        if (_tr.blocks == null) {
+        if (_tr.transitions == null) {
             return false;
         }
 
-        for (int i=0; i<blocks.length; i++) {
-            for(int j=0; j<_tr.blocks.length; j++) {
-                if (blocks[i] == _tr.blocks[j]) {
+        for (int i=0; i<transitions.length; i++) {
+            for(int j=0; j<_tr.transitions.length; j++) {
+                if (transitions[i].getBlock() == _tr.transitions[j].getBlock()) {
                     return true;
                 }
             }
@@ -134,6 +118,7 @@ public class SpecificationTransition  {
         return false;
     }
 
+    
     public boolean hasBlockIndex(int _index) {
         if (blocksInt == null) {
             return false;
@@ -151,19 +136,17 @@ public class SpecificationTransition  {
     public String toString() {
         String ret = "Trans: ";
 
-        if (blocks != null) {
-            for (int i=0; i<blocks.length; i++) {
-                ret += "/ Block" + i  + ": " + blocks[i].getName();
-            }
+//        if (blocks != null) {
+//            for (int i=0; i<blocks.length; i++) {
+//                ret += "/ Block" + i  + ": " + blocks[i].getName();
+//            }
+//        }
+        if (transitions != null) {
+            for (int i = 0; i < transitions.length; i++) {
+                ret += "/ Block" + i  + ": " + transitions[i].getBlock().getName() + "/" + transitions[i];
+        	}
         }
         
-	
-	
-	if (transitions != null) {
-	    for (int i=0; i<transitions.length; i++) {
-		ret += "/" + transitions[i];
-	    }
-	}
         return ret;
     }