package models.dataFlowModel;

import java.util.AbstractMap;
import java.util.AbstractMap.SimpleEntry;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import models.algebra.Constant;
import models.algebra.Expression;
import models.algebra.InvalidMessage;
import models.algebra.Parameter;
import models.algebra.ParameterizedIdentifierIsFutureWork;
import models.algebra.Position;
import models.algebra.Term;
import models.algebra.UnificationFailed;
import models.algebra.ValueUndefined;
import models.algebra.Variable;
import models.dataConstraintModel.*;

public class DataTransferChannel extends Channel {
	protected Set<ChannelMember> inputChannelMembers = null;
	protected Set<ChannelMember> outputChannelMembers = null;
	protected Set<ChannelMember> referenceChannelMembers = null;
	
	public DataTransferChannel(String channelName) {
		super(channelName);
		inputChannelMembers = new HashSet<>();
		outputChannelMembers = new HashSet<>();
		referenceChannelMembers = new HashSet<>();
	}
	
	public DataTransferChannel(String channelName, Variable variable) {
		super(channelName, variable);
		inputChannelMembers = new HashSet<>();
		outputChannelMembers = new HashSet<>();
		referenceChannelMembers = new HashSet<>();
	}
	
	public DataTransferChannel(String channelName, List<Variable> variables) {
		super(channelName, variables);
		inputChannelMembers = new HashSet<>();
		outputChannelMembers = new HashSet<>();
		referenceChannelMembers = new HashSet<>();
	}

	public Set<ChannelMember> getInputChannelMembers() {
		return inputChannelMembers;
	}
	
	public void setInputChannelMembers(Set<ChannelMember> inputChannelMembers) {
		this.inputChannelMembers = inputChannelMembers;
	}
	
	private void addInputChannelMember(ChannelMember inputChannelMember) {
		inputChannelMembers.add(inputChannelMember);
	}
	
	public Set<ChannelMember> getOutputChannelMembers() {
		return outputChannelMembers;
	}
	
	public void setOutputChannelMembers(Set<ChannelMember> outputChannelMembers) {
		this.outputChannelMembers = outputChannelMembers;
	}
	
	private void addOutputChannelMember(ChannelMember outputChannelMember) {
		outputChannelMembers.add(outputChannelMember);
	}
	
	public Set<ChannelMember> getReferenceChannelMembers() {
		return referenceChannelMembers;
	}
	
	public void setReferenceChannelMembers(Set<ChannelMember> referenceChannelMembers) {
		this.referenceChannelMembers = referenceChannelMembers;
	}
	
	private void addReferenceChannelMember(ChannelMember referenceChannelMember) {
		referenceChannelMembers.add(referenceChannelMember);
	}
		
	public void addChannelMemberAsInput(ChannelMember inputChannelMember) {
		addChannelMember(inputChannelMember);
		addInputChannelMember(inputChannelMember);
	}
	
	public void addChannelMemberAsOutput(ChannelMember outputChannelMember) {
		addChannelMember(outputChannelMember);
		addOutputChannelMember(outputChannelMember);
	}
	
	public void addChannelMemberAsReference(ChannelMember referenceChannelMember) {
		addChannelMember(referenceChannelMember);
		addReferenceChannelMember(referenceChannelMember);
	}
	
	public void removeChannelMember(ResourcePath id) {
		for (ChannelMember cm: inputChannelMembers) {
			if (cm.getResource() == id) {
				inputChannelMembers.remove(cm);
				super.removeChannelMember(id);
				return;
			}
		}
		for (ChannelMember cm: outputChannelMembers) {
			if (cm.getResource() == id) {
				outputChannelMembers.remove(cm);
				super.removeChannelMember(id);
				return;
			}
		}
		for (ChannelMember cm: referenceChannelMembers) {
			if (cm.getResource() == id) {
				referenceChannelMembers.remove(cm);
				super.removeChannelMember(id);
				return;
			}
		}
	}
	
	public Set<ResourcePath> getInputResources() {
		Set<ResourcePath> inputResources = new HashSet<>();
		for (ChannelMember member: inputChannelMembers) {
			inputResources.add(member.getResource());
		}
		return inputResources;
	}
	
	public Set<ResourcePath> getOutputResources() {
		Set<ResourcePath> outputResources = new HashSet<>();
		for (ChannelMember member: outputChannelMembers) {
			outputResources.add(member.getResource());
		}
		return outputResources;
	}
	
