diff --git a/src/main/java/avatartranslator/AvatarActionAssignment.java b/src/main/java/avatartranslator/AvatarActionAssignment.java index 8a558a16bb35a92a92d64cf184b25e6c8eeaec43..40d0c911d5892dbcc116cb1c75b654110ed71eef 100644 --- a/src/main/java/avatartranslator/AvatarActionAssignment.java +++ b/src/main/java/avatartranslator/AvatarActionAssignment.java @@ -42,6 +42,8 @@ import myutil.TraceManager; import java.util.Map; +import avatartranslator.modelchecker.SpecificationBlock; + /** * Class AvatarActionAssignment * Creation: 16/09/2015 @@ -51,10 +53,14 @@ import java.util.Map; public class AvatarActionAssignment implements AvatarAction { AvatarLeftHand leftHand; AvatarTerm rightHand; + AvatarExpressionSolver actionSolver; + private AvatarExpressionAttribute leftAttribute; public AvatarActionAssignment (AvatarLeftHand _leftHand, AvatarTerm _rightHand) { this.leftHand = _leftHand; this.rightHand = _rightHand; + this.actionSolver = null; + this.leftAttribute = null; } public boolean isAVariableSetting () { @@ -72,6 +78,10 @@ public class AvatarActionAssignment implements AvatarAction { public AvatarTerm getRightHand () { return this.rightHand; } + + public AvatarExpressionSolver getActionSolver() { + return actionSolver; + } public boolean isABasicVariableSetting () { return (this.leftHand instanceof AvatarAttribute || this.leftHand instanceof AvatarTuple) && @@ -85,6 +95,19 @@ public class AvatarActionAssignment implements AvatarAction { public String toString () { return this.leftHand.getName() + " = " + this.rightHand.getName(); } + + public boolean buildActionSolver(AvatarBlock block) { + boolean res; + actionSolver = new AvatarExpressionSolver(rightHand.getName()); + res = actionSolver.buildExpression((AvatarBlock) block); + leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName()); + res &= !leftAttribute.hasError(); + return res; + } + + public void executeActionSolver(SpecificationBlock sb) { + leftAttribute.setValue(sb, actionSolver.getResult(sb)); + } @Override public boolean containsAMethodCall () { diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java index 264eef134bcdbf1805e5568c6e870334d9c11b4e..5f8ccad448546216a70744bd00f51b9a661b3334 100644 --- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java +++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java @@ -190,6 +190,30 @@ public class AvatarExpressionAttribute { return value; } + public void setValue(SpecificationState ss, int value) { + int v = value; + + if (isNot) { + v = (value == 0) ? 1 : 0; + } else if (isNegated) { + v = -value; + } + + ss.blocks[blockIndex].values[accessIndex] = v; + } + + public void setValue(SpecificationBlock sb, int value) { + int v = value; + + if (isNot) { + v = (value == 0) ? 1 : 0; + } else if (isNegated) { + v = -value; + } + + sb.values[accessIndex] = v; + } + public String toString() { String res = ""; if (isNot) { diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java index b90ea40fbada911b2b7980c6e66174b1953dc1aa..ca5d24b9e9e46f574329152b12a00a2b2ae85278 100644 --- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java +++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java @@ -159,20 +159,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { public AvatarSpecification getReworkedAvatarSpecification() { return spec; } - - private void initExpressionSolvers() { - for (AvatarBlock block : spec.getListOfBlocks()) { - AvatarStateMachine asm = block.getStateMachine(); - - for (AvatarStateMachineElement elt : asm.getListOfElements()) { - if (elt instanceof AvatarTransition) { - if (((AvatarTransition) elt).isGuarded()) { - ((AvatarTransition) elt).buildGuardSolver(); - } - } - } - } - } public int getNbOfStates() { if (states == null) { @@ -448,6 +434,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { nbOfThreads = Runtime.getRuntime().availableProcessors(); + nbOfThreads = 1; TraceManager.addDev("Starting the model checking with " + nbOfThreads + " threads"); TraceManager.addDev("Ignore internal state:" + ignoreInternalStates); startModelChecking(nbOfThreads); @@ -680,6 +667,28 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { } nbOfCurrentComputations = 0; } + + private void initExpressionSolvers() { + AvatarTransition at; + + for (AvatarBlock block : spec.getListOfBlocks()) { + AvatarStateMachine asm = block.getStateMachine(); + + for (AvatarStateMachineElement elt : asm.getListOfElements()) { + if (elt instanceof AvatarTransition) { + at = (AvatarTransition) elt; + if (at.isGuarded()) { + at.buildGuardSolver(); + } + for (AvatarAction aa : at.getActions()) { + if (aa instanceof AvatarActionAssignment) { + ((AvatarActionAssignment) aa).buildActionSolver(block); + } + } + } + } + } + } private void prepareTransitionsOfState(SpecificationState _ss) { @@ -1419,23 +1428,25 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { if (retAction == null) { retAction = nameOfVar + "=" + act; } - - int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar); - AvatarType type = block.getAttribute(indexVar).getType(); - if (indexVar != -1) { - if (type == AvatarType.INTEGER) { - //TraceManager.addDev("Evaluating int expr=" + act); - int result = evaluateIntExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]); - _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result; - } else if (type == AvatarType.BOOLEAN) { - boolean bool = evaluateBoolExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]); - if (bool) { - _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 1; - } else { - _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 0; - } - } - } + + ((AvatarActionAssignment) aAction).executeActionSolver(_newState.blocks[_st.blocksInt[0]]); + +// int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar); +// AvatarType type = block.getAttribute(indexVar).getType(); +// if (indexVar != -1) { +// if (type == AvatarType.INTEGER) { +// //TraceManager.addDev("Evaluating int expr=" + act); +// int result = evaluateIntExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]); +// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result; +// } else if (type == AvatarType.BOOLEAN) { +// boolean bool = evaluateBoolExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]); +// if (bool) { +// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 1; +// } else { +// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 0; +// } +// } +// } } }