package models.dataConstraintModel; import java.util.ArrayList; import java.util.HashMap; import java.util.Map.Entry; import models.dataFlowModel.ResolvingMultipleDefinitionIsFutureWork; public class StateTransition { private Expression curStateExpression = null; private Expression nextStateExpression = null; private Expression messageExpression = null; public Expression getCurStateExpression() { return curStateExpression; } public void setCurStateExpression(Expression curStateExpression) { this.curStateExpression = curStateExpression; } public Expression getNextStateExpression() { return nextStateExpression; } public void setNextStateExpression(Expression nextStateExpression) { this.nextStateExpression = nextStateExpression; } public Expression getMessageExpression() { return messageExpression; } public void setMessageExpression(Expression messageExpression) { this.messageExpression = messageExpression; } public Expression deriveMessageConstraintFor(Expression curState, Expression nextState) throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork { HashMap<Variable, ArrayList<Expression>> bindings = new HashMap<>(); Expression curStateTerm = getCurStateExpression(); HashMap<Position, Variable> curStateVars = curStateTerm.getVariables(); for (Entry<Position, Variable> curStateVarEnt: curStateVars.entrySet()) { Variable var = curStateVarEnt.getValue(); Position varPos = curStateVarEnt.getKey(); Expression valueCalc = curStateTerm.getInverseMap(curState, varPos); if (valueCalc != null) { ArrayList<Expression> values = bindings.get(var); if (values == null) { values = new ArrayList<Expression>(); bindings.put(var, values); } values.add(valueCalc); } } Expression nextStateTerm = getNextStateExpression(); HashMap<Position, Variable> nextStateVars = nextStateTerm.getVariables(); for (Entry<Position, Variable> nextStateVarEnt: nextStateVars.entrySet()) { Variable var = nextStateVarEnt.getValue(); Position varPos = nextStateVarEnt.getKey(); Expression valueCalc = nextStateTerm.getInverseMap(nextState, varPos); if (valueCalc != null) { ArrayList<Expression> values = bindings.get(var); if (values == null) { values = new ArrayList<Expression>(); bindings.put(var, values); } values.add(valueCalc); } } Expression messageTerm = getMessageExpression(); if (!(messageTerm instanceof Term)) throw new InvalidMessage(); HashMap<Position, Variable> messageVars = messageTerm.getVariables(); for (Variable var: messageVars.values()) { if (bindings.get(var) != null) { if (bindings.get(var).size() > 1) throw new ResolvingMultipleDefinitionIsFutureWork(); messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next()); } } return messageTerm; } public Expression deriveNextStateExpressionFor(Expression curState, Term concreteMessage) throws ResolvingMultipleDefinitionIsFutureWork, ValueUndefined { HashMap<Variable, Expression> bindings = new HashMap<>(); Expression curStateTerm = getCurStateExpression(); HashMap<Position, Variable> curStateVars = curStateTerm.getVariables(); for (Entry<Position, Variable> curStateVarEnt: curStateVars.entrySet()) { Variable var = curStateVarEnt.getValue(); Position varPos = curStateVarEnt.getKey(); Expression valueCalc = curStateTerm.getInverseMap(curState, varPos); if (valueCalc != null) { if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork(); bindings.put(var, valueCalc); } } Expression messageTerm = getMessageExpression(); HashMap<Position, Variable> messageVars = messageTerm.getVariables(); for (Entry<Position, Variable> messageVarEnt: messageVars.entrySet()) { Variable var = messageVarEnt.getValue(); Position varPos = messageVarEnt.getKey(); Expression valueCalc = concreteMessage.getSubTerm(varPos); if (valueCalc != null) { if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork(); bindings.put(var, valueCalc); } } Expression nextStateTerm = getNextStateExpression(); if (nextStateTerm instanceof Variable) { nextStateTerm = bindings.get((Variable) nextStateTerm); if (nextStateTerm == null) throw new ValueUndefined(); } else { for (Variable var: bindings.keySet()) { nextStateTerm = ((Term) nextStateTerm).substitute(var, bindings.get(var)); } } return nextStateTerm; } }