Agent Environment Obsvars: end Obsvars Vars: active_monitor: 0 .. 6; current_node: 1 .. 6; send_status: { message, process }; state: { sending, timed_out_ack, timed_out_message, waiting_ack, waiting_message }; timeout: 0 .. 2; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { none, send_node_1_B, send_node_1_C, send_node_1_N, send_node_1_RP, send_node_2_B, send_node_2_C, send_node_2_N, send_node_2_RP, send_node_3_B, send_node_3_C, send_node_3_N, send_node_3_RP, send_node_4_B, send_node_4_C, send_node_4_N, send_node_4_RP, send_node_5_B, send_node_5_C, send_node_5_N, send_node_5_RP, send_node_6_B, send_node_6_C, send_node_6_N, send_node_6_RP, timeout_node_1, timeout_node_2, timeout_node_3, timeout_node_4, timeout_node_5, timeout_node_6 }; Protocol: state = waiting_message: { none }; state = waiting_ack: { none }; state = timed_out_message: { none }; state = timed_out_ack: { none }; (((state = sending and send_status = message) and timeout = 0) and current_node = 1): { timeout_node_1 }; (((state = sending and send_status = message) and timeout = 0) and current_node = 2): { timeout_node_2 }; (((state = sending and send_status = message) and timeout = 0) and current_node = 3): { timeout_node_3 }; (((state = sending and send_status = message) and timeout = 0) and current_node = 4): { timeout_node_4 }; (((state = sending and send_status = message) and timeout = 0) and current_node = 5): { timeout_node_5 }; (((state = sending and send_status = message) and timeout = 0) and current_node = 6): { timeout_node_6 }; (state = sending and send_status = process): { none }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 1): { send_node_1_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 1): { send_node_1_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 1): { send_node_1_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 1): { send_node_1_B }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 2): { send_node_2_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 2): { send_node_2_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 2): { send_node_2_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 2): { send_node_2_B }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 3): { send_node_3_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 3): { send_node_3_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 3): { send_node_3_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 3): { send_node_3_B }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 4): { send_node_4_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 4): { send_node_4_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 4): { send_node_4_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 4): { send_node_4_B }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 5): { send_node_5_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 5): { send_node_5_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 5): { send_node_5_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 5): { send_node_5_B }; ((((state = sending and timeout > 0) and send_status = message) and token = N) and current_node = 6): { send_node_6_N }; ((((state = sending and timeout > 0) and send_status = message) and token = C) and current_node = 6): { send_node_6_C }; ((((state = sending and timeout > 0) and send_status = message) and token = RP) and current_node = 6): { send_node_6_RP }; ((((state = sending and timeout > 0) and send_status = message) and token = B) and current_node = 6): { send_node_6_B }; end Protocol Evolution: state = timed_out_message if (state = waiting_message and timeout = 0); state = timed_out_ack if (state = waiting_ack and timeout = 0); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 1) and ! Node_1.Action = send_N) and ! Node_1.Action = send_C) and ! Node_1.Action = send_RP) and ! Node_1.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 2) and ! Node_2.Action = send_N) and ! Node_2.Action = send_C) and ! Node_2.Action = send_RP) and ! Node_2.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 3) and ! Node_3.Action = send_N) and ! Node_3.Action = send_C) and ! Node_3.Action = send_RP) and ! Node_3.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 4) and ! Node_4.Action = send_N) and ! Node_4.Action = send_C) and ! Node_4.Action = send_RP) and ! Node_4.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 5) and ! Node_5.Action = send_N) and ! Node_5.Action = send_C) and ! Node_5.Action = send_RP) and ! Node_5.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_message and timeout > 0) and current_node = 6) and ! Node_6.Action = send_N) and ! Node_6.Action = send_C) and ! Node_6.Action = send_RP) and ! Node_6.Action = send_B); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 1) and ! Node_1.Action = send_recieved) and ! Node_1.Action = send_recieved) and ! Node_1.Action = send_recieved) and ! Node_1.Action = send_recieved); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 2) and ! Node_2.Action = send_recieved) and ! Node_2.Action = send_recieved) and ! Node_2.Action = send_recieved) and ! Node_2.Action = send_recieved); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 3) and ! Node_3.Action = send_recieved) and ! Node_3.Action = send_recieved) and ! Node_3.Action = send_recieved) and ! Node_3.Action = send_recieved); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 4) and ! Node_4.Action = send_recieved) and ! Node_4.Action = send_recieved) and ! Node_4.Action = send_recieved) and ! Node_4.Action = send_recieved); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 5) and ! Node_5.Action = send_recieved) and ! Node_5.Action = send_recieved) and ! Node_5.Action = send_recieved) and ! Node_5.Action = send_recieved); timeout = timeout - 1 if ((((((state = waiting_ack and timeout > 0) and current_node = 6) and ! Node_6.Action = send_recieved) and ! Node_6.Action = send_recieved) and ! Node_6.Action = send_recieved) and ! Node_6.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 1) and Node_1.Action = send_recieved) and Node_1.Action = send_recieved) and Node_1.Action = send_recieved) and Node_1.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 2) and Node_2.Action = send_recieved) and Node_2.Action = send_recieved) and Node_2.Action = send_recieved) and Node_2.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 3) and Node_3.Action = send_recieved) and Node_3.Action = send_recieved) and Node_3.Action = send_recieved) and Node_3.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 4) and Node_4.Action = send_recieved) and Node_4.Action = send_recieved) and Node_4.Action = send_recieved) and Node_4.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 5) and Node_5.Action = send_recieved) and Node_5.Action = send_recieved) and Node_5.Action = send_recieved) and Node_5.Action = send_recieved); timeout = 2 and state = waiting_message if ((((((state = waiting_ack and timeout > 0) and current_node = 6) and Node_6.Action = send_recieved) and Node_6.Action = send_recieved) and Node_6.Action = send_recieved) and Node_6.Action = send_recieved); state = sending and send_status = process and current_node = 2 and token = N if (((state = waiting_message and timeout > 0) and current_node = 1) and Node_1.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 2 and token = C if (((state = waiting_message and timeout > 0) and current_node = 1) and Node_1.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 2 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 1) and Node_1.Action = send_RP); state = sending and send_status = process and current_node = 2 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 1) and Node_1.Action = send_RP); state = sending and send_status = process and current_node = 2 and token = B if (((state = waiting_message and timeout > 0) and current_node = 1) and Node_1.Action = send_B); state = sending and send_status = process and current_node = 3 and token = N if (((state = waiting_message and timeout > 0) and current_node = 2) and Node_2.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 3 and token = C if (((state = waiting_message and timeout > 0) and current_node = 2) and Node_2.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 3 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 2) and Node_2.Action = send_RP); state = sending and send_status = process and current_node = 3 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 2) and Node_2.Action = send_RP); state = sending and send_status = process and current_node = 3 and token = B if (((state = waiting_message and timeout > 0) and current_node = 2) and Node_2.Action = send_B); state = sending and send_status = process and current_node = 4 and token = N if (((state = waiting_message and timeout > 0) and current_node = 3) and Node_3.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 4 and token = C if (((state = waiting_message and timeout > 0) and current_node = 3) and Node_3.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 4 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 3) and Node_3.Action = send_RP); state = sending and send_status = process and current_node = 4 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 3) and Node_3.Action = send_RP); state = sending and send_status = process and current_node = 4 and token = B if (((state = waiting_message and timeout > 0) and current_node = 3) and Node_3.Action = send_B); state = sending and send_status = process and current_node = 5 and token = N if (((state = waiting_message and timeout > 0) and current_node = 4) and Node_4.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 5 and token = C if (((state = waiting_message and timeout > 0) and current_node = 4) and Node_4.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 5 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 4) and Node_4.Action = send_RP); state = sending and send_status = process and current_node = 5 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 4) and Node_4.Action = send_RP); state = sending and send_status = process and current_node = 5 and token = B if (((state = waiting_message and timeout > 0) and current_node = 4) and Node_4.Action = send_B); state = sending and send_status = process and current_node = 6 and token = N if (((state = waiting_message and timeout > 0) and current_node = 5) and Node_5.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 6 and token = C if (((state = waiting_message and timeout > 0) and current_node = 5) and Node_5.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 6 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 5) and Node_5.Action = send_RP); state = sending and send_status = process and current_node = 6 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 5) and Node_5.Action = send_RP); state = sending and send_status = process and current_node = 6 and token = B if (((state = waiting_message and timeout > 0) and current_node = 5) and Node_5.Action = send_B); state = sending and send_status = process and current_node = 1 and token = N if (((state = waiting_message and timeout > 0) and current_node = 6) and Node_6.Action = send_N); active_monitor = 0 and state = sending and send_status = process and current_node = 1 and token = C if (((state = waiting_message and timeout > 0) and current_node = 6) and Node_6.Action = send_C); active_monitor = current_node and state = sending and send_status = process and current_node = 1 and token = RP if ((((active_monitor = 0 and state = waiting_message) and timeout > 0) and current_node = 6) and Node_6.Action = send_RP); state = sending and send_status = process and current_node = 1 and token = RP if ((((active_monitor > 0 and state = waiting_message) and timeout > 0) and current_node = 6) and Node_6.Action = send_RP); state = sending and send_status = process and current_node = 1 and token = B if (((state = waiting_message and timeout > 0) and current_node = 6) and Node_6.Action = send_B); send_status = message if (((state = sending and send_status = process) and current_node = 1) and ! Node_1.Action = disconnected); send_status = message if (((state = sending and send_status = process) and current_node = 2) and ! Node_2.Action = disconnected); send_status = message if (((state = sending and send_status = process) and current_node = 3) and ! Node_3.Action = disconnected); send_status = message if (((state = sending and send_status = process) and current_node = 4) and ! Node_4.Action = disconnected); send_status = message if (((state = sending and send_status = process) and current_node = 5) and ! Node_5.Action = disconnected); send_status = message if (((state = sending and send_status = process) and current_node = 6) and ! Node_6.Action = disconnected); current_node = 2 if (((state = sending and send_status = process) and current_node = 1) and Node_1.Action = disconnected); current_node = 3 if (((state = sending and send_status = process) and current_node = 2) and Node_2.Action = disconnected); current_node = 4 if (((state = sending and send_status = process) and current_node = 3) and Node_3.Action = disconnected); current_node = 5 if (((state = sending and send_status = process) and current_node = 4) and Node_4.Action = disconnected); current_node = 6 if (((state = sending and send_status = process) and current_node = 5) and Node_5.Action = disconnected); current_node = 1 if (((state = sending and send_status = process) and current_node = 6) and Node_6.Action = disconnected); state = waiting_ack and timeout = 2 if (state = sending and send_status = message); state = sending and send_status = process and timeout = 0 and current_node = active_monitor if ((state = timed_out_message or state = timed_out_ack) and active_monitor > 0); state = sending and send_status = process and timeout = 0 and current_node = 2 if ((current_node = 1 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = process and timeout = 0 and current_node = 3 if ((current_node = 2 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = process and timeout = 0 and current_node = 4 if ((current_node = 3 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = process and timeout = 0 and current_node = 5 if ((current_node = 4 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = process and timeout = 0 and current_node = 6 if ((current_node = 5 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = process and timeout = 0 and current_node = 1 if ((current_node = 6 and state = timed_out_message) and active_monitor = 0); state = sending and send_status = message and timeout = 0 if (state = timed_out_ack and active_monitor = 0); end Evolution end Agent Agent Token Vars: node_info: 0 .. 7; end Vars RedStates: end RedStates Actions = { five, four, free, one, six, three, two, seven }; Protocol: node_info = 0: { free }; node_info = 1: { one }; node_info = 2: { two }; node_info = 3: { three }; node_info = 4: { four }; node_info = 5: { five }; node_info = 6: { six }; node_info = 7: { seven }; end Protocol Evolution: node_info = 7 if TKwd.Action = inject; --- note that we leave out !inject for the following transitions as it offers performance improvement node_info = 5 if Node_2.Action = set_token_N; node_info = 2 if Node_5.Action = set_token_N; node_info = 1 if Node_1.Action = set_token_C; node_info = 2 if Node_2.Action = set_token_C; node_info = 3 if Node_3.Action = set_token_C; node_info = 4 if Node_4.Action = set_token_C; node_info = 5 if Node_5.Action = set_token_C; node_info = 6 if Node_6.Action = set_token_C; node_info = 0 if Node_1.Action = set_token_free; node_info = 0 if Node_2.Action = set_token_free; node_info = 0 if Node_3.Action = set_token_free; node_info = 0 if Node_4.Action = set_token_free; node_info = 0 if Node_5.Action = set_token_free; node_info = 0 if Node_6.Action = set_token_free; node_info = 6 if (Node_1.Action = set_token_B and ! Node_6.Action = disconnected); node_info = 5 if ((Node_1.Action = set_token_B and Node_6.Action = disconnected) and ! Node_5.Action = disconnected); node_info = 4 if (((Node_1.Action = set_token_B and Node_6.Action = disconnected) and Node_5.Action = disconnected) and ! Node_4.Action = disconnected); node_info = 3 if ((((Node_1.Action = set_token_B and Node_6.Action = disconnected) and Node_5.Action = disconnected) and Node_4.Action = disconnected) and ! Node_3.Action = disconnected); node_info = 2 if (((((Node_1.Action = set_token_B and Node_6.Action = disconnected) and Node_5.Action = disconnected) and Node_4.Action = disconnected) and Node_3.Action = disconnected) and ! Node_2.Action = disconnected); node_info = 1 if (Node_2.Action = set_token_B and ! Node_1.Action = disconnected); node_info = 6 if ((Node_2.Action = set_token_B and Node_1.Action = disconnected) and ! Node_6.Action = disconnected); node_info = 5 if (((Node_2.Action = set_token_B and Node_1.Action = disconnected) and Node_6.Action = disconnected) and ! Node_5.Action = disconnected); node_info = 4 if ((((Node_2.Action = set_token_B and Node_1.Action = disconnected) and Node_6.Action = disconnected) and Node_5.Action = disconnected) and ! Node_4.Action = disconnected); node_info = 3 if (((((Node_2.Action = set_token_B and Node_1.Action = disconnected) and Node_6.Action = disconnected) and Node_5.Action = disconnected) and Node_4.Action = disconnected) and ! Node_3.Action = disconnected); node_info = 2 if (Node_3.Action = set_token_B and ! Node_2.Action = disconnected); node_info = 1 if ((Node_3.Action = set_token_B and Node_2.Action = disconnected) and ! Node_1.Action = disconnected); node_info = 6 if (((Node_3.Action = set_token_B and Node_2.Action = disconnected) and Node_1.Action = disconnected) and ! Node_6.Action = disconnected); node_info = 5 if ((((Node_3.Action = set_token_B and Node_2.Action = disconnected) and Node_1.Action = disconnected) and Node_6.Action = disconnected) and ! Node_5.Action = disconnected); node_info = 4 if (((((Node_3.Action = set_token_B and Node_2.Action = disconnected) and Node_1.Action = disconnected) and Node_6.Action = disconnected) and Node_5.Action = disconnected) and ! Node_4.Action = disconnected); node_info = 3 if (Node_4.Action = set_token_B and ! Node_3.Action = disconnected); node_info = 2 if ((Node_4.Action = set_token_B and Node_3.Action = disconnected) and ! Node_2.Action = disconnected); node_info = 1 if (((Node_4.Action = set_token_B and Node_3.Action = disconnected) and Node_2.Action = disconnected) and ! Node_1.Action = disconnected); node_info = 6 if ((((Node_4.Action = set_token_B and Node_3.Action = disconnected) and Node_2.Action = disconnected) and Node_1.Action = disconnected) and ! Node_6.Action = disconnected); node_info = 5 if (((((Node_4.Action = set_token_B and Node_3.Action = disconnected) and Node_2.Action = disconnected) and Node_1.Action = disconnected) and Node_6.Action = disconnected) and ! Node_5.Action = disconnected); node_info = 4 if (Node_5.Action = set_token_B and ! Node_4.Action = disconnected); node_info = 3 if ((Node_5.Action = set_token_B and Node_4.Action = disconnected) and ! Node_3.Action = disconnected); node_info = 2 if (((Node_5.Action = set_token_B and Node_4.Action = disconnected) and Node_3.Action = disconnected) and ! Node_2.Action = disconnected); node_info = 1 if ((((Node_5.Action = set_token_B and Node_4.Action = disconnected) and Node_3.Action = disconnected) and Node_2.Action = disconnected) and ! Node_1.Action = disconnected); node_info = 6 if (((((Node_5.Action = set_token_B and Node_4.Action = disconnected) and Node_3.Action = disconnected) and Node_2.Action = disconnected) and Node_1.Action = disconnected) and ! Node_6.Action = disconnected); node_info = 5 if (Node_6.Action = set_token_B and ! Node_5.Action = disconnected); node_info = 4 if ((Node_6.Action = set_token_B and Node_5.Action = disconnected) and ! Node_4.Action = disconnected); node_info = 3 if (((Node_6.Action = set_token_B and Node_5.Action = disconnected) and Node_4.Action = disconnected) and ! Node_3.Action = disconnected); node_info = 2 if ((((Node_6.Action = set_token_B and Node_5.Action = disconnected) and Node_4.Action = disconnected) and Node_3.Action = disconnected) and ! Node_2.Action = disconnected); node_info = 1 if (((((Node_6.Action = set_token_B and Node_5.Action = disconnected) and Node_4.Action = disconnected) and Node_3.Action = disconnected) and Node_2.Action = disconnected) and ! Node_1.Action = disconnected); end Evolution end Agent Agent Token_bit Vars: bit: boolean; end Vars RedStates: end RedStates Actions = { set, unset }; Protocol: bit = false: { unset }; bit = true: { set }; end Protocol Evolution: bit = false if (((Node_1.Action = set_token_N or Node_1.Action = set_token_B) or Node_1.Action = set_token_C) or Node_1.Action = set_token_free); bit = false if (((Node_2.Action = set_token_N or Node_2.Action = set_token_B) or Node_2.Action = set_token_C) or Node_2.Action = set_token_free); bit = false if (((Node_3.Action = set_token_N or Node_3.Action = set_token_B) or Node_3.Action = set_token_C) or Node_3.Action = set_token_free); bit = false if (((Node_4.Action = set_token_N or Node_4.Action = set_token_B) or Node_4.Action = set_token_C) or Node_4.Action = set_token_free); bit = false if (((Node_5.Action = set_token_N or Node_5.Action = set_token_B) or Node_5.Action = set_token_C) or Node_5.Action = set_token_free); bit = false if (((Node_6.Action = set_token_N or Node_6.Action = set_token_B) or Node_6.Action = set_token_C) or Node_6.Action = set_token_free); bit = true if Node_1.Action = set_token_bit; bit = true if Node_2.Action = set_token_bit; bit = true if Node_3.Action = set_token_bit; bit = true if Node_4.Action = set_token_bit; bit = true if Node_5.Action = set_token_bit; bit = true if Node_6.Action = set_token_bit; end Evolution end Agent Agent Node_1 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: active_monitor = false if N1sm.Action = inject; --- note that we leave out !inject for the following transitions as it offers performance improvement state = processing and token = N if (state = waiting and Environment.Action = send_node_1_N); state = processing and token = C if (state = waiting and Environment.Action = send_node_1_C); state = processing and token = RP if (state = waiting and Environment.Action = send_node_1_RP); state = processing and token = B if (state = waiting and Environment.Action = send_node_1_B); state = timeout if Environment.Action = timeout_node_1; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false); state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = one); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = set_token and free_token = false and substate = claiming if ((state = processing and token = C) and ((((Token.Action = six or Token.Action = five) or Token.Action = four) or Token.Action = three) or Token.Action = two)); state = set_token and rec = true and free_token = true and substate = repeating if ((state = processing and token = N) and Token.Action = one); state = sending and substate = repeating if ((state = processing and token = N) and Token.Action = free); state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = one); state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = one); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = one); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = one); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = one) and number_beacons_recieved < 1); number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = one); state = disconnected if (((state = processing and token = B) and Token.Action = one) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent Node_2 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; sent_message: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: state = processing and token = N if (state = waiting and Environment.Action = send_node_2_N); state = processing and token = C if (state = waiting and Environment.Action = send_node_2_C); state = processing and token = RP if (state = waiting and Environment.Action = send_node_2_RP); state = processing and token = B if (state = waiting and Environment.Action = send_node_2_B); state = timeout if Environment.Action = timeout_node_2; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token and !sN2ns.Action = inject; state = waiting and free_token = false and seen_token = false if state = set_token and sN2ns.Action = inject; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and !sN2ns.Action = inject; state = waiting and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and sN2ns.Action = inject; state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = two); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = set_token and free_token = false and substate = claiming if ((state = processing and token = C) and (((Token.Action = six or Token.Action = five) or Token.Action = four) or Token.Action = three)); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = sending and free_token = false and substate = repeating if ((state = processing and token = C) and Token.Action = one) and !sN2ns.Action = inject; number_beacons_recieved = 0 and number_beacons_failed = 0 and state = waiting and free_token = false and substate = repeating if ((state = processing and token = C) and Token.Action = one) and sN2ns.Action = inject; state = set_token and rec = true and free_token = true and substate = repeating if ((state = processing and token = N) and Token.Action = two); sent_message = true and state = set_token and substate = repeating and free_token = false if ((((state = processing and token = N) and rec = false) and Token.Action = free) and sent_message = false); sent_message = false and state = sending and substate = repeating if ((((state = processing and token = N) and rec = false) and Token.Action = free) and sent_message = true) and !sN2ns.Action = inject; sent_message = false and state = waiting and substate = repeating if ((((state = processing and token = N) and rec = false) and Token.Action = free) and sent_message = true) and sN2ns.Action = inject; state = sending and substate = repeating if (((state = processing and token = N) and Token.Action = free) and rec = true) and !sN2ns.Action = inject; state = waiting and substate = repeating if (((state = processing and token = N) and Token.Action = free) and rec = true) and sN2ns.Action = inject; state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = two) and !sN2ns.Action = inject; state = waiting and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = two) and sN2ns.Action = inject; state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = two); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = two); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = two); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = two) and number_beacons_recieved < 1) and !sN2ns.Action = inject; number_beacons_recieved = number_beacons_recieved + 1 and state = waiting and substate = repeating if (((state = processing and token = B) and Token.Action = two) and number_beacons_recieved < 1) and sN2ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = two) and !sN2ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = waiting and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = two) and sN2ns.Action = inject; state = disconnected if (((state = processing and token = B) and Token.Action = two) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent Node_3 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: state = processing and token = N if (state = waiting and Environment.Action = send_node_3_N); state = processing and token = C if (state = waiting and Environment.Action = send_node_3_C); state = processing and token = RP if (state = waiting and Environment.Action = send_node_3_RP); state = processing and token = B if (state = waiting and Environment.Action = send_node_3_B); state = timeout if Environment.Action = timeout_node_3; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token and !hN3ns.Action = inject; state = waiting and free_token = false and seen_token = false if state = set_token and hN3ns.Action = inject; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and !hN3ns.Action = inject; state = waiting and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and hN3ns.Action = inject; state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = three); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = set_token and free_token = false and substate = claiming if ((state = processing and token = C) and ((Token.Action = six or Token.Action = five) or Token.Action = four)); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = sending and free_token = false and substate = repeating if ((state = processing and token = C) and (Token.Action = one or Token.Action = two)) and !hN3ns.Action = inject; number_beacons_recieved = 0 and number_beacons_failed = 0 and state = waiting and free_token = false and substate = repeating if ((state = processing and token = C) and (Token.Action = one or Token.Action = two)) and hN3ns.Action = inject; state = set_token and rec = true and free_token = true and substate = repeating if ((state = processing and token = N) and Token.Action = three); state = sending and substate = repeating if ((state = processing and token = N) and Token.Action = free) and !hN3ns.Action = inject; state = waiting and substate = repeating if ((state = processing and token = N) and Token.Action = free) and hN3ns.Action = inject; state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = three) and !hN3ns.Action = inject; state = waiting and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = three) and hN3ns.Action = inject; state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = three); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = three); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = three); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = three) and number_beacons_recieved < 1) and !hN3ns.Action = inject; number_beacons_recieved = number_beacons_recieved + 1 and state = waiting and substate = repeating if (((state = processing and token = B) and Token.Action = three) and number_beacons_recieved < 1) and hN3ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = three) and !hN3ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = waiting and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = three) and hN3ns.Action = inject; state = disconnected if (((state = processing and token = B) and Token.Action = three) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent Node_4 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: state = processing and token = N if (state = waiting and Environment.Action = send_node_4_N) and !hN4nr.Action = inject; state = waiting and token = N if (state = waiting and Environment.Action = send_node_4_N) and hN4nr.Action = inject; state = processing and token = C if (state = waiting and Environment.Action = send_node_4_C) and !hN4nr.Action = inject; state = waiting and token = C if (state = waiting and Environment.Action = send_node_4_C) and hN4nr.Action = inject; state = processing and token = RP if (state = waiting and Environment.Action = send_node_4_RP) and !hN4nr.Action = inject; state = waiting and token = RP if (state = waiting and Environment.Action = send_node_4_RP) and hN4nr.Action = inject; state = processing and token = B if (state = waiting and Environment.Action = send_node_4_B) and !hN4nr.Action = inject; state = waiting and token = B if (state = waiting and Environment.Action = send_node_4_B) and hN4nr.Action = inject; state = timeout if Environment.Action = timeout_node_4; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false); state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = four); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = set_token and free_token = false and substate = claiming if ((state = processing and token = C) and (Token.Action = six or Token.Action = five)); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = sending and free_token = false and substate = repeating if ((state = processing and token = C) and ((Token.Action = one or Token.Action = two) or Token.Action = three)); state = set_token and rec = true and free_token = true and substate = repeating if ((state = processing and token = N) and Token.Action = four); state = sending and substate = repeating if ((state = processing and token = N) and Token.Action = free); state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = four); state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = four); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = four); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = four); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = four) and number_beacons_recieved < 1); number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = four); state = disconnected if (((state = processing and token = B) and Token.Action = four) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent Node_5 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: state = processing and token = N if (state = waiting and Environment.Action = send_node_5_N); state = processing and token = C if (state = waiting and Environment.Action = send_node_5_C); state = processing and token = RP if (state = waiting and Environment.Action = send_node_5_RP); state = processing and token = B if (state = waiting and Environment.Action = send_node_5_B); state = timeout if Environment.Action = timeout_node_5; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false); state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = five); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = set_token and free_token = false and substate = claiming if ((state = processing and token = C) and Token.Action = six); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = sending and free_token = false and substate = repeating if ((state = processing and token = C) and (((Token.Action = one or Token.Action = two) or Token.Action = three) or Token.Action = four)); state = set_token and rec = true and free_token = false and substate = repeating if ((state = processing and token = N) and Token.Action = five); state = sending and substate = repeating if ((state = processing and token = N) and Token.Action = free); state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = five); state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = five); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = five); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = five); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = five) and number_beacons_recieved < 1); number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = five); state = disconnected if (((state = processing and token = B) and Token.Action = five) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent Node_6 Vars: active_monitor: boolean; free_token: boolean; number_beacons_failed: 0 .. 2; number_beacons_recieved: 0 .. 1; rec: boolean; seen_token: boolean; state: { disconnected, processing, sending, set_token, timeout, waiting }; substate: { beaconing, claiming, repeating, ringpolling }; token: { B, C, N, RP }; end Vars RedStates: end RedStates Actions = { disconnected, none, send_B, send_C, send_N, send_RP, send_recieved, set_token_B, set_token_C, set_token_N, set_token_bit, set_token_free }; Protocol: state = waiting: { none }; state = processing: { send_recieved }; state = timeout: { send_recieved }; (((state = set_token and token = N) and free_token = false) and seen_token = false): { set_token_N }; ((state = set_token and token = B) and free_token = false): { set_token_B }; ((state = set_token and token = C) and free_token = false): { set_token_C }; (state = set_token and token = RP): { set_token_free }; (state = set_token and free_token = true): { set_token_free }; (state = set_token and seen_token = true): { set_token_bit }; (state = sending and token = N): { send_N }; (state = sending and token = RP): { send_RP }; (state = sending and token = C): { send_C }; (state = sending and token = B): { send_B }; state = disconnected: { disconnected }; end Protocol Evolution: state = processing and token = N if (state = waiting and Environment.Action = send_node_6_N); state = processing and token = C if (state = waiting and Environment.Action = send_node_6_C); state = processing and token = RP if (state = waiting and Environment.Action = send_node_6_RP); state = processing and token = B if (state = waiting and Environment.Action = send_node_6_B); state = timeout if Environment.Action = timeout_node_6; state = set_token and substate = ringpolling and token = RP if ((state = timeout and active_monitor = true) and substate = repeating); state = set_token and active_monitor = false and substate = claiming and token = C if ((state = timeout and active_monitor = true) and substate = ringpolling); state = set_token and substate = claiming and token = C if ((state = timeout and active_monitor = false) and substate = repeating); state = set_token and substate = beaconing and token = B if (state = timeout and substate = claiming); state = set_token and number_beacons_failed = number_beacons_failed + 1 and substate = beaconing and token = B if ((state = timeout and substate = beaconing) and number_beacons_failed < 2); state = disconnected if ((state = timeout and substate = beaconing) and number_beacons_failed > 1); state = sending and free_token = false and seen_token = false if state = set_token and !hN6ns.Action = inject; state = waiting and free_token = false and seen_token = false if state = set_token and hN6ns.Action = inject; state = sending and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and !hN6ns.Action = inject; state = waiting and substate = repeating and number_beacons_failed = 0 and number_beacons_recieved = 0 if ((state = processing and token = RP) and active_monitor = false) and hN6ns.Action = inject; state = set_token and free_token = true and token = N and substate = repeating if ((state = processing and token = RP) and active_monitor = true); state = set_token and free_token = true and active_monitor = true and token = RP and number_beacons_failed = 0 and number_beacons_recieved = 0 and substate = ringpolling if ((state = processing and token = C) and Token.Action = six); number_beacons_recieved = 0 and number_beacons_failed = 0 and state = sending and substate = repeating if ((state = processing and token = C) and ! Token.Action = six) and !hN6ns.Action = inject; number_beacons_recieved = 0 and number_beacons_failed = 0 and state = waiting and substate = repeating if ((state = processing and token = C) and ! Token.Action = six) and hN6ns.Action = inject; state = set_token and rec = true and free_token = true and substate = repeating if ((state = processing and token = N) and Token.Action = six); state = sending and substate = repeating if ((state = processing and token = N) and Token.Action = free) and !hN6ns.Action = inject; state = waiting and substate = repeating if ((state = processing and token = N) and Token.Action = free) and hN6ns.Action = inject; state = sending and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = six) and !hN6ns.Action = inject; state = waiting and substate = repeating if ((((active_monitor = false and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = six) and hN6ns.Action = inject; state = set_token and free_token = false and seen_token = true and substate = repeating if (((((active_monitor = true and Token_bit.Action = unset) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = six); state = set_token and free_token = true and seen_token = false and substate = repeating if (((((active_monitor = true and Token_bit.Action = set) and state = processing) and token = N) and ! Token.Action = free) and ! Token.Action = six); state = set_token and token = C and substate = claiming and number_beacons_failed = 0 and number_beacons_recieved = 0 if (((state = processing and substate = beaconing) and token = B) and ! Token.Action = six); number_beacons_recieved = number_beacons_recieved + 1 and state = sending and substate = repeating if (((state = processing and token = B) and Token.Action = six) and number_beacons_recieved < 1) and !hN6ns.Action = inject; number_beacons_recieved = number_beacons_recieved + 1 and state = waiting and substate = repeating if (((state = processing and token = B) and Token.Action = six) and number_beacons_recieved < 1) and hN6ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = sending and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = six) and !hN6ns.Action = inject; number_beacons_failed = 0 and number_beacons_recieved = 0 and state = waiting and substate = repeating if (((state = processing and ! substate = beaconing) and token = B) and ! Token.Action = six) and hN6ns.Action = inject; state = disconnected if (((state = processing and token = B) and Token.Action = six) and number_beacons_recieved > 0); state = waiting and free_token = false and seen_token = false if state = sending; end Evolution end Agent Agent sN2ns Vars: status: {fault_i, fault_ni, nofault, stop_i, stop_ni, w_astt, w_rstt}; end Vars RedStates: end RedStates Actions = {inject, notinject, start}; Protocol: status = fault_i : {inject}; status = fault_ni : {inject}; status = nofault : {notinject}; status = stop_i : {notinject}; status = stop_ni : {notinject}; status = w_astt : {notinject}; status = w_rstt : {notinject, start}; end Protocol Evolution: status = fault_ni if status = w_astt and Node_1.Action=send_N; status = w_astt if status = w_rstt and sN2ns.Action = start; status = fault_i if (status = fault_i or status = fault_ni) and sN2ns.Action = inject and !Node_1.Action=send_C; status = stop_i if ((status = fault_i or status = fault_ni) and Node_1.Action=send_C) and sN2ns.Action = inject; status = stop_ni if status = stop_i; end Evolution end Agent Agent hN3ns Vars: status: {fault_i, fault_ni, nofault, stop_i, stop_ni, w_astt, w_rstt}; end Vars RedStates: end RedStates Actions = {inject, notinject, start}; Protocol: status = fault_i : {inject}; status = fault_ni : {inject}; status = nofault : {notinject}; status = stop_i : {notinject}; status = stop_ni : {notinject}; status = w_astt : {notinject}; status = w_rstt : {notinject, start}; end Protocol Evolution: status = fault_ni if status = w_astt and !Node_3.Action = disconnected and Node_2.Action=send_N; status = w_astt if status = w_rstt and hN3ns.Action = start; status = fault_i if (status = fault_i or status = fault_ni) and hN3ns.Action = inject and !Node_3.Action=disconnected; status = stop_i if ((status = fault_i or status = fault_ni) and Node_3.Action=disconnected) and hN3ns.Action = inject; status = stop_ni if status = stop_i; end Evolution end Agent Agent hN4nr Vars: status: {fault_i, fault_ni, nofault, stop_i, stop_ni, w_astt, w_rstt}; end Vars RedStates: end RedStates Actions = {inject, notinject, start}; Protocol: status = fault_i : {inject}; status = fault_ni : {inject}; status = nofault : {notinject}; status = stop_i : {notinject}; status = stop_ni : {notinject}; status = w_astt : {notinject}; status = w_rstt : {notinject, start}; end Protocol Evolution: status = fault_ni if status = w_astt and Node_3.Action=send_N; status = w_astt if status = w_rstt and hN4nr.Action = start; status = fault_i if (status = fault_i or status = fault_ni) and hN4nr.Action = inject and !Node_4.Action=disconnected; status = stop_i if ((status = fault_i or status = fault_ni) and Node_4.Action=disconnected) and hN4nr.Action = inject; status = stop_ni if status = stop_i; end Evolution end Agent Agent hN6ns Vars: status: {fault_i, fault_ni, nofault, stop_i, stop_ni, w_astt, w_rstt}; end Vars RedStates: end RedStates Actions = {inject, notinject, start}; Protocol: status = fault_i : {inject}; status = fault_ni : {inject}; status = nofault : {notinject}; status = stop_i : {notinject}; status = stop_ni : {notinject}; status = w_astt : {notinject}; status = w_rstt : {notinject, start}; end Protocol Evolution: status = fault_ni if status = w_astt and Node_5.Action=send_N; status = w_astt if status = w_rstt and hN6ns.Action = start; status = fault_i if (status = fault_i or status = fault_ni) and hN6ns.Action = inject and !Node_6.Action=disconnected; status = stop_i if ((status = fault_i or status = fault_ni) and Node_6.Action=disconnected) and hN6ns.Action = inject; status = stop_ni if status = stop_i; end Evolution end Agent Agent N1sm Vars: status: {nofault,fault_ni,stop_i, stop_ni, w_rstt, w_astt}; end Vars RedStates: end RedStates Actions = {dont_inject,inject,start}; Protocol: status = stop_ni : {dont_inject}; status = stop_i : {dont_inject}; status = fault_ni : {inject}; status = w_astt : {dont_inject}; status = w_rstt : {dont_inject,start}; status = nofault : {dont_inject}; end Protocol Evolution: status = stop_ni if status = stop_i; status = stop_i if status = fault_ni; status = fault_ni if status = w_astt and Node_1.Action = send_N; status = w_astt if status = w_rstt and N1sm.Action = start; end Evolution end Agent Agent TKwd Vars: status: {nofault,fault_ni,stop_i, w_rstt, stop_ni, w_astt}; end Vars RedStates: end RedStates Actions = {dont_inject,inject,start}; Protocol: status = stop_ni : {dont_inject}; status = stop_i : {dont_inject}; status = fault_ni : {inject}; status = w_astt : {dont_inject}; status = w_rstt : {dont_inject,start}; status = nofault : {dont_inject}; end Protocol Evolution: status = stop_ni if status = stop_i; status = stop_i if status = fault_ni; status = fault_ni if status = w_astt and Node_2.Action = send_N; status = w_astt if status = w_rstt and TKwd.Action = start; end Evolution end Agent Evaluation sN2ns_faulty if !sN2ns.status = nofault; sN2ns_injected if sN2ns.status = fault_i or sN2ns.status = stop_i; sN2ns_stopped if sN2ns.status = stop_ni; hN3ns_faulty if !hN3ns.status = nofault; hN3ns_injected if hN3ns.status = fault_i or hN3ns.status = stop_i; hN3ns_stopped if hN3ns.status = stop_ni; hN4nr_faulty if !hN4nr.status = nofault; hN4nr_injected if hN4nr.status = fault_i or hN4nr.status = stop_i; hN4nr_stopped if hN4nr.status = stop_ni; hN6ns_faulty if !hN6ns.status = nofault; hN6ns_injected if hN6ns.status = fault_i or hN6ns.status = stop_i; hN6ns_stopped if hN6ns.status = stop_ni; sN2ns_wait if sN2ns.status = w_rstt; hN3ns_wait if hN3ns.status = w_rstt; hN4nr_wait if hN4nr.status = w_rstt; hN6ns_wait if hN6ns.status = w_rstt; TKwd_wait if TKwd.status = w_rstt; N1sm_wait if N1sm.status = w_rstt; sN2ns_fair if !sN2ns.status = w_rstt; hN3ns_fair if !hN3ns.status = w_rstt; hN4nr_fair if !hN4nr.status = w_rstt; hN6ns_fair if !hN6ns.status = w_rstt; TKwd_fair if ! TKwd.status = w_rstt; N1sm_fair if !N1sm.status = w_rstt; N1sm_faulty if !N1sm.status = nofault; TKwd_faulty if !TKwd.status = nofault; TKwd_injected if TKwd.status = stop_i; N1sm_injected if N1sm.status = stop_i; n1sm_i if N1sm.status = stop_i; n1sm_f if !N1sm.status = nofault; tkwd_f if !TKwd.status = nofault; n1sm_s if N1sm.status = stop_ni; hn3ns_is if hN3ns.status = fault_i or hN3ns.status = stop_i; hn4nr_is if hN4nr.status = fault_i or hN4nr.status = stop_i; --- from paper ----- tests Node1di if Node_1.state = disconnected; Node2di if Node_2.state = disconnected; Node3di if Node_3.state = disconnected; Node4di if Node_4.state = disconnected; Node5di if Node_5.state = disconnected; Node6di if Node_6.state = disconnected; Node1AM if Node_1.active_monitor = true; Node2AM if Node_2.active_monitor = true; Node3AM if Node_3.active_monitor = true; Node4AM if Node_4.active_monitor = true; Node5AM if Node_5.active_monitor = true; Node6AM if Node_6.active_monitor = true; Node_1Timeout if Node_1.state = timeout; -- propositions no_f if hN3ns.status = nofault and hN4nr.status = nofault and hN6ns.status = nofault and sN2ns.status = nofault and TKwd.status = nofault and N1sm.status = nofault; msgsent if Node_2.sent_message = true; recack if Node_2.rec= true; timeout if Node_1.state = timeout or Node_2.state = timeout or Node_3.state = timeout or Node_4.state = timeout or Node_5.state = timeout or Node_6.state = timeout; timeoutnoam if Node_2.state = timeout or Node_3.state = timeout or Node_4.state = timeout or Node_5.state = timeout or Node_6.state = timeout; beaconing if Node_1.substate = beaconing or Node_2.substate = beaconing or Node_3.substate = beaconing or Node_4.substate = beaconing or Node_5.substate = beaconing or Node_6.substate = beaconing; token_free if Token.node_info = 0; am if Node_1.active_monitor = true or Node_2.active_monitor = true or Node_3.active_monitor = true or Node_4.active_monitor = true or Node_5.active_monitor = true or Node_6.active_monitor = true; n1toam if Node_1.state = timeout and Node_1.active_monitor = true; n1tonam if Node_1.state = timeout and Node_1.active_monitor = false; -- This is a better description of Node 3 disconnecting as we only want to reason about it when it first disconnects n3d if ((Node_3.state = timeout and Node_3.substate = beaconing) and Node_3.number_beacons_failed > 1) or (((Node_3.state = processing and Node_3.token = B) and Token.node_info = 3) and Node_3.number_beacons_recieved > 0); --n3d if Node_3.state = disconnected; n4sb if Node_3.substate = beaconing and Node_3.number_beacons_failed = 0; hard_f if (!hN3ns.status = nofault) or (!hN4nr.status = nofault) or (!hN6ns.status = nofault); hard_i if (hN3ns.status = fault_i) or (hN4nr.status = fault_i) or (hN6ns.status = stop_i); hard_is if hN4nr.status = fault_i or hN4nr.status = stop_ni or hN4nr.status = stop_i or hN3ns.status = fault_i or hN3ns.status = stop_ni or hN3ns.status = stop_i or hN6ns.status = fault_i or hN6ns.status = stop_ni or hN6ns.status = stop_i; soft_i if sN2ns.status = fault_i; soft_f if !sN2ns.status = nofault; allhs_s if (sN2ns.status = stop_ni) and (hN3ns.status = stop_ni or hN4nr.status = stop_ni) and (hN6ns.status = stop_ni); allhs_f if (!sN2ns.status = nofault) and (!hN3ns.status = nofault) and (!hN4nr.status = nofault) and (!hN6ns.status = nofault); anyhs_i if (sN2ns.status = fault_i) or (hN3ns.status = fault_i) or (hN4nr.status = fault_i) or (hN6ns.status = fault_i); anyhs_is if (sN2ns.status = fault_i) or (hN3ns.status = fault_i) or (hN4nr.status = fault_i) or (hN6ns.status = fault_i) or (sN2ns.status = stop_i) or (hN3ns.status = stop_i) or (hN4nr.status = stop_i) or (hN6ns.status = stop_i); nohs_f if (hN3ns.status = nofault) and (hN4nr.status = nofault) and (hN6ns.status = nofault) and sN2ns.status = nofault; end Evaluation InitStates ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((Environment.state = waiting_message and Environment.token = N) and Environment.timeout = 2) and Environment.send_status = process) and Environment.current_node = 1) and Environment.active_monitor = 0) and Node_1.state = set_token) and Node_1.token = C) and Node_1.free_token = false) and Node_1.number_beacons_failed = 0) and Node_1.number_beacons_recieved = 0) and Node_1.rec = false) and Node_1.seen_token = false) and Node_1.substate = claiming) and Node_1.active_monitor = false) and Node_2.state = waiting) and Node_2.token = C) and Node_2.free_token = false) and Node_2.number_beacons_failed = 0) and Node_2.number_beacons_recieved = 0) and Node_2.rec = false) and Node_2.seen_token = false) and Node_2.substate = repeating) and Node_2.active_monitor = false) and Node_3.state = waiting) and Node_3.token = C) and Node_3.free_token = false) and Node_3.number_beacons_failed = 0) and Node_3.number_beacons_recieved = 0) and Node_3.rec = false) and Node_3.seen_token = false) and Node_3.substate = repeating) and Node_3.active_monitor = false) and Node_4.state = waiting) and Node_4.token = C) and Node_4.free_token = false) and Node_4.number_beacons_failed = 0) and Node_4.number_beacons_recieved = 0) and Node_4.rec = false) and Node_4.seen_token = false) and Node_4.substate = repeating) and Node_4.active_monitor = false) and Node_5.state = waiting) and Node_5.token = C) and Node_5.free_token = false) and Node_5.number_beacons_failed = 0) and Node_5.number_beacons_recieved = 0) and Node_5.rec = false) and Node_5.seen_token = false) and Node_5.substate = repeating) and Node_5.active_monitor = false) and Node_6.state = waiting) and Node_6.token = C) and Node_6.free_token = false) and Node_6.number_beacons_failed = 0) and Node_6.number_beacons_recieved = 0) and Node_6.rec = false) and Node_6.seen_token = false) and Node_6.substate = repeating) and Node_6.active_monitor = false) and Node_2.sent_message = false) and Token.node_info = 0) and Token_bit.bit = false) and (sN2ns.status = w_rstt or sN2ns.status = nofault) and (hN3ns.status=w_rstt or hN3ns.status = nofault) and (hN4nr.status = w_rstt or hN4nr.status = nofault) and (hN6ns.status = w_rstt or hN6ns.status = nofault) and ( N1sm.status = nofault or N1sm.status = w_rstt) and ( TKwd.status = nofault or TKwd.status = w_rstt); end InitStates Groups g1 = {Node_1,Node_2,Node_3,Node_4,Node_5,Node_6}; end Groups Fairness sN2ns_wait->sN2ns_fair; hN3ns_wait->hN3ns_fair; hN4nr_wait->hN4nr_fair; hN6ns_wait->hN6ns_fair; N1sm_wait->N1sm_fair; TKwd_wait->TKwd_fair; end Fairness Formulae --- First section 6.5 AF(msgsent); AF(no_f-> recack); AF(!no_f-> recack); AG(!am->AF(am)); AG((!n1sm_f and !am)->AF(am)); AG(!token_free -> AF(token_free)); AG(((!n1sm_f or !tkwd_f) and !token_free)->AF(token_free)); AG(!beaconing); AF(!hard_f->!beaconing); AG(!timeout); AG(!hard_f -> !timeout); AG(!soft_f -> !timeout); AG((!hard_f and !soft_f) -> !timeout); AG((!n1sm_f and !soft_f)-> !timeoutnoam); AG((!n1sm_f and !hard_f)-> !timeoutnoam); --- Tolerance to intermittent faults AG(n1sm_s -> !am); AG((n1sm_s and nohs_f) -> !am); AG((n1sm_s and anyhs_i)-> AF(am)); --- Recoverability AG((anyhs_i and msgsent) -> AF(recack)); AG(((!n1sm_f or !tkwd_f) and msgsent and anyhs_i) -> AF(recack)); --- Diagnosability AG((!n1sm_f and n1tonam) -> K(Node_1,hN6ns_faulty)); AG((!n1sm_f and allhs_f and n1toam) -> (K(Node_1,anyhs_i) and !K(Node_1,hard_i) and !K(Node_1,soft_i))); !E((!n1sm_f and !anyhs_i) U (anyhs_i and !AF(K(Node_1,(anyhs_i))))); !E((!n1sm_f and !anyhs_i) U (anyhs_i and !AF(GK(g1,(anyhs_i))))); !E((!n1sm_f and !DK(g1,(anyhs_i))) U DK(g1,(anyhs_i)) and !AF(GK(g1,(anyhs_i)))); AG((!n1sm_f and allhs_f and n4sb ) -> (K(Node_4,((hN3ns_injected or hN3ns_stopped) or (hN4nr_injected or hN4nr_stopped))) and !K(Node_4,((hN3ns_injected or hN3ns_stopped))) and !K(Node_4,((hN4nr_injected or hN4nr_stopped))))); AG( (!n1sm_f and allhs_f and n3d) -> (K(Node_3, K(Node_4,((hN3ns_injected or hN3ns_stopped) or (hN4nr_injected or hN4nr_stopped)) and !K(Node_4,((hN3ns_injected or hN3ns_stopped))) and !K(Node_4,(hN4nr_injected or hN4nr_stopped)))))); !E((!n1sm_f and !hN3ns_injected) U (hN3ns_injected and !AF(K(Node_4,((hN3ns_injected or hN3ns_stopped) or (hN4nr_injected or hN4nr_stopped)))))); !E((!n1sm_f and !hN4nr_injected) U (hN4nr_injected and !AF(K(Node_4,((hN3ns_injected or hN3ns_stopped) or (hN4nr_injected or hN4nr_stopped)))))); !E((!n1sm_f and !DK(g1,(hN3ns_injected or hN4nr_injected))) U DK(g1,(hN3ns_injected or hN4nr_injected )) and !AF(GK(g1,((hN3ns_injected or hN3ns_stopped) or (hN4nr_injected or hN4nr_stopped))))); !E(!n1sm_f and !DK(g1,(hN3ns_injected or hN4nr_injected)) U (DK(g1,(hN3ns_injected or hN4nr_injected)) and !AF(GK(g1,(hard_is))))); !E(!n1sm_f and !GK(g1,hard_is) U (GK(g1,hard_is) and !AF(GCK(g1,hard_is )))); ------------ Check all faults start -- should return false AG(!sN2ns_injected); AG(!hN3ns_injected); AG(!hN4nr_injected); AG(!hN6ns_injected); AG(!TKwd_injected); AG(!N1sm_injected); ------------ Check that nothing else apart from 3 4 and 6 disconnect AG(!Node1di); AG(!Node2di); AG(!Node3di); AG(!Node4di); AG(!Node5di); AG(!Node6di); ------------ Check that Node 1 always becomes active monitor and is the only active monitor AG(!Node1AM); AG(!Node2AM); AG(!Node3AM); AG(!Node4AM); AG(!Node5AM); AG(!Node6AM); end Formulae