	public Set<ResourcePath> getReferenceResources() {
		Set<ResourcePath> referenceResources = new HashSet<>();
		for (ChannelMember member: referenceChannelMembers) {
			referenceResources.add(member.getResource());
		}
		return referenceResources;
	}
	
	/**
	 * Derive the update expression of the state of the target channel member.
	 * @param targetMember a channel member whose state is to be updated
	 * @return the derived update expression
	 * @throws ParameterizedIdentifierIsFutureWork
	 * @throws ResolvingMultipleDefinitionIsFutureWork
	 * @throws InvalidMessage
	 * @throws UnificationFailed
	 * @throws ValueUndefined
	 */
	public Expression deriveUpdateExpressionOf(ChannelMember targetMember) throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {
		IResourceStateAccessor defaultStateAccessor = new IResourceStateAccessor() {
			HashMap<String, Parameter> curStateParams = new HashMap<>();
			HashMap<String, Parameter> nextStateParams = new HashMap<>();

			@Override
			public Expression getCurrentStateAccessorFor(ChannelMember target, ChannelMember from) {
				String resource = target.getResource().getLeafResourceName();
				Parameter curStateParam = curStateParams.get(resource);
				if (curStateParam == null) {
					curStateParam = new Parameter("cur" + resource);
					curStateParams.put(resource, curStateParam);
				}
				return curStateParam;
			}

			@Override
			public Expression getNextStateAccessorFor(ChannelMember target, ChannelMember from) {
				String resource = target.getResource().getLeafResourceName();
				Parameter nextStateParam = nextStateParams.get(resource);
				if (nextStateParam == null) {
					nextStateParam = new Parameter("next" + target);
					nextStateParams.put(resource, nextStateParam);
				}
				return nextStateParam;
			}

			@Override
			public Expression getDirectStateAccessorFor(ResourcePath target, ResourcePath from) {
				String resource = target.getLeafResourceName();
				Parameter curStateParam = curStateParams.get(resource);
				if (curStateParam == null) {
					curStateParam = new Parameter("cur" + resource);
					curStateParams.put(resource, curStateParam);
				}
				return curStateParam;
			}
		};
		return deriveUpdateExpressionOf(targetMember, defaultStateAccessor).getKey();
	}
	
	/**
	 * Derive the state update calculation of the target channel member with a given resource push/pull state accessor.
	 * @param targetMember a channel member whose state is to be updated
	 * @param stateAccessor a push/pull resource state accessor
	 * @return the derived update calculation and the unified message
	 * @throws ParameterizedIdentifierIsFutureWork
	 * @throws ResolvingMultipleDefinitionIsFutureWork
	 * @throws InvalidMessage
	 * @throws UnificationFailed
	 * @throws ValueUndefined
	 */
	public Map.Entry<Expression, Expression> deriveUpdateExpressionOf(ChannelMember targetMember, IResourceStateAccessor stateAccessor) 
			throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {
		return deriveUpdateExpressionOf(targetMember, stateAccessor, null);
	}

	public Map.Entry<Expression, Expression> deriveUpdateExpressionOf(ChannelMember targetMember, IResourceStateAccessor stateAccessor, Map<ChannelMember, IResourceStateAccessor> inputResourceToStateAccessor) 
			throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {
		if (!getOutputChannelMembers().contains(targetMember)) return null;
		
		// Calculate unified message constraints
		Map<ChannelMember, Set<Position>> substitutedPositionsFromChannels = new HashMap<>();
		Term unifiedMessage = calcUnifiedMessage(targetMember, stateAccessor, inputResourceToStateAccessor, substitutedPositionsFromChannels);
		
		// Calculate the next state of target resource from the unified message and the current resource state
		Expression curOutputStateAccessor = stateAccessor.getCurrentStateAccessorFor(targetMember, targetMember);
		if (unifiedMessage == null) {
			// for IOChannel
			if (targetMember.getStateTransition().getMessageExpression() instanceof Term) {
				unifiedMessage = (Term) targetMember.getStateTransition().getMessageExpression();
			}
		}
		return new AbstractMap.SimpleEntry<>(targetMember.getStateTransition().deriveNextStateExpressionFor(curOutputStateAccessor, unifiedMessage), unifiedMessage);
	}
	
