diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 8f49bfb67ec2339c653b353afb192c24869fd9a2..91a7c71a55cbb0dda96de2c0b6572fd714a55978 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -63,6 +63,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
private String globalCode;
private int booleanOffset;
+ private int attributeOptRatio;
public AvatarBlock(String _name, AvatarSpecification _avspec, Object _referenceObject) {
@@ -74,6 +75,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
signals = new LinkedList<AvatarSignal>();
asm = new AvatarStateMachine(this, "statemachineofblock__" + _name, _referenceObject);
booleanOffset = -1;
+ attributeOptRatio = 1;
}
@@ -726,6 +728,19 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public int getBooleanOffset() {
return booleanOffset;
}
+
+
+ public int getAttributeOptRatio() {
+ return attributeOptRatio;
+ }
+
+ public void setAttributeOptRatio(int attributeOptRatio) {
+ if (attributeOptRatio == 2 || attributeOptRatio == 4) {
+ this.attributeOptRatio = attributeOptRatio;
+ } else {
+ this.attributeOptRatio = 1;
+ }
+ }
@Override
diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index c3db148a262a2e2ddd9fcece0d19432efe8f4474..0e589c0147a6f57654eb8dcd39b9bc8462121b9a 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -53,11 +53,12 @@ public class AvatarExpressionAttribute {
private AvatarBlock block;
private int blockIndex;
private int accessIndex;
- private int accessOffset;
private AvatarStateMachineElement state;
private String s;
private boolean isState;
private boolean error;
+ private int shift;
+ private int mask;
public AvatarExpressionAttribute(AvatarSpecification spec, String s) {
@@ -80,7 +81,8 @@ public class AvatarExpressionAttribute {
state = asme;
error = false;
accessIndex = -1;
- accessOffset = -1;
+ shift = 0;
+ mask = 0xFFFFFFFF;
block = null;
}
@@ -113,7 +115,8 @@ public class AvatarExpressionAttribute {
int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
- accessOffset = -1;
+ shift = 0;
+ mask = 0xFFFFFFFF;
if (attributeIndex == -1) {
// state?
@@ -125,11 +128,19 @@ public class AvatarExpressionAttribute {
accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
} else {
int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
if (offset == -1 || attributeIndex < offset) {
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
+ accessIndex = attributeIndex / optRatio + SpecificationBlock.ATTR_INDEX;
+ shift = (attributeIndex % optRatio) * (32 / optRatio);
+ if (optRatio == 2) {
+ mask = 0xFFFF;
+ } else if (optRatio == 4) {
+ mask = 0xFF;
+ }
} else {
accessIndex = SpecificationBlock.ATTR_INDEX + offset + ((attributeIndex - offset) / 32);
- accessOffset = (attributeIndex - offset) % 32;
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
}
}
return true;
@@ -146,7 +157,8 @@ public class AvatarExpressionAttribute {
int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
- accessOffset = -1;
+ shift = 0;
+ mask = 0xFFFFFFFF;
if (attributeIndex == -1) {
// state?
@@ -158,11 +170,19 @@ public class AvatarExpressionAttribute {
accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
} else {
int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
if (offset == -1 || attributeIndex < offset) {
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
+ accessIndex = attributeIndex / optRatio + SpecificationBlock.ATTR_INDEX;
+ shift = (attributeIndex % optRatio) * (32 / optRatio);
+ if (optRatio == 2) {
+ mask = 0xFFFF;
+ } else if (optRatio == 4) {
+ mask = 0xFF;
+ }
} else {
accessIndex = SpecificationBlock.ATTR_INDEX + offset + ((attributeIndex - offset) / 32);
- accessOffset = (attributeIndex - offset) % 32;
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
}
}
return true;
@@ -186,11 +206,7 @@ public class AvatarExpressionAttribute {
}
}
- if (accessOffset == -1) {
- value = ss.blocks[blockIndex].values[accessIndex];
- } else {
- value = (ss.blocks[blockIndex].values[accessIndex] >> accessOffset) & 1;
- }
+ value = (ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
return value;
}
@@ -202,11 +218,7 @@ public class AvatarExpressionAttribute {
return (state == asme) ? 1 : 0;
}
- if (accessOffset == -1) {
- value = ss.blocks[blockIndex].values[accessIndex];
- } else {
- value = (ss.blocks[blockIndex].values[accessIndex] >> accessOffset) & 1;
- }
+ value = (ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
return value;
}
@@ -225,11 +237,7 @@ public class AvatarExpressionAttribute {
}
}
- if (accessOffset == -1) {
- value = sb.values[accessIndex];
- } else {
- value = (sb.values[accessIndex] >> accessOffset) & 1;
- }
+ value = (sb.values[accessIndex] >> shift) & mask;
return value;
}
@@ -242,11 +250,7 @@ public class AvatarExpressionAttribute {
}
//Cancel offset based on Specification Blocks
- if (accessOffset == -1) {
- value = attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX];
- } else {
- value = (attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX] >> accessOffset) & 1;
- }
+ value = (attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX] >> shift) & mask;
return value;
}
@@ -256,11 +260,7 @@ public class AvatarExpressionAttribute {
return;
}
- if (accessOffset == -1) {
- ss.blocks[blockIndex].values[accessIndex] = value;
- } else {
- ss.blocks[blockIndex].values[accessIndex] ^= ((-(value & 1))^ ss.blocks[blockIndex].values[accessIndex]) & (1 << accessOffset);
- }
+ ss.blocks[blockIndex].values[accessIndex] = (ss.blocks[blockIndex].values[accessIndex] & (~(mask << shift))) | ((value & mask) << shift);
}
public void setValue(SpecificationBlock sb, int value) {
@@ -268,11 +268,12 @@ public class AvatarExpressionAttribute {
return;
}
- if (accessOffset == -1) {
- sb.values[accessIndex] = value;
- } else {
- sb.values[accessIndex] ^= ((-(value & 1))^ sb.values[accessIndex]) & (1 << accessOffset);
- }
+// if (shift == -1) {
+// sb.values[accessIndex] = value;
+// } else {
+// sb.values[accessIndex] ^= ((-(value & 1))^ sb.values[accessIndex]) & (1 << shift);
+// }
+ sb.values[accessIndex] = (sb.values[accessIndex] & (~(mask << shift))) | ((value & mask) << shift);
}
//Link state to access index in the state machine
@@ -290,8 +291,12 @@ public class AvatarExpressionAttribute {
public int getAttributeType() {
if (isState) {
return AvatarExpressionSolver.IMMEDIATE_BOOL;
- } else if (accessOffset == -1) {
- if (block.getAttribute(accessIndex - SpecificationBlock.ATTR_INDEX).getType() == AvatarType.BOOLEAN) {
+ }
+ int offset = block.getBooleanOffset();
+ int ratio = block.getAttributeOptRatio();
+ int attributeIndex = (accessIndex - SpecificationBlock.ATTR_INDEX) * ratio + shift * ratio / 32;
+ if (offset == -1 || (attributeIndex < offset)) {
+ if (block.getAttribute((accessIndex - SpecificationBlock.ATTR_INDEX)).getType() == AvatarType.BOOLEAN) {
return AvatarExpressionSolver.IMMEDIATE_BOOL;
} else {
return AvatarExpressionSolver.IMMEDIATE_INT;
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index c20f5683e4745da4a2c8dfe084f80b13de054c61..fa50768658b38fddda8026d33d9480fe639ab93c 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -84,6 +84,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean ignoreEmptyTransitions;
private boolean ignoreConcurrenceBetweenInternalActions;
private boolean ignoreInternalStates;
+ private boolean verboseInfo;
// RG
private boolean computeRG;
@@ -150,6 +151,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
timeLimit = 500;
counterexample = false;
freeIntermediateStateCoding = true;
+ verboseInfo = true;
}
public AvatarSpecification getInitialSpec() {
@@ -420,6 +422,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyRI = studyReinit;
genRG = computeRG;
genTrace = counterexample;
+ verboseInfo = false;
//then compute livenesses
computeRG = false;
@@ -522,6 +525,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studyR || genRG) {
if (genRG) {
deadlocks = 0;
+ verboseInfo = true;
}
studyReachability = studyR;
computeRG = genRG;
@@ -934,6 +938,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (counterexample) {
counterTrace.reset();
traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ verboseInfo = true;
}
}
@@ -956,6 +961,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
}
+ verboseInfo = false;
}
@@ -1096,8 +1102,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute the hash of the new state, and create the link to the right next state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + tr.clockMin + "..." + tr.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + tr.clockMin + "..." + tr.clockMax + "]";
+ link.action = action;
+ }
newState.computeHash(blockValues);
//SpecificationState similar = states.get(newState.getHash(blockValues));
@@ -1200,8 +1208,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (similar != null) {
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + st.clockMin + "..." + st.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + st.clockMin + "..." + st.clockMax + "]";
+ link.action = action;
+ }
link.destinationState = similar;
nbOfLinks++;
_ss.addNext(link);
@@ -1211,8 +1221,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//already elaborated, add that state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + "0...0" + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + "0...0" + "]";
+ link.action = action;
+ }
link.destinationState = newState;
synchronized (this) {
similar = states.get(newState.getHash(blockValues));
@@ -1251,8 +1263,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
similar = findSimilarState(newState);
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + st.clockMin + "..." + st.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + st.clockMin + "..." + st.clockMax + "]";
+ link.action = action;
+ }
if (similar != null) {
link.destinationState = similar;
} else {
@@ -1301,8 +1315,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//Creating new link
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + "0...0" + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + "0...0" + "]";
+ link.action = action;
+ }
synchronized (this) {
similar = states.get(newState.getHash(blockValues));
if (similar == null) {
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
index e4ac934785f85e99de98d498b97b74617bc88a11..23fd69ac1236b62268fe1b3121624c3bc753d8d3 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
@@ -86,10 +86,15 @@ public class SpecificationBlock {
//TraceManager.addDev("Nb of attributes:" + attrs.size());
//TraceManager.addDev("in block=" + _block.toString());
int booleanIndex = _block.getBooleanOffset();
+ int optRatio = _block.getAttributeOptRatio();
if (!compress || booleanIndex == -1) {
values = new int[HEADER_VALUES+attrs.size()];
} else {
- values = new int[HEADER_VALUES+booleanIndex+((attrs.size()-booleanIndex+31)/32)];
+ if (optRatio > 1) {
+ values = new int[HEADER_VALUES+(booleanIndex+optRatio-1)/optRatio+((attrs.size()-booleanIndex+31)/32)];
+ } else {
+ values = new int[HEADER_VALUES+booleanIndex+((attrs.size()-booleanIndex+31)/32)];
+ }
}
// Initial state
@@ -112,18 +117,25 @@ public class SpecificationBlock {
}
} else {
int i = 0;
- for(AvatarAttribute attr: attrs) {
- if (i < booleanIndex) {
- values[cpt++] = attr.getInitialValueInInt();
- } else if (((i - booleanIndex) % 32) == 0) {
- values[cpt] = attr.getInitialValueInInt();
- } else {
- values[cpt] |= attr.getInitialValueInInt() << ((i - booleanIndex) % 32);
- if (((i - booleanIndex) % 32) == 31) {
- cpt++;
- }
- }
- i++;
+ for(AvatarAttribute attr: attrs) {
+ if (i < booleanIndex) {
+ if (i % optRatio == 0) {
+ values[cpt] = attr.getInitialValueInInt();
+ } else {
+ values[cpt] |= attr.getInitialValueInInt() << ((i % optRatio) * (32 / optRatio));
+ }
+ if (i % optRatio + 1 == optRatio) {
+ cpt++;
+ }
+ } else if (((i - booleanIndex) % 32) == 0) {
+ values[cpt] = attr.getInitialValueInInt();
+ } else {
+ values[cpt] |= attr.getInitialValueInInt() << ((i - booleanIndex) % 32);
+ if (((i - booleanIndex) % 32) == 31) {
+ cpt++;
+ }
+ }
+ i++;
}
}
}