Bug fix for CFSerializer

diff --git a/main.jpf b/main.jpf
index 0293eb94063e37278851ba893921fc18c0ec0909..a1d2ecacc91de19dd06585540f0a40ecb359e7a2 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -45,7 +45,7 @@ apps=App1,App2
 
 # Debug mode for StateReducer
 printout_state_transition=true
-#activate_state_reduction=false
+activate_state_reduction=true
 file_output=moreStatistics
 
 # Timeout in minutes (default is 0 which means no timeout)

diff --git a/moreStatistics b/moreStatistics
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0b9af175098b2a6c9bc26578863fb4853d5e505f 100644 (file)
--- a/moreStatistics
+++ b/moreStatistics
@@ -0,0 +1,4 @@
+==> DEBUG: State reduction mode  : true
+==> DEBUG: Number of conflicts   : 4
+==> DEBUG: Number of transitions : 7
+

diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index f6663eb31b94338b54e8a09e9eafa6ef5091ec1f..7b5817761c9b354ffb94849914ac965f69e91efa 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -55,21 +55,14 @@ public class CFSerializer extends FilteringSerializer {
   // over the serialized objects to reset their sids. This works by resetting
   // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
   // from -1, but store the absolute value in the serialization stream
-  boolean positiveSid;
-
-  int sidCount;
+  int initsidCount=0;
+  int sidCount=1;
 
   @Override
   protected void initReferenceQueue() {
     super.initReferenceQueue();
-
-    if (positiveSid){
-      positiveSid = false;
-      sidCount = -1;
-    } else {
-      positiveSid = true;
-      sidCount = 1;
-    }
+    
+    initsidCount = sidCount - 1;
   }
 
   // might be overriden in subclasses to conditionally queue objects
@@ -86,30 +79,20 @@ public class CFSerializer extends FilteringSerializer {
       ClassInfo ci = ei.getClassInfo();
 
       if (SmartThingsConfig.instance.ignoreClass(ci)) {
-        ei.setSid(0);
+        ei.setSid(initsidCount);
         buf.add(0);
         return;
       }
-      
       int sid = ei.getSid();
-
-      if (positiveSid){ // count sid upwards from 1
-        if (sid <= 0){  // not seen before in this serialization run
+      
+      if (sid <= initsidCount){ // count sid upwards from 1
           sid = sidCount++;
           ei.setSid(sid);
           queueReference(ei);
-        }
-      } else { // count sid downwards from -1
-        if (sid >= 0){ // not seen before in this serialization run
-          sid = sidCount--;
-          ei.setSid(sid);
-          queueReference(ei);
-        }
-        sid = -sid;
       }
 
       // note that we always add the absolute sid value
-      buf.add(sid);
+      buf.add(sid - initsidCount);
     }
   }
 
@@ -188,6 +171,6 @@ public class CFSerializer extends FilteringSerializer {
   
   @Override
   protected int getSerializedReferenceValue (ElementInfo ei){
-    return Math.abs(ei.getSid());
+    return ei.getSid()-initsidCount;
   }
 }