diff --git a/src/main/java/avatartranslator/intboolsolver/AvatarIBSAttributeClass.java b/src/main/java/avatartranslator/intboolsolver/AvatarIBSAttributeClass.java
index 761e7975e50b541c10b38cf67ed817f918737fb4..a58bf3ae32a311187e5a9ba5d9120a6c86675e46 100644
--- a/src/main/java/avatartranslator/intboolsolver/AvatarIBSAttributeClass.java
+++ b/src/main/java/avatartranslator/intboolsolver/AvatarIBSAttributeClass.java
@@ -100,6 +100,12 @@ public class AvatarIBSAttributeClass extends IBSStdAttributeClass<
attributesMap.put((AvatarElement) _state, _att);
}
protected Attribute getAttribute() {return new Attribute();}
+ //@Override
+ public String getStateName(AvatarBlock _comp, AvatarStateMachineElement _state)
+ {
+ return _state.getName();
+ }
+
public static AvatarElement getElement(String s, AvatarSpecification spec) {
//Extract Block and Attribute
String[] splitS;
@@ -331,12 +337,6 @@ public class AvatarIBSAttributeClass extends IBSStdAttributeClass<
}
}
-
-
- public String getStateName(AvatarBlock _comp, AvatarStateMachineElement _state){
- return (_state).getName();
- }
-
public int getValue(SpecificationState _ss) {
int value;
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 0c3dff51994d15b7def78519ba4cded767e5f9ae..1a3a33bb960ef3ecbc52f00180f21aaf2168023e 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -39,6 +39,8 @@
package avatartranslator.modelchecker;
import avatartranslator.*;
+import avatartranslator.intboolsolver.*;
+import myutil.intboolsolver.*;
import myutil.TraceManager;
@@ -54,9 +56,9 @@ public class SafetyProperty {
private String rawProperty;
private String refProperty;
private int errorOnProperty;
- private AvatarExpressionSolver safetySolver;
- private AvatarExpressionSolver safetySolverLead;
- private SpecificationPropertyPhase phase;
+ private AvatarIBSExpressionClass.BExpr safetySolver;
+ private AvatarIBSExpressionClass.BExpr safetySolverLead;
+ private SpecificationPropertyPhase phase;
private AvatarStateMachineElement state;
// Error on property
@@ -102,9 +104,10 @@ public class SafetyProperty {
public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state, int _safetyType) {
//create liveness safety
- AvatarExpressionAttribute attribute = new AvatarExpressionAttribute(block, state);
- safetySolver = new AvatarExpressionSolver();
- safetySolver.buildExpression(attribute);
+ AvatarIBSAttributeClass.Attribute attribute =
+ (AvatarIBSAttributeClass.Attribute)AvatarIBSolver.attrC.getTypedAttribute(block, state).getAttribute();
+ safetySolver = (AvatarIBSExpressionClass.BExpr) AvatarIBSolver.parser.makeBool(attribute);
+
propertyType = BLOCK_STATE;
safetyType = _safetyType;
result = true;
@@ -161,7 +164,8 @@ public class SafetyProperty {
public void initLead() {
- AvatarExpressionSolver tmp;
+ AvatarIBSExpressionClass.BExpr tmp;
+
int type;
tmp = safetySolver;
safetySolver = safetySolverLead;
@@ -175,7 +179,7 @@ public class SafetyProperty {
public void restoreLead() {
//to be used only after initLead()
- AvatarExpressionSolver tmp;
+ AvatarIBSExpressionClass.BExpr tmp;
int type;
tmp = safetySolver;
safetySolver = safetySolverLead;
@@ -208,20 +212,18 @@ public class SafetyProperty {
public boolean getSolverResult(SpecificationState _ss) {
- return safetySolver.getResult(_ss) != 0;
+ return safetySolver.eval(_ss);
}
public boolean getSolverResult(SpecificationState _ss, AvatarStateMachineElement _asme) {
- return safetySolver.getResult(_ss, _asme) != 0;
+ return safetySolver.eval(_ss, _asme);
}
-
-
+
public boolean getSolverLeadResult(SpecificationState _ss, AvatarStateMachineElement _asme) {
- return safetySolverLead.getResult(_ss, _asme) != 0;
+ return safetySolverLead.eval(_ss, _asme);
}
-
-
+
public SpecificationPropertyPhase getPhase() {
return phase;
}
@@ -234,13 +236,11 @@ public class SafetyProperty {
phase = SpecificationPropertyPhase.NONSATISFIED;
}
}
-
-
+
public AvatarStateMachineElement getState() {
return state;
}
-
-
+
public void linkSolverStates() {
//linking to states so that normal bool elaborations are possible
if (safetySolver != null) {
@@ -250,8 +250,7 @@ public class SafetyProperty {
safetySolverLead.linkStates();
}
}
-
-
+
public String toString() {
String ret = rawProperty;
switch(phase) {
@@ -325,39 +324,40 @@ public class SafetyProperty {
private boolean initSafetyTrace(AvatarSpecification _spec, String p) {
- safetySolver = new AvatarExpressionSolver(p);
- boolean exprRet = safetySolver.buildExpression(_spec);
+ safetySolver = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(_spec,p);
+
- if (exprRet == false) {
+ if (safetySolver==null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
}
- if (safetySolver.hasState()) {
+ if (safetySolver.hasStates()) {
propertyType = BLOCK_STATE;
} else {
propertyType = BOOL_EXPR;
}
- return exprRet;
+ return true;
}
private boolean initSafetyTrace(AvatarBlock block, AvatarSpecification _spec, String p) {
- safetySolver = new AvatarExpressionSolver(p);
- boolean exprRet = safetySolver.buildExpression(block);
+ safetySolver = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(block,p);
- if (exprRet == false) {
+ if (safetySolver == null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
}
- safetySolver.setBlockIndex(_spec);
+ safetySolver.linkComps(_spec);
- if (safetySolver.hasState()) {
+ if (safetySolver.hasStates()) {
propertyType = BLOCK_STATE;
} else {
propertyType = BOOL_EXPR;
}
- return exprRet;
+ return true;
}
@@ -375,29 +375,27 @@ public class SafetyProperty {
pp = pFields[0].trim();
pq = pFields[1].trim();
- safetySolver = new AvatarExpressionSolver(pp);
- exprRet = safetySolver.buildExpression(_spec);
-
- if (exprRet == false) {
+ safetySolver = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(_spec,pp);
+
+ if (safetySolver==null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
return false;
}
- safetySolverLead = new AvatarExpressionSolver(pq);
- exprRet = safetySolverLead.buildExpression(_spec);
+ safetySolverLead = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(_spec,pq);
- if (exprRet == false) {
+ if (safetySolverLead==null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
return false;
}
- if (safetySolver.hasState()) {
+ if (safetySolver.hasStates()) {
propertyType = BLOCK_STATE;
} else {
propertyType = BOOL_EXPR;
}
- if (safetySolverLead.hasState()) {
+ if (safetySolverLead.hasStates()) {
leadType = BLOCK_STATE;
} else {
leadType = BOOL_EXPR;
@@ -420,33 +418,31 @@ public class SafetyProperty {
pp = pFields[0].trim();
pq = pFields[1].trim();
- safetySolver = new AvatarExpressionSolver(pp);
- exprRet = safetySolver.buildExpression(block);
+ safetySolver = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(block,pp);
- if (exprRet == false) {
+ if (safetySolver==null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
return false;
}
- safetySolver.setBlockIndex(_spec);
+ safetySolver.linkComps(_spec);
- safetySolverLead = new AvatarExpressionSolver(pq);
- exprRet = safetySolverLead.buildExpression(block);
+ safetySolverLead = (AvatarIBSExpressionClass.BExpr)AvatarIBSolver.parser.parseBool(block,pq);
- if (exprRet == false) {
+ if (safetySolverLead==null) {
errorOnProperty = BAD_PROPERTY_STRUCTURE;
return false;
}
- safetySolverLead.setBlockIndex(_spec);
+ safetySolverLead.linkComps(_spec);
- if (safetySolver.hasState()) {
+ if (safetySolver.hasStates()) {
propertyType = BLOCK_STATE;
} else {
propertyType = BOOL_EXPR;
}
- if (safetySolverLead.hasState()) {
+ if (safetySolverLead.hasStates()) {
leadType = BLOCK_STATE;
} else {
leadType = BOOL_EXPR;
diff --git a/src/main/java/myutil/intboolsolver/IBSStdAttributeClass.java b/src/main/java/myutil/intboolsolver/IBSStdAttributeClass.java
index 8eaa56ae26eb5a461958497a68ba4b4f01ae9b80..665ad5e1441efde088e6406c611889714cf97d74 100644
--- a/src/main/java/myutil/intboolsolver/IBSStdAttributeClass.java
+++ b/src/main/java/myutil/intboolsolver/IBSStdAttributeClass.java
@@ -374,7 +374,7 @@ public class IBSStdAttributeClass<
// $$$$$$$$$$$$$$$ provided implementation, should not be modified $$$$$$$$$$$$$$
-
+ public boolean isState() { return isState; }
/**
* get the type of the attribute. <b>do not override</b>
* @return a type among NullAttr, BoolConst, IntConst,
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index e0b9d320c59941bc0776d57802e08b6aa7fb7737..f66dbe84c4a9c46bbe3ec6169b0d1150dda5927c 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -259,7 +259,7 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
/*for(int i=0; i<s1.length(); i++) {
System.out.println(i + "\t" + s1.substring(i, i+1) + " " + s2.substring(i, i+1));
}*/
-
+ System.out.println("S1: " + s1 + "\nS2: " + s2);
assertTrue(s1.equals(s2));
}