	/**
	 * Derive the state update calculation of the target channel member with a message and a given resource push/pull state accessor.
	 * @param targetMember a channel member whose state is to be updated
	 * @param message a message on the channel
	 * @param stateAccessor a push/pull resource state accessor
	 * @return the derived update calculation
	 * @throws ParameterizedIdentifierIsFutureWork
	 * @throws ResolvingMultipleDefinitionIsFutureWork
	 * @throws InvalidMessage
	 * @throws UnificationFailed
	 * @throws ValueUndefined
	 */
	public Expression deriveUpdateExpressionOf(ChannelMember targetMember, Term message, IResourceStateAccessor stateAccessor) 
			throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {
		if (!getOutputChannelMembers().contains(targetMember)) return null;
		
		// Calculate the next state of target resource from the unified message and the current resource state
		Expression curOutputStateAccessor = stateAccessor.getCurrentStateAccessorFor(targetMember, targetMember);
		return targetMember.getStateTransition().deriveNextStateExpressionFor(curOutputStateAccessor, message);
	}
	
	/**
	 * Fill outside resource paths with a given resource push/pull state accessor.
	 * @param targetMember a channel member whose state is to be updated
	 * @param stateAccessor a push/pull resource state accessor
	 * @return map from a depending channel member to the pair of the filled resource path and the set of the depended channel members
	 * @throws ParameterizedIdentifierIsFutureWork
	 * @throws ResolvingMultipleDefinitionIsFutureWork
	 * @throws InvalidMessage
	 * @throws UnificationFailed
	 * @throws ValueUndefined
	 */
	public Map<ChannelMember, Entry<ResourcePath, Set<ChannelMember>>> fillOutsideResourcePaths(ChannelMember targetMember, IResourceStateAccessor stateAccessor) 
			throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {		
		return fillOutsideResourcePaths(targetMember, stateAccessor, null);
	}

	public Map<ChannelMember, Entry<ResourcePath, Set<ChannelMember>>> fillOutsideResourcePaths(ChannelMember targetMember, IResourceStateAccessor stateAccessor, Map<ChannelMember, IResourceStateAccessor> inputResourceToStateAccessor) 
			throws ParameterizedIdentifierIsFutureWork, ResolvingMultipleDefinitionIsFutureWork, InvalidMessage, UnificationFailed, ValueUndefined {
		if (!getOutputChannelMembers().contains(targetMember)) return null;
		Map<ChannelMember, Entry<ResourcePath, Set<ChannelMember>>> resourcePaths = new HashMap<>();
		
		// Calculate unified message constraints from input and reference state transitions
		Map<ChannelMember, Set<Position>> substitutedPositionsInMessageFromChannels = new HashMap<>();
		Term unifiedMessage = calcUnifiedMessage(targetMember, stateAccessor, inputResourceToStateAccessor, substitutedPositionsInMessageFromChannels);
		
		// Fill outside resource paths
		if (unifiedMessage != null) {
			for (ChannelMember cm: getInputChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = new HashSet<>();
					ResourcePath filledResPath = fillOutsideResourcePath(cm.getResource(), unifiedMessage, targetMember.getStateTransition().getMessageExpression(), dependingVarPosInMessage);
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessageFromChannels.keySet()) {
						for (Position otherPos: substitutedPositionsInMessageFromChannels.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					resourcePaths.put(cm, new AbstractMap.SimpleEntry<>(filledResPath, dependingChannelMembers));
				}
			}
			for (ChannelMember cm: getReferenceChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = new HashSet<>();
					ResourcePath filledResPath = fillOutsideResourcePath(cm.getResource(), unifiedMessage, targetMember.getStateTransition().getMessageExpression(), dependingVarPosInMessage);
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessageFromChannels.keySet()) {
						for (Position otherPos: substitutedPositionsInMessageFromChannels.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					resourcePaths.put(cm, new AbstractMap.SimpleEntry<>(filledResPath, dependingChannelMembers));
				}
			}
			for (ChannelMember cm: getOutputChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = new HashSet<>();
					ResourcePath filledResPath = fillOutsideResourcePath(cm.getResource(), unifiedMessage, targetMember.getStateTransition().getMessageExpression(), dependingVarPosInMessage);
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessageFromChannels.keySet()) {
						for (Position otherPos: substitutedPositionsInMessageFromChannels.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					resourcePaths.put(cm, new AbstractMap.SimpleEntry<>(filledResPath, dependingChannelMembers));
				}
			}
		}
		return resourcePaths;
	}
	
