diff --git a/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model new file mode 100644 index 0000000..4012b23 --- /dev/null +++ b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model @@ -0,0 +1,33 @@ +channel Signup { + out accounts(adb:Map, signUp(aid:Str, name:Str)) = insert(adb, aid, {"name": name, "point": 0}) +} + +channel ChangeName(aid:Str) { + out accounts.{aid}.name(prev_name:Str, changeName(name)) = name +} + +channel CreateRoom { + out rooms(rdb:Map, createRoom(rid:Str)) = insert(rdb, rid, {"members": nil, "battle": false}) +} + +channel AddRoomMember(rid:Str) { + out rooms.{rid}.members(mList:List, addRoomMember(id:Str)) = append(mList, {"id": id}) +} + +channel Battle(rid:Str) { + out rooms.{rid}.battle(prev_result, battle(result:Bool)) = result +} + +channel RoomName(rid:Str, mno:Int) { + in rooms.{rid}.members.{mno}.id(prev_mid:Str, sync(mid, name)) = mid + in accounts.{mid}.name(prev_name:Str, sync(mid, name)) = name + out rooms.{rid}.members.{mno}.name(prev_name:Str, sync(mid, name)) = name +} + +channel RoomResult(rid:Str) { + in rooms.{rid}.battle(prev_result, sync2(result, mid)) = result + sub RoomResult2(mno:Int) { + in rooms.{rid}.members.{mno}.id(prev_mid:Str, sync2(result, mid)) = mid + out accounts.{mid}.point(prev_point:Int, sunc2(result, mid)) = if(result, prev_point + 1, prev_point) + } +} diff --git a/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java b/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java index ac41269..6957304 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java +++ b/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java @@ -128,6 +128,8 @@ @Override public Expression unify(Expression another) { if (another instanceof Variable) return (Expression) this.clone(); + if (this instanceof Constant) return (Expression) this.clone(); + if (another instanceof Constant) return (Expression) another.clone(); if (another instanceof Term) { Term anotherTerm = (Term) another; if (!symbol.equals(anotherTerm.symbol)) return null; diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/Channel.java b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/Channel.java index af144c8..022644b 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/Channel.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/Channel.java @@ -60,6 +60,7 @@ public void addChild(Channel child) { children.add(child); child.parent = this; + child.refleshOutside(); } public List getSelectors() { @@ -115,6 +116,28 @@ } } + public void refleshOutside() { + for (ChannelMember channelMember: channelMembers) { + if (getAllSelectors().size() > 0) { + Set params = new HashSet<>(); + for (Selector s: getAllSelectors()) { + params.add(s.getExpression()); + } + if (!params.containsAll(channelMember.getResource().getPathParams())) { + channelMember.setOutside(true); + } else { + channelMember.setOutside(false); + } + } else { + if (channelMember.getResource().getPathParams().size() == 0) { + channelMember.setOutside(false); + } else { + channelMember.setOutside(true); + } + } + } + } + public void removeChannelMember(ResourcePath res) { for (ChannelMember cm: channelMembers) { if (cm.getResource() == res) { diff --git a/AlgebraicDataflowArchitectureModel/src/simulator/Event.java b/AlgebraicDataflowArchitectureModel/src/simulator/Event.java index b9cf65c..b6382f6 100644 --- a/AlgebraicDataflowArchitectureModel/src/simulator/Event.java +++ b/AlgebraicDataflowArchitectureModel/src/simulator/Event.java @@ -201,6 +201,9 @@ return dependingParameters; } + public Set getChildren() { + return childEvents; + } /** * Update the values of the depending channel selectors @@ -209,6 +212,21 @@ * @return calculated message constraint by this event */ public Term constructMessageAndDescendantEvents(IResourceStateValueProvider resourceStateValueProvider, boolean doesUpdateDependingParameters) { + + try { + Map> substitutedPositionsInMessageFromChannels = new HashMap<>(); + return constructMessageAndDesdendantEvents(resourceStateValueProvider, substitutedPositionsInMessageFromChannels, doesUpdateDependingParameters); + } catch (ResolvingMultipleDefinitionIsFutureWork | InvalidMessage | UnificationFailed e) { + e.printStackTrace(); + } + return null; + } + + private Term constructMessageAndDesdendantEvents(IResourceStateValueProvider resourceStateValueProvider, + Map> substitutedPositionsInMessageFromChannels, boolean doesUpdateDependingParameters) + throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork, UnificationFailed { + Term unifiedMessage = null; + Expression messageConstraint = null; IResourceStateAccessor resouceStateAccessor = new IResourceStateAccessor() { @Override public Expression getCurrentStateAccessorFor(ChannelMember target, ChannelMember from) { @@ -228,26 +246,11 @@ return resourceStateValueProvider.getCurrentStateValueOf(resId); } }; - - try { - Map> substitutedPositionsInMessageFromChannels = new HashMap<>(); - return constructMessageAndDesdendantEvents(this.channel, resouceStateAccessor, substitutedPositionsInMessageFromChannels, doesUpdateDependingParameters); - } catch (ResolvingMultipleDefinitionIsFutureWork | InvalidMessage | UnificationFailed e) { - e.printStackTrace(); - } - return null; - } - - private Term constructMessageAndDesdendantEvents(DataTransferChannel channel, IResourceStateAccessor resouceStateAccessor, - Map> substitutedPositionsInMessageFromChannels, boolean doesUpdateDependingParameters) - throws InvalidMessage, ResolvingMultipleDefinitionIsFutureWork, UnificationFailed { - Term unifiedMessage = null; // Calculate message constraints from leaf channel members on the channel member dependency graph. Map> dependency = channel.getMemberDependency(); if (dependency.size() == 0) { // No channel member dependency. - Expression messageConstraint = null; for (ChannelMember channelMember: channel.getInputChannelMembers()) { // Calculate message constraint from an input state transition messageConstraint = channel.calcMessageConstraintForInputMember(channelMember, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); @@ -272,85 +275,25 @@ } } } - return unifiedMessage; - } - Set toResolve = new HashSet<>(); - Set resolved = new HashSet<>(); - for (Set depended: dependency.values()) { - toResolve.addAll(depended); - } - for (ChannelMember depending: dependency.keySet()) { - toResolve.remove(depending); - } - Expression messageConstraint = null; - if ((messageConstraint = getMessage()) instanceof Term) { - unifiedMessage = (Term) messageConstraint; - } - for (ChannelMember leafMember: toResolve) { - if (channel.getInputChannelMembers().contains(leafMember)) { - // Calculate message constraint from an input state transition - messageConstraint = channel.calcMessageConstraintForInputMember(leafMember, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); - } else if (channel.getReferenceChannelMembers().contains(leafMember)) { - // Calculate message constraint from a reference state transition - messageConstraint = channel.calcMessageConstraintForReferenceMember(leafMember, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); + } else { + Set toResolve = new HashSet<>(); + Set resolved = new HashSet<>(); + for (Set depended: dependency.values()) { + toResolve.addAll(depended); } - if (unifiedMessage == null) { + for (ChannelMember depending: dependency.keySet()) { + toResolve.remove(depending); + } + if ((messageConstraint = getMessage()) instanceof Term) { unifiedMessage = (Term) messageConstraint; - } else { - unifiedMessage = (Term) unifiedMessage.unify(messageConstraint); - if (unifiedMessage == null) { - throw new UnificationFailed(); - } } - } - resolved.addAll(toResolve); - toResolve.clear(); - - // Calculate message constraints from remaining members on the channel member dependency graph. - for (;;) { - for (Map.Entry> dependEnt: dependency.entrySet()) { - ChannelMember dependingMem = dependEnt.getKey(); - Set dependedMems = dependEnt.getValue(); - if (!resolved.contains(dependingMem) && resolved.containsAll(dependedMems)) { - toResolve.add(dependingMem); - } - } - if (toResolve.size() == 0) break; - for (ChannelMember dependingMem: toResolve) { - // Fill the path parameters of the resource path of a depending channel member. - if (doesUpdateDependingParameters) { - Set dependingVarPosInMessage = new HashSet<>(); - ResourcePath filledResPath = channel.fillOutsideResourcePath(dependingMem.getResource(), unifiedMessage, dependingMem.getStateTransition().getMessageExpression(), dependingVarPosInMessage); - ResourcePath unfilledResPath = dependingMem.getResource(); - for (int i = 0; i < unfilledResPath.getPathParamsAndConstraints().size(); i++) { - Expression var = unfilledResPath.getPathParamsAndConstraints().get(i).getKey(); - Expression val = filledResPath.getPathParamsAndConstraints().get(i).getKey(); - Expression constraint = unfilledResPath.getPathParamsAndConstraints().get(i).getValue(); - if (constraint != null && !constraint.equals(val)) { - // The value of the path parameter does not satisfy the constraint defined for the parameter. - return null; // Not to fire this event. - } - boolean isSelector = false; - for (Selector sel: channel.getAllSelectors()) { - if (sel.getExpression().equals(var)) { - isSelector = true; - break; - } - } - if (!isSelector) { - // Update a depending channel parameter - updateDependingParameter(var, val); - } - } - } - - // Calculate message constraint - if (channel.getInputChannelMembers().contains(dependingMem)) { + for (ChannelMember leafMember: toResolve) { + if (channel.getInputChannelMembers().contains(leafMember)) { // Calculate message constraint from an input state transition - messageConstraint = channel.calcMessageConstraintForInputMember(dependingMem, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); - } else if (channel.getReferenceChannelMembers().contains(dependingMem)) { + messageConstraint = channel.calcMessageConstraintForInputMember(leafMember, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); + } else if (channel.getReferenceChannelMembers().contains(leafMember)) { // Calculate message constraint from a reference state transition - messageConstraint = channel.calcMessageConstraintForReferenceMember(dependingMem, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); + messageConstraint = channel.calcMessageConstraintForReferenceMember(leafMember, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); } if (unifiedMessage == null) { unifiedMessage = (Term) messageConstraint; @@ -363,25 +306,114 @@ } resolved.addAll(toResolve); toResolve.clear(); + + // Calculate message constraints from remaining members on the channel member dependency graph. + for (;;) { + for (Map.Entry> dependEnt: dependency.entrySet()) { + ChannelMember dependingMem = dependEnt.getKey(); + Set dependedMems = dependEnt.getValue(); + if (!resolved.contains(dependingMem) && resolved.containsAll(dependedMems)) { + toResolve.add(dependingMem); + } + } + if (toResolve.size() == 0) break; + for (ChannelMember dependingMem: toResolve) { + // Fill the path parameters of the resource path of a depending channel member. + if (doesUpdateDependingParameters) { + Set dependingVarPosInMessage = new HashSet<>(); + ResourcePath filledResPath = channel.fillOutsideResourcePath(dependingMem.getResource(), unifiedMessage, dependingMem.getStateTransition().getMessageExpression(), dependingVarPosInMessage); + ResourcePath unfilledResPath = dependingMem.getResource(); + for (int i = 0; i < unfilledResPath.getPathParamsAndConstraints().size(); i++) { + Expression var = unfilledResPath.getPathParamsAndConstraints().get(i).getKey(); + Expression val = filledResPath.getPathParamsAndConstraints().get(i).getKey(); + Expression constraint = unfilledResPath.getPathParamsAndConstraints().get(i).getValue(); + if (constraint != null && !constraint.equals(val)) { + // The value of the path parameter does not satisfy the constraint defined for the parameter. + return null; // Not to fire this event. + } + boolean isSelector = false; + for (Selector sel: channel.getAllSelectors()) { + if (sel.getExpression().equals(var)) { + isSelector = true; + break; + } + } + if (!isSelector) { + // Update a depending channel parameter + updateDependingParameter(var, val); + } + } + } + + // Calculate message constraint + if (channel.getInputChannelMembers().contains(dependingMem)) { + // Calculate message constraint from an input state transition + messageConstraint = channel.calcMessageConstraintForInputMember(dependingMem, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); + } else if (channel.getReferenceChannelMembers().contains(dependingMem)) { + // Calculate message constraint from a reference state transition + messageConstraint = channel.calcMessageConstraintForReferenceMember(dependingMem, null, resouceStateAccessor, null, substitutedPositionsInMessageFromChannels); + } + if (unifiedMessage == null) { + unifiedMessage = (Term) messageConstraint; + } else { + unifiedMessage = (Term) unifiedMessage.unify(messageConstraint); + if (unifiedMessage == null) { + throw new UnificationFailed(); + } + } + } + resolved.addAll(toResolve); + toResolve.clear(); + } } - // Calculate message constraints from child channels. -// for (Channel childChannel: channel.getChildren()) { -// for (Selector nextSelector: childChannel.getSelectors()) { -// -// } -// Event childEvent = new Event((DataTransferChannel) childChannel, (Expression) messageConstraint.clone(), null, null); -// messageConstraint = constructMessageAndDesdendantEvents((DataTransferChannel) childChannel, resouceStateAccessor, substitutedPositionsInMessageFromChannels); -// if (unifiedMessage == null) { -// unifiedMessage = (Term) messageConstraint; -// } else { -// unifiedMessage = (Term) unifiedMessage.unify(messageConstraint); -// if (unifiedMessage == null) { -// throw new UnificationFailed(); -// } -// } -// childEvents.add(childEvent); -// } + // Trigger child events and calculate message constraints from child channels. + for (Channel childChannel: channel.getChildren()) { + // Search the deepest input side resource path in each child channel that matches the channel parameters. + ChannelMember in = null; + for (ChannelMember cm: ((DataTransferChannel) childChannel).getInputChannelMembers()) { + if (!cm.isOutside()) { + ResourcePath resPath = cm.getResource(); + boolean bContainsAll = true; + for (Selector sel: childChannel.getAllSelectors()) { + if (!resPath.getPathParams().contains(sel.getExpression())) { + bContainsAll = false; + break; + } + } + if (bContainsAll) { + in = cm; + break; + } + } + } + if (in != null) { + // Trigger events for all resources under this event's input resource that matches the deepest input side resource path. + Resource baseResource = inputResource; + while (baseResource.getResourceHierarchy().getNumParameters() == 0) { + if (baseResource.getParent() == null) break; + baseResource = baseResource.getParent(); + } + Term parentEventMessage = (Term) unifiedMessage.clone(); + for (Resource res: baseResource.getDescendants(in.getResource().getResourceHierarchy())) { + Event childEvent = new Event((DataTransferChannel) childChannel, in.getResource(), res); + childEvent.setMessage(parentEventMessage); + messageConstraint = childEvent.constructMessageAndDesdendantEvents(resourceStateValueProvider, substitutedPositionsInMessageFromChannels, true); + if (messageConstraint != null) { + childEvent.setMessage(messageConstraint); + if (unifiedMessage == null) { + unifiedMessage = (Term) messageConstraint; + } else { + unifiedMessage = (Term) unifiedMessage.unify(messageConstraint); + if (unifiedMessage == null) { + throw new UnificationFailed(); + } + } + childEvents.add(childEvent); + } + } + } + } return unifiedMessage; } diff --git a/AlgebraicDataflowArchitectureModel/src/simulator/Resource.java b/AlgebraicDataflowArchitectureModel/src/simulator/Resource.java index 6ddf8d4..8cd943f 100644 --- a/AlgebraicDataflowArchitectureModel/src/simulator/Resource.java +++ b/AlgebraicDataflowArchitectureModel/src/simulator/Resource.java @@ -1,8 +1,10 @@ package simulator; import java.util.Collection; +import java.util.HashSet; import java.util.LinkedHashMap; import java.util.Map; +import java.util.Set; import models.algebra.Constant; import models.algebra.Expression; @@ -177,6 +179,20 @@ return children; } + public Set getDescendants(ResourceHierarchy res) { + if (this.getResourceHierarchy().equals(res)) { + Set descendants = new HashSet<>(); + descendants.add(this); + return descendants; + } + if (!res.toString().startsWith(this.getResourceHierarchy().toString())) return new HashSet<>(); + Set descendants = new HashSet<>(); + for (Resource child: getChildren()) { + descendants.addAll(child.getDescendants(res)); + } + return descendants; + } + public Resource getDescendant(ResourceIdentifier resId) { if (this.getResourceIdentifier().equals(resId)) return this; if (!resId.startsWith(this.getResourceIdentifier())) return null; diff --git a/AlgebraicDataflowArchitectureModel/src/simulator/Simulator.java b/AlgebraicDataflowArchitectureModel/src/simulator/Simulator.java index f1f84bd..bd2ca59 100644 --- a/AlgebraicDataflowArchitectureModel/src/simulator/Simulator.java +++ b/AlgebraicDataflowArchitectureModel/src/simulator/Simulator.java @@ -197,8 +197,14 @@ return res.getState().getValue(); } }; - - DataTransferChannel channel = event.getChannel(); + + // First, fire the all child events. + for (Event childEvent: event.getChildren()) { + fireEvent(childEvent, curSystemState, nextSystemState); + } + + // Fire this event. + DataTransferChannel channel = event.getChannel(); if (channel.getOutputResources().size() > 0) { // For each output resource, calculate the next state. for (ChannelMember out: channel.getOutputChannelMembers()) {