// Lock/Unlock for distributed
Persistent_GETX, desc="Another processor has priority to read/write";
Persistent_GETS, desc="Another processor has priority to read";
+ Persistent_GETS_Last_Token, desc="Another processor has priority to read, no more tokens";
Own_Lock_or_Unlock, desc="This processor now has priority";
// Triggers
Entry getCacheEntry(Address addr), return_by_ref="yes" {
if (L1DcacheMemory.isTagPresent(addr)) {
+ assert(L1IcacheMemory.isTagPresent(addr) == false);
return static_cast(Entry, L1DcacheMemory[addr]);
} else {
return static_cast(Entry, L1IcacheMemory[addr]);
int getTokens(Address addr) {
if (L1DcacheMemory.isTagPresent(addr)) {
+ assert(L1IcacheMemory.isTagPresent(addr) == false);
return static_cast(Entry, L1DcacheMemory[addr]).Tokens;
} else if (L1IcacheMemory.isTagPresent(addr)) {
return static_cast(Entry, L1IcacheMemory[addr]).Tokens;
// Make sure the token count is in range
assert(getCacheEntry(addr).Tokens >= 0);
assert(getCacheEntry(addr).Tokens <= max_tokens());
+ assert(getCacheEntry(addr).Tokens != (max_tokens() / 2));
if ((state == State:I_L) ||
(state == State:IM_L) ||
} else if ((state == State:S_L) ||
(state == State:SM_L)) {
assert(getCacheEntry(addr).Tokens >= 1);
+ assert(getCacheEntry(addr).Tokens < (max_tokens() / 2));
// Make sure the line is locked...
// assert(persistentTable.isLocked(addr));
// You have at least half the token in O-like states
if (state == State:O && state == State:OM) {
- assert(getCacheEntry(addr).Tokens >= 1); // Must have at least one token
- assert(getCacheEntry(addr).Tokens >= (max_tokens() / 2)); // Only mostly true; this might not always hold
+ assert(getCacheEntry(addr).Tokens > (max_tokens() / 2));
}
getCacheEntry(addr).CacheState := state;
trigger(Event:Own_Lock_or_Unlock, in_msg.Address);
} else {
if (persistentTable.typeOfSmallest(in_msg.Address) == AccessType:Read) {
- trigger(Event:Persistent_GETS, in_msg.Address);
+ if (getTokens(in_msg.Address) == 1 ||
+ getTokens(in_msg.Address) == (max_tokens() / 2) + 1) {
+ trigger(Event:Persistent_GETS_Last_Token, in_msg.Address);
+ } else {
+ trigger(Event:Persistent_GETS, in_msg.Address);
+ }
} else {
trigger(Event:Persistent_GETX, in_msg.Address);
}
trigger(Event:Transient_GETX, in_msg.Address);
}
} else if (in_msg.Type == CoherenceRequestType:GETS) {
- if ( (L1DcacheMemory.isTagPresent(in_msg.Address) || L1IcacheMemory.isTagPresent(in_msg.Address)) && getCacheEntry(in_msg.Address).Tokens == 1) {
+ if (getTokens(in_msg.Address) == 1 ||
+ getTokens(in_msg.Address) == (max_tokens() / 2) + 1) {
if (in_msg.isLocal) {
trigger(Event:Transient_Local_GETS_Last_Token, in_msg.Address);
}
if (getTokens(in_msg.Address) + in_msg.Tokens != max_tokens()) {
if (in_msg.Type == CoherenceResponseType:ACK) {
+ assert(in_msg.Tokens < (max_tokens() / 2));
trigger(Event:Ack, in_msg.Address);
} else if (in_msg.Type == CoherenceResponseType:DATA_OWNER) {
trigger(Event:Data_Owner, in_msg.Address);
} else if (in_msg.Type == CoherenceResponseType:DATA_SHARED) {
+ assert(in_msg.Tokens < (max_tokens() / 2));
trigger(Event:Data_Shared, in_msg.Address);
} else {
error("Unexpected message");
}
} else {
if (in_msg.Type == CoherenceResponseType:ACK) {
+ assert(in_msg.Tokens < (max_tokens() / 2));
trigger(Event:Ack_All_Tokens, in_msg.Address);
} else if (in_msg.Type == CoherenceResponseType:DATA_OWNER || in_msg.Type == CoherenceResponseType:DATA_SHARED) {
trigger(Event:Data_All_Tokens, in_msg.Address);
getCacheEntry(address).Tokens := 0;
}
- action(cc_sharedReplacement, "\c", desc="Issue dirty writeback") {
+ action(cc_sharedReplacement, "\c", desc="Issue shared writeback") {
// don't send writeback if replacing block with no tokens
- if (getCacheEntry(address).Tokens != 0) {
+ assert (getCacheEntry(address).Tokens > 0);
+ enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
+ out_msg.Address := address;
+ out_msg.Sender := machineID;
+
+ out_msg.Destination.add(mapAddressToRange(address,
+ MachineType:L2Cache,
+ l2_select_low_bit,
+ l2_select_num_bits));
+
+ out_msg.Tokens := getCacheEntry(address).Tokens;
+ out_msg.DataBlk := getCacheEntry(address).DataBlk;
+ // assert(getCacheEntry(address).Dirty == false);
+ out_msg.Dirty := false;
+
+ out_msg.MessageSize := MessageSizeType:Writeback_Data;
+ out_msg.Type := CoherenceResponseType:WB_SHARED_DATA;
+ }
+ getCacheEntry(address).Tokens := 0;
+ }
+
+ action(tr_tokenReplacement, "tr", desc="Issue token writeback") {
+ if (getCacheEntry(address).Tokens > 0) {
enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
out_msg.Sender := machineID;
out_msg.Dirty := false;
// always send the data?
- if (getCacheEntry(address).Tokens > 1) {
- out_msg.MessageSize := MessageSizeType:Writeback_Data;
- out_msg.Type := CoherenceResponseType:WB_SHARED_DATA;
- } else {
- out_msg.MessageSize := MessageSizeType:Writeback_Control;
- out_msg.Type := CoherenceResponseType:WB_TOKENS;
- }
+ out_msg.MessageSize := MessageSizeType:Writeback_Control;
+ out_msg.Type := CoherenceResponseType:WB_TOKENS;
}
- getCacheEntry(address).Tokens := 0;
}
+ getCacheEntry(address).Tokens := 0;
}
action(d_sendDataWithNTokenIfAvail, "\dd", desc="Send data and a token from cache to requestor") {
peek(requestNetwork_in, RequestMsg) {
- if (getCacheEntry(address).Tokens > N_tokens) {
+ if (getCacheEntry(address).Tokens > (N_tokens + (max_tokens() / 2))) {
enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
out_msg.Type := CoherenceResponseType:DATA_SHARED;
out_msg.Type := CoherenceResponseType:DATA_OWNER;
out_msg.Sender := machineID;
out_msg.Destination.add(in_msg.Requestor);
- assert(getCacheEntry(address).Tokens >= 1);
+ assert(getCacheEntry(address).Tokens > (max_tokens() / 2));
out_msg.Tokens := getCacheEntry(address).Tokens;
out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.Dirty := getCacheEntry(address).Dirty;
if (getCacheEntry(address).Tokens > 0) {
enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
- out_msg.Type := CoherenceResponseType:ACK;
+ if (getCacheEntry(address).Tokens > (max_tokens() / 2)) {
+ out_msg.Type := CoherenceResponseType:DATA_OWNER;
+ } else {
+ out_msg.Type := CoherenceResponseType:ACK;
+ }
out_msg.Sender := machineID;
out_msg.Destination.add(persistentTable.findSmallest(address));
assert(getCacheEntry(address).Tokens >= 1);
out_msg.Tokens := getCacheEntry(address).Tokens;
+ out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.MessageSize := MessageSizeType:Response_Control;
}
}
out_msg.Type := CoherenceResponseType:DATA_OWNER;
out_msg.Sender := machineID;
out_msg.Destination.add(persistentTable.findSmallest(address));
- assert(getCacheEntry(address).Tokens >= 1);
+ assert(getCacheEntry(address).Tokens > (max_tokens() / 2));
out_msg.Tokens := getCacheEntry(address).Tokens;
out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.Dirty := getCacheEntry(address).Dirty;
if (getCacheEntry(address).Tokens > 1) {
enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
- out_msg.Type := CoherenceResponseType:ACK;
+ if (getCacheEntry(address).Tokens > (max_tokens() / 2)) {
+ out_msg.Type := CoherenceResponseType:DATA_OWNER;
+ } else {
+ out_msg.Type := CoherenceResponseType:ACK;
+ }
out_msg.Sender := machineID;
out_msg.Destination.add(persistentTable.findSmallest(address));
assert(getCacheEntry(address).Tokens >= 1);
} else {
out_msg.Tokens := getCacheEntry(address).Tokens - 1;
}
+ out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.MessageSize := MessageSizeType:Response_Control;
}
}
action(ff_sendDataWithAllButNorOneTokens, "\f", desc="Send data and out tokens but one to starver") {
//assert(persistentTable.findSmallest(address) != id); // Make sure we never bounce tokens to ourself
- assert(getCacheEntry(address).Tokens > 0);
- if (getCacheEntry(address).Tokens > 1) {
- enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
+ assert(getCacheEntry(address).Tokens > ((max_tokens() / 2) + 1));
+ enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
out_msg.Type := CoherenceResponseType:DATA_OWNER;
out_msg.Sender := machineID;
out_msg.Destination.add(persistentTable.findSmallest(address));
- assert(getCacheEntry(address).Tokens >= 1);
- if (getCacheEntry(address).Tokens > N_tokens) {
+ if (getCacheEntry(address).Tokens > (N_tokens + (max_tokens() / 2))) {
out_msg.Tokens := getCacheEntry(address).Tokens - N_tokens;
} else {
out_msg.Tokens := getCacheEntry(address).Tokens - 1;
}
+ assert(out_msg.Tokens > (max_tokens() / 2));
out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.Dirty := getCacheEntry(address).Dirty;
out_msg.MessageSize := MessageSizeType:Response_Data;
- }
- if (getCacheEntry(address).Tokens > N_tokens) {
- getCacheEntry(address).Tokens := N_tokens;
- } else {
- getCacheEntry(address).Tokens := 1;
- }
+ }
+ if (getCacheEntry(address).Tokens > (N_tokens + (max_tokens() / 2))) {
+ getCacheEntry(address).Tokens := N_tokens;
+ } else {
+ getCacheEntry(address).Tokens := 1;
}
}
+ action(fo_sendDataWithOwnerToken, "fo", desc="Send data and owner tokens") {
+ assert(getCacheEntry(address).Tokens == ((max_tokens() / 2) + 1));
+ enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
+ out_msg.Address := address;
+ out_msg.Type := CoherenceResponseType:DATA_OWNER;
+ out_msg.Sender := machineID;
+ out_msg.Destination.add(persistentTable.findSmallest(address));
+ out_msg.Tokens := getCacheEntry(address).Tokens;
+ assert(out_msg.Tokens > (max_tokens() / 2));
+ out_msg.DataBlk := getCacheEntry(address).DataBlk;
+ out_msg.Dirty := getCacheEntry(address).Dirty;
+ out_msg.MessageSize := MessageSizeType:Response_Data;
+ }
+ getCacheEntry(address).Tokens := 0;
+ }
+
action(g_bounceResponseToStarver, "g", desc="Redirect response to starving processor") {
// assert(persistentTable.isLocked(address));
peek(requestNetwork_in, RequestMsg) {
enqueue(responseNetwork_out, ResponseMsg, latency = l1_response_latency) {
out_msg.Address := address;
- out_msg.Type := CoherenceResponseType:ACK;
+ if (getCacheEntry(address).Tokens > (max_tokens() / 2)) {
+ out_msg.Type := CoherenceResponseType:DATA_OWNER;
+ } else {
+ out_msg.Type := CoherenceResponseType:ACK;
+ }
out_msg.Sender := machineID;
out_msg.Destination.add(in_msg.Requestor);
assert(getCacheEntry(address).Tokens >= 1);
out_msg.Tokens := getCacheEntry(address).Tokens;
+ out_msg.DataBlk := getCacheEntry(address).DataBlk;
out_msg.MessageSize := MessageSizeType:Response_Control;
}
}
}
action(gg_deallocateL1CacheBlock, "\g", desc="Deallocate cache block. Sets the cache to invalid, allowing a replacement in parallel with a fetch.") {
+ assert(getTokens(address) == 0);
if (L1DcacheMemory.isTagPresent(address)) {
L1DcacheMemory.deallocate(address);
} else {
m_popRequestQueue;
}
- transition(NP, {Persistent_GETX, Persistent_GETS}, I_L) {
+ transition(NP, {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token}, I_L) {
l_popPersistentQueue;
}
}
transition(I, L1_Replacement) {
- cc_sharedReplacement;
+ tr_tokenReplacement;
gg_deallocateL1CacheBlock;
}
m_popRequestQueue;
}
- transition(I, {Persistent_GETX, Persistent_GETS}, I_L) {
+ transition(I, {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token}, I_L) {
e_sendAckWithCollectedTokens;
l_popPersistentQueue;
}
- transition(I_L, {Persistent_GETX, Persistent_GETS}) {
+ transition(I_L, {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token}) {
l_popPersistentQueue;
}
l_popPersistentQueue;
}
- transition(S, Persistent_GETS, S_L) {
+ transition(S, {Persistent_GETS, Persistent_GETS_Last_Token}, S_L) {
f_sendAckWithAllButNorOneTokens;
l_popPersistentQueue;
}
- transition(S_L, Persistent_GETS) {
+ transition(S_L, {Persistent_GETS, Persistent_GETS_Last_Token}) {
l_popPersistentQueue;
}
l_popPersistentQueue;
}
+ transition(O, Persistent_GETS_Last_Token, I_L) {
+ fo_sendDataWithOwnerToken;
+ l_popPersistentQueue;
+ }
+
transition(O, Transient_GETS) {
d_sendDataWithToken;
m_popRequestQueue;
m_popRequestQueue;
}
- transition(IS, {Persistent_GETX, Persistent_GETS}, IS_L) {
+ transition(IS, {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token}, IS_L) {
e_sendAckWithCollectedTokens;
l_popPersistentQueue;
}
l_popPersistentQueue;
}
- transition(IM, {Persistent_GETX, Persistent_GETS}, IM_L) {
+ transition(IM, {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token}, IM_L) {
e_sendAckWithCollectedTokens;
l_popPersistentQueue;
}
l_popPersistentQueue;
}
- transition(SM, Persistent_GETS, SM_L) {
+ transition(SM, {Persistent_GETS, Persistent_GETS_Last_Token}, SM_L) {
f_sendAckWithAllButNorOneTokens;
l_popPersistentQueue;
}
- transition(SM_L, Persistent_GETS) {
+ transition(SM_L, {Persistent_GETS, Persistent_GETS_Last_Token}) {
l_popPersistentQueue;
}
l_popPersistentQueue;
}
+ transition(OM, Persistent_GETS_Last_Token, IM_L) {
+ fo_sendDataWithOwnerToken;
+ l_popPersistentQueue;
+ }
+
// Transitions from IM/SM
transition({IM, SM}, Ack) {
// Lock/Unlock
Persistent_GETX, desc="Another processor has priority to read/write";
Persistent_GETS, desc="Another processor has priority to read";
+ Persistent_GETS_Last_Token, desc="Another processor has priority to read";
Own_Lock_or_Unlock, desc="This processor now has priority";
}
// Make sure the token count is in range
assert(getL2CacheEntry(addr).Tokens >= 0);
assert(getL2CacheEntry(addr).Tokens <= max_tokens());
+ assert(getL2CacheEntry(addr).Tokens != (max_tokens() / 2));
// Make sure we have no tokens in L
if ((state == State:I_L) ) {
// You have at least half the token in O-like states
if (state == State:O ) {
- assert(getL2CacheEntry(addr).Tokens >= 1); // Must have at least one token
- // assert(getL2CacheEntry(addr).Tokens >= (max_tokens() / 2)); // Only mostly true; this might not always hold
+ assert(getL2CacheEntry(addr).Tokens > (max_tokens() / 2));
}
getL2CacheEntry(addr).CacheState := state;
if (persistentTable.isLocked(in_msg.Address)) {
if (persistentTable.typeOfSmallest(in_msg.Address) == AccessType:Read) {
- trigger(Event:Persistent_GETS, in_msg.Address);
+ if (getTokens(in_msg.Address) == 1 ||
+ getTokens(in_msg.Address) == (max_tokens() / 2) + 1) {
+ trigger(Event:Persistent_GETS_Last_Token, in_msg.Address);
+ } else {
+ trigger(Event:Persistent_GETS, in_msg.Address);
+ }
} else {
trigger(Event:Persistent_GETX, in_msg.Address);
}
if (in_msg.Type == CoherenceRequestType:GETX) {
trigger(Event:L1_GETX, in_msg.Address);
} else if (in_msg.Type == CoherenceRequestType:GETS) {
- if (L2cacheMemory.isTagPresent(in_msg.Address) && getL2CacheEntry(in_msg.Address).Tokens == 1) {
+ if (getTokens(in_msg.Address) == 1 ||
+ getTokens(in_msg.Address) == (max_tokens() / 2) + 1) {
trigger(Event:L1_GETS_Last_Token, in_msg.Address);
}
else {
assert(in_msg.Destination.isElement(machineID));
if (getTokens(in_msg.Address) + in_msg.Tokens != max_tokens()) {
if (in_msg.Type == CoherenceResponseType:ACK) {
+ assert(in_msg.Tokens < (max_tokens() / 2));
trigger(Event:Ack, in_msg.Address);
} else if (in_msg.Type == CoherenceResponseType:DATA_OWNER) {
trigger(Event:Data_Owner, in_msg.Address);
}
} else {
if (in_msg.Type == CoherenceResponseType:ACK) {
+ assert(in_msg.Tokens < (max_tokens() / 2));
trigger(Event:Ack_All_Tokens, in_msg.Address);
} else if (in_msg.Type == CoherenceResponseType:DATA_OWNER || in_msg.Type == CoherenceResponseType:DATA_SHARED) {
trigger(Event:Data_All_Tokens, in_msg.Address);
action(d_sendDataWithTokens, "d", desc="Send data and a token from cache to requestor") {
peek(requestNetwork_in, RequestMsg) {
- if (getL2CacheEntry(address).Tokens > N_tokens) {
+ if (getL2CacheEntry(address).Tokens > (N_tokens + (max_tokens() / 2))) {
enqueue(responseNetwork_out, ResponseMsg, latency=l2_response_latency) {
out_msg.Address := address;
out_msg.Type := CoherenceResponseType:DATA_SHARED;
action(ff_sendDataWithAllButOneTokens, "\f", desc="Send data and out tokens but one to starver") {
//assert(persistentTable.findSmallest(address) != id); // Make sure we never bounce tokens to ourself
- assert(getL2CacheEntry(address).Tokens > 0);
- if (getL2CacheEntry(address).Tokens > 1) {
- enqueue(responseNetwork_out, ResponseMsg, latency=l2_response_latency) {
+ assert(getL2CacheEntry(address).Tokens > (max_tokens() / 2) + 1);
+ enqueue(responseNetwork_out, ResponseMsg, latency=l2_response_latency) {
out_msg.Address := address;
out_msg.Type := CoherenceResponseType:DATA_OWNER;
out_msg.Sender := machineID;
out_msg.Destination.add(persistentTable.findSmallest(address));
- assert(getL2CacheEntry(address).Tokens >= 1);
out_msg.Tokens := getL2CacheEntry(address).Tokens - 1;
out_msg.DataBlk := getL2CacheEntry(address).DataBlk;
out_msg.Dirty := getL2CacheEntry(address).Dirty;
out_msg.MessageSize := MessageSizeType:Response_Data;
- }
- getL2CacheEntry(address).Tokens := 1;
}
+ getL2CacheEntry(address).Tokens := 1;
+ }
+
+ action(fa_sendDataWithAllTokens, "fa", desc="Send data and out tokens but one to starver") {
+ //assert(persistentTable.findSmallest(address) != id); // Make sure we never bounce tokens to ourself
+ assert(getL2CacheEntry(address).Tokens == (max_tokens() / 2) + 1);
+ enqueue(responseNetwork_out, ResponseMsg, latency=l2_response_latency) {
+ out_msg.Address := address;
+ out_msg.Type := CoherenceResponseType:DATA_OWNER;
+ out_msg.Sender := machineID;
+ out_msg.Destination.add(persistentTable.findSmallest(address));
+ out_msg.Tokens := getL2CacheEntry(address).Tokens;
+ out_msg.DataBlk := getL2CacheEntry(address).DataBlk;
+ out_msg.Dirty := getL2CacheEntry(address).Dirty;
+ out_msg.MessageSize := MessageSizeType:Response_Data;
+ }
+ getL2CacheEntry(address).Tokens := 0;
}
if (in_msg.Type == CoherenceResponseType:WB_SHARED_DATA) {
out_msg.Type := CoherenceResponseType:DATA_SHARED;
} else {
+ assert(in_msg.Tokens < (max_tokens() / 2));
out_msg.Type := CoherenceResponseType:ACK;
}
out_msg.Sender := machineID;
action(k_dataOwnerFromL2CacheToL1Requestor, "\k", desc="Send data and a token from cache to L1 requestor") {
peek(L1requestNetwork_in, RequestMsg) {
- assert(getL2CacheEntry(address).Tokens > 0);
+ assert(getL2CacheEntry(address).Tokens == (max_tokens() / 2) + 1);
enqueue(responseNetwork_out, ResponseMsg, latency=l2_response_latency) {
out_msg.Address := address;
out_msg.Type := CoherenceResponseType:DATA_OWNER;
out_msg.DataBlk := getL2CacheEntry(address).DataBlk;
out_msg.Dirty := getL2CacheEntry(address).Dirty;
out_msg.MessageSize := MessageSizeType:ResponseL2hit_Data;
- out_msg.Tokens := 1;
+ out_msg.Tokens := getL2CacheEntry(address).Tokens;
}
- getL2CacheEntry(address).Tokens := getL2CacheEntry(address).Tokens - 1;
+ getL2CacheEntry(address).Tokens := 0;
}
}
action(w_assertIncomingDataAndCacheDataMatch, "w", desc="Assert that the incoming data and the data in the cache match") {
peek(responseNetwork_in, ResponseMsg) {
- assert(getL2CacheEntry(address).DataBlk == in_msg.DataBlk);
+ if (in_msg.Type != CoherenceResponseType:ACK &&
+ in_msg.Type != CoherenceResponseType:WB_TOKENS) {
+ assert(getL2CacheEntry(address).DataBlk == in_msg.DataBlk);
+ }
}
}
}
- transition(NP, {Persistent_GETX, Persistent_GETS}, I_L) {
+ transition(NP,
+ {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token},
+ I_L) {
l_popPersistentQueue;
}
m_popRequestQueue;
}
- transition(I, {Persistent_GETX, Persistent_GETS}, I_L) {
+ transition(I,
+ {Persistent_GETX, Persistent_GETS, Persistent_GETS_Last_Token},
+ I_L) {
e_sendAckWithCollectedTokens;
l_popPersistentQueue;
}
}
- transition(S, Persistent_GETS, S_L) {
+ transition(S, {Persistent_GETS, Persistent_GETS_Last_Token}, S_L) {
f_sendAckWithAllButOneTokens;
l_popPersistentQueue;
}
l_popPersistentQueue;
}
+ transition(O, Persistent_GETS_Last_Token, I_L) {
+ fa_sendDataWithAllTokens;
+ l_popPersistentQueue;
+ }
+
transition(O, Transient_GETS) {
// send multiple tokens
r_clearExclusive;
l_popPersistentQueue;
}
- transition(S_L, Persistent_GETS) {
+ transition(S_L, {Persistent_GETS, Persistent_GETS_Last_Token}) {
l_popPersistentQueue;
}