diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 4a631bbdd5b69062c49db47a29e8b0797d9c9d3e..63fbc332ddb1c541c794e089963161d5f0fdaf9a 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -51,7 +51,7 @@ import java.util.List;
* @author Ludovic APVRILLE, Raja GATGOUT
* @version 1.1 01/07/2014
*/
-public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwner, IBSParamComp {
+public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwner, IBSParamComp, myutil.intboolsolver2.IBSParamComp {
private AvatarBlock father;
private List<AvatarAttribute> attributes;
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 55ff4e9944946b6b8a3283e60e2602bedc22de4e..455dc46413c83e5402ca38b138a6fd77b3ded7aa 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -51,7 +51,7 @@ import java.util.*;
* @author Ludovic APVRILLE
* @version 1.0 20/05/2010
*/
-public class AvatarSpecification extends AvatarElement implements IBSParamSpec {
+public class AvatarSpecification extends AvatarElement implements IBSParamSpec, myutil.intboolsolver2.IBSParamSpec {
public final static int UPPAAL_MAX_INT = 32767;
diff --git a/src/main/java/avatartranslator/AvatarStateMachineElement.java b/src/main/java/avatartranslator/AvatarStateMachineElement.java
index 18c27f1061527e447c27e6f70ab8188d3bf1154b..426d8b9552834b61a5abf0b7bddd88622ccbad37 100644
--- a/src/main/java/avatartranslator/AvatarStateMachineElement.java
+++ b/src/main/java/avatartranslator/AvatarStateMachineElement.java
@@ -55,7 +55,7 @@ import java.util.List;
* @author Ludovic APVRILLE
* @version 1.0 20/05/2010
*/
-public abstract class AvatarStateMachineElement extends AvatarElement implements IBSParamState {
+public abstract class AvatarStateMachineElement extends AvatarElement implements IBSParamState, myutil.intboolsolver2.IBSParamState {
protected List<AvatarStateMachineElement> nexts;
private AvatarState myState;
diff --git a/src/main/java/avatartranslator/intboolsolver2/AvatarIBSOriginParser.java b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSOriginParser.java
new file mode 100644
index 0000000000000000000000000000000000000000..719f602604e2263d6d933b99ecd0d59e0741938a
--- /dev/null
+++ b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSOriginParser.java
@@ -0,0 +1,78 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+package avatartranslator.intboolsolver2;
+
+import myutil.intboolsolver2.*;
+
+/**
+ * class IBSStdClosedFormulaSolver is a complete implementation
+ * and instantiation of {@link IBSOriginParser
+ * IBSolver} for closed Formulas.
+ *
+ * <p> It is provided for documentation together with
+ * {@link IBSStdClosedFormulaAttributeClass
+ * IBSStdClosedFormulaAttributeClass} and
+ * {@link IBSStdClosedFormulaAttributeClass
+ * IBSStdClosedFormulaAttribute}}</p>
+ *
+ * <p>These three
+ * classes provides the same features as
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttribute},
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttributeClass} and
+ * {@link IBSClosedFormulaParser
+ * IBSClosedFormulaSolver} (together).</p>
+ *
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public class AvatarIBSOriginParser extends IBSOriginParser<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState> {
+ AvatarIBSOriginParser() {
+ super(new AvatarIBSStdAttributeClass(), new AvatarIBSStdExpressionClass());
+ }
+}
\ No newline at end of file
diff --git a/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdAttributeClass.java b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdAttributeClass.java
new file mode 100644
index 0000000000000000000000000000000000000000..e03e1bcab3baaa7505a732ca5c1aa157413c311c
--- /dev/null
+++ b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdAttributeClass.java
@@ -0,0 +1,495 @@
+package avatartranslator.intboolsolver2;
+
+import avatartranslator.*;
+import avatartranslator.modelchecker.SpecificationBlock;
+import avatartranslator.modelchecker.SpecificationState;
+import myutil.intboolsolver.IBSAttributeTypes;
+import myutil.intboolsolver.IBSStdAttribute;
+import myutil.intboolsolver2.IBSAttributeClass;
+import myutil.intboolsolver2.IBSStdAttributeClass;
+import myutil.intboolsolver2.IBSStdExpressionClass;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class AvatarIBSStdAttributeClass extends IBSStdAttributeClass<
+ AvatarSpecification,
+ AvatarBlock,
+ AvatarStateMachineElement,
+ SpecificationState,
+ SpecificationBlock
+ > {
+ private static Map<AvatarElement, TypedAttribute> attributesMap;
+ // handling already covered attributes (memorisation)
+ private static AvatarSpecification findSpec = null;
+ private static AvatarBlock findComp = null;
+ private static String findString = "";
+ private static AvatarElement keyElement;
+ public AvatarIBSStdAttributeClass(){}
+
+ public void initBuild(){
+ if (attributesMap == null) {
+ attributesMap = new HashMap<AvatarElement, TypedAttribute>();
+ }
+ }
+ public void initBuild(AvatarSpecification _spec){ initBuild(); }
+ public void initBuild(AvatarBlock _comp){ initBuild(); }
+
+ public TypedAttribute findAttribute(AvatarSpecification _spec, String _s){
+ AvatarElement ae = getElement(_s, _spec);
+ if (ae != null && attributesMap.containsKey(ae)) {
+ TypedAttribute ta = attributesMap.get(ae);
+ if (ta.isAttribute()){
+ //might be uninitialized
+ ((Attribute)(ta.getAttribute())).linkComp(_spec);
+ }
+ return ta;
+ }
+ findString = _s;
+ findSpec = _spec;
+ keyElement = ae;
+ return null;
+ }
+ public void addAttribute(AvatarSpecification _spec, String _s, TypedAttribute _att){
+ AvatarElement ae;
+ if ( _s == findString && _spec == findSpec )
+ ae = keyElement;
+ else
+ ae = getElement(_s, _spec);
+ if (ae != null){
+ if (_att.isAttribute() && !(_att.getAttribute() instanceof Attribute))
+ return; // should be an error
+ attributesMap.put(ae, _att);
+ }
+ }
+
+ public TypedAttribute findAttribute(AvatarBlock _cmp, String _s){
+ AvatarBlock _comp = _cmp;
+ AvatarElement ae = getElement(_s, _comp);
+ if (ae != null && attributesMap.containsKey(ae)) {
+ TypedAttribute ta = attributesMap.get(ae);
+ return ta;
+ }
+ findString = _s;
+ findComp = _cmp;
+ keyElement = ae;
+ return null;
+ }
+
+ public void addAttribute(AvatarBlock _comp, String _s, TypedAttribute _att){
+ AvatarElement ae;
+ if ( _s == findString && _comp == findComp )
+ ae = keyElement;
+ else
+ ae = getElement(_s, _comp);
+ if (ae != null){
+ if (_att.isAttribute() && !(_att.getAttribute() instanceof Attribute))
+ return; // should be an error
+ attributesMap.put(ae, _att);
+ }
+ }
+
+ public TypedAttribute findAttribute(AvatarBlock _comp, AvatarStateMachineElement _st){
+ AvatarElement _state = (AvatarElement)_st;
+ if (_state != null && attributesMap.containsKey(_state)) {
+ TypedAttribute ta = attributesMap.get(_state);
+ return ta;
+ }
+ return null;
+ }
+
+ public void addAttribute(AvatarBlock _comp, AvatarStateMachineElement _state, TypedAttribute _att) {
+ if (_att == null ||
+ (_att.isAttribute() &&
+ (!(_att.getAttribute() instanceof Attribute) ||
+ !( _att.getAttribute()).isState() ||
+ _state != ( (Attribute)_att.getAttribute()).state
+ )
+ )
+ )
+ return; // should be an error
+ attributesMap.put((AvatarElement) _state, _att);
+ }
+ protected Attribute getAttribute() { return this.new Attribute();}
+ public static AvatarElement getElement(String s, AvatarSpecification spec) {
+ //Extract Block and Attribute
+ String[] splitS;
+ String blockString;
+ String fieldString;
+ AvatarBlock block;
+ int blockIndex;
+
+ if (spec == null) {
+ return null;
+ }
+
+ if (s.matches(".+\\..+")) {
+ splitS = s.split("\\.");
+ blockString = splitS[0];
+ fieldString = splitS[1];
+ } else {
+ return null;
+ }
+
+ block = spec.getBlockWithName(blockString);
+
+ if (block == null) {
+ return null;
+ }
+
+ blockIndex = spec.getBlockIndex(block);
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
+
+ if (attributeIndex == -1) {
+ attributeIndex = block.getIndexOfConstantWithName(fieldString);
+ if (attributeIndex == -1) {
+ // state?
+ return block.getStateMachine().getStateWithName(fieldString);
+ } else {
+ //not created for constants
+ return null;
+ }
+ } else {
+ return block.getAvatarAttributeWithName(fieldString);
+ }
+ }
+
+ public static AvatarElement getElement(String s, AvatarBlock block) {
+ //Extract Attribute
+ if (block == null) {
+ return null;
+ }
+
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
+
+ if (attributeIndex == -1) {
+ attributeIndex = block.getIndexOfConstantWithName(s);
+ if (attributeIndex == -1) {
+ // state?
+ return block.getStateMachine().getStateWithName(s);
+ } else {
+ //not created for constants
+ return null;
+ }
+ } else {
+ return block.getAvatarAttributeWithName(s);
+ }
+ }
+ public class Attribute extends IBSStdAttributeClass<
+ AvatarSpecification,
+ AvatarBlock,
+ AvatarStateMachineElement,
+ SpecificationState,
+ SpecificationBlock
+ >.Attribute {
+
+ // attribute access information
+ private AvatarBlock block;
+ private int blockIndex; // Similar to the one of the block "block".
+ // For performance reason
+ private int accessIndex;
+ private int shift;
+ private int mask;
+
+ protected int initAttribute(AvatarSpecification _spec) {
+
+ //Extract Block and Attribute
+ String[] splitS;
+ String blockString;
+ String fieldString;
+
+ if (_spec == null) {
+ return IBSAttributeTypes.NullAttr;
+ }
+
+ if (s.matches(".+\\..+")) {
+ splitS = s.split("\\.");
+ blockString = splitS[0];
+ fieldString = splitS[1];
+ } else {
+ return IBSAttributeTypes.NullAttr;
+ }
+
+ block = _spec.getBlockWithName(blockString);
+
+ if (block == null) {
+ return IBSAttributeTypes.NullAttr;
+ }
+
+ blockIndex = _spec.getBlockIndex(block);
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
+
+ shift = 0;
+ mask = 0xFFFFFFFF;
+
+ if (attributeIndex == -1) {
+ attributeIndex = block.getIndexOfConstantWithName(fieldString);
+ if (attributeIndex == -1) {
+ // state?
+ state = block.getStateMachine().getStateWithName(fieldString);
+ if (state == null) {
+ return IBSAttributeTypes.NullAttr;
+ }
+ isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ return IBSAttributeTypes.BoolAttr;
+ } else { //constant
+ accessIndex = attributeIndex;
+ AvatarAttribute attr = block.getConstantWithIndex(accessIndex);
+ constantInt = attr.getInitialValueInInt();
+ return (attr.isBool() ? IBSAttributeTypes.BoolConst : IBSAttributeTypes.IntConst);
+ }
+ } else {
+ int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
+ if (offset == -1 || attributeIndex < offset) {
+ 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 + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
+ }
+ return this.attributeType();
+ }
+ }
+
+
+ protected int initAttribute(AvatarBlock _block) {
+
+ //Extract Attribute
+ if (_block == null) {
+ return IBSAttributeTypes.NullAttr;
+ }
+
+ this.block = _block;
+ this.blockIndex = -1; //not initialized
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
+
+ shift = 0;
+ mask = 0xFFFFFFFF;
+
+ if (attributeIndex == -1) {
+ attributeIndex = _block.getIndexOfConstantWithName(s);
+ if (attributeIndex == -1) {
+ // state?
+ state = block.getStateMachine().getStateWithName(s);
+ if (state == null) {
+ return IBSAttributeTypes.NullAttr;
+ }
+ isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ return IBSAttributeTypes.BoolAttr;
+ } else { //constant
+ accessIndex = attributeIndex;
+ AvatarAttribute attr = block.getConstantWithIndex(accessIndex);
+ constantInt = attr.getInitialValueInInt();
+ return (attr.isBool() ? IBSAttributeTypes.BoolConst : IBSAttributeTypes.IntConst);
+ }
+ } else {
+ int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
+ if (offset == -1 || attributeIndex < offset) {
+ 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 + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
+ }
+ return this.attributeType();
+ }
+ }
+
+ protected int initStateAttribute(AvatarBlock _comp) {
+ accessIndex = -1;
+ shift = 0;
+ mask = 0xFFFFFFFF;
+ block = null;
+ return IBSAttributeTypes.BoolAttr;
+ }
+
+ private int attributeType() {
+ if (isState) { // should not happen
+ return IBSAttributeTypes.BoolAttr;
+ }
+ 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 IBSAttributeTypes.BoolAttr;
+ } else {
+ return IBSAttributeTypes.IntAttr;
+ }
+ } else {
+ return IBSAttributeTypes.BoolAttr;
+ }
+ }
+
+
+
+ public String getStateName(AvatarBlock _comp, AvatarStateMachineElement _state){
+ return (_state).getName();
+ }
+
+ public int getValue(SpecificationState _ss) {
+ int value;
+
+ if (isState) {
+ if (_ss.blocks == null || accessIndex == -1) {
+ return 0;
+ }
+ if (_ss.blocks[blockIndex].values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+ return 1;
+ } else {
+ return 0;
+ }
+ }
+
+ value = (_ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
+
+ if (mask > 1 && value > (mask >> 1)) {
+ //convert to negative
+ value = ~((value ^ mask) + 1) + 1;
+ }
+
+ return value;
+ }
+
+
+ public int getValue(SpecificationBlock _sb) {
+ int value;
+
+ if (isState) {
+ if (_sb == null || accessIndex == -1) {
+ return 0;
+ }
+ if (_sb.values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+ return 1;
+ } else {
+ return 0;
+ }
+ }
+
+ value = (_sb.values[accessIndex] >> shift) & mask;
+
+ if (mask > 1 && value > (mask >> 1)) {
+ //convert to negative
+ value = ~((value ^ mask) + 1) + 1;
+ }
+
+ return value;
+ }
+
+ public int getValue(Object _quickstate) {
+ int[] _attributesValues = (int[]) _quickstate;
+ int value;
+
+ if (isState) {
+ return 0;
+ }
+
+ //Cancel offset based on Specification Blocks
+ value = (_attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX] >> shift) & mask;
+
+ if (mask > 1 && value > (mask >> 1)) {
+ //convert to negative
+ value = ~(value ^ mask + 1) + 1;
+ }
+
+ return value;
+ }
+
+ public int getValue(SpecificationState _ss, AvatarStateMachineElement _asme) {
+ int value;
+
+ if (isState) {
+ return (state == _asme) ? 1 : 0;
+ }
+
+ value = (_ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
+
+ if (mask > 1 && value > (mask >> 1)) {
+ //convert to negative
+ value = ~((value ^ mask) + 1) + 1;
+ }
+
+ return value;
+ }
+
+ public void setValue(SpecificationState _ss, int _value) {
+ if (isState) {
+ return;
+ }
+
+ _ss.blocks[blockIndex].values[accessIndex] = (_ss.blocks[blockIndex].values[accessIndex] & (~(mask << shift))) | ((_value & mask) << shift);
+ }
+
+ public void setValue(SpecificationBlock _sb, int _value) {
+ if (isState) {
+ return;
+ }
+ _sb.values[accessIndex] = (_sb.values[accessIndex] & (~(mask << shift))) | ((_value & mask) << shift);
+ }
+
+ public void linkComp(AvatarSpecification spec) {
+ if (blockIndex == -1) {
+ //initialize it
+ blockIndex = spec.getBlockIndex(block);
+ }
+ }
+
+ public void linkState() {
+ if (isState) {
+ if (block != null) {
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = -1;
+ }
+ }
+ }
+
+ }
+ /*===============================================================*/
+ /* uniquement pour test */
+
+ public static boolean containsElementAttribute(AvatarElement ae) {
+ if (attributesMap != null) {
+ return attributesMap.containsKey(ae);
+ } else {
+ return false;
+ }
+ }
+ public static TypedAttribute getElementAttribute(AvatarElement ae) {
+ if (attributesMap != null) {
+ return attributesMap.get(ae);
+ } else {
+ return null;
+ }
+ }
+ public static void addElementAttribute(AvatarElement ae, TypedAttribute aexa) {
+ if (attributesMap == null) {
+ attributesMap = new HashMap<AvatarElement, TypedAttribute>();
+ }
+ attributesMap.put(ae, aexa);
+ }
+ public void clearAttributes(){
+ attributesMap = new HashMap<AvatarElement, TypedAttribute>();
+ }
+}
diff --git a/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdExpressionClass.java b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdExpressionClass.java
new file mode 100644
index 0000000000000000000000000000000000000000..5ff77e511d4c214ef7e6e34d8e087ce80d1d1509
--- /dev/null
+++ b/src/main/java/avatartranslator/intboolsolver2/AvatarIBSStdExpressionClass.java
@@ -0,0 +1,77 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+package avatartranslator.intboolsolver2;
+
+import myutil.intboolsolver2.*;
+
+/**
+ * class IBSStdClosedFormulaAttributeClass is a complete implementation
+ * and instantiation of {@link IBSStdAttributeClass
+ * IBSStdAttributeClass} for closed Formulas.
+ *
+ * <p> It is provided for documentation together with
+ * {@link IBSStdClosedFormulaAttributeClass
+ * IBSStdClosedFormulaAttribute} and
+ * {@link AvatarIBSOriginParser
+ * IBSStdClosedFormulaSolver}}</p>
+ *
+ * <p>These three
+ * classes provides the same features as
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttribute},
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttributeClass} and
+ * {@link IBSClosedFormulaParser
+ * IBSClosedFormulaSolver} (together).</p>
+ *
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public class AvatarIBSStdExpressionClass extends IBSStdExpressionClass<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState
+ > {
+ AvatarIBSStdExpressionClass(){}
+}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
index 8b62c67ed70b38d0ee7ba8f209e5b6af8d20ca87..8508469b8841423b8306e08a551716437d2e5398 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
@@ -54,7 +54,7 @@ import java.util.Vector;
* @author Ludovic APVRILLE
* @version 1.0 31/05/2016
*/
-public class SpecificationBlock implements IBSParamCompState {
+public class SpecificationBlock implements IBSParamCompState, myutil.intboolsolver2.IBSParamCompState {
public static final int HEADER_VALUES = 3;
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 70cd150317cf56994d65f18fa85a7785747822ea..54163b62c7f484fadfb680b9b47f705604a3588b 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -57,7 +57,7 @@ import java.util.LinkedList;
* @version 1.0 31/05/2016
* @author Ludovic APVRILLE
*/
-public class SpecificationState implements IBSParamSpecState, Comparable<SpecificationState> {
+public class SpecificationState implements IBSParamSpecState, Comparable<SpecificationState>, myutil.intboolsolver2.IBSParamSpecState {
public SpecificationBlock [] blocks;
public int hashValue;
public boolean hashComputed;
diff --git a/src/main/java/myutil/intboolsovler2/IBSAttributeClass.java b/src/main/java/myutil/intboolsolver2/IBSAttributeClass.java
similarity index 96%
rename from src/main/java/myutil/intboolsovler2/IBSAttributeClass.java
rename to src/main/java/myutil/intboolsolver2/IBSAttributeClass.java
index 0caeda2d2734265700f69139a14b270678e99ab1..e600f3edb4f9084cfa830faa4602558f1e344e6a 100644
--- a/src/main/java/myutil/intboolsovler2/IBSAttributeClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSAttributeClass.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* class IBSAttribute (interface), describing the "static" generic part
@@ -68,10 +68,9 @@ public class IBSAttributeClass<
public static final int BoolAttr =3; // val is a bool IBSAttribute.
public static final int IntAttr =4; // val is an int IBSAttribute.
public final TypedAttribute NullTypedAttribute = new TypedAttribute();
-
public class TypedAttribute {
- private Attribute attrVal = null;
- private int constVal =0;
+ protected Attribute attrVal = null;
+ protected int constVal =0;
private int type = NullAttr;
private TypedAttribute(){} //intVal=0; attVal=null; type=NullAttr;
public TypedAttribute(int i,boolean isbool) {
@@ -131,7 +130,7 @@ public class IBSAttributeClass<
int getValue(Object _quickstate) { return 0; }
void setValue(SpecState _ss, int _val) {}
void setValue(CompState _cs, int _val) {}
- boolean isState() { return false; }
+ public boolean isState() { return false; }
/**
* links state attributes to their environment (spec, comp).
* If possible... (attributes must have internal information about
@@ -143,7 +142,7 @@ public class IBSAttributeClass<
* If possible... (attributes must have internal information about
* their components). Too specific, to enhance in the future...
*/
- void linkComp(Spec _spec) {}
+ public void linkComp(Spec _spec) {}
public String toString() { return ""; }
}
diff --git a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaAttributeClass.java
similarity index 95%
rename from src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java
rename to src/main/java/myutil/intboolsolver2/IBSClosedFormulaAttributeClass.java
index bb06cfdc380d0a240066e20635d54cccd3b282b9..a09e2ed5d403f26c5d2a57485c50fb06b6725ce0 100644
--- a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaAttributeClass.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* class IBSClosedFormulaAttributeClass is a complete implementation
@@ -53,4 +53,6 @@ public class IBSClosedFormulaAttributeClass extends IBSAttributeClass<
IBSParamComp,
IBSParamState,
IBSParamSpecState,
- IBSParamCompState> {}
+ IBSParamCompState> {
+ IBSClosedFormulaAttributeClass(){}
+}
diff --git a/src/main/java/myutil/intboolsolver2/IBSClosedFormulaExpressionClass.java b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaExpressionClass.java
new file mode 100644
index 0000000000000000000000000000000000000000..0d8cbdab04b98ef0f5e310d8f1be974198b67d76
--- /dev/null
+++ b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaExpressionClass.java
@@ -0,0 +1,58 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+package myutil.intboolsolver2;
+
+/**
+ * class IBSClosedFormulaAttributeClass is a complete implementation
+ * and instantiation of {@link IBSAttributeClass
+ * IBSAttributeClass} for closed Formulas.
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+
+public class IBSClosedFormulaExpressionClass extends IBSOriginExpressionClass<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState> {
+ IBSClosedFormulaExpressionClass(){}
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaParser.java
similarity index 91%
rename from src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java
rename to src/main/java/myutil/intboolsolver2/IBSClosedFormulaParser.java
index 81db89d43403b31b2c40147a3d8ec4f81ee28ed6..bc3cf5c294f0b14814ff02db7ec6bcb8d769ba45 100644
--- a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java
+++ b/src/main/java/myutil/intboolsolver2/IBSClosedFormulaParser.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* class IBSClosedFormulaSolver is a complete implementation
@@ -50,13 +50,13 @@ package myutil.intboolsovler2;
* @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
*/
-public class IBSClosedFormulaSolver extends IBSolver<
+public class IBSClosedFormulaParser extends IBSOriginParser<
IBSParamSpec,
IBSParamComp,
IBSParamState,
IBSParamSpecState,
IBSParamCompState> {
- IBSClosedFormulaSolver() {
- super(new IBSClosedFormulaAttributeClass());
+ IBSClosedFormulaParser() {
+ super(new IBSClosedFormulaAttributeClass(), new IBSClosedFormulaExpressionClass());
}
}
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsovler2/IBSExpressionClass.java b/src/main/java/myutil/intboolsolver2/IBSExpressionClass.java
similarity index 99%
rename from src/main/java/myutil/intboolsovler2/IBSExpressionClass.java
rename to src/main/java/myutil/intboolsolver2/IBSExpressionClass.java
index 9d14b8372cfed589fb8874a533705c7d5bd1cf61..2b1598cb66403db63463c36b5a60ecfeea5665ad 100644
--- a/src/main/java/myutil/intboolsovler2/IBSExpressionClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSExpressionClass.java
@@ -1,4 +1,4 @@
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
public class IBSExpressionClass<
Spec extends IBSParamSpec,
diff --git a/src/main/java/myutil/intboolsovler2/OriginExpr.java b/src/main/java/myutil/intboolsolver2/IBSOriginExpressionClass.java
similarity index 99%
rename from src/main/java/myutil/intboolsovler2/OriginExpr.java
rename to src/main/java/myutil/intboolsolver2/IBSOriginExpressionClass.java
index be48aa5a4e95e0f75bdc0c2b1519c8b46347c2e3..7ef2f9df56abef7e9b16cd7890bac053f7815142 100644
--- a/src/main/java/myutil/intboolsovler2/OriginExpr.java
+++ b/src/main/java/myutil/intboolsolver2/IBSOriginExpressionClass.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
import java.util.ArrayList;
@@ -48,7 +48,7 @@ import java.util.ArrayList;
* @version 0.0 27/02/2023
*/
-public class OriginExpr<
+public class IBSOriginExpressionClass<
Spec extends IBSParamSpec,
Comp extends IBSParamComp,
State extends IBSParamState,
diff --git a/src/main/java/myutil/intboolsovler2/OriginParser.java b/src/main/java/myutil/intboolsolver2/IBSOriginParser.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/OriginParser.java
rename to src/main/java/myutil/intboolsolver2/IBSOriginParser.java
index d39099349b22d9131acaff857078fe7be5d84aea..7ec16628a0d3bf09c46604bf7866bda7b9eba46b 100644
--- a/src/main/java/myutil/intboolsovler2/OriginParser.java
+++ b/src/main/java/myutil/intboolsolver2/IBSOriginParser.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
import myutil.TraceManager;
@@ -51,14 +51,14 @@ import static java.lang.Integer.max;
* {@link myutil.intboolsolver package page}.</p>
*
* <p>For documentation about exported API, see
- * {@link OriginParser IBSolverAPI}</p>
+ * {@link IBSOriginParser IBSolverAPI}</p>
* Creation: 27/02/2023
*
* @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
* @version 0.0 27/02/2023
*/
// IBSExpression<Spec,Comp,State,SpecState,CompState>
-public class OriginParser<
+public class IBSOriginParser<
Spec extends IBSParamSpec,
Comp extends IBSParamComp,
State extends IBSParamState,
@@ -70,13 +70,13 @@ public class OriginParser<
private HashSet<String> badIdents;
private boolean syntaxError = false;
- public OriginParser(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c,
- IBSExpressionClass<Spec,Comp,State,SpecState,CompState> _e){
+ public IBSOriginParser(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c,
+ IBSExpressionClass<Spec,Comp,State,SpecState,CompState> _e){
attC = _c;
exprC = _e;
badIdents = new HashSet<String>();
}
- public OriginParser(){
+ public IBSOriginParser(){
badIdents = new HashSet<String>();
}
public void setAttributeClass(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c){
@@ -229,7 +229,9 @@ public class OriginParser<
attC.getTypedAttribute(_spec, expression);
switch (att.getType()) {
case IBSAttributeClass.NullAttr:
- case IBSAttributeClass.BoolConst: return -1;
+ case IBSAttributeClass.BoolConst:
+ badIdents.add(expression);
+ return -1;
case IBSAttributeClass.IntConst:
return exprC.make_iConst(att.getConstant());
default:
@@ -293,7 +295,9 @@ public class OriginParser<
attC.getTypedAttribute(_comp, expression);
switch (att.getType()) {
case IBSAttributeClass.NullAttr:
- case IBSAttributeClass.BoolConst: return -1;
+ case IBSAttributeClass.BoolConst:
+ badIdents.add(expression);
+ return -1;
case IBSAttributeClass.IntConst:
return exprC.make_iConst(att.getConstant());
default:
@@ -415,6 +419,7 @@ public class OriginParser<
attC.getTypedAttribute(_spec, expression);
switch (att.getType()) {
case IBSAttributeClass.NullAttr:
+ badIdents.add(expression);
return -1;
case IBSAttributeClass.BoolConst:
return exprC.make_bConst((att.getConstant() == 0 ? true : false));
@@ -663,6 +668,7 @@ public class OriginParser<
attC.getTypedAttribute(_comp, expression);
switch (att.getType()) {
case IBSAttributeClass.NullAttr:
+ badIdents.add(expression);
return -1;
case IBSAttributeClass.BoolConst:
return exprC.make_bConst((att.getConstant() == 0 ? true : false));
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamComp.java b/src/main/java/myutil/intboolsolver2/IBSParamComp.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/IBSParamComp.java
rename to src/main/java/myutil/intboolsolver2/IBSParamComp.java
index 065b77466b2f4350659a353e1ea1a85316bbf5bc..027ae882d189cf1a8b82e98b2160542e013a886b 100644
--- a/src/main/java/myutil/intboolsovler2/IBSParamComp.java
+++ b/src/main/java/myutil/intboolsolver2/IBSParamComp.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Interface IBSParamComp, to be implemented by classes intended to
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamCompState.java b/src/main/java/myutil/intboolsolver2/IBSParamCompState.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/IBSParamCompState.java
rename to src/main/java/myutil/intboolsolver2/IBSParamCompState.java
index 9ee8a1b7e7f6eea702eacb775caa8d00b4f2d28f..2e364ed4dbf88fc4272347bf7c8f67dd91746245 100644
--- a/src/main/java/myutil/intboolsovler2/IBSParamCompState.java
+++ b/src/main/java/myutil/intboolsolver2/IBSParamCompState.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Interface IBSParamCompState, to be implemented by classes intended to
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamSpec.java b/src/main/java/myutil/intboolsolver2/IBSParamSpec.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/IBSParamSpec.java
rename to src/main/java/myutil/intboolsolver2/IBSParamSpec.java
index 6e95b7dd5365c871972678d3af5a3d012de32181..19db445707b592e2565dab81fe73e918b658f226 100644
--- a/src/main/java/myutil/intboolsovler2/IBSParamSpec.java
+++ b/src/main/java/myutil/intboolsolver2/IBSParamSpec.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Interface IBSParamSpec, to be implemented by classes intended to
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamSpecState.java b/src/main/java/myutil/intboolsolver2/IBSParamSpecState.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/IBSParamSpecState.java
rename to src/main/java/myutil/intboolsolver2/IBSParamSpecState.java
index 70d17cd7e928f07d872d4aa618baf56b675efaaa..4f7d208591817617d53d7e794e496271c087ff9b 100644
--- a/src/main/java/myutil/intboolsovler2/IBSParamSpecState.java
+++ b/src/main/java/myutil/intboolsolver2/IBSParamSpecState.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Interface IBSParamSpecState, to be implemented by classes intended to
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamState.java b/src/main/java/myutil/intboolsolver2/IBSParamState.java
similarity index 98%
rename from src/main/java/myutil/intboolsovler2/IBSParamState.java
rename to src/main/java/myutil/intboolsolver2/IBSParamState.java
index a97c7143feb31c1f18a84b41a85a28f07dcb7756..2a061cb955251f866551cda1f43c204c98ffd692 100644
--- a/src/main/java/myutil/intboolsovler2/IBSParamState.java
+++ b/src/main/java/myutil/intboolsolver2/IBSParamState.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Interface IBSParamState, to be implemented by classes intended to
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java b/src/main/java/myutil/intboolsolver2/IBSStdAttributeClass.java
similarity index 96%
rename from src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java
rename to src/main/java/myutil/intboolsolver2/IBSStdAttributeClass.java
index f581662f5f55593f38255af1424431204189411e..ef201b9f0dc8781838201c48b1a3150a671961f1 100644
--- a/src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSStdAttributeClass.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* Abstract Class IBSStdAttributeClass, partially
@@ -161,13 +161,20 @@ public class IBSStdAttributeClass<
*/
public String getStateName(Comp _comp, State _state) { return ""; }
-
+ /**
+ * Call to default Attribute constructor to override in subclasses.
+ *
+ * <p> Overriding this method in subclasses (with exactly the same code)
+ * allows to obtain instances of the subclasses when getTypedAttribute
+ * is called from these subclasses.</p>
+ * @return a new fresh instance of Attribute (call default constructor)
+ */
+ protected Attribute getAttribute() { return this.new Attribute();}
// The three following getTypesAttribute methods are fully implemented and do not need to be overriden.
-
public final IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute getTypedAttribute(Spec _spec, String _s) {
IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute a = findAttribute(_spec, _s);
if (a == null) {
- IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = new Attribute(); // replaced...
+ IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = getAttribute();
x.classInitAttribute(_spec,_s);
switch (x.getType()) {
case IBSAttributeClass.NullAttr: {
@@ -196,7 +203,7 @@ public class IBSStdAttributeClass<
public final IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute getTypedAttribute(Comp _comp, String _s) {
IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute a = findAttribute(_comp, _s);
if (a == null) {
- IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = new Attribute(); // replaced...
+ IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = getAttribute();
x.classInitAttribute(_comp,_s);
switch (x.getType()) {
case IBSAttributeClass.NullAttr: {
@@ -225,7 +232,7 @@ public class IBSStdAttributeClass<
public final IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute getTypedAttribute(Comp _comp, State _state) {
IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute a = findAttribute(_comp, _state);
if (a == null) {
- IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = new Attribute(); // replaced...
+ IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute x = getAttribute();
x.classInitAttribute(_comp,_state);
switch (x.getType()) {
case IBSAttributeClass.NullAttr: {
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaAttributeClass.java
similarity index 95%
rename from src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java
rename to src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaAttributeClass.java
index d35603ec97d63f81e11796fdbba4f0af12c569ad..0d47f71bfc44542d7835476fb412ac5ec65d5de3 100644
--- a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaAttributeClass.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* class IBSStdClosedFormulaAttributeClass is a complete implementation
@@ -44,9 +44,9 @@ package myutil.intboolsovler2;
* IBSStdAttributeClass} for closed Formulas.
*
* <p> It is provided for documentation together with
- * {@link IBSStdClosedFormulaAttribute
+ * {@link IBSStdClosedFormulaAttributeClass
* IBSStdClosedFormulaAttribute} and
- * {@link IBSStdClosedFormulaSolver
+ * {@link IBSStdClosedFormulaParser
* IBSStdClosedFormulaSolver}}</p>
*
* <p>These three
@@ -55,7 +55,7 @@ package myutil.intboolsovler2;
* IBSClosedFormulaAttribute},
* {@link IBSClosedFormulaAttributeClass
* IBSClosedFormulaAttributeClass} and
- * {@link IBSClosedFormulaSolver
+ * {@link IBSClosedFormulaParser
* IBSClosedFormulaSolver} (together).</p>
*
* Creation: 07/03/2023
diff --git a/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaExpressionClass.java b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaExpressionClass.java
new file mode 100644
index 0000000000000000000000000000000000000000..f0313d5981fcc8e60dbd46b8f4a63efa27bef95a
--- /dev/null
+++ b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaExpressionClass.java
@@ -0,0 +1,75 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+package myutil.intboolsolver2;
+
+/**
+ * class IBSStdClosedFormulaAttributeClass is a complete implementation
+ * and instantiation of {@link IBSStdAttributeClass
+ * IBSStdAttributeClass} for closed Formulas.
+ *
+ * <p> It is provided for documentation together with
+ * {@link IBSStdClosedFormulaAttribute
+ * IBSStdClosedFormulaAttribute} and
+ * {@link IBSStdClosedFormulaParser
+ * IBSStdClosedFormulaSolver}}</p>
+ *
+ * <p>These three
+ * classes provides the same features as
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttribute},
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttributeClass} and
+ * {@link IBSClosedFormulaParserIBS
+ * IBSClosedFormulaSolver} (together).</p>
+ *
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public class IBSStdClosedFormulaExpressionClass extends IBSStdExpressionClass<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState
+ > {
+ IBSStdClosedFormulaExpressionClass(){}
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaParser.java
similarity index 89%
rename from src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java
rename to src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaParser.java
index 166da22a8a70854bf7bf45f4a3dc2761c97a9cce..d8f1a95ed92f87611c3cd210e92ee7cdac450ad5 100644
--- a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java
+++ b/src/main/java/myutil/intboolsolver2/IBSStdClosedFormulaParser.java
@@ -36,11 +36,11 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
/**
* class IBSStdClosedFormulaSolver is a complete implementation
- * and instantiation of {@link IBSolver
+ * and instantiation of {@link IBSOriginParser
* IBSolver} for closed Formulas.
*
* <p> It is provided for documentation together with
@@ -55,7 +55,7 @@ package myutil.intboolsovler2;
* IBSClosedFormulaAttribute},
* {@link IBSClosedFormulaAttributeClass
* IBSClosedFormulaAttributeClass} and
- * {@link IBSClosedFormulaSolver
+ * {@link IBSClosedFormulaParser
* IBSClosedFormulaSolver} (together).</p>
*
* Creation: 07/03/2023
@@ -64,13 +64,13 @@ package myutil.intboolsovler2;
* @author Sophie Coudert
*/
-public class IBSStdClosedFormulaSolver extends IBSolver<
+public class IBSStdClosedFormulaParser extends IBSOriginParser<
IBSParamSpec,
IBSParamComp,
IBSParamState,
IBSParamSpecState,
IBSParamCompState> {
- IBSStdClosedFormulaSolver() {
- super(new IBSClosedFormulaAttributeClass());
+ IBSStdClosedFormulaParser() {
+ super(new IBSStdClosedFormulaAttributeClass(), new IBSStdClosedFormulaExpressionClass());
}
}
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java b/src/main/java/myutil/intboolsolver2/IBSStdExpressionClass.java
similarity index 99%
rename from src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java
rename to src/main/java/myutil/intboolsolver2/IBSStdExpressionClass.java
index 7f600d69444c0f25b29aca94c8214da7b9b25d60..348c1d07e45c0c43f4eb31d0c714b503c25e8c31 100644
--- a/src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java
+++ b/src/main/java/myutil/intboolsolver2/IBSStdExpressionClass.java
@@ -1,4 +1,4 @@
-package myutil.intboolsovler2;
+package myutil.intboolsolver2;
import java.util.ArrayList;
diff --git a/src/main/java/myutil/intboolsovler2/package-info.java b/src/main/java/myutil/intboolsolver2/package-info.java
similarity index 99%
rename from src/main/java/myutil/intboolsovler2/package-info.java
rename to src/main/java/myutil/intboolsolver2/package-info.java
index 2082c23b60cdc6c523cd5fc8d261a6bb299a5a1b..62c015aeddeb98b76e1ca51c18a9472ca7ca7122 100644
--- a/src/main/java/myutil/intboolsovler2/package-info.java
+++ b/src/main/java/myutil/intboolsolver2/package-info.java
@@ -251,4 +251,4 @@
*
* @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
*/
- package myutil.intboolsovler2;
\ No newline at end of file
+ package myutil.intboolsolver2;
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsovler2/IBSolver.java b/src/main/java/myutil/intboolsovler2/IBSolver.java
deleted file mode 100644
index b091e88407b4aa84899a115baeb2a775897cc4ed..0000000000000000000000000000000000000000
--- a/src/main/java/myutil/intboolsovler2/IBSolver.java
+++ /dev/null
@@ -1,1051 +0,0 @@
-/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- */
-
-package myutil.intboolsovler2;
-
-import java.util.HashSet;
-
-/**
- * Class IBSolver implements the generic solver.
- *
- * <p>For general information about the solver, see
- * {@link myutil.intboolsolver package page}.</p>
- *
- * <p>For documentation about exported API, see
- * {@link IBSolver IBSolverAPI}</p>
- * Creation: 27/02/2023
- *
- * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
- * @version 0.0 27/02/2023
- */
-
-public class IBSolver <
- Spec extends IBSParamSpec,
- Comp extends IBSParamComp,
- State extends IBSParamState,
- SpecState extends IBSParamSpecState,
- CompState extends IBSParamCompState
- > {
- public static final int IMMEDIATE_NO = 0;
- public static final int IMMEDIATE_INT = 1;
- public static final int IMMEDIATE_BOOL = 2;
- public IBSAttributeClass<Spec,Comp,State,SpecState,CompState> attC; // Attribute Class
- private HashSet<String> freeIdents;
-
- public IBSolver(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c){
- attC = _c;
- freeIdents = new HashSet<String>();
- }
- public IBSolver(){
- freeIdents = new HashSet<String>();
- }
- public void setAttributeClass(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c){
- attC = _c;
- }
- public IBSAttributeClass<Spec,Comp,State,SpecState,CompState> getAttributeClass(){ return attC; }
- public HashSet<String> getFreeIdents() {
- return freeIdents;
- }
- public void clearFreeIdents() {
- freeIdents = new HashSet<String>();
- }
-
- public class Expr {
- private Expr left, right;
- private char operator;
- private String expression;
- private boolean isLeaf; //variable
- private boolean isNot;
- private boolean isNegated;
- private int isImmediateValue; //0: No; 1: Int; 2: Boolean;
- private int intValue;
- private IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute leaf;
-
- public Expr() {
- left = null;
- right = null;
- isLeaf = true;
- isImmediateValue = IMMEDIATE_NO;
- intValue = 0;
- }
-
- public Expr(String expression) {
- //TraceManager.addDev("Making from expression");
- this.expression = expression.trim();
- removeUselessBrackets();
- replaceOperators();
- left = null;
- right = null;
- isLeaf = true;
- isImmediateValue = IMMEDIATE_NO;
- intValue = 0;
- isNot = false;
- isNegated = false;
- }
-
- public void setExpression(String expression) {
- this.expression = expression;
- replaceOperators();
- }
-
-
- public boolean buildExpression(Spec spec) {
- boolean returnVal;
- freeIdents.clear();
- attC.initBuild(spec);
- returnVal = buildExpressionRec(spec);
-
- if (!returnVal) {
- return false;
- }
- return checkIntegrity();
- }
-
- public boolean buildExpression(Comp _comp) {
- boolean returnVal;
- freeIdents.clear();
- attC.initBuild(_comp);
- returnVal = buildExpressionRec(_comp);
-
- if (!returnVal) {
- return false;
- }
- return checkIntegrity();
- }
-
- public boolean buildExpression() {
- boolean returnVal;
- freeIdents.clear();
- attC.initBuild();
- returnVal = buildExpressionRec();
- if (!returnVal) {
- return false;
- }
-
- return checkIntegrity();
- }
-
- public boolean buildExpression(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _attr) {
- this.expression = _attr.toString();
- isLeaf = true;
- isImmediateValue = IMMEDIATE_NO;
- leaf = _attr;
- return true;
- }
-
-
- public boolean buildExpressionRec(Spec _spec) {
- boolean returnVal;
-
- removeUselessBrackets();
- returnVal = checkNot();
- returnVal &= checkNegated();
- if (!returnVal) return false;
-
- if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
- // leaf
- isLeaf = true;
- if (!checkNegatedNoBrackets()) return false;
- checkNegatedNoBrackets();
- if (expression.equals("true")) {
- intValue = 1;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.equals("false")) {
- intValue = 0;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.matches("-?\\d+")) {
- intValue = Integer.parseInt(expression);
- isImmediateValue = IMMEDIATE_INT;
- return true;
- } else {
- IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
- attC.getTypedAttribute(_spec, expression);
- switch (att.getType()) {
- case IBSAttributeClass.NullAttr: {
- return false;
- }
- case IBSAttributeClass.BoolConst: {
- intValue = att.getConstant();
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- }
- case IBSAttributeClass.IntConst: {
- intValue = att.getConstant();
- isImmediateValue = IMMEDIATE_INT;
- return true;
- }
- default: {
- leaf = att.getAttribute();
- return true;
- }
- }
- }
- }
-
- isLeaf = false;
-
- int index = getOperatorIndex();
-
- if (index == -1) {
- return false;
- }
-
- operator = expression.charAt(index);
-
- //split and recur
- String leftExpression = expression.substring(0, index).trim();
- String rightExpression = expression.substring(index + 1, expression.length()).trim();
-
- left = new Expr(leftExpression);
- right = new Expr(rightExpression);
- returnVal = left.buildExpressionRec(_spec);
- returnVal &= right.buildExpressionRec(_spec);
-
- return returnVal;
- }
-
- public boolean buildExpressionRec(Comp _comp) {
- boolean returnVal;
-
- removeUselessBrackets();
- returnVal = checkNot();
- returnVal &= checkNegated();
-
- if (!returnVal) return false;
-
- if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
- // leaf
- isLeaf = true;
- checkNegatedNoBrackets();
- if (expression.equals("true")) {
- intValue = 1;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.equals("false")) {
- intValue = 0;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.matches("-?\\d+")) {
- intValue = Integer.parseInt(expression);
- isImmediateValue = IMMEDIATE_INT;
- return true;
- } else {
- IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
- attC.getTypedAttribute(_comp, expression);
- switch (att.getType()) {
- case IBSAttributeClass.NullAttr: {
- return false;
- }
- case IBSAttributeClass.BoolConst: {
- intValue = att.getConstant();
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- }
- case IBSAttributeClass.IntConst: {
- intValue = att.getConstant();
- isImmediateValue = IMMEDIATE_INT;
- return true;
- }
- default: {
- leaf = att.getAttribute();
- return true;
- }
- }
- }
- }
- isLeaf = false;
-
- int index = getOperatorIndex();
-
- if (index == -1) {
- return false;
- }
-
- operator = expression.charAt(index);
-
- //split and recur
- String leftExpression = expression.substring(0, index).trim();
- String rightExpression = expression.substring(index + 1, expression.length()).trim();
- left = new Expr(leftExpression);
- right = new Expr(rightExpression);
- returnVal = left.buildExpressionRec(_comp);
- returnVal &= right.buildExpressionRec(_comp);
-
- return returnVal;
- }
-
-
- public boolean buildExpressionRec() {
- boolean returnVal;
-
- removeUselessBrackets();
- returnVal = checkNot();
- returnVal &= checkNegated();
-
- if (!returnVal) return false;
-
- if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
- // leaf
- isLeaf = true;
- checkNegatedNoBrackets();
- if (expression.equals("true")) {
- intValue = 1;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.equals("false")) {
- intValue = 0;
- isImmediateValue = IMMEDIATE_BOOL;
- return true;
- } else if (expression.matches("-?\\d+")) {
- intValue = Integer.parseInt(expression);
- isImmediateValue = IMMEDIATE_INT;
- return true;
- } else {
- return false;
- }
- }
-
- isLeaf = false;
-
-
- int index = getOperatorIndex();
-
- if (index == -1) {
- return false;
- }
-
- operator = expression.charAt(index);
-
- //split and recur
- String leftExpression = expression.substring(0, index).trim();
- String rightExpression = expression.substring(index + 1, expression.length()).trim();
-
- left = new Expr(leftExpression);
- right = new Expr(rightExpression);
-
- returnVal = left.buildExpressionRec();
- returnVal &= right.buildExpressionRec();
-
- return returnVal;
- }
-
- private void replaceOperators() {
- expression = expression.replaceAll("\\|\\|", "\\|").trim();
- expression = expression.replaceAll("&&", "&").trim();
- expression = expression.replaceAll("==", "=").trim();
- expression = expression.replaceAll("!=", "\\$").trim();
- expression = expression.replaceAll(">=", ":").trim();
- expression = expression.replaceAll("<=", ";").trim();
- expression = expression.replaceAll("\\bor\\b", "\\|").trim();
- expression = expression.replaceAll("\\band\\b", "&").trim();
- //expression.replaceAll("\\btrue\\b", "t").trim();
- //expression.replaceAll("\\bfalse\\b", "f").trim();
- }
-
- private boolean checkNot() {
- boolean notStart1, notStart2;
-
- notStart1 = expression.startsWith("not(");
- notStart2 = expression.startsWith("!(");
-
- while (notStart1 || notStart2) {
- if (notStart1) {
- //not bracket must be closed in the last char
- int closingIndex = getClosingBracket(4);
-
- if (closingIndex == -1) {
- return false;
- }
- if (closingIndex == expression.length() - 1) {
- //not(expression)
- isNot = !isNot;
- expression = expression.substring(4, expression.length() - 1).trim();
- } else {
- return true;
- }
- } else if (notStart2) {
- int closingIndex = getClosingBracket(2);
-
- if (closingIndex == -1) {
- return false;
- }
- if (closingIndex == expression.length() - 1) {
- //not(expression)
- isNot = !isNot;
- expression = expression.substring(2, expression.length() - 1).trim();
- } else {
- return true;
- }
- }
- notStart1 = expression.startsWith("not(");
- notStart2 = expression.startsWith("!(");
- }
- return true;
- }
-
- private boolean checkNegated() {
- while (expression.startsWith("-(")) {
- //not bracket must be closed in the last char
- int closingIndex = getClosingBracket(2);
-
- if (closingIndex == -1) {
- return false;
- }
- if (closingIndex == expression.length() - 1) {
- //-(expression)
- isNegated = !isNegated;
- expression = expression.substring(2, expression.length() - 1).trim();
- } else {
- return true;
- }
- }
- return true;
- }
-
- private boolean checkNegatedNoBrackets() {
- if (expression.startsWith("-")) {
- isNegated = true;
- expression = expression.substring(1, expression.length()).trim();
- }
- return true;
- }
-
- private int getOperatorIndex() {
- int index;
- // find the last executed operator
- int i, level, priority;
- boolean subVar = true; //when a subtraction is only one one variable
- char a;
- level = 0;
- priority = 0;
- for (i = 0, index = -1; i < expression.length(); i++) {
- a = expression.charAt(i);
- switch (a) {
- case '|':
- if (level == 0) {
- index = i;
- priority = 5;
- }
- break;
- case '&':
- if (level == 0 && priority < 5) {
- index = i;
- priority = 4;
- }
- break;
- case '=':
- if (level == 0 && priority < 4) {
- index = i;
- priority = 3;
- }
- subVar = true;
- break;
- case '$':
- if (level == 0 && priority < 4) {
- index = i;
- priority = 3;
- }
- subVar = true;
- break;
- case '<':
- if (level == 0 && priority < 3) {
- index = i;
- priority = 2;
- }
- subVar = true;
- break;
- case '>':
- if (level == 0 && priority < 3) {
- index = i;
- priority = 2;
- }
- subVar = true;
- break;
- case ':':
- if (level == 0 && priority < 3) {
- index = i;
- priority = 2;
- }
- subVar = true;
- break;
- case ';':
- if (level == 0 && priority < 3) {
- index = i;
- priority = 2;
- }
- subVar = true;
- break;
- case '-':
- if (level == 0 && !subVar && priority < 2) {
- index = i;
- priority = 1;
- }
- break;
- case '+':
- if (level == 0 && !subVar && priority < 2) {
- index = i;
- priority = 1;
- }
- break;
- case '/':
- if (level == 0 && priority == 0) {
- index = i;
- }
- break;
- case '*':
- if (level == 0 && priority == 0) {
- index = i;
- }
- break;
- case '(':
- level++;
- subVar = true;
- break;
- case ')':
- level--;
- subVar = false;
- break;
- case ' ':
- break;
- default:
- subVar = false;
- break;
- }
- }
- return index;
- }
-
-
- public int getResult() {
- int res;
- if (isLeaf) {
- if (isImmediateValue != IMMEDIATE_NO) {
- res = intValue;
- } else {
- return 0;
- }
- } else {
- res = getChildrenResult(left.getResult(), right.getResult());
- }
-
- if (isNot) {
- res = (res == 0) ? 1 : 0;
- } else if (isNegated) {
- res = -res;
- }
- return res;
- }
-
- public int getResult(SpecState _ss) {
- int res;
- if (isLeaf) {
- if (isImmediateValue != IMMEDIATE_NO) {
- res = intValue;
- } else {
- res = leaf.getValue(_ss);
- }
- } else {
- res = getChildrenResult(left.getResult(_ss), right.getResult(_ss));
- }
-
- if (isNot) {
- res = (res == 0) ? 1 : 0;
- } else if (isNegated) {
- res = -res;
- }
- return res;
- }
-
- public int getResult(SpecState _ss, State _st) {
- int res;
- if (isLeaf) {
- if (isImmediateValue != IMMEDIATE_NO) {
- res = intValue;
- } else {
- res = leaf.getValue(_ss, _st);
- }
- } else {
- res = getChildrenResult(left.getResult(_ss, _st), right.getResult(_ss, _st));
- }
-
- if (isNot) {
- res = (res == 0) ? 1 : 0;
- } else if (isNegated) {
- res = -res;
- }
- return res;
- }
-
- public int getResult(CompState _cs) {
- int res;
- if (isLeaf) {
- if (isImmediateValue != IMMEDIATE_NO) {
- res = intValue;
- } else {
- res = leaf.getValue(_cs);
- }
- } else {
- res = getChildrenResult(left.getResult(_cs), right.getResult(_cs));
- }
-
- if (isNot) {
- res = (res == 0) ? 1 : 0;
- } else if (isNegated) {
- res = -res;
- }
- return res;
- }
-
- public int getResult(Object _qs) {
- int res;
- if (isLeaf) {
- if (isImmediateValue != IMMEDIATE_NO) {
- res = intValue;
- } else {
- res = leaf.getValue(_qs);
- }
- } else {
- res = getChildrenResult(left.getResult(_qs), right.getResult(_qs));
- }
-
- if (isNot) {
- res = (res == 0) ? 1 : 0;
- } else if (isNegated) {
- res = -res;
- }
- return res;
- }
-
- private int getChildrenResult(int leftV, int rightV) {
- int result;
-
- switch (operator) {
- case '=':
- result = (leftV == rightV) ? 1 : 0;
- break;
- case '$':
- result = (leftV != rightV) ? 1 : 0;
- break;
- case '<':
- result = (leftV < rightV) ? 1 : 0;
- break;
- case '>':
- result = (leftV > rightV) ? 1 : 0;
- break;
- case ':':
- result = (leftV >= rightV) ? 1 : 0;
- break;
- case ';':
- result = (leftV <= rightV) ? 1 : 0;
- break;
- case '-':
- result = leftV - rightV;
- break;
- case '+':
- result = leftV + rightV;
- break;
- case '|':
- result = (leftV == 0 && rightV == 0) ? 0 : 1;
- break;
- case '/':
- result = leftV / rightV;
- break;
- case '*':
- result = leftV * rightV;
- break;
- case '&':
- result = (leftV == 0 || rightV == 0) ? 0 : 1;
- break;
- default:
- //System.out.println("Error in EquationSolver::getResult");
- result = 0;
- break;
- }
- //System.out.println(leftV + " " + operator + " " + rightV + " = " + result);
- return result;
- }
-
- public String toString() {
- String retS;
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- retS = leaf.toString();
- } else if (isImmediateValue == IMMEDIATE_INT) {
- retS = String.valueOf(intValue);
- } else {
- if (intValue == 0) {
- retS = "false";
- } else {
- retS = "true";
- }
- }
- if (isNegated) {
- retS = "-(" + retS + ")";
- }
- if (isNot) {
- retS = "not(" + retS + ")";
- }
- } else {
- String leftString = left.toString();
- String rightString = right.toString();
- String opString;
- switch (operator) {
- case '=':
- opString = "==";
- break;
- case '$':
- opString = "!=";
- break;
- case ':':
- opString = ">=";
- break;
- case ';':
- opString = "<=";
- break;
- case '|':
- opString = "||";
- break;
- case '&':
- opString = "&&";
- break;
- default:
- opString = "" + operator;
- break;
- }
- retS = "(" + leftString + " " + opString + " " + rightString + ")";
- if (isNegated) {
- retS = "-" + retS;
- }
- if (isNot) {
- retS = "not" + retS;
- }
- }
- return retS;
- }
-
- public boolean hasState() {
- boolean hasState;
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- return leaf.isState();
- } else {
- return false;
- }
- } else {
- hasState = left.hasState();
- hasState |= right.hasState();
- return hasState;
- }
- }
-
- //!! replaces setBlockIndex(AvatarSpecification spec)
- public void linkComp(Spec spec) {
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- leaf.linkComp(spec);
- }
- } else {
- left.linkComp(spec);
- right.linkComp(spec);
- }
- }
-
- public void linkStates() {
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- leaf.linkState();
- }
- } else {
- left.linkStates();
- right.linkStates();
- }
- }
-
- private boolean checkIntegrity() {
- int optype, optypel, optyper;
- boolean returnVal;
-
- if (isLeaf) {
- if (isNot) {
- return getReturnType() == IMMEDIATE_BOOL;
- } else if (isNegated) {
- return getReturnType() == IMMEDIATE_INT;
- } else {
- return true;
- }
- }
-
- optype = getType();
- optypel = left.getReturnType();
- optyper = right.getReturnType();
-
- switch (optype) {
- case IMMEDIATE_NO:
- returnVal = false; //Error
- break;
- case IMMEDIATE_INT:
- returnVal = (optypel == IMMEDIATE_INT && optyper == IMMEDIATE_INT) ? true : false;
- break;
- case IMMEDIATE_BOOL:
- returnVal = (optypel == IMMEDIATE_BOOL && optyper == IMMEDIATE_BOOL) ? true : false;
- break;
- case 3:
- returnVal = (optypel == optyper) ? true : false;
- break;
- default:
- returnVal = false;
- }
-
- if (returnVal == false) {
- return false;
- }
-
- returnVal = left.checkIntegrity();
- returnVal &= right.checkIntegrity();
-
- return returnVal;
- }
-
- private void removeUselessBrackets() {
- //TraceManager.addDev("Removing first / final brackets");
- while (expression.startsWith("(") && expression.endsWith(")")) {
- if (getClosingBracket(1) == expression.length() - 1) {
- expression = expression.substring(1, expression.length() - 1).trim();
- } else {
- break;
- }
- }
-
- //TraceManager.addDev("Removing dual brackets");
- // Removing duplicate brackets
- // typically ((x)) -> (x)
- // Parse expression step by step, search for "((" schemes and look for corresponding brackets
- for (int i = 0; i < expression.length() - 2; i++) {
- String s1 = expression.substring(i, i + 1);
- if (s1.startsWith("(")) {
- String s2 = expression.substring(i + 1, i + 2);
- if (s2.startsWith("(")) {
- //TraceManager.addDev("Found dual at i=" + i);
- int index1 = getClosingBracket(i + 1);
- int index2 = getClosingBracket(i + 2);
- //TraceManager.addDev("Found dual at i=" + i + " index1=" + index1 + " index2=" + index2 + " expr=" + expression);
- if (index1 == index2 + 1) {
- // Two following brackets. We can remove one of them
- //TraceManager.addDev("old expression:" + expression);
- expression = expression.substring(0, i + 1) + expression.substring(i + 2, index2) + expression.substring(index1);
- //TraceManager.addDev("new expression:" + expression);
- }
- }
- }
- }
- }
-
- private int getClosingBracket(int startChar) {
- int level = 0;
- char a;
- for (int i = startChar; i < expression.length(); i++) {
- a = expression.charAt(i);
- if (a == ')') {
- if (level == 0) {
- return i;
- } else {
- level--;
- }
- } else if (a == '(') {
- level++;
- }
- }
- return -1;
- }
- public final int getAttributeType(int type) {
- switch (type) {
- case IBSAttributeClass.BoolConst:
- case IBSAttributeClass.BoolAttr: return IBSolver.IMMEDIATE_BOOL;
- case IBSAttributeClass.IntConst:
- case IBSAttributeClass.IntAttr: return IBSolver.IMMEDIATE_INT;
- default: return IBSolver.IMMEDIATE_NO;
- }
- }
-
- private int getType() {
- int optype;
-
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- return getAttributeType(leaf.getType());
- } else {
- return isImmediateValue;
- }
- }
-
- switch (operator) {
- case '=':
- case '$':
- optype = 3; //BOTH sides must have the same type
- break;
- case '<':
- case '>':
- case ':':
- case ';':
- case '-':
- case '+':
- case '/':
- case '*':
- optype = IMMEDIATE_INT;
- break;
- case '|':
- case '&':
- optype = IMMEDIATE_BOOL;
- break;
- default:
- optype = IMMEDIATE_NO; //ERROR
- break;
- }
-
- return optype;
- }
-
- public int getReturnType() {
- int optype;
-
- if (isLeaf) {
- if (isImmediateValue == IMMEDIATE_NO) {
- return getAttributeType(leaf.getType());
- } else {
- return isImmediateValue;
- }
- }
-
- switch (operator) {
- case '-':
- case '+':
- case '/':
- case '*':
- optype = IMMEDIATE_INT;
- break;
- case '|':
- case '&':
- case '=':
- case '$':
- case '<':
- case '>':
- case ':':
- case ';':
- optype = IMMEDIATE_BOOL;
- break;
- default:
- optype = IMMEDIATE_NO; //ERROR
- break;
- }
-
- return optype;
- }
-
- }
- //!! A Deplacer ailleurs !!!!!!!!!!! methode statique
- public int indexOfVariable(String expr, String variable) {
- int index;
- String tmp = expr;
- int removed = 0;
- //System.out.println("\nHandling expr: " + expr);
-
- while ((index = tmp.indexOf(variable)) > -1) {
- char c1, c2;
- if (index > 0) {
- c1 = tmp.charAt(index - 1);
- } else {
- c1 = ' ';
- }
-
- if (index + variable.length() < tmp.length())
- c2 = tmp.charAt(index + variable.length());
- else
- c2 = ' ';
-
- //System.out.println("tmp=" + tmp + " c1=" + c1 + " c2=" + c2);
-
- if (!(Character.isLetterOrDigit(c1) || (c1 == '_'))) {
- if (!(Character.isLetterOrDigit(c2) || (c2 == '_'))) {
- //System.out.println("Found at index=" + index + " returnedIndex=" + (index+removed));
- return index + removed;
- }
- }
- tmp = tmp.substring(index + variable.length(), tmp.length());
- //System.out.println("tmp=" + tmp);
- removed = index + variable.length();
- if (tmp.length() == 0) {
- return -1;
- }
- // We cut until we find a non alphanumerical character
- while (Character.isLetterOrDigit(tmp.charAt(0)) || (tmp.charAt(0) == '_')) {
- tmp = tmp.substring(1, tmp.length());
- if (tmp.length() == 0) {
- return -1;
- }
- removed++;
- }
- //System.out.println("after remove: tmp=" + tmp);
-
- }
- return -1;
- }
-
- //!! A Deplacer ailleurs !!!!!!!!!!! methode statique
- public String replaceVariable(String expr, String oldVariable, String newVariable) {
- if (oldVariable.compareTo(newVariable) == 0) {
- return expr;
- }
- int index;
- String tmp = expr;
-
- while ((index = indexOfVariable(tmp, oldVariable)) > -1) {
- String tmp1 = "";
- if (index > 0) {
- tmp1 = tmp.substring(0, index);
- }
- tmp1 += newVariable;
- tmp1 += tmp.substring(index + oldVariable.length(), tmp.length());
- tmp = tmp1;
- }
-
- return tmp;
- }
-
-}