From 2591916226ee77eedbcd1d4dfc84fbeeeddff3b5 Mon Sep 17 00:00:00 2001
From: Sophie Coudert <sophie.coudert@telecom-paris.fr>
Date: Mon, 13 Mar 2023 19:51:13 +0100
Subject: [PATCH] restructuring in progress in myutil.intboolsolver2
---
.../intboolsovler2/IBSAttributeClass.java | 151 +++
.../IBSClosedFormulaAttributeClass.java | 56 +
.../IBSClosedFormulaSolver.java | 62 +
.../IBSExpr.java | 183 ++-
.../myutil/intboolsovler2/IBSExpression.java | 43 +
.../myutil/intboolsovler2/IBSParamComp.java | 58 +
.../intboolsovler2/IBSParamCompState.java | 58 +
.../myutil/intboolsovler2/IBSParamSpec.java | 58 +
.../intboolsovler2/IBSParamSpecState.java | 57 +
.../myutil/intboolsovler2/IBSParamState.java | 58 +
.../intboolsovler2/IBSStdAttributeClass.java | 389 ++++++
.../IBSStdClosedFormulaAttributeClass.java | 75 ++
.../IBSStdClosedFormulaSolver.java | 76 ++
.../java/myutil/intboolsovler2/IBSolver.java | 1051 +++++++++++++++++
.../myutil/intboolsovler2/package-info.java | 254 ++++
15 files changed, 2606 insertions(+), 23 deletions(-)
create mode 100644 src/main/java/myutil/intboolsovler2/IBSAttributeClass.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java
rename src/main/java/myutil/{intboolsolver => intboolsovler2}/IBSExpr.java (67%)
create mode 100644 src/main/java/myutil/intboolsovler2/IBSExpression.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSParamComp.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSParamCompState.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSParamSpec.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSParamSpecState.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSParamState.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java
create mode 100644 src/main/java/myutil/intboolsovler2/IBSolver.java
create mode 100644 src/main/java/myutil/intboolsovler2/package-info.java
diff --git a/src/main/java/myutil/intboolsovler2/IBSAttributeClass.java b/src/main/java/myutil/intboolsovler2/IBSAttributeClass.java
new file mode 100644
index 0000000000..0caeda2d27
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSAttributeClass.java
@@ -0,0 +1,151 @@
+/* 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;
+
+/**
+ * class IBSAttribute (interface), describing the "static" generic part
+ * shared by all open leaves of {@link IBSolver
+ * IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> This interface describes the features required from the
+ * class of {@link IBSolver IBSolver}
+ * attributes (methods that do not depend on attribute instances).
+ * Its implementations are intended to instantiate
+ * the {@code AtC} parameter of the generic
+ * {@link IBSolver IBSolver} </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+
+public class IBSAttributeClass<
+ Spec extends IBSParamSpec,
+ Comp extends IBSParamComp,
+ State extends IBSParamState,
+ SpecState extends IBSParamSpecState,
+ CompState extends IBSParamCompState
+ > {
+ public static final int NullAttr =0; // val is null
+ public static final int BoolConst =1; // val is an Int integer
+ public static final int IntConst =2; // val is an Int boolean (0 or 1)
+ 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;
+ private int type = NullAttr;
+ private TypedAttribute(){} //intVal=0; attVal=null; type=NullAttr;
+ public TypedAttribute(int i,boolean isbool) {
+ constVal = i;
+ if (isbool) type=BoolConst; else type=IntConst;
+ }
+ public TypedAttribute(Attribute a,boolean isbool) {
+ attrVal = a;
+ if (isbool) type=BoolAttr; else type=IntAttr;
+ }
+ public int getType() { return type; }
+ public int getConstant() { return constVal; }
+ public Attribute getAttribute() { return attrVal; }
+ public boolean isAttribute() { return (type >= BoolAttr); }
+ }
+
+ public TypedAttribute getTypedAttribute(Spec _spec, String _s) {
+ return NullTypedAttribute;
+ }
+ public TypedAttribute getTypedAttribute(Comp _comp, String _s) {
+ return NullTypedAttribute;
+ }
+ public TypedAttribute getTypedAttribute(Comp _comp, State _st) {
+ return NullTypedAttribute;
+ }
+ /**
+ * Initialisation before parsing an expression.
+ *
+ * <p> Automatically called by {@code buildExpression(Spec _spec)} </p>
+ * @param _spec the specification that associates structures to open
+ * leaves
+ */
+ public void initBuild(Spec _spec){}
+ /**
+ * Initialisation before parsing an expression.
+ *
+ * <p> Automatically called by {@code buildExpression(Comp _comp)} </p>
+ * @param _comp the component that associates structures to open
+ * leaves
+ */
+ public void initBuild(Comp _comp){}
+ /**
+ * Initialisation before parsing an expression.
+ *
+ * <p> Automatically called by {@code buildExpression()} </p>
+ */
+ public void initBuild(){}
+
+ public class Attribute {
+ // returns a type from IBSolver (to modify)
+ // (i.e. among IMMEDIATE_(BOOL,INT,NO))
+ int getType() { return NullAttr; }
+ int getValue(SpecState _ss) { return 0; }
+ int getValue(SpecState _ss, State _st) { return 0; }
+ int getValue(CompState _cs) { return 0; }
+ // for efficiency, to allow low level objects as state
+ int getValue(Object _quickstate) { return 0; }
+ void setValue(SpecState _ss, int _val) {}
+ void setValue(CompState _cs, int _val) {}
+ boolean isState() { return false; }
+ /**
+ * links state attributes to their environment (spec, comp).
+ * If possible... (attributes must have internal information about
+ * this environment). Too specific, to enhance in the future...
+ */
+ void linkState() {}
+ /**
+ * links components of attributes to their environment (spec).
+ * If possible... (attributes must have internal information about
+ * their components). Too specific, to enhance in the future...
+ */
+ void linkComp(Spec _spec) {}
+ public String toString() { return ""; }
+ }
+
+
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java b/src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java
new file mode 100644
index 0000000000..bb06cfdc38
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSClosedFormulaAttributeClass.java
@@ -0,0 +1,56 @@
+/* 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;
+
+/**
+ * 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 IBSClosedFormulaAttributeClass extends IBSAttributeClass<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState> {}
diff --git a/src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java b/src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java
new file mode 100644
index 0000000000..81db89d434
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSClosedFormulaSolver.java
@@ -0,0 +1,62 @@
+/* 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;
+
+/**
+ * class IBSClosedFormulaSolver is a complete implementation
+ * and instantiation of {@link IBSolver
+ * IBSolver} for closed Formulas.
+ *
+ * <p> It can be used as it is.</p>
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+
+public class IBSClosedFormulaSolver extends IBSolver<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState> {
+ IBSClosedFormulaSolver() {
+ super(new IBSClosedFormulaAttributeClass());
+ }
+}
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsolver/IBSExpr.java b/src/main/java/myutil/intboolsovler2/IBSExpr.java
similarity index 67%
rename from src/main/java/myutil/intboolsolver/IBSExpr.java
rename to src/main/java/myutil/intboolsovler2/IBSExpr.java
index e43ca81842..f07446b5ba 100644
--- a/src/main/java/myutil/intboolsolver/IBSExpr.java
+++ b/src/main/java/myutil/intboolsovler2/IBSExpr.java
@@ -1,13 +1,12 @@
-package myutil.intboolsolver;
+package myutil.intboolsovler2;
public class IBSExpr <
Spec extends IBSParamSpec,
Comp extends IBSParamComp,
State extends IBSParamState,
SpecState extends IBSParamSpecState,
- CompState extends IBSParamCompState,
- ATT extends IBSAttribute<Spec,Comp,State,SpecState,CompState>
- > {
+ CompState extends IBSParamCompState
+ > extends IBSExpression{
private final int[] prios = { 2 , 2 , 1 , 1 , 1 , 1 , 2 , 3 , 3 , 3 , 3 , 3 , 3 , 3 , 3 };
private final String[] opString = {"+","-","*","/","%","&&","||","==","==","!=","!=","<",">","<=",">=","-","!"};
private final int iiiPlus = 0;
@@ -27,6 +26,26 @@ public class IBSExpr <
private final int biiGeq = 14;
private final int iNeg = 13;
private final int bNot = 14;
+ private final int biExpr = 1000; // no associated symbol
+
+ public IExpr make_iiiPlus(IExpr left, IExpr right) { return null; }
+ public IExpr make_iiiMinus(IExpr left, IExpr right) { return null; }
+ public IExpr make_iiiMult(IExpr left, IExpr right) { return null; }
+ public IExpr make_iiiDiv(IExpr left, IExpr right) { return null; }
+ public IExpr make_iiiMod(IExpr left, IExpr right) { return null; }
+ public BExpr make_bbbAnd(BExpr left, BExpr right) { return null; }
+ public BExpr make_bbbOr(BExpr left, BExpr right) { return null; }
+ public BExpr make_biiEq(IExpr left, IExpr right) { return null; }
+ public BExpr make_bbbEq(BExpr left, BExpr right) { return null; }
+ public BExpr make_biiDif(IExpr left, IExpr right) { return null; }
+ public BExpr make_bbbDif(BExpr left, BExpr right) { return null; }
+ public BExpr make_biiLt(IExpr left, IExpr right) { return null; }
+ public BExpr make_biiGt(IExpr left, IExpr right) { return null; }
+ public BExpr make_biiLeq(IExpr left, IExpr right) { return null; }
+ public BExpr make_biiGeq(IExpr left, IExpr right) { return null; }
+ public IExpr make_iNeg(IExpr expr) { return null; }
+ public BExpr make_bNot(BExpr expr) { return null; }
+ public BExpr make_biExpr(IExpr expr) { return null; }
public abstract class Expr{
public abstract int getPrio();
@@ -61,7 +80,7 @@ public class IBSExpr <
right.linkComps(_spec);
}
}
- public abstract class BBinOp extends IExpr{
+ public abstract class BBinOp extends BExpr{
public Expr left;
public Expr right;
public boolean hasStates(){
@@ -79,17 +98,31 @@ public class IBSExpr <
public abstract class IIIBinOp extends IBinOp{
public IExpr left;
public IExpr right;
+ public IIIBinOp(IExpr _l, IExpr _r){
+ left = _l;
+ right = _r;
+ }
}
public abstract class BIIBinOp extends BBinOp{
public IExpr left;
public IExpr right;
+ public BIIBinOp(IExpr _l, IExpr _r){
+ left = _l;
+ right = _r;
+ }
}
public abstract class BBBBinOp extends BBinOp{
public BExpr left;
public BExpr right;
+ public BBBBinOp(BExpr _l, BExpr _r){
+ left = _l;
+ right = _r;
+ }
}
public abstract class IConst extends IExpr {
+ public final boolean isNeg = false;
public int constant;
+ public IConst(int _i){ constant = _i; }
public int eval(){ return constant; }
public int eval(SpecState _ss) { return constant; }
public int eval(SpecState _ss, State _st) { return constant; }
@@ -101,7 +134,9 @@ public class IBSExpr <
public void linkComps(Spec _spec) {}
}
public class BConst extends BExpr {
+ public final boolean isNot = false;
public int constant;
+ public BConst(int _i){ constant = _i; }
public int getPrio(){ return 0; }
public int eval(){ return constant; }
public int eval(SpecState _ss) { return constant; }
@@ -114,7 +149,13 @@ public class IBSExpr <
public void linkComps(Spec _spec) {}
}
public class IVar extends IExpr {
- public ATT var;
+ public IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute var;
+ public IVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v)
+ throws Error {
+ if (_v.getType() == IBSAttributeClass.BoolAttr)
+ var = _v;
+ else throw new Error("IVar: Bad Attribute Type");
+ }
public int getPrio(){ return 0; }
public int eval(){ return 0; }
public int eval(SpecState _ss) { return var.getValue(_ss); }
@@ -125,14 +166,19 @@ public class IBSExpr <
if (isNeg)
return opString[iNeg] + var.toString();
return var.toString();
-
}
public boolean hasStates() { return false; }
public void linkStates() {var.linkState();}
public void linkComps(Spec _spec) {var.linkComp(_spec);}
}
public class BVar extends BExpr {
- public ATT var;
+ public IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute var;
+ public BVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v)
+ throws Error {
+ if (_v.getType() == IBSAttributeClass.BoolAttr)
+ var = _v;
+ else throw new Error("IVar: Bad Attribute Type");
+ }
public int getPrio(){ return 0; }
public int eval(){ return 0; }
public int eval(SpecState _ss) { return var.getValue(_ss); }
@@ -144,11 +190,12 @@ public class IBSExpr <
return opString[bNot] + var.toString();
return var.toString();
}
- public boolean hasStates() { return false; }
+ public boolean hasStates() { return var.isState(); }
public void linkStates() {var.linkState();}
public void linkComps(Spec _spec) {var.linkComp(_spec);}
}
public class IIIPlus extends IIIBinOp {
+ public IIIPlus(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[iiiPlus]; }
public int eval() { return left.eval() + right.eval(); }
public int eval(SpecState _ss) { return left.eval(_ss) + right.eval(_ss); }
@@ -158,10 +205,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[iiiPlus] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[iiiPlus] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[iiiPlus] + " " + r;
+ if (isNeg)
+ return opString[iNeg] + "(" + l + " " + opString[iiiPlus] + " " + r + ")";
+ else
+ return l + " " + opString[iiiPlus] + " " + r;
}
}
public class IIIMinus extends IIIBinOp {
+ public IIIMinus(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[iiiMinus]; }
public int eval() { return left.eval() - right.eval(); }
public int eval(SpecState _ss) { return left.eval(_ss) - right.eval(_ss); }
@@ -171,10 +222,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[iiiMinus] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[iiiMinus] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[iiiMinus] + " " + r;
+ if (isNeg)
+ return opString[iNeg] + "(" + l + " " + opString[iiiMinus] + " " + r + ")";
+ else
+ return l + " " + opString[iiiMinus] + " " + r;
}
}
public class IIIMult extends IIIBinOp {
+ public IIIMult(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[iiiMult]; }
public int eval() { return left.eval() * right.eval(); }
public int eval(SpecState _ss) { return left.eval(_ss) * right.eval(_ss); }
@@ -184,10 +239,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[iiiMult] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[iiiMult] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[iiiMult] + " " + r;
+ if (isNeg)
+ return opString[iNeg] + "(" + l + " " + opString[iiiMult] + " " + r + ")";
+ else
+ return l + " " + opString[iiiMult] + " " + r;
}
}
public class IIIDiv extends IIIBinOp {
+ public IIIDiv(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[iiiDiv]; }
public int eval() { return left.eval() / right.eval(); }
public int eval(SpecState _ss) { return left.eval(_ss) / right.eval(_ss); }
@@ -197,10 +256,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[iiiDiv] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[iiiDiv] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[iiiDiv] + " " + r;
+ if (isNeg)
+ return opString[iNeg] + "(" + l + " " + opString[iiiDiv] + " " + r + ")";
+ else
+ return l + " " + opString[iiiDiv] + " " + r;
}
}
public class IIIMod extends IIIBinOp {
+ public IIIMod(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[iiiMod]; }
public int eval() { return left.eval() % right.eval(); }
public int eval(SpecState _ss) { return left.eval(_ss) % right.eval(_ss); }
@@ -210,10 +273,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[iiiMod] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[iiiMod] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[iiiMod] + " " + r;
+ if (isNeg)
+ return opString[iNeg] + "(" + l + " " + opString[iiiMod] + " " + r + ")";
+ else
+ return l + " " + opString[iiiMod] + " " + r;
}
}
public class BBBAnd extends BBBBinOp {
+ public BBBAnd(BExpr _l, BExpr _r) { super(_l, _r); }
public int getPrio() { return prios[bbbAnd]; }
public int eval() { return (left.eval()!=0 && right.eval()!=0?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss)!=0 && right.eval(_ss)!=0?1:0); }
@@ -223,10 +290,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[bbbAnd] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[bbbAnd] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[bbbAnd] + " " + r;
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[bbbAnd] + " " + r + ")";
+ else
+ return l + " " + opString[bbbAnd] + " " + r;
}
}
public class BBBOr extends BBBBinOp {
+ public BBBOr(BExpr _l, BExpr _r){ super(_l, _r); }
public int getPrio() { return prios[bbbOr]; }
public int eval() { return (left.eval()!=0 || right.eval()!=0?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss)!=0 || right.eval(_ss)!=0?1:0); }
@@ -236,10 +307,14 @@ public class IBSExpr <
public String toString() {
String l = (left.getPrio() > prios[bbbOr] ? "(" + left.toString() + ")" : left.toString());
String r = (right.getPrio() > prios[bbbOr] ? "(" + right.toString() + ")" : right.toString());
- return l + " " + opString[bbbOr] + " " + r;
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[bbbOr] + " " + r + ")";
+ else
+ return l + " " + opString[bbbOr] + " " + r;
}
}
public class BIIEq extends BIIBinOp {
+ public BIIEq(IExpr _l, IExpr _r){ super(_l, _r); }
public int getPrio() { return prios[biiEq]; }
public int eval() { return (left.eval() == right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) == right.eval(_ss)?1:0); }
@@ -247,10 +322,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) == right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) == right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiEq] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiEq] + " " + r + ")";
+ else
+ return l + " " + opString[biiEq] + " " + r;
}
}
public class BBBEq extends BBBBinOp {
+ public BBBEq(BExpr _l, BExpr _r){ super(_l, _r); }
public int getPrio() { return prios[bbbEq]; }
public int eval() { return (left.eval() == right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) == right.eval(_ss)?1:0); }
@@ -258,10 +339,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) == right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) == right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[bbbEq] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[bbbEq] + " " + r + ")";
+ else
+ return l + " " + opString[bbbEq] + " " + r;
}
}
public class BIIDif extends BIIBinOp {
+ public BIIDif(IExpr _l, IExpr _r){ super(_l, _r); }
public int getPrio() { return prios[biiDif]; }
public int eval() { return (left.eval() != right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) != right.eval(_ss)?1:0); }
@@ -269,10 +356,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) != right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) != right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiDif] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiDif] + " " + r + ")";
+ else
+ return l + " " + opString[biiDif] + " " + r;
}
}
public class BBBDif extends BBBBinOp {
+ public BBBDif(BExpr _l, BExpr _r){ super(_l, _r); }
public int getPrio() { return prios[bbbDif]; }
public int eval() { return (left.eval() != right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) != right.eval(_ss)?1:0); }
@@ -284,6 +377,7 @@ public class IBSExpr <
}
}
public class BIILt extends BIIBinOp {
+ public BIILt(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[biiLt]; }
public int eval() { return (left.eval() < right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) < right.eval(_ss)?1:0); }
@@ -291,10 +385,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) < right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) < right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiLt] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiLt] + " " + r + ")";
+ else
+ return l + " " + opString[biiLt] + " " + r;
}
}
public class BIIGt extends BIIBinOp {
+ public BIIGt(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[biiGt]; }
public int eval() { return (left.eval() > right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) > right.eval(_ss)?1:0); }
@@ -302,10 +402,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) > right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) > right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiGt] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiGt] + " " + r + ")";
+ else
+ return l + " " + opString[biiGt] + " " + r;
}
}
public class BIILeq extends BIIBinOp {
+ public BIILeq(IExpr _l, IExpr _r){ super(_l, _r); }
public int getPrio() { return prios[biiLeq]; }
public int eval() { return (left.eval() <= right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) <= right.eval(_ss)?1:0); }
@@ -313,10 +419,16 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) <= right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) <= right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiLeq] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiLeq] + " " + r + ")";
+ else
+ return l + " " + opString[biiLeq] + " " + r;
}
}
public class BIIGeq extends BIIBinOp {
+ public BIIGeq(IExpr _l, IExpr _r) { super(_l, _r); }
public int getPrio() { return prios[biiGeq]; }
public int eval() { return (left.eval() >= right.eval()?1:0); }
public int eval(SpecState _ss) { return (left.eval(_ss) >= right.eval(_ss)?1:0); }
@@ -324,7 +436,32 @@ public class IBSExpr <
public int eval(CompState _cs) { return (left.eval(_cs) >= right.eval(_cs)?1:0); }
public int eval(Object _qs) { return (left.eval(_qs) >= right.eval(_qs)?1:0); }
public String toString() {
- return left.toString() + " " + opString[biiGeq] + " " + right.toString();
+ String l = left.toString();
+ String r = right.toString();
+ if (isNot)
+ return opString[bNot] + "(" + l + " " + opString[biiGeq] + " " + r + ")";
+ else
+ return l + " " + opString[biiGeq] + " " + r;
}
}
+ public class biExpr extends BExpr {
+ IExpr iExpr;
+ public biExpr(IExpr _e) { iExpr=_e; }
+ public int getPrio() { return 0; }
+ public int eval() { return (iExpr.eval()!=0?1:0); }
+ public int eval(SpecState _ss) { return (iExpr.eval(_ss)!=0?1:0); }
+ public int eval(SpecState _ss, State _st) { return (iExpr.eval(_ss,_st)!=0?1:0); }
+ public int eval(CompState _cs) { return (iExpr.eval(_cs)!=0?1:0); }
+ public int eval(Object _qs) { return (iExpr.eval(_qs)!=0?1:0); }
+ public String toString() {
+ String s = iExpr.toString();
+ if (isNot)
+ return opString[bNot] + "(" + s + ")";
+ else
+ return s;
+ };
+ public boolean hasStates() { return false; };
+ public void linkStates() { iExpr.linkStates(); };
+ public void linkComps(Spec _spec) { iExpr.linkComps(_spec); };
+ }
}
diff --git a/src/main/java/myutil/intboolsovler2/IBSExpression.java b/src/main/java/myutil/intboolsovler2/IBSExpression.java
new file mode 100644
index 0000000000..3a78d90636
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSExpression.java
@@ -0,0 +1,43 @@
+package myutil.intboolsovler2;
+
+public class IBSExpression <
+ Spec extends IBSParamSpec,
+ Comp extends IBSParamComp,
+ State extends IBSParamState,
+ SpecState extends IBSParamSpecState,
+ CompState extends IBSParamCompState
+ > {
+ public IExpr make_iiiPlus(IExpr _left, IExpr _right) { return null; }
+ public IExpr make_iiiMinus(IExpr _left, IExpr _right) { return null; }
+ public IExpr make_iiiMult(IExpr _left, IExpr _right) { return null; }
+ public IExpr make_iiiDiv(IExpr _left, IExpr _right) { return null; }
+ public IExpr make_iiiMod(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_bbbAnd(BExpr _left, BExpr _right) { return null; }
+ public BExpr make_bbbOr(BExpr _left, BExpr _right) { return null; }
+ public BExpr make_biiEq(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_bbbEq(BExpr _left, BExpr _right) { return null; }
+ public BExpr make_biiDif(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_bbbDif(BExpr _left, BExpr _right) { return null; }
+ public BExpr make_biiLt(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_biiGt(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_biiLeq(IExpr _left, IExpr _right) { return null; }
+ public BExpr make_biiGeq(IExpr _left, IExpr _right) { return null; }
+ public IExpr make_iNeg(IExpr _expr) { return null; }
+ public BExpr make_bNot(BExpr _expr) { return null; }
+ public BExpr make_biExpr(IExpr _expr) { return null; }
+
+ public abstract class Expr {
+ public abstract int getPrio();
+ public abstract int eval();
+ public abstract int eval(SpecState _ss);
+ public abstract int eval(SpecState _ss, State _st);
+ public abstract int eval(CompState _cs);
+ public abstract int eval(Object _qs);
+ public abstract String toString();
+ public abstract boolean hasStates();
+ public abstract void linkStates();
+ public abstract void linkComps(Spec _spec);
+ }
+ public abstract class IExpr extends Expr {}
+ public abstract class BExpr extends Expr {}
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamComp.java b/src/main/java/myutil/intboolsovler2/IBSParamComp.java
new file mode 100644
index 0000000000..065b77466b
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSParamComp.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.intboolsovler2;
+
+/**
+ * Interface IBSParamComp, to be implemented by classes intended to
+ * instantiate the {@code Comp} parameter of
+ * {@link IBSolver IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> The {@code Comp} parameter of
+ * {@link IBSolver IBSolver} may be instantiated
+ * by any class without modification, except that the class must implement
+ * this interface and none of the other IBSParamXXX interface.
+ * </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public interface IBSParamComp {
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamCompState.java b/src/main/java/myutil/intboolsovler2/IBSParamCompState.java
new file mode 100644
index 0000000000..9ee8a1b7e7
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSParamCompState.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.intboolsovler2;
+
+/**
+ * Interface IBSParamCompState, to be implemented by classes intended to
+ * instantiate the {@code CompState} parameter of
+ * {@link IBSolver IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> The {@code CompState} parameter of
+ * {@link IBSolver IBSolver} may be instantiated
+ * by any class without modification, except that the class must implement
+ * this interface and none of the other IBSParamXXX interface.
+ * </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public interface IBSParamCompState {
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamSpec.java b/src/main/java/myutil/intboolsovler2/IBSParamSpec.java
new file mode 100644
index 0000000000..6e95b7dd53
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSParamSpec.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.intboolsovler2;
+
+/**
+ * Interface IBSParamSpec, to be implemented by classes intended to
+ * instantiate the {@code Spec} parameter of
+ * {@link IBSolver IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> The {@code Spec} parameter of
+ * {@link IBSolver IBSolver} may be instantiated
+ * by any class without modification, except that the class must implement
+ * this interface and none of the other IBSParamXXX interface.
+ * </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public interface IBSParamSpec {
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamSpecState.java b/src/main/java/myutil/intboolsovler2/IBSParamSpecState.java
new file mode 100644
index 0000000000..70d17cd7e9
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSParamSpecState.java
@@ -0,0 +1,57 @@
+/* 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;
+
+/**
+ * Interface IBSParamSpecState, to be implemented by classes intended to
+ * instantiate the {@code SpecState} parameter of
+ * {@link IBSolver IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> The {@code SpecState} parameter of
+ * {@link IBSolver IBSolver} may be instantiated
+ * by any class without modification, except that the class must implement
+ * this interface and none of the other IBSParamXXX interface.
+ * </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+public interface IBSParamSpecState {
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSParamState.java b/src/main/java/myutil/intboolsovler2/IBSParamState.java
new file mode 100644
index 0000000000..a97c7143fe
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSParamState.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.intboolsovler2;
+
+/**
+ * Interface IBSParamState, to be implemented by classes intended to
+ * instantiate the {@code State} parameter of
+ * {@link IBSolver IBSolver}.
+ * Creation: 07/03/2023
+ *
+ * <p> The {@code State} parameter of
+ * {@link IBSolver IBSolver} may be instantiated
+ * by any class without modification, except that the class must implement
+ * this interface and none of the other IBSParamXXX interface.
+ * </p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public interface IBSParamState {
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java b/src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java
new file mode 100644
index 0000000000..f581662f5f
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSStdAttributeClass.java
@@ -0,0 +1,389 @@
+/* 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;
+
+/**
+ * Abstract Class IBSStdAttributeClass, partially
+ * implementing {@link IBSAttributeClass
+ * IBSAttributeClass} for systems with states as boolean leaves.
+ * Creation: 07/03/2023
+ *
+ * <p> This class (together with
+ * {@link IBSStdAttributeClass
+ * IBSStdAttribute}) is a step toward an instantiation
+ * of the solver for systems with states as boolean leaves.</p>
+ * <p> To instantiate the solver using this approach, a fully
+ * implemented extension of this class must be provided.
+ * To make instantiation easier, functions that remain abstract are
+ * grouped at the beginning of the code file and commented</p>
+ * <HR>
+ * <p> The proposed implementation allow instances to provides a
+ * mechanism that memorize attributes that have already
+ * been build. Using this mechanism avoids creating isomorphic
+ * instances of a single attribute.</p>
+ *
+ * <p> To allow the handling of this "memory", some methods must
+ * be implemented, enumerated below. Associated comments below
+ * are guided by this typical implementation semantics.</p>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+
+public class IBSStdAttributeClass<
+ Spec extends IBSParamSpec,
+ Comp extends IBSParamComp,
+ State extends IBSParamState,
+ SpecState extends IBSParamSpecState,
+ CompState extends IBSParamCompState
+ > extends IBSAttributeClass<
+ Spec ,
+ Comp ,
+ State ,
+ SpecState ,
+ CompState
+ > {
+ // TO OVERRIDE, Inherited from IBSAttributeClass.
+ // public void initBuild(Spec _spec);
+ // public void initBuild(Comp _comp);
+ // public void initBuild();
+
+ /**
+ * Find a memorized typed attribute or returns null (<b> to override </b>).
+ *
+ * <p> Tf the attribute corresponding to _s has been memorized,
+ * it is returned. Otherwise null is returned </p>
+ * @param _spec the specification that associates structures to open
+ * leaves
+ * @param _s the string that identifies the searched attribute.
+ * @return the found or created typed attribute
+ */
+ public IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute findAttribute(Spec _spec, String _s) { return null; }
+
+ /**
+ * Add an attribute to the memorized ones (<b> to override </b>).
+ * @param _spec the specification that associates structures to open
+ * leaves
+ * @param _s the string that identifies (in _spec) the attribute to add
+ * @param _att the attribute to add
+ */
+ public void addAttribute(Spec _spec, String _s, IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute _att) {}
+ /**
+ * Find a memorized typed attribute or returns null (<b> to override </b>).
+ *
+ * <p> Tf the attribute corresponding to _s has been memorized,
+ * it is returned. Otherwise null is returned </p>
+ * @param _comp the component that associates structures to open
+ * leaves
+ * @param _s the string that identifies the searched attribute.
+ * @return the found or created typed attribute
+ */
+ public IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute findAttribute(Comp _comp, String _s) { return null; }
+ /**
+ * Add an attribute to the memorized ones (<b> to override </b>).
+ * @param _comp the component that associates structures to open
+ * leaves
+ * @param _s the string that identifies (in _comp) the attribute to add
+ * @param _att the attribute to add
+ */
+ public void addAttribute(Comp _comp, String _s, IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute _att) {}
+ /**
+ * Find a memorized attribute or returns null (<b> to override </b>).
+ *
+ * <p> Tf the attribute corresponding to _s has been memorized,
+ * it is returned. Otherwise null is returned </p>
+ * @param _comp the component that associates structures to open
+ * leaves
+ * @param _state the string that identifies the searched attribute.
+ * @return the found or created typed attribute.
+ */
+ public IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute findAttribute(Comp _comp, State _state) { return null; }
+ /**
+ * Add an attribute to the memorized ones (<b> to override </b>).
+ * @param _comp the component that associates structures to open
+ * leaves
+ * @param _state the state that identifies (in _comp) the attribute to add
+ * @param _att the attribute to add
+ */
+ public void addAttribute(Comp _comp, State _state, IBSStdAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute _att) {}
+
+ /**
+ * Clear the memorized attributes (<b> to override </b>).
+ */
+ public void clearAttributes() {}
+ /**
+ * get the name associated to a state by the instance (<b> to override </b>).
+ *
+ * <p> Note: although this method seems to be in the scope of the static
+ * part of attributes (IBSAttributeClass), it must be here because
+ * it is used here, where AttributeClass cannot be made visible
+ * (genericity limits).</p>
+ * @param _comp the component that associates structures to attribute
+ * strings
+ * @param _state the state of which we want the name
+ * @return the name associated to _state by _comp
+ */
+ public String getStateName(Comp _comp, State _state) { return ""; }
+
+
+ // 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...
+ x.classInitAttribute(_spec,_s);
+ switch (x.getType()) {
+ case IBSAttributeClass.NullAttr: {
+ return this.NullTypedAttribute;
+ }
+ case IBSAttributeClass.BoolConst: {
+ a = new TypedAttribute(x.getConstant(),true);
+ break;
+ }
+
+ case IBSAttributeClass.IntConst: {
+ a = new TypedAttribute(x.getConstant(),false);
+ break;
+ }
+ case IBSAttributeClass.BoolAttr: {
+ a = new TypedAttribute(x, true);
+ }
+ case IBSAttributeClass.IntAttr: {
+ a = new TypedAttribute(x, false);
+ }
+ }
+ addAttribute(_spec, _s, a);
+ }
+ return a;
+ }
+ 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...
+ x.classInitAttribute(_comp,_s);
+ switch (x.getType()) {
+ case IBSAttributeClass.NullAttr: {
+ return this.NullTypedAttribute;
+ }
+ case IBSAttributeClass.BoolConst: {
+ a = new TypedAttribute(x.getConstant(),true);
+ break;
+ }
+
+ case IBSAttributeClass.IntConst: {
+ a = new TypedAttribute(x.getConstant(),false);
+ break;
+ }
+ case IBSAttributeClass.BoolAttr: {
+ a = new TypedAttribute(x, true);
+ }
+ case IBSAttributeClass.IntAttr: {
+ a = new TypedAttribute(x, false);
+ }
+ }
+ addAttribute(_comp, _s, a);
+ }
+ return a;
+ }
+ 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...
+ x.classInitAttribute(_comp,_state);
+ switch (x.getType()) {
+ case IBSAttributeClass.NullAttr: {
+ return this.NullTypedAttribute;
+ }
+ case IBSAttributeClass.BoolConst: {
+ a = new TypedAttribute(x.getConstant(),true);
+ break;
+ }
+
+ case IBSAttributeClass.IntConst: {
+ a = new TypedAttribute(x.getConstant(),false);
+ break;
+ }
+ case IBSAttributeClass.BoolAttr: {
+ a = new TypedAttribute(x, true);
+ }
+ case IBSAttributeClass.IntAttr: {
+ a = new TypedAttribute(x, false);
+ }
+ }
+ addAttribute(_comp, _state, a);
+ }
+ return a;
+ }
+
+ /**
+ * Abstract Class IBSStdAttribute partially implementing {@link
+ * Attribute IBSAttribute} for systems with
+ * states as boolean leaves.
+ * Creation: 07/03/2023
+ *
+ * <p> This class (together with
+ * {@link IBSStdAttributeClass
+ * IBSStdAttributeClass}) is a (little) step toward an instantiation
+ * of the solver for systems with states as boolean leaves.</p>
+ * <p> To instantiate the solver using this approach, a fully
+ * implemented extension of this class must be provided.
+ * To make instantiation easier, functions that remain abstract are
+ * grouped at the beginning of the code file and commented</p>
+ * <HR>
+ * <p>Subclasses must not export any constructors but provide access to
+ * their default one through {@code public SubClass getNew()}). They also
+ * provide initialisation functions to be called after the default
+ * constructor.</p>
+ * <p> More technically, the creation process of attributes is the following one:</p>
+ * <ul>
+ * <li> Subclass Default Constructor (subclass provides {@code public
+ * SubClass getNew()})
+ * </li>
+ * <li> IBSStdAttribute initialisation function (implemented here)
+ * </li>
+ * <li> Subclass specific initialisation function (subclass provides
+ * {@code int initAttribute(...)})
+ * </li>
+ * <li> IBSStdtAttribute initialisation postprocessing (implemented here)
+ * </li>
+ * </ul>
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+
+ public class Attribute extends IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute {
+
+ // partial implementation: Variable and State attributes
+ public State state =null;
+ protected String s = null;
+ protected boolean isState = false;
+ protected int type = IBSAttributeClass.NullAttr;
+ protected int constantInt = 0;
+
+ // TO OVERRIDE, Inherited from IBSAttributeClass.
+ // public abstract int getValue(SpecState _ss);
+ // public abstract int getValue(CompState sb);
+ // public abstract int getValue(Object _quickstate);
+ // public abstract void setValue(SpecState _ss, int val);
+ // public abstract void setValue(CompState _cs, int val);
+
+ // public abstract void linkComp(Spec _spec);
+ // public abstract void linkState();
+
+ /** Subclass specific initialisation functions for attributes (<b> To override </b>).
+ *
+ * <p> Part of attribute initialisation that is specific to instantiation.
+ * Member "s" (attribute string), can be used as it has been set by
+ * IBSStdAttribute initialisation, which has been called just before.</p>
+ *
+ * <p> The returned value is among (IBSTypedAttribute.) None, BoolConst,
+ * IntConst, BoolAttr and IntAttr, according to the type of attribute that
+ * has been identified.</p>
+ *
+ * <p> If the returned type is BoolConst or IntConst, constantInt must contain
+ * associated constant value when returning (expected by postprocessing)</p>
+ * @param _spec the specification that associates structures to attribute
+ * strings
+ * @return the type of the identified attribute, among (IBSTypedAttribute.)
+ * None, BoolConst, IntConst, BoolAttr and IntAttr. (IntConst set if relevant)
+ */
+ // to implement
+ protected int initAttribute(Spec _spec) { return IBSAttributeClass.NullAttr; }
+ /** Subclass specific initialisation functions for attributes (<b> To override </b>).
+ *
+ * <p> Part of attribute initialisation that is specific to instantiation.
+ * Member "s" (attribute string), can be used as it has been set by
+ * IBSStdAttribute initialisation, which has been called just before.</p>
+ *
+ * <p> The returned value is among (IBSTypedAttribute.) None, BoolConst,
+ * IntConst, BoolAttr and IntAttr, according to the type of attribute that
+ * has been identified.</p>
+ *
+ * <p> If the returned type is BoolConst or IntConst, constantInt must contain
+ * associated constant value when returning (expected by postprocessing)</p>
+ * @param _comp the component that associates structures to attribute
+ * strings
+ * @return the type of the identified attribute, among (IBSTypedAttribute.)
+ * None, BoolConst, IntConst, BoolAttr and IntAttr. (IntConst set if relevant)
+ */
+ protected int initAttribute(Comp _comp) { return IBSAttributeClass.NullAttr; }
+ /** Subclass specific initialisation functions for attributes (<b> To override </b>).
+ *
+ * <p> Part of attribute initialisation that is specific to instantiation.
+ * Members s, isState and state have already been set by IBSStdAttribute
+ * initialisation, which has been called just before.</p>
+ * <p> Returned type should be BoolAttr, or None if the attribute is not
+ * a state attribute (error case).</p>
+ */
+ protected int initStateAttribute(Comp _comp) { return IBSAttributeClass.NullAttr; }
+
+
+ // $$$$$$$$$$$$$$$ provided implementation, should not be modified $$$$$$$$$$$$$$
+ public final int getType(){ return type; }
+ // Nothing to do.
+ public final int getConstant(){ return constantInt; }
+ public int getValue(SpecState _ss, State _st) {
+ if (isState) {
+ return (state == _st) ? 1 : 0;
+ }
+ return(getValue(_ss));
+ }
+ // public boolean isState() { return isState; }
+ public String toString() { return s; }
+ public final void classInitAttribute(Spec _spec, String _s) {
+ this.s = _s;
+ type = initAttribute(_spec);
+ }
+ public final void classInitAttribute(Comp _comp, String _s) {
+ this.s = _s;
+ type = initAttribute(_comp);
+ }
+
+ //!! for the moment, _comp is useless... Reviser...
+ public final void classInitAttribute(Comp _comp, State _state) {
+ this.s = getStateName(_comp,_state);
+ isState = true;
+ state = _state;
+ type = initStateAttribute(_comp);
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java b/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.java
new file mode 100644
index 0000000000..d35603ec97
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaAttributeClass.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.intboolsovler2;
+
+/**
+ * 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 IBSStdClosedFormulaSolver
+ * IBSStdClosedFormulaSolver}}</p>
+ *
+ * <p>These three
+ * classes provides the same features as
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttribute},
+ * {@link IBSClosedFormulaAttributeClass
+ * IBSClosedFormulaAttributeClass} and
+ * {@link IBSClosedFormulaSolver
+ * IBSClosedFormulaSolver} (together).</p>
+ *
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public class IBSStdClosedFormulaAttributeClass extends IBSStdAttributeClass<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState
+ > {
+ IBSStdClosedFormulaAttributeClass(){}
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java b/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java
new file mode 100644
index 0000000000..166da22a8a
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSStdClosedFormulaSolver.java
@@ -0,0 +1,76 @@
+/* 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;
+
+/**
+ * class IBSStdClosedFormulaSolver is a complete implementation
+ * and instantiation of {@link IBSolver
+ * 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 IBSClosedFormulaSolver
+ * IBSClosedFormulaSolver} (together).</p>
+ *
+ * Creation: 07/03/2023
+ *
+ * @version 0.1 07/03/2023
+ * @author Sophie Coudert
+ */
+
+public class IBSStdClosedFormulaSolver extends IBSolver<
+ IBSParamSpec,
+ IBSParamComp,
+ IBSParamState,
+ IBSParamSpecState,
+ IBSParamCompState> {
+ IBSStdClosedFormulaSolver() {
+ super(new IBSClosedFormulaAttributeClass());
+ }
+}
\ No newline at end of file
diff --git a/src/main/java/myutil/intboolsovler2/IBSolver.java b/src/main/java/myutil/intboolsovler2/IBSolver.java
new file mode 100644
index 0000000000..b091e88407
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSolver.java
@@ -0,0 +1,1051 @@
+/* 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;
+ }
+
+}
diff --git a/src/main/java/myutil/intboolsovler2/package-info.java b/src/main/java/myutil/intboolsovler2/package-info.java
new file mode 100644
index 0000000000..2082c23b60
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/package-info.java
@@ -0,0 +1,254 @@
+ /* 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 intboolsolver, a generic parser/evaluator for boolean/integer
+ * expressions with open leaves (i.e identifiers).
+ * Creation: 27/02/2023.
+ *
+ * <p>
+ * The parser may be instantiated by usual expressions with variables
+ * and their usual evaluation, but it is more generally dedicated to
+ * two-level structured systems, i.e global specifications build over
+ * a set of components. For example we can consider identifiers
+ * associated to local states that define together a global state.
+ * Default parameters are provided to instantiate solvers that do not
+ * use all the features, such as for example a solver for closed
+ * expressions (which is provided).
+ *
+ * </p>
+ * <ul>
+ * <li> {@link myutil.intboolsolver.IBSolverAPI
+ * IBSolverAPI} provides documentation about the functions
+ * exported by the solver after it has been instantiated.
+ * </li>
+ * <li> <p>{@link myutil.intboolsolver.IBSolver IBSolver} is the solver
+ * implementation. It relies on the common structure of all expressions,
+ * which only differ on the way the open leaves are handled.</p>
+ *
+ * <p>The way leaves are handled depends on the notions of specification,
+ * component, specification state, component state and (state machine)
+ * state of the instance. Thus they are parameters of the generic solver
+ * and <b> in order to instantiate the solver, we will have to
+ * provide:</b></p>
+ * <ul>
+ * <li> <p>{@code Spec} class, which must implement {@link
+ * myutil.intboolsolver.IBSParamSpec IBSParamSpec}: The class of
+ * global system specifications, which intuitively associates
+ * leave structures to (spec-dedicated) leave identifiers).</p>
+ * </li>
+ * <li> <p>{@code Comp} class, which <b>must implement</b> {@link
+ * myutil.intboolsolver.IBSParamComp IBSParamComp}: the class
+ * of system components, which intuitively associates leave
+ * structures to (comp-dedicated) leave identifiers).</p>
+ * </li>
+ * <li> <p>{@code State} class, which <b>must implement</b>
+ * {@link myutil.intboolsolver.IBSParamState IBSParamState}:
+ * a class of states. It is intended to receive state machine
+ * states in provided extensions but can be used another way
+ * (in the provided extensions, there are state leaves that
+ * may be true or false in different contexts...).</p>
+ * </li>
+ * <li> <p>{@code SpecState} class, which <b>must implement</b>
+ * {@link myutil.intboolsolver.IBSParamSpecState
+ * IBSParamSpecState}: the class of specification state, which
+ * intuitively associates leaves to int/bool values.</p>
+ * </li>
+ * <li> <p>{@code CompState} class, which <b>must implement</b>
+ * {@link myutil.intboolsolver.IBSParamCompState
+ * IBSParamCompState}: the class of component states, which
+ * intuitively associates leaves to int/bool values.</p>
+ * </li>
+ * </ul>
+ * <p><b>WARNING!!</b> A successful instantiation requires that
+ * class <i>xxx</i> (with <i>xxx</i> among {@code Spec}, {@code Comp},
+ * {@code SpecState}, {@code CompState} and {@code State}) does
+ * not implement any IBS<i>yyy</i>Param with <i>yyy</i>
+ * ≠ <i>xxx</i>.</p>
+ * <p>{@link myutil.intboolsolver.IBSParamSpec IBSParamSpec},
+ * {@link myutil.intboolsolver.IBSParamComp IBSParamComp},
+ * {@link myutil.intboolsolver.IBSParamState IBSParamState},
+ * {@link myutil.intboolsolver.IBSParamSpecState IBSParamSpecState}
+ * and
+ * {@link myutil.intboolsolver.IBSParamCompState IBSParamCompState}
+ * can be used as default parameters to instanciate solvers that do
+ * not implement the corresponding concepts.</p>
+ * <p>The structure of leaf expressions is instantiation dependent.
+ * Thus it is parametrized by "attribute" parameters (themselves
+ * parametrized by the five classes above) for which an
+ * implementation must also be provided in order to instantiate
+ * {@link myutil.intboolsolver.IBSolver IBSolver}. Attribute
+ * parameters are decomposed into two classes:</p>
+ * <ul>
+ * <li> <p>an "Attribute" class which allow to create
+ * attribute instances with instance dependent methods.</p>
+ * </li>
+ * <li> <p>an "Attribute Class" class which contains all the
+ * methods that do not depend on attribute instances</p>
+ * </li>
+ * </ul>
+ * </li>
+ * <li><p>{@link myutil.intboolsolver.IBSAttribute
+ * IBSAttribute} is the interface describing the features
+ * to provide in order to instantiate the "Attribute" class
+ * of {@link myutil.intboolsolver.IBSolver
+ * IBSolver} (features that depend on attribute instances).
+ * <b> implementation must be provides </b>. It can be
+ * implemented directly or using the provided extensions.</p>
+ * </li>
+ * <li><p>{@link myutil.intboolsolver.IBSAttributeClass
+ * IBSAttributeClass} is the interface describing the features
+ * to provide in order to instantiate the "attribute class"
+ * class of {@link myutil.intboolsolver.IBSolver IBSolver}
+ * (features that do not depend on attribute instances).
+ * <b> implementation must be provided </b>. It requires to
+ * instanciate an "Attribute" parameter by a class that extends
+ * {@link myutil.intboolsolver.IBSAttribute IBSAttribute},
+ * (with the same {@code Spec}, {@code Comp}, {@code SpecState},
+ * {@code CompState} and {@code State} parameters).
+ * Implementation can also be implemented using provided
+ * extensions, which refine the couple
+ * ({@link myutil.intboolsolver.IBSAttribute IBSAttribute},
+ * {@link myutil.intboolsolver.IBSAttributeClass
+ * IBSAttributeClass}).</p>
+ * </li>
+ * </ul>
+ * <p><a id="instanciation_sumary"> <b>Instantiation
+ * summary:</b></a></p>
+ * <ul>
+ * <li> provide {@code Spec}, {@code Comp}, {@code SpecState},
+ * {@code CompState} and {@code State} as they are, but making
+ * them extend their associated parameter IBS<i>xxx</i>Param
+ * and not making them extend any IBS<i>yyy</i>Param with
+ * <i>xxx</i> ≠ <i>yyy</i>
+ * </li>
+ * <li> provide an implementation {@code Attrib} of
+ * {@link myutil.intboolsolver.IBSAttribute IBSAttribute}
+ * for {@code Spec}, {@code Comp}, {@code SpecState},
+ * {@code CompState} and {@code State}.
+ <PRE>
+ known from context (package, imports): intboolsolver,
+ Spec, Comp, SpecState, CompState, State
+
+ public class Attrib
+ implements IBSAttribute[Spec,Comp,SpecState,CompState,State] {
+ !!! put implementation of IBSAttribute here
+ }
+ * </PRE>
+ * </li>
+ * <li> provide an implementation {@code AttribClass} of
+ * {@link myutil.intboolsolver.IBSAttributeClass
+ * IBSAttributeClass} for {@code Spec}, {@code Comp},
+ * {@code SpecState}, {@code CompState}, {@code State} and
+ * {@code Attrib}.
+ <PRE>
+ known from context (package, imports): intboolsolver,
+ Spec, Comp, SpecState, CompState, State, Attrib
+
+ public class AttribClass
+ extends IBSAttribute[Spec, Comp, SpecState, CompState,
+ State,Attrib] {
+ !!! put implementation of IBSAttributeClass here
+ }
+ * </PRE>
+ * <li> build solver instance following this model:
+ <PRE>
+ known from context (package, imports): intboolsolver,
+ Spec, Comp, SpecState, CompState, State, Attrib, AttribClass
+ public class Solver
+ extends IBSolver [ Spec,Comp, SpecState, CompState, State,
+ Attrib, AttribClass ] {
+ Solver() {
+ super(new AttribClass());
+ }
+ !!! or (sometimes required, I don't know why...)
+ Solver() {
+ super();
+ setAttributeClass(new AttribClass());
+ }
+ !!! put your solver's specific features here (or extends...)
+ }
+ * </PRE>
+ * </li>
+ * </ul>
+ *
+ * <hr>
+ * <span style="font-size: 120%"> Extension Standard Attributes </span>
+ * <p> This extension provides a skeleton for a typical
+ * implementation with (boolean) state leaves. It provides a guided
+ * way to implement some methods of
+ * {@link myutil.intboolsolver.IBSAttribute IBSAttribute} and
+ * {@link myutil.intboolsolver.IBSAttributeClass
+ * IBSAttributeClass}</p>
+ * <p> Following the proposed approach, some partial implementation
+ * is provided. It is sometime provided as code in comments that must
+ * be copied in final instantiation (when genericity disappear).</p>
+ * <p> This extension refines the two abstract class for
+ * attributes</p>
+ * <p> Note: the two following classes should be abstract
+ * (future work) making the remaining work to do more clear</p>
+ * <ul>
+ * <li><p>{@link myutil.intboolsolver.IBSStdAttribute
+ * IBSStdAttribute} implements
+ * {@link myutil.intboolsolver.IBSAttribute IBSAttribute}.
+ * To instantiate the solver using this approach, <b>a fully
+ * implemented extension of this class must be provided</b>.
+ * Comments in the file say what remains to implement
+ * (in the futur, abstraction, for automatic checking...).
+ * </li>
+ * <li><p>{@link myutil.intboolsolver.IBSStdAttributeClass
+ * IBSStdAttributeClass} implements
+ * {@link myutil.intboolsolver.IBSAttributeClass
+ * IBSAttributeClass}.
+ * To instantiate the solver using this approach, <b>a fully
+ * implemented extension of this class must be provided</b>.
+ * Comments in the file say what remains to implement
+ * (in the futur, abstraction, for automatic checking...).
+ * </li>
+ * </ul>
+ *
+ * <p><b>Instantiation summary:</b></p>
+ * <p> similar to <a href="#instanciation_sumary"> the previously
+ * described process</a>, replacing IBSAttribute by IBSStdAttribute
+ * and IBSAttributeClass by IBSStdAttributeClass.</p>
+ *
+ * @version 0.1 07/03/2023
+ *
+ * @author Sophie Coudert (rewrite from Alessandro TEMPIA CALVINO)
+ */
+ package myutil.intboolsovler2;
\ No newline at end of file
--
GitLab