	public Map<ChannelMember, Set<ChannelMember>> getMemberDependency() {
		Map<ChannelMember, Set<ChannelMember>> dependency = new HashMap<>();
		
		// Collect depended channel members and their positions in the message
		Map<ChannelMember, Set<Position>> substitutedPositionsInMessage = getDependedChannelMembersAndTheirPositionsInMessage();
		
		// Resolve dependency for each outside resource path
		if (substitutedPositionsInMessage != null) {
			for (ChannelMember cm: getInputChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = getPossitionsInMessageThatChannelMemberDependsOn(cm.getResource(), cm.getStateTransition().getMessageExpression());
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessage.keySet()) {
						for (Position otherPos: substitutedPositionsInMessage.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					dependency.put(cm, dependingChannelMembers);
				}
			}
			for (ChannelMember cm: getReferenceChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = getPossitionsInMessageThatChannelMemberDependsOn(cm.getResource(), cm.getStateTransition().getMessageExpression());
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessage.keySet()) {
						for (Position otherPos: substitutedPositionsInMessage.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					dependency.put(cm, dependingChannelMembers);
				}
			}
			for (ChannelMember cm: getOutputChannelMembers()) {
				if (cm.isOutside()) {
					Set<Position> dependingVarPosInMessage = getPossitionsInMessageThatChannelMemberDependsOn(cm.getResource(), cm.getStateTransition().getMessageExpression());
					Set<ChannelMember> dependingChannelMembers =  new HashSet<>();
					for (ChannelMember otherCm: substitutedPositionsInMessage.keySet()) {
						for (Position otherPos: substitutedPositionsInMessage.get(otherCm)) {
							for (Position thisPos: dependingVarPosInMessage) {
								if (thisPos.isAncestorOf(otherPos)) {
									dependingChannelMembers.add(otherCm);
									break;
								}
							}
							if (dependingChannelMembers.contains(otherCm)) break;
						}
					}
					dependency.put(cm, dependingChannelMembers);
				}
			}
		}
		return dependency;
	}
	
	private Term calcUnifiedMessage(ChannelMember targetMember, IResourceStateAccessor stateAccessor, 
			Map<ChannelMember, IResourceStateAccessor> inputResourceToStateAccessor, Map<ChannelMember, Set<Position>> substitutedPositionsInMessageFromChannels)
			throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork, UnificationFailed {
		Set<Term> messageConstraints = new HashSet<>();
		
		// Calculate message constraints from input state transitions
		for (ChannelMember inputMember: getInputChannelMembers()) {
			Expression messageConstraintByInput = calcMessageConstraintForInputMember(inputMember, targetMember, stateAccessor, inputResourceToStateAccessor, substitutedPositionsInMessageFromChannels);
			messageConstraints.add((Term) messageConstraintByInput);
		}

		// Calculate message constraints from reference state transitions
		for (ChannelMember referenceMember: getReferenceChannelMembers()) {
			Expression messageConstraintByReference = calcMessageConstraintForReferenceMember(referenceMember, targetMember, stateAccessor, inputResourceToStateAccessor, substitutedPositionsInMessageFromChannels);
			messageConstraints.add((Term) messageConstraintByReference);
		}

		// Unify message constraints
		Term unifiedMessage = null;
		for (Term messageContraint: messageConstraints) {
			if (unifiedMessage == null) {
				unifiedMessage = messageContraint;
			} else {
				unifiedMessage = (Term) unifiedMessage.unify(messageContraint);
				if (unifiedMessage == null) {
					throw new UnificationFailed();
				}
			}
		}
		return unifiedMessage;
	}

	public Expression calcMessageConstraintForInputMember(ChannelMember inputMember, ChannelMember targetMember, IResourceStateAccessor stateAccessor, 
			Map<ChannelMember, IResourceStateAccessor> inputResourceToStateAccessor, Map<ChannelMember, Set<Position>> substitutedPositionsInMessageFromChannels)
			throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork {
		Expression curInputStateAccessor = null;
		Expression nextInputStateAccessor = null;
		if (inputResourceToStateAccessor == null) {
			curInputStateAccessor = stateAccessor.getCurrentStateAccessorFor(inputMember, targetMember);
			nextInputStateAccessor = stateAccessor.getNextStateAccessorFor(inputMember, targetMember);
		} else {
			curInputStateAccessor = inputResourceToStateAccessor.get(inputMember).getCurrentStateAccessorFor(inputMember, targetMember);
			nextInputStateAccessor = inputResourceToStateAccessor.get(inputMember).getNextStateAccessorFor(inputMember, targetMember);
		}
		Set<Position> substitutedPositionsInMessage = new HashSet<>();
		Expression messageConstraintByInput = inputMember.getStateTransition().deriveMessageConstraintFor(curInputStateAccessor, nextInputStateAccessor, substitutedPositionsInMessage);
		if (substitutedPositionsInMessage.size() > 0) substitutedPositionsInMessageFromChannels.put(inputMember, substitutedPositionsInMessage);
		return messageConstraintByInput;
	}

	public Expression calcMessageConstraintForReferenceMember(ChannelMember referenceMember, ChannelMember targetMember, IResourceStateAccessor stateAccessor,
			Map<ChannelMember, IResourceStateAccessor> inputResourceToStateAccessor, Map<ChannelMember, Set<Position>> substitutedPositionsInMessageFromChannels)
			throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork {
		Expression curInputStateAccessor = null;
		if (inputResourceToStateAccessor == null) {
			curInputStateAccessor = stateAccessor.getCurrentStateAccessorFor(referenceMember, targetMember);
		} else {
			curInputStateAccessor = inputResourceToStateAccessor.get(referenceMember).getCurrentStateAccessorFor(referenceMember, targetMember);
		}
		Set<Position> substitutedPositions = new HashSet<>();
		Expression messageConstraintByReference = referenceMember.getStateTransition().deriveMessageConstraintFor(curInputStateAccessor, substitutedPositions);
		if (substitutedPositions.size() > 0) substitutedPositionsInMessageFromChannels.put(referenceMember, substitutedPositions);
		return messageConstraintByReference;
	}
	
	/**
	 * Get depended channel members and their positions in the message.
	 * 
	 * @return depended channel members and their positions in the message
	 */
	private Map<ChannelMember, Set<Position>> getDependedChannelMembersAndTheirPositionsInMessage() {
		Map<ChannelMember, Set<Position>> channelMembersMessageDependsOn = new HashMap<>();
		// Collect channel members that the message depends on from input state transitions
		for (ChannelMember inputMember: getInputChannelMembers()) {
			Set<Position> substitutedPositionsInMessage = new HashSet<>();
			Expression messageTerm = inputMember.getStateTransition().getMessageExpression();
			Expression curStateTerm = inputMember.getStateTransition().getCurStateExpression();
			Expression nextStateTerm = inputMember.getStateTransition().getNextStateExpression();
			HashMap<Position, Variable> messageVars = messageTerm.getVariables();
			for (Entry<Position, Variable> varEnt: messageVars.entrySet()) {
				Variable var = varEnt.getValue();
				if (curStateTerm.getVariables().values().contains(var) || nextStateTerm.getVariables().values().contains(var)) {
					if (messageTerm instanceof Term) {
						substitutedPositionsInMessage.add(varEnt.getKey());
					} else if (messageTerm instanceof Variable) {
						if (messageTerm.equals(var)) {
							substitutedPositionsInMessage.add(new Position());
						}
					}
				}
			}
			if (substitutedPositionsInMessage.size() > 0) channelMembersMessageDependsOn.put(inputMember, substitutedPositionsInMessage);
		}

		// Collect channel members that the message depends on from reference state transitions
		for (ChannelMember referenceMember: getReferenceChannelMembers()) {
			Set<Position> substitutedPositionsInMessage = new HashSet<>();
			Expression messageTerm = referenceMember.getStateTransition().getMessageExpression();
			Expression curStateTerm = referenceMember.getStateTransition().getCurStateExpression();
			Expression nextStateTerm = referenceMember.getStateTransition().getNextStateExpression();
			HashMap<Position, Variable> messageVars = messageTerm.getVariables();
			for (Entry<Position, Variable> varEnt: messageVars.entrySet()) {
				Variable var = varEnt.getValue();
				if (curStateTerm.getVariables().values().contains(var) || nextStateTerm.getVariables().values().contains(var)) {
					if (messageTerm instanceof Term) {
						substitutedPositionsInMessage.add(varEnt.getKey());
					} else if (messageTerm instanceof Variable) {
						if (messageTerm.equals(var)) {
							substitutedPositionsInMessage.add(new Position());
						}
					}
				}
			}
			if (substitutedPositionsInMessage.size() > 0) channelMembersMessageDependsOn.put(referenceMember, substitutedPositionsInMessage);
		}
		return channelMembersMessageDependsOn;
	}

	public ResourcePath fillOutsideResourcePath(ResourcePath resource, Term unifiedMessage, Expression messageTerm, Set<Position> dependingVarPosInMessage) 
			throws ResolvingMultipleDefinitionIsFutureWork {
		ResourcePath filledResourcePath = new ResourcePath(resource);
		
		Map<Variable, Entry<Position, Expression>> bindings = new HashMap<>();
		Map<Position, Variable> messageVars = messageTerm.getVariables();
		for (Entry<Position, Variable> messageVarEnt: messageVars.entrySet()) {
			Variable var = messageVarEnt.getValue();
			Position varPos = messageVarEnt.getKey();
			Expression valueCalc = unifiedMessage.getSubTerm(varPos);
			if (valueCalc != null) {
				if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork();
				bindings.put(var, new AbstractMap.SimpleEntry<>(varPos, valueCalc));
			}
		}
		
		List<Expression> dstParams = filledResourcePath.getPathParams();
		for (int i = 0; i < filledResourcePath.getPathParams().size(); i++) {
			Expression pathParam = dstParams.get(i);
			if (pathParam instanceof Variable) {
				dstParams.set(i, bindings.get((Variable) pathParam).getValue());		// Replace a path parameter with a value in the unified message.
				dependingVarPosInMessage.add(bindings.get((Variable) pathParam).getKey());		// The position of the replaced variable in the message.
			} else if (pathParam instanceof Term) {
				Map<Position, Variable> pathParamVars = ((Term) pathParam).getVariables();
				for (Variable var: bindings.keySet()) {
					if (pathParamVars.values().contains(var)) {			// var is a subterm of a path parameter
						pathParam = ((Term) pathParam).substitute(var, bindings.get(var).getValue());	// Substitute a value in the unified message to var.
						dependingVarPosInMessage.add(bindings.get((Variable) var).getKey());		// The position of the replaced variable in the message.
					}
				}
				if (!(pathParam instanceof Constant)) {
					pathParam = ((Term) pathParam).reduce();
				}
				dstParams.set(i, pathParam);		// Replace a path parameter with the substituted term.
			}
		}
		return filledResourcePath;
	}
	
	private Set<Position> getPossitionsInMessageThatChannelMemberDependsOn(ResourcePath resourcePath, Expression messageTerm) {
		Set<Position> dependingVarPosInMessage = new HashSet<>();
		Map<Position, Variable> messageVars = messageTerm.getVariables();
		for (Expression pathParam: resourcePath.getPathParams()) {
			if (pathParam instanceof Variable) {
				for (Entry<Position, Variable> messageVarEnt: messageVars.entrySet()) {
					Variable var = messageVarEnt.getValue();
					Position varPos = messageVarEnt.getKey();
					if (pathParam.equals(var)) {
						dependingVarPosInMessage.add(varPos);
					}
				}
			} else if (pathParam instanceof Term) {
				Map<Position, Variable> pathParamVars = ((Term) pathParam).getVariables();
				for (Entry<Position, Variable> messageVarEnt: messageVars.entrySet()) {
					Variable var = messageVarEnt.getValue();
					Position varPos = messageVarEnt.getKey();
					if (pathParamVars.values().contains(var)) {
						dependingVarPosInMessage.add(varPos);
					}
				}
			}
		}
		return dependingVarPosInMessage;
	}
	
	@Override
	public String toString() {
		String channelSource = "channel " + getChannelName() + " {\n";
		for (ChannelMember inputMember: inputChannelMembers) {
			channelSource += "\t in " + inputMember + "\n";
		}
		for (ChannelMember refMember: referenceChannelMembers) {
			channelSource += "\t ref " + refMember + "\n";
		}
		for (ChannelMember outputMember: outputChannelMembers) {
			channelSource += "\t out " + outputMember + "\n";
		}
		channelSource += "}\n";
		return channelSource;
	}
	
	public interface IResourceStateAccessor {
		Expression getCurrentStateAccessorFor(ChannelMember target, ChannelMember from);
		Expression getNextStateAccessorFor(ChannelMember target, ChannelMember from);
		Expression getDirectStateAccessorFor(ResourcePath targetRes, ResourcePath fromRes);
	}
}