%% Time Sharing Example. %% Written by Shinya Umeno time_sharing: CONTEXT = BEGIN %%%%%%%%% Processes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% RED processes RED_SIZE: NATURAL = 2; FIRST_RED_ID: NATURAL = 1; LAST_RED_ID: NATURAL = FIRST_RED_ID + RED_SIZE - 1; RED_ID: TYPE = [FIRST_RED_ID .. LAST_RED_ID]; %% BLUE processes BLUE_SIZE: NATURAL = 2; FIRST_BLUE_ID: NATURAL = LAST_RED_ID + 1; LAST_BLUE_ID: NATURAL = FIRST_BLUE_ID + BLUE_SIZE - 1; BLUE_ID: TYPE = [FIRST_BLUE_ID .. LAST_BLUE_ID]; %% Entire processes FIRST_PROCESS_ID: NATURAL = FIRST_RED_ID; LAST_PROCESS_ID: NATURAL = LAST_BLUE_ID; PROCESS_ID: TYPE = [FIRST_PROCESS_ID .. LAST_PROCESS_ID]; is_RED(id: PROCESS_ID): BOOLEAN = (id >= FIRST_RED_ID AND id <= LAST_RED_ID); is_BLUE(id: PROCESS_ID): BOOLEAN = (id >= FIRST_BLUE_ID AND id <= LAST_BLUE_ID); %%%%%%%% Interaction instances %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Interaction instances INTERACT_INST_SIZE: NATURAL = 10; INTERACT_INST: TYPE = [0 .. INTERACT_INST_SIZE]; %% 0 represents the special "bottom" symbol. %% The number of interaction instances stored in one process. %% In this case study, there are one + # of processes in one group %% (my_interact_inst and ack_interact_inst[]). PROCESS_INTERACT_INST_NUM: NATURAL = 1 + max(RED_SIZE, BLUE_SIZE); PROCESS_INTERACT_INST_INDEX: TYPE = [1 .. PROCESS_INTERACT_INST_NUM]; PROCESS_INTERACT_INSTS: TYPE = ARRAY PROCESS_INTERACT_INST_INDEX OF INTERACT_INST; %% A vector of interaction instances that processes are currently using. %% This vector is used for finding out an unused interaction instance. INTERACT_INST_VECTOR: TYPE = ARRAY PROCESS_ID OF PROCESS_INTERACT_INSTS; %%%%%%%% Time Data %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Time nonces NUMBER_OF_TIME_NONCES: NATURAL = 8; FIRST_TN_ID: NATURAL = 1; LAST_TN_ID: NATURAL = FIRST_TN_ID + NUMBER_OF_TIME_NONCES - 1; TIME_NONCE_ID: TYPE = [FIRST_TN_ID .. LAST_TN_ID]; %% A set of time nonces is represented by a Boolean array. TIME_NONCE_SET: TYPE = ARRAY TIME_NONCE_ID OF BOOLEAN; empty_time_nonce_set: TIME_NONCE_SET = [[id: TIME_NONCE_ID] FALSE]; singleton_tn_set(tn_id: TIME_NONCE_ID): TIME_NONCE_SET = [[id: TIME_NONCE_ID] tn_id = id]; %% Compute the union of two time nonce sets. union_tn_sets(tn_set1, tn_set2: TIME_NONCE_SET): TIME_NONCE_SET = [[tn_id: TIME_NONCE_ID] tn_set1[tn_id] OR tn_set2[tn_id]]; %% Time stamps NUMBER_OF_TIME_STAMPS: NATURAL = 6; FIRST_TS_ID: NATURAL = 1; LAST_TS_ID: NATURAL = FIRST_TS_ID + NUMBER_OF_TIME_STAMPS - 1; TIME_STAMP_ID: TYPE = [FIRST_TS_ID .. LAST_TS_ID]; %% A set of time stamps is represented by a Boolean array. TIME_STAMP_SET: TYPE = ARRAY TIME_STAMP_ID OF BOOLEAN; empty_time_stamp_set: TIME_STAMP_SET = [[id: TIME_STAMP_ID] FALSE]; singleton_ts_set(ts_id: TIME_STAMP_ID): TIME_STAMP_SET = [[id: TIME_STAMP_ID] ts_id = id]; %% Compute the union of two time stamp sets. union_ts_sets(ts_set1, ts_set2: TIME_STAMP_SET): TIME_STAMP_SET = [[ts_id: TIME_STAMP_ID] ts_set1[ts_id] OR ts_set2[ts_id]]; %% Time data is represented by a record containing a set of time nonces and a set of time stamps. TIME_DATA: TYPE = [# tnset: TIME_NONCE_SET, tsset: TIME_STAMP_SET #]; bottom_time_data: TIME_DATA = (# tnset := empty_time_nonce_set, tsset:= empty_time_stamp_set #); %% Is given time data represents zero? is_zero_td(td: TIME_DATA): BOOLEAN = (FORALL (tn: TIME_NONCE_ID): NOT td.tnset[tn]) AND (FORALL (ts: TIME_STAMP_ID): NOT td.tsset[ts]); %% Creating time data from time nonce ID set tn2td(tn_set: TIME_NONCE_SET): TIME_DATA = (# tnset := tn_set, tsset := empty_time_stamp_set #); %% Creating time data from time stamp ID set ts2td(ts_set: TIME_STAMP_SET): TIME_DATA = (# tnset := empty_time_nonce_set, tsset := ts_set #); %% Computing a `max' operation max_tn_td(tn_set: TIME_NONCE_SET, td: TIME_DATA): TIME_DATA = (# tnset := union_tn_sets(tn_set, td.tnset), tsset := td.tsset #); max_ts_td(ts_set: TIME_STAMP_SET, td: TIME_DATA): TIME_DATA = (# tnset := td.tnset, tsset := union_ts_sets(ts_set, td.tsset) #); max_td(td1, td2: TIME_DATA): TIME_DATA = (# tnset := union_tn_sets(td1.tnset, td2.tnset), tsset := union_ts_sets(td1.tsset, td2.tsset) #); %% Element-wise union of time nonce and time stamp sets in time data. (same as max_td). union_td(td1, td2: TIME_DATA): TIME_DATA = (# tnset := union_tn_sets(td1.tnset, td2.tnset), tsset := union_ts_sets(td1.tsset, td2.tsset) #); %% Element-wise set-subtraction of time nonce and time stamp sets in time data. subtract_td(td1, td2: TIME_DATA): TIME_DATA = (# tnset := [[tn_id: TIME_NONCE_ID] td1.tnset(tn_id) AND NOT td2.tnset(tn_id)], tsset := [[ts_id: TIME_STAMP_ID] td1.tsset(ts_id) AND NOT td2.tsset(ts_id)] #); %% The value represented by td1 is less than or equal to the value represented by td2. %% Computed by element-wise set-inclusion of two sets in symbolic time data. td1_lt_eq_td2(td1, td2: TIME_DATA): BOOLEAN = (FORALL (tn_id: TIME_NONCE_ID): td1.tnset[tn_id] => td2.tnset[tn_id]) AND (FORALL (ts_id: TIME_STAMP_ID): td1.tsset[ts_id] => td2.tsset[ts_id]); %% Timeout time stored in timeout variables TIMEOUT_TIME: TYPE = [# td: TIME_DATA, slack_added: BOOLEAN, is_set: BOOLEAN #]; unset_timeout: TIMEOUT_TIME = (# td := bottom_time_data, slack_added := FALSE, is_set := FALSE #); %% A vector of timeout times. %% This vector is used for finding out an unused time nonce/stamp ID. TO_VECTOR: TYPE = ARRAY PROCESS_ID OF TIMEOUT_TIME; %% Computes whether there exists a timeout that is set before %% the given time data. exists_timeout_set_before(td: TIME_DATA, to_vec: TO_VECTOR): BOOLEAN = EXISTS (i: PROCESS_ID): NOT to_vec(i).slack_added AND td1_lt_eq_td2(to_vec(i).td, td); %% The number of timed variables in a process. %% In this case study, there is only one (proposing_time_nonce). PROCESS_TV_NUM: NATURAL = 1; PROCESS_TV_INDEX: TYPE = [1 .. PROCESS_TV_NUM]; PROCESS_TIMED_VARS: TYPE = ARRAY PROCESS_TV_INDEX OF TIME_DATA; %% A vector of values (time data) in timed variables. %% This vector is used for finding out an unused time nonce/stamp ID. TV_VECTOR: TYPE = ARRAY PROCESS_ID OF PROCESS_TIMED_VARS; %%%%%%% Messages, Channel Buffers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% MESSAGE_TYPE: TYPE = {CONST, CUSTOM, ACK, BROKEN}; MESSAGE: TYPE = [# td: TIME_DATA, msg_type: MESSAGE_TYPE, intr_inst: INTERACT_INST #]; %% A message with broken contents. broken_msg: MESSAGE = (# td := bottom_time_data, msg_type := BROKEN, intr_inst := 0 #); %% A dummy message used for initialization for buffers. not actually used by processees. init_msg: MESSAGE = (# td := bottom_time_data, msg_type := BROKEN, intr_inst := 0 #); %% The buffer of channels BUFFER_SIZE: NATURAL = 1; BUFFER_RANGE: TYPE = [1 .. BUFFER_SIZE]; BUFFER_POINTER: TYPE = [0 .. BUFFER_SIZE]; BUFFER: TYPE = ARRAY BUFFER_RANGE OF MESSAGE; empty_buffer: BUFFER = [[entry: BUFFER_RANGE] init_msg]; R2B_BUFFERS: TYPE = ARRAY RED_ID OF ARRAY BLUE_ID OF BUFFER; R2B_BPS: TYPE = ARRAY RED_ID OF ARRAY BLUE_ID OF BUFFER_POINTER; B2R_BUFFERS: TYPE = ARRAY BLUE_ID OF ARRAY RED_ID OF BUFFER; B2R_BPS: TYPE = ARRAY BLUE_ID OF ARRAY RED_ID OF BUFFER_POINTER; %%%%%%%% Checking availability of an interaction instance %%%%%%%%%%%%%%%%%%%%%% %%%%%%%% Finding the smallest available interaction instance %%%%%%%%%%%%%%%%%%%% %% Checking availability of a given interaction instance. this_intr_inst_available(this_intr_inst: INTERACT_INST, intr_inst_vec: INTERACT_INST_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): BOOLEAN = (FORALL (proc_id: PROCESS_ID, inst_num: PROCESS_INTERACT_INST_INDEX): intr_inst_vec[proc_id][inst_num] /= this_intr_inst) AND (FORALL (red_id: RED_ID, blue_id: BLUE_ID, r2b_buff_entry: BUFFER_RANGE): ((r2b_buff_entry <= r2b_bps[red_id][blue_id]) => %% If this entry is not empty, then r2b_buff[red_id][blue_id][r2b_buff_entry].intr_inst /= this_intr_inst)) AND (FORALL (blue_id: BLUE_ID, red_id: RED_ID, b2r_buff_entry: BUFFER_RANGE): ((b2r_buff_entry <= b2r_bps[blue_id][red_id]) => %% If this entry is not empty, then b2r_buff[blue_id][red_id][b2r_buff_entry].intr_inst /= this_intr_inst)); %% Computing the smallest available interaction instance in the current state of the composed system. smallest_intr_inst_rec(intr_inst_rec: INTERACT_INST, intr_inst_vec: INTERACT_INST_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): INTERACT_INST = IF this_intr_inst_available(intr_inst_rec, intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) THEN intr_inst_rec ELSIF intr_inst_rec < INTERACT_INST_SIZE THEN smallest_intr_inst_rec(intr_inst_rec + 1, intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) ELSE 0 %% an available interaction instance is not found ENDIF; smallest_intr_inst(intr_inst_vec: INTERACT_INST_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): INTERACT_INST = smallest_intr_inst_rec(1, intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps); %%%%%%%%%%%% Checking availability of time data IDs (time nonce IDs and time stamp IDs) %%%%%%%%%%%%% %%%%%%%%%%%% Finding the smallest available time nonce ID and time stamp ID %%%%%%%%%%%%%%%%%%%%%%%%% %% Checking availability of a given time nonce ID this_tn_ID_available(this_tn_id: TIME_NONCE_ID, to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): BOOLEAN = (FORALL (proc_id: PROCESS_ID): (to_vec[proc_id].is_set => NOT to_vec[proc_id].td.tnset(this_tn_id)) AND (FORALL (proc_tv_index: PROCESS_TV_INDEX): NOT tv_vec[proc_id][proc_tv_index].tnset(this_tn_id))) AND (FORALL (red_id: RED_ID, blue_id: BLUE_ID, r2b_buff_entry: BUFFER_RANGE): ((r2b_buff_entry <= r2b_bps[red_id][blue_id]) => %% If this entry is not empty, then NOT r2b_buff[red_id][blue_id][r2b_buff_entry].td.tnset(this_tn_id))) AND (FORALL (blue_id: BLUE_ID, red_id: RED_ID, b2r_buff_entry: BUFFER_RANGE): ((b2r_buff_entry <= b2r_bps[blue_id][red_id]) => %% If this entry is not empty, then NOT b2r_buff[blue_id][red_id][b2r_buff_entry].td.tnset(this_tn_id))); %% Checking availability of a given time stamp ID this_ts_ID_available(this_ts_id: TIME_STAMP_ID, to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): BOOLEAN = (FORALL (proc_id: PROCESS_ID): (to_vec[proc_id].is_set => NOT to_vec[proc_id].td.tsset(this_ts_id)) AND (FORALL (proc_tv_index: PROCESS_TV_INDEX): NOT tv_vec[proc_id][proc_tv_index].tsset(this_ts_id))) AND (FORALL (red_id: RED_ID, blue_id: BLUE_ID, r2b_buff_entry: BUFFER_RANGE): ((r2b_buff_entry <= r2b_bps[red_id][blue_id]) => %% If this entry is not empty, then NOT r2b_buff[red_id][blue_id][r2b_buff_entry].td.tsset(this_ts_id))) AND (FORALL (blue_id: BLUE_ID, red_id: RED_ID, b2r_buff_entry: BUFFER_RANGE): ((b2r_buff_entry <= b2r_bps[blue_id][red_id]) => %% If this entry is not empty, then NOT b2r_buff[blue_id][red_id][b2r_buff_entry].td.tsset(this_ts_id))); %% Time-nonce-ID and Time-stamp_ID types augmented with a "not-found" Boolean. %% These types are used for a return value of the function 'smallest_tn_ID' that computes %% the smallest available time nonce ID. TIME_NONCE_ID_WITH_NOT_FOUND: TYPE = [# tn_id: TIME_NONCE_ID, not_found: BOOLEAN #]; init_tn_id_with_not_found: TIME_NONCE_ID_WITH_NOT_FOUND = (# tn_id := FIRST_TN_ID, not_found := false #); init_tn_id_with_not_found_true: TIME_NONCE_ID_WITH_NOT_FOUND = (# tn_id := FIRST_TN_ID, not_found := true #); TIME_STAMP_ID_WITH_NOT_FOUND: TYPE = [# ts_id: TIME_STAMP_ID, not_found: BOOLEAN #]; init_ts_id_with_not_found: TIME_STAMP_ID_WITH_NOT_FOUND = (# ts_id := FIRST_TS_ID, not_found := FALSE #); init_ts_id_with_not_found_true: TIME_STAMP_ID_WITH_NOT_FOUND = (# ts_id := FIRST_TS_ID, not_found := TRUE #); %% Computing the smallest available time nonce ID smallest_tn_ID_rec(tn_id_rec: TIME_NONCE_ID, to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIME_NONCE_ID_WITH_NOT_FOUND = IF this_tn_ID_available(tn_id_rec, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) THEN (# tn_id := tn_id_rec, not_found := FALSE #) ELSIF tn_id_rec < LAST_TN_ID THEN smallest_tn_ID_rec(tn_id_rec + 1, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) ELSE (# tn_id := FIRST_TN_ID, not_found := TRUE #) ENDIF; smallest_tn_ID(to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID_rec(FIRST_TN_ID, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps); %% Computing the smallest available time stamp ID smallest_ts_ID_rec(ts_id_rec: TIME_STAMP_ID, to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIME_STAMP_ID_WITH_NOT_FOUND = IF this_ts_ID_available(ts_id_rec, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) THEN (# ts_id := ts_id_rec, not_found := FALSE #) ELSIF ts_id_rec < LAST_TS_ID THEN smallest_ts_ID_rec(ts_id_rec + 1, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) ELSE (# ts_id := FIRST_TS_ID, not_found := TRUE #) ENDIF; smallest_ts_ID(to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID_rec(FIRST_TS_ID, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps); %%%%%%%% Cunstructing a set of time stamp IDs that are currently used in the system. %%%%%%%% %%%%%%%% This is for the time-stamp-estimation trick. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% construct_existing_ts_set(to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIME_STAMP_SET = [[ts_id: TIME_STAMP_ID] NOT this_ts_ID_available(ts_id, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps)]; %%%%%%%% Setting a timeout %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Setting a timeout with the slack (epsilon) added. set_timeout_with_slack(given_td: TIME_DATA): TIMEOUT_TIME = (# td := given_td, slack_added := TRUE, is_set := TRUE #); %% Setting a timeout without the slack. set_timeout_without_slack(given_td: TIME_DATA): TIMEOUT_TIME = (# td := given_td, slack_added := FALSE, is_set := TRUE #); %% Updating a timeout using a max. A timeout with the slack e (and zero timeout) %% must be updated using a new timeout with the slack, %% and a timeout without the slack e (except for zero timeout) must be updated %% using a new timeout without the slack. We check this consistency %% in automaton transitions that use updates. update_timeout(timeout1: TIMEOUT_TIME, timeout2: TIMEOUT_TIME): TIMEOUT_TIME = (# td := max_td(timeout1.td, timeout2.td), slack_added := timeout1.slack_added OR timeout2.slack_added, %% Disjunction for updating zero timeout. is_set := TRUE #); check_timeout_consistency(timeout1: TIMEOUT_TIME, timeout2: TIMEOUT_TIME): BOOLEAN = (timeout1.slack_added = timeout2.slack_added); %% Updating a server's timeout using max(clock _ u _ 2e, timeout_time). update_timeout_estimation_trick(given_to: TIMEOUT_TIME, to_vec: TO_VECTOR, tv_vec: TV_VECTOR, r2b_buff: R2B_BUFFERS, r2b_bps: R2B_BPS, b2r_buff: B2R_BUFFERS, b2r_bps: B2R_BPS ): TIMEOUT_TIME = LET existing_ts_set: TIME_STAMP_SET = construct_existing_ts_set(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (# td := max_ts_td(existing_ts_set, given_to.td), slack_added := TRUE, is_set := TRUE #); %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% Modules %%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ACTIONS: TYPE = {bcast_CONST, bcast_CUSTOM, send_ACK, rcv_CONST, rcv_CUSTOM, rcv_ACK, rcv_BROKEN, timeout}; PROCESS_PROGRAM_COUNTER: TYPE = {idle, waiting_for_ack, sending_ack, waiting_for_timeout, crit_ready, crit}; COLOR: TYPE = {RED, BLUE}; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% RED process %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% RED_Process[my_id: PROCESS_ID]: MODULE = BEGIN OUTPUT pc: PROCESS_PROGRAM_COUNTER OUTPUT timeout_time: TIMEOUT_TIME LOCAL my_interact_inst: INTERACT_INST LOCAL ack_interact_inst: ARRAY BLUE_ID OF INTERACT_INST LOCAL proposing_time_nonce: TIME_DATA LOCAL ack_rcvd_list: ARRAY BLUE_ID of BOOLEAN LOCAL ack_sending_list: ARRAY BLUE_ID of BOOLEAN LOCAL waiting_for_msg: ARRAY BLUE_ID of BOOLEAN %% For expiration check %%%%%%%%%%%%%%%%%%%%%%%%% LOCAL td_plus_e_expired: BOOLEAN %INPUT expired_tn_ts_list: TIME_DATA %% For synchronizing actions %%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Scheduling control INPUT LAST_action: ACTIONS INPUT LAST_sender_actor: PROCESS_ID INPUT LAST_receiver: PROCESS_ID %%% Auxiliary variables for value passing by action synchronization. INPUT receiving_msgs: ARRAY BLUE_ID OF MESSAGE OUTPUT sending_msg: MESSAGE OUTPUT sending_target: PROCESS_ID OUTPUT bcast_target: ARRAY PROCESS_ID OF BOOLEAN %%% Precondition (guard) of actions OUTPUT ENABLED_bcast_CONST: BOOLEAN OUTPUT ENABLED_bcast_CUSTOM: BOOLEAN OUTPUT ENABLED_send_ACK: BOOLEAN OUTPUT ENABLED_timeout: BOOLEAN %% For finding an available interaction instance or time nonce/stamp ID %%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT intr_inst_vec: INTERACT_INST_VECTOR INPUT to_vec: TO_VECTOR INPUT tv_vec: TV_VECTOR INPUT r2b_buff: R2B_BUFFERS INPUT r2b_bps: R2B_BPS INPUT b2r_buff: B2R_BUFFERS INPUT b2r_bps: B2R_BPS OUTPUT intr_insts: PROCESS_INTERACT_INSTS OUTPUT tvs: PROCESS_TIMED_VARS %% Errors asociation with unabailability of interaction instances and time nonce/stamp IDs OUTPUT ERROR_new_intr_inst_unavailable: BOOLEAN OUTPUT ERROR_new_time_nonce_unavailable: BOOLEAN OUTPUT ERROR_new_time_stamp_unavailable: BOOLEAN OUTPUT ERROR_timeout_update_inconsistent: BOOLEAN INITIALIZATION pc = crit_ready; %% pc is initialized to crit_ready for RED processes. timeout_time = unset_timeout; my_interact_inst = 0; ack_interact_inst = [[blue_id: BLUE_ID] 0]; proposing_time_nonce = bottom_time_data; ack_rcvd_list = [[blue_id: BLUE_ID] FALSE]; ack_sending_list = [[blue_id: BLUE_ID] FALSE]; waiting_for_msg = [[blue_id: BLUE_ID] TRUE]; %% td_plus_e_expired = FALSE; %% * %% sending_msg = broken_msg; %% * sending_target = FIRST_BLUE_ID; %% * %% ERROR_new_intr_inst_unavailable = FALSE; ERROR_new_time_nonce_unavailable = FALSE; ERROR_new_time_stamp_unavailable = FALSE; ERROR_timeout_update_inconsistent = FALSE; %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. DEFINITION %% Precondition of transitions ENABLED_bcast_CONST = (pc = crit_ready); ENABLED_bcast_CUSTOM = (pc = crit_ready); ENABLED_send_ACK = (pc = sending_ack); ENABLED_timeout = (timeout_time.is_set); %% Outputing interaction instances and time data stored in the state variables. intr_insts = [[ind: PROCESS_INTERACT_INST_INDEX] IF ind = 1 THEN my_interact_inst ELSIF is_BLUE(ind-1) THEN ack_interact_inst[ind-1] ELSE 0 ENDIF]; tvs = [[ind: PROCESS_TV_INDEX] proposing_time_nonce]; %% Just one timed variable is used in this case study. %% Target for broadcast is always same, and is all BLUE processes. bcast_target = [[i:PROCESS_ID] is_BLUE(i)]; TRANSITION [ bcast_CONST: LAST_action' = bcast_CONST AND LAST_sender_actor' = my_id --> pc' = crit; timeout_time' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN set_timeout_without_slack(ts2td(singleton_ts_set(new_time_stamp.ts_id))); %% Finding an error ERROR_new_time_stamp_unavailable' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_time_stamp.not_found; %% For action synchronization sending_msg' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (# td := ts2td(singleton_ts_set(new_time_stamp.ts_id)), msg_type := CONST, intr_inst := 0 #); [] bcast_CUSTOM: LAST_action' = bcast_CUSTOM AND LAST_sender_actor' = my_id --> pc' = waiting_for_ack; proposing_time_nonce' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN tn2td(singleton_tn_set(new_time_nonce.tn_id)); my_interact_inst' = LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_intr_inst; %% Finding errors ERROR_new_time_nonce_unavailable' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_time_nonce.not_found; ERROR_new_intr_inst_unavailable' = LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (new_intr_inst = 0); %% For action synchronization sending_msg' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (# td := tn2td(singleton_tn_set(new_time_nonce.tn_id)), msg_type := CUSTOM, intr_inst := new_intr_inst #); [] rcv_CONST: LAST_action' = rcv_CONST AND LAST_receiver' = my_id --> td_plus_e_expired' in IF exists_timeout_set_before(receiving_msgs[LAST_sender_actor'].td, to_vec) THEN {FALSE} ELSE {TRUE, FALSE} ENDIF; waiting_for_msg' = IF pc /= crit THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; proposing_time_nonce' = IF pc /= crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_rcvd_list' = IF pc /= crit THEN [[blue_id: BLUE_ID] FALSE] ELSE ack_rcvd_list ENDIF; pc' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN IF pc /= sending_ack THEN waiting_for_timeout ELSE pc ENDIF ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN update_timeout(timeout_time, set_timeout_with_slack(receiving_msgs[LAST_sender_actor'].td)) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF ELSE ERROR_timeout_update_inconsistent ENDIF; [] rcv_CUSTON: LAST_action' = rcv_CUSTOM AND LAST_receiver' = my_id --> %% if there exists a timeout that is without the slack and is less than the received value, %% then ts_u + e <= clock_i must be false. %% else choose. %% in this "choose" case, if (>) is true, put ts_u to the expired list. td_plus_e_expired' in IF exists_timeout_set_before(receiving_msgs[LAST_sender_actor'].td, to_vec) THEN {FALSE} ELSE {TRUE, FALSE} ENDIF; waiting_for_msg' = IF pc /= crit THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; proposing_time_nonce' = IF pc /= crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_rcvd_list' = IF pc /= crit THEN [[blue_id: BLUE_ID] FALSE] ELSE ack_rcvd_list ENDIF; pc' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN sending_ack ELSE pc ENDIF ELSE pc ENDIF; ack_interact_inst' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN ack_interact_inst WITH [LAST_sender_actor'] := receiving_msgs[LAST_sender_actor'].intr_inst ELSE ack_interact_inst ENDIF ELSE ack_interact_inst ENDIF; timeout_time' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN update_timeout(timeout_time, set_timeout_with_slack(receiving_msgs[LAST_sender_actor'].td)) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF ELSE ERROR_timeout_update_inconsistent ENDIF; ack_sending_list' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN ack_sending_list WITH [LAST_sender_actor'] := TRUE ELSE ack_sending_list ENDIF ELSE ack_sending_list ENDIF; [] rcv_BROKEN: LAST_action' = rcv_BROKEN AND LAST_receiver' = my_id --> ack_rcvd_list' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN [[blue_id: BLUE_ID] FALSE] ELSE ack_rcvd_list ENDIF; waiting_for_msg' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; pc' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN IF pc = idle THEN waiting_for_timeout ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN update_timeout_estimation_trick(timeout_time, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF; [] send_ACK: LAST_action' = send_ACK AND LAST_sender_actor' = my_id --> sending_target' in {j: BLUE_ID | ack_sending_list[j]}; sending_msg' = (# msg_type := ACK, td := bottom_time_data, intr_inst := ack_interact_inst[sending_target'] #); ack_sending_list' = ack_sending_list WITH [sending_target'] := FALSE; [] rcv_ACK: LAST_action' = rcv_ACK AND LAST_receiver' = my_id --> ack_rcvd_list' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN ack_rcvd_list WITH [LAST_sender_actor'] := TRUE ELSE ack_rcvd_list ENDIF; pc' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN IF (FORALL (j: BLUE_ID): ack_rcvd_list'[j] = TRUE) THEN crit ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN IF (FORALL (j: BLUE_ID): ack_rcvd_list'[j] = TRUE) THEN set_timeout_without_slack(proposing_time_nonce) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; [] timeout: LAST_action' = timeout AND LAST_sender_actor' = my_id --> timeout_time' = unset_timeout; pc' = IF pc = crit THEN idle ELSIF (pc = waiting_for_timeout OR pc = sending_ack) AND (FORALL (j: BLUE_ID): NOT waiting_for_msg[j]) THEN crit_ready ELSE pc ENDIF; waiting_for_msg' = IF pc = crit THEN [[blue_id: BLUE_ID] TRUE] ELSE waiting_for_msg ENDIF; ack_rcvd_list' = IF pc = crit THEN [[j: BLUE_ID] FALSE] ELSE ack_rcvd_list ENDIF; proposing_time_nonce' = IF pc = crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_sending_list' = IF (pc = waiting_for_timeout OR pc = sending_ack) AND (FORALL (j: BLUE_ID): NOT waiting_for_msg[j]) THEN [[j: BLUE_ID] FALSE] ELSE ack_sending_list ENDIF; [] ELSE --> ]; END; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% BLUE process %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BLUE_Process[my_id: PROCESS_ID]: MODULE = BEGIN OUTPUT pc: PROCESS_PROGRAM_COUNTER OUTPUT timeout_time: TIMEOUT_TIME LOCAL my_interact_inst: INTERACT_INST LOCAL ack_interact_inst: ARRAY RED_ID OF INTERACT_INST LOCAL proposing_time_nonce: TIME_DATA LOCAL ack_rcvd_list: ARRAY RED_ID of BOOLEAN LOCAL ack_sending_list: ARRAY RED_ID of BOOLEAN LOCAL waiting_for_msg: ARRAY RED_ID of BOOLEAN %% For expiration check %%%%%%%%%%%%%%%%%%%%%%%%% LOCAL td_plus_e_expired: BOOLEAN %% For synchronizing actions %%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Scheduling control INPUT LAST_action: ACTIONS INPUT LAST_sender_actor: PROCESS_ID INPUT LAST_receiver: PROCESS_ID %%% Auxiliary variables for value passing by action synchronization. INPUT receiving_msgs: ARRAY RED_ID OF MESSAGE OUTPUT sending_msg: MESSAGE OUTPUT sending_target: PROCESS_ID OUTPUT bcast_target: ARRAY PROCESS_ID OF BOOLEAN %%% Precondition (guard) of actions OUTPUT ENABLED_bcast_CONST: BOOLEAN OUTPUT ENABLED_bcast_CUSTOM: BOOLEAN OUTPUT ENABLED_send_ACK: BOOLEAN OUTPUT ENABLED_timeout: BOOLEAN %% For finding an available interaction instance or time nonce/stamp ID %%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT intr_inst_vec: INTERACT_INST_VECTOR INPUT to_vec: TO_VECTOR INPUT tv_vec: TV_VECTOR INPUT r2b_buff: R2B_BUFFERS INPUT r2b_bps: R2B_BPS INPUT b2r_buff: B2R_BUFFERS INPUT b2r_bps: B2R_BPS OUTPUT intr_insts: PROCESS_INTERACT_INSTS OUTPUT tvs: PROCESS_TIMED_VARS %% Errors asociation with unabailability of interaction instances and time nonce/stamp IDs OUTPUT ERROR_new_intr_inst_unavailable: BOOLEAN OUTPUT ERROR_new_time_nonce_unavailable: BOOLEAN OUTPUT ERROR_new_time_stamp_unavailable: BOOLEAN OUTPUT ERROR_timeout_update_inconsistent: BOOLEAN INITIALIZATION pc = idle; %% pc is initialized to idle for BLUE processes. timeout_time = unset_timeout; my_interact_inst = 0; ack_interact_inst = [[red_id: RED_ID] 0]; proposing_time_nonce = bottom_time_data; ack_rcvd_list = [[red_id: RED_ID] FALSE]; ack_sending_list = [[red_id: RED_ID] FALSE]; waiting_for_msg = [[red_id: RED_ID] TRUE]; %% td_plus_e_expired = FALSE; %% * %% sending_msg = broken_msg; %% * sending_target = FIRST_RED_ID; %% * %% ERROR_new_intr_inst_unavailable = FALSE; ERROR_new_time_nonce_unavailable = FALSE; ERROR_new_time_stamp_unavailable = FALSE; ERROR_timeout_update_inconsistent = FALSE; %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. DEFINITION %% Precondition of transitions ENABLED_bcast_CONST = (pc = crit_ready); ENABLED_bcast_CUSTOM = (pc = crit_ready); ENABLED_send_ACK = (pc = sending_ack); ENABLED_timeout = (timeout_time.is_set); %% Outputing interaction instances and time data stored in the state variables. intr_insts = [[ind: PROCESS_INTERACT_INST_INDEX] IF ind = 1 THEN my_interact_inst ELSIF is_RED(ind - 1) THEN %ind <= 1 + RED_SIZE THEN ack_interact_inst[ind - 1] ELSE 0 ENDIF]; tvs = [[ind: PROCESS_TV_INDEX] proposing_time_nonce]; %% Just one timed variable is used in this case study. %% Target for broadcast is always same, and is all RED processes. bcast_target = [[i:PROCESS_ID] is_RED(i)]; TRANSITION [ bcast_CONST: LAST_action' = bcast_CONST AND LAST_sender_actor' = my_id --> pc' = crit; timeout_time' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN set_timeout_without_slack(ts2td(singleton_ts_set(new_time_stamp.ts_id))); %% Finding an error ERROR_new_time_stamp_unavailable' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_time_stamp.not_found; %% For action synchronization sending_msg' = LET new_time_stamp: TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (# td := ts2td(singleton_ts_set(new_time_stamp.ts_id)), msg_type := CONST, intr_inst := 0 #); [] bcast_CUSTOM: LAST_action' = bcast_CUSTOM AND LAST_sender_actor' = my_id --> pc' = waiting_for_ack; proposing_time_nonce' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN tn2td(singleton_tn_set(new_time_nonce.tn_id)); my_interact_inst' = LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_intr_inst; %% Finding errors ERROR_new_time_nonce_unavailable' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN new_time_nonce.not_found; ERROR_new_intr_inst_unavailable' = LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (new_intr_inst = 0); %% For action synchronization sending_msg' = LET new_time_nonce: TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID(to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN LET new_intr_inst: INTERACT_INST = smallest_intr_inst(intr_inst_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) IN (# td := tn2td(singleton_tn_set(new_time_nonce.tn_id)), msg_type := CUSTOM, intr_inst := new_intr_inst #); [] rcv_CONST: LAST_action' = rcv_CONST AND LAST_receiver' = my_id --> td_plus_e_expired' in IF exists_timeout_set_before(receiving_msgs[LAST_sender_actor'].td, to_vec) THEN {FALSE} ELSE {TRUE, FALSE} ENDIF; waiting_for_msg' = IF pc /= crit THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; proposing_time_nonce' = IF pc /= crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_rcvd_list' = IF pc /= crit THEN [[red_id: RED_ID] FALSE] ELSE ack_rcvd_list ENDIF; pc' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN IF pc /= sending_ack THEN waiting_for_timeout ELSE pc ENDIF ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN update_timeout(timeout_time, set_timeout_with_slack(receiving_msgs[LAST_sender_actor'].td)) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF ELSE ERROR_timeout_update_inconsistent ENDIF; [] rcv_CUSTOM: LAST_action' = rcv_CUSTOM AND LAST_receiver' = my_id --> %% if there exists a timeout that is without the slack and is less than the received value, %% then ts_u + e <= clock_i must be false. %% else choose. %% in this "choose" case, if (>) is true, put ts_u to the expired list. td_plus_e_expired' in IF exists_timeout_set_before(receiving_msgs[LAST_sender_actor'].td, to_vec) THEN {FALSE} ELSE {TRUE, FALSE} ENDIF; waiting_for_msg' = IF pc /= crit THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; proposing_time_nonce' = IF pc /= crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_rcvd_list' = IF pc /= crit THEN [[red_id: RED_ID] FALSE] ELSE ack_rcvd_list ENDIF; pc' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN sending_ack ELSE pc ENDIF ELSE pc ENDIF; ack_interact_inst' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN ack_interact_inst WITH [LAST_sender_actor'] := receiving_msgs[LAST_sender_actor'].intr_inst ELSE ack_interact_inst ENDIF ELSE ack_interact_inst ENDIF; timeout_time' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN update_timeout(timeout_time, set_timeout_with_slack(receiving_msgs[LAST_sender_actor'].td)) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF ELSE ERROR_timeout_update_inconsistent ENDIF; ack_sending_list' = IF pc /= crit THEN IF NOT td_plus_e_expired THEN ack_sending_list WITH [LAST_sender_actor'] := TRUE ELSE ack_sending_list ENDIF ELSE ack_sending_list ENDIF; [] rcv_BROKEN: LAST_action' = rcv_BROKEN AND LAST_receiver' = my_id --> ack_rcvd_list' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN [[red_id: RED_ID] FALSE] ELSE ack_rcvd_list ENDIF; waiting_for_msg' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN waiting_for_msg WITH [LAST_sender_actor'] := FALSE ELSE waiting_for_msg ENDIF; pc' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN IF pc = idle THEN waiting_for_timeout ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN update_timeout_estimation_trick(timeout_time, to_vec, tv_vec, r2b_buff, r2b_bps, b2r_buff, b2r_bps) ELSE timeout_time ENDIF; ERROR_timeout_update_inconsistent' = IF (pc = idle OR pc = waiting_for_timeout OR pc = sending_ack) THEN (NOT timeout_time.slack_added AND NOT is_zero_td(timeout_time.td)) ELSE ERROR_timeout_update_inconsistent ENDIF; [] send_ACK: LAST_action' = send_ACK AND LAST_sender_actor' = my_id --> sending_target' in {j: RED_ID | ack_sending_list[j]}; sending_msg' = (# msg_type := ACK, td := bottom_time_data, intr_inst := ack_interact_inst[sending_target'] #); ack_sending_list' = ack_sending_list WITH [sending_target'] := FALSE; [] rcv_ACK: LAST_action' = rcv_ACK AND LAST_receiver' = my_id --> ack_rcvd_list' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN ack_rcvd_list WITH [LAST_sender_actor'] := TRUE ELSE ack_rcvd_list ENDIF; pc' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN IF (FORALL (j: RED_ID): ack_rcvd_list'[j] = TRUE) THEN crit ELSE pc ENDIF ELSE pc ENDIF; timeout_time' = IF pc = waiting_for_ack AND receiving_msgs[LAST_sender_actor'].intr_inst = my_interact_inst THEN IF (FORALL (j: RED_ID): ack_rcvd_list'[j] = TRUE) THEN set_timeout_without_slack(proposing_time_nonce) ELSE timeout_time ENDIF ELSE timeout_time ENDIF; [] timeout: LAST_action' = timeout AND LAST_sender_actor' = my_id --> timeout_time' = unset_timeout; pc' = IF pc = crit THEN idle ELSIF (pc = waiting_for_timeout OR pc = sending_ack) AND (FORALL (j: RED_ID): NOT waiting_for_msg[j]) THEN crit_ready ELSE pc ENDIF; waiting_for_msg' = IF pc = crit THEN [[red_id: RED_ID] TRUE] ELSE waiting_for_msg ENDIF; ack_rcvd_list' = IF pc = crit THEN [[j: RED_ID] FALSE] ELSE ack_rcvd_list ENDIF; proposing_time_nonce' = IF pc = crit THEN bottom_time_data ELSE proposing_time_nonce ENDIF; ack_sending_list' = IF (pc = waiting_for_timeout OR pc = sending_ack) AND (FORALL (j: RED_ID): NOT waiting_for_msg[j]) THEN [[j: RED_ID] FALSE] ELSE ack_sending_list ENDIF; [] ELSE --> ]; END; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Channel between processes %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Adding an message to the buffer. If the buffer is full, then the message is discarded. buffer_add(buffer: BUFFER, msg: MESSAGE, pointer: BUFFER_POINTER): BUFFER = IF pointer < BUFFER_SIZE THEN buffer WITH [pointer+1] := msg ELSE buffer ENDIF; buffer_remove(buffer: BUFFER): BUFFER = [[i: BUFFER_RANGE] IF i = BUFFER_SIZE THEN init_msg ELSE buffer[i+1] ENDIF]; %%% Channel module %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Channel[i, j: PROCESS_ID]: MODULE = BEGIN OUTPUT buffer: BUFFER OUTPUT pointer: BUFFER_POINTER %% Pointer for the smallest filled entry. Zero if the buffer is empty. OUTPUT head: MESSAGE %% Head entry of the buffer FIFO queue. %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT LAST_action: ACTIONS INPUT LAST_sender_actor: PROCESS_ID INPUT LAST_receiver: PROCESS_ID INPUT sending_msg: MESSAGE INPUT sending_target_vec: ARRAY PROCESS_ID OF PROCESS_ID INPUT bcast_target_vec: ARRAY PROCESS_ID OF ARRAY PROCESS_ID OF BOOLEAN % OUTPUT buffer_full: BOOLEAN %% Precondition (guard) of the channel's action OUTPUT ENABLED_rcv_CONST: BOOLEAN OUTPUT ENABLED_rcv_CUSTOM: BOOLEAN OUTPUT ENABLED_rcv_ACK: BOOLEAN OUTPUT ENABLED_rcv_BROKEN: BOOLEAN INITIALIZATION buffer = empty_buffer; pointer = 0; %% The buffer is empty DEFINITION head = buffer[1]; %% ENABLED_rcv_CONST = (pointer > 0 AND head.msg_type = CONST); ENABLED_rcv_CUSTOM = (pointer > 0 AND head.msg_type = CUSTOM); ENABLED_rcv_ACK = (pointer > 0 AND head.msg_type = ACK); ENABLED_rcv_BROKEN = (pointer > 0 AND head.msg_type = BROKEN); %% % buffer_full = (pointer = BUFFER_SIZE); TRANSITION [ Channel_bcast: (LAST_action' = bcast_CONST OR LAST_action' = bcast_CUSTOM) AND LAST_sender_actor' = i AND bcast_target_vec'[LAST_sender_actor'][j] --> buffer' in {buffer_add(buffer, sending_msg', pointer), buffer_add(buffer, broken_msg, pointer) }; %% Message containts may become broken non-deterministically. pointer' = IF pointer < BUFFER_SIZE THEN pointer + 1 ELSE pointer ENDIF; [] Channel_send: (LAST_action' = send_ACK) AND LAST_sender_actor' = i AND sending_target_vec'[LAST_sender_actor'] = j --> buffer' in {buffer_add(buffer, sending_msg', pointer), buffer_add(buffer, broken_msg, pointer) }; %% Message containts may become broken non-deterministically. pointer' = IF pointer < BUFFER_SIZE THEN pointer + 1 ELSE pointer ENDIF; [] Channel_rcv: (LAST_action' = rcv_CONST OR LAST_action' = rcv_CUSTOM OR LAST_action' = rcv_ACK OR LAST_action' = rcv_BROKEN) AND LAST_sender_actor' = i AND LAST_receiver' = j --> buffer' = buffer_remove(buffer); pointer' = pointer - 1; %% rcv transition is enabled only when the buffer is not empty. [] ELSE --> ]; END; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Scheduler %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Scheduler: MODULE = BEGIN OUTPUT LAST_action: ACTIONS OUTPUT LAST_sender_actor: PROCESS_ID OUTPUT LAST_receiver: PROCESS_ID %% Target(s) for send and broadcast. INPUT sending_target_vec: ARRAY PROCESS_ID OF PROCESS_ID INPUT bcast_target_vec: ARRAY PROCESS_ID OF ARRAY PROCESS_ID OF BOOLEAN %% Preconditions of actions INPUT ENABLED_bcast_CONST_: ARRAY PROCESS_ID OF BOOLEAN INPUT ENABLED_bcast_CUSTOM_: ARRAY PROCESS_ID OF BOOLEAN INPUT ENABLED_send_ACK_: ARRAY PROCESS_ID OF BOOLEAN INPUT ENABLED_rcv_CONST_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN INPUT ENABLED_rcv_CONST_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN INPUT ENABLED_rcv_CUSTOM_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN INPUT ENABLED_rcv_CUSTOM_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN INPUT ENABLED_rcv_BROKEN_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN INPUT ENABLED_rcv_BROKEN_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN INPUT ENABLED_rcv_ACK_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN INPUT ENABLED_rcv_ACK_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN INPUT ENABLED_timeout_: ARRAY PROCESS_ID OF BOOLEAN %% to_vec_out is once input to the scheduler and output as to_vec %% similar for intr_inst_vec and tv_vec. INPUT to_vec_out: TO_VECTOR INPUT tv_vec_out: TV_VECTOR INPUT intr_inst_vec_out: INTERACT_INST_VECTOR OUTPUT to_vec: TO_VECTOR OUTPUT tv_vec: TV_VECTOR OUTPUT intr_inst_vec: INTERACT_INST_VECTOR DEFINITION to_vec = to_vec_out; tv_vec = tv_vec_out; intr_inst_vec = intr_inst_vec_out; INITIALIZATION LAST_action = bcast_CONST; % * LAST_sender_actor = FIRST_RED_ID; % * LAST_receiver = FIRST_BLUE_ID; % * %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. TRANSITION [ Schedule_bcast_CONST: EXISTS (i: PROCESS_ID): ENABLED_bcast_CONST_[i] --> LAST_action' = bcast_CONST; LAST_sender_actor' in {i: PROCESS_ID| ENABLED_bcast_CONST_[i]}; [] Schedule_bcast_CUSTOM: EXISTS (i: PROCESS_ID): ENABLED_bcast_CUSTOM_[i] --> LAST_action' = bcast_CUSTOM; LAST_sender_actor' in {i: PROCESS_ID| ENABLED_bcast_CUSTOM_[i]}; [] Schedule_send_ACK: EXISTS (i: PROCESS_ID): ENABLED_send_ACK_[i] --> LAST_action' = send_ACK; LAST_sender_actor' in {i: PROCESS_ID| ENABLED_send_ACK_[i]}; LAST_receiver' = sending_target_vec'[LAST_sender_actor']; [] Schedule_rcv_CONST_RED2BLUE: EXISTS (red_id: RED_ID, blue_id: BLUE_ID): ENABLED_rcv_CONST_RED2BLUE[red_id][blue_id] --> LAST_action' = rcv_CONST; LAST_sender_actor' in {i: RED_ID| EXISTS (j: BLUE_ID): ENABLED_rcv_CONST_RED2BLUE[i][j]}; LAST_receiver' in {j: BLUE_ID| ENABLED_rcv_CONST_RED2BLUE[LAST_sender_actor'][j]}; [] Schedule_rcv_CONST_BLUE2RED: EXISTS (blue_id: BLUE_ID, red_id: RED_ID): ENABLED_rcv_CONST_BLUE2RED[blue_id][red_id] --> LAST_action' = rcv_CONST; LAST_sender_actor' in {i: BLUE_ID| EXISTS (j: RED_ID): ENABLED_rcv_CONST_BLUE2RED[i][j]}; LAST_receiver' in {j: RED_ID| ENABLED_rcv_CONST_BLUE2RED[LAST_sender_actor'][j]}; [] Schedule_rcv_CUSTOM_RED2BLUE: EXISTS (red_id: RED_ID, blue_id: BLUE_ID): ENABLED_rcv_CUSTOM_RED2BLUE[red_id][blue_id] --> LAST_action' = rcv_CUSTOM; LAST_sender_actor' in {i: RED_ID| EXISTS (j: BLUE_ID): ENABLED_rcv_CUSTOM_RED2BLUE[i][j]}; LAST_receiver' in {j: BLUE_ID| ENABLED_rcv_CUSTOM_RED2BLUE[LAST_sender_actor'][j]}; [] Schedule_rcv_CUSTOM_BLUE2RED: EXISTS (blue_id: BLUE_ID, red_id: RED_ID): ENABLED_rcv_CUSTOM_BLUE2RED[blue_id][red_id] --> LAST_action' = rcv_CUSTOM; LAST_sender_actor' in {i: BLUE_ID| EXISTS (j: RED_ID): ENABLED_rcv_CUSTOM_BLUE2RED[i][j]}; LAST_receiver' in {j: RED_ID| ENABLED_rcv_CUSTOM_BLUE2RED[LAST_sender_actor'][j]}; [] Schedule_rcv_BROKEN_RED2BLUE: EXISTS (red_id: RED_ID, blue_id: BLUE_ID): ENABLED_rcv_BROKEN_RED2BLUE[red_id][blue_id] --> LAST_action' = rcv_BROKEN; LAST_sender_actor' in {i: RED_ID| EXISTS (j: BLUE_ID): ENABLED_rcv_BROKEN_RED2BLUE[i][j]}; LAST_receiver' in {j: BLUE_ID| ENABLED_rcv_BROKEN_RED2BLUE[LAST_sender_actor'][j]}; [] Schedule_rcv_BROKEN_BLUE2RED: EXISTS (blue_id: BLUE_ID, red_id: RED_ID): ENABLED_rcv_BROKEN_BLUE2RED[blue_id][red_id] --> LAST_action' = rcv_BROKEN; LAST_sender_actor' in {i: BLUE_ID| EXISTS (j: RED_ID): ENABLED_rcv_BROKEN_BLUE2RED[i][j]}; LAST_receiver' in {j: RED_ID| ENABLED_rcv_BROKEN_BLUE2RED[LAST_sender_actor'][j]}; [] Schedule_rcv_ACK_RED2BLUE: EXISTS (red_id: RED_ID, blue_id: BLUE_ID): ENABLED_rcv_ACK_RED2BLUE[red_id][blue_id] --> LAST_action' = rcv_ACK; LAST_sender_actor' in {i: RED_ID| EXISTS (j: BLUE_ID): ENABLED_rcv_ACK_RED2BLUE[i][j]}; LAST_receiver' in {j: BLUE_ID| ENABLED_rcv_ACK_RED2BLUE[LAST_sender_actor'][j]}; [] Schedule_rcv_ACK_BLUE2RED: EXISTS (blue_id: BLUE_ID, red_id: RED_ID): ENABLED_rcv_ACK_BLUE2RED[blue_id][red_id] --> LAST_action' = rcv_ACK; LAST_sender_actor' in {i: BLUE_ID| EXISTS (j: RED_ID): ENABLED_rcv_ACK_BLUE2RED[i][j]}; LAST_receiver' in {j: RED_ID| ENABLED_rcv_ACK_BLUE2RED[LAST_sender_actor'][j]}; [] Schedule_timeout: EXISTS (i: PROCESS_ID): ENABLED_timeout_[i] AND (to_vec[i].slack_added => NOT exists_timeout_set_before(to_vec[i].td, to_vec)) --> LAST_action' = timeout; LAST_sender_actor' in {i: PROCESS_ID| ENABLED_timeout_[i] AND (to_vec[i].slack_added => NOT exists_timeout_set_before(to_vec[i].td, to_vec))}; [] ELSE --> ]; END; %%% --------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Composed System %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% --------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Composition of RED and BLUE processes Processes: MODULE = WITH OUTPUT proc_pc: ARRAY PROCESS_ID OF PROCESS_PROGRAM_COUNTER WITH OUTPUT to_vec_out: ARRAY PROCESS_ID OF TIMEOUT_TIME WITH OUTPUT tv_vec_out: ARRAY PROCESS_ID OF PROCESS_TIMED_VARS WITH OUTPUT intr_inst_vec_out: ARRAY PROCESS_ID OF PROCESS_INTERACT_INSTS WITH OUTPUT sending_msg_vec: ARRAY PROCESS_ID OF MESSAGE WITH OUTPUT sending_target_vec: ARRAY PROCESS_ID OF PROCESS_ID WITH OUTPUT bcast_target_vec: ARRAY PROCESS_ID OF ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ENABLED_bcast_CONST_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ENABLED_bcast_CUSTOM_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ENABLED_send_ACK_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ENABLED_timeout_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ERROR_new_intr_inst_unavailable_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ERROR_new_time_nonce_unavailable_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ERROR_new_time_stamp_unavailable_: ARRAY PROCESS_ID OF BOOLEAN WITH OUTPUT ERROR_timeout_update_inconsistent_: ARRAY PROCESS_ID OF BOOLEAN WITH INPUT receiving_msgs_RED: ARRAY RED_ID OF ARRAY BLUE_ID OF MESSAGE WITH INPUT receiving_msgs_BLUE: ARRAY BLUE_ID OF ARRAY RED_ID OF MESSAGE (|| (i: RED_ID): RENAME pc TO proc_pc[i] IN RENAME timeout_time TO to_vec_out[i] IN RENAME tvs TO tv_vec_out[i] IN RENAME intr_insts TO intr_inst_vec_out[i] IN RENAME sending_msg TO sending_msg_vec[i] IN RENAME sending_target TO sending_target_vec[i] IN RENAME bcast_target TO bcast_target_vec[i] IN RENAME ENABLED_bcast_CONST TO ENABLED_bcast_CONST_[i] IN RENAME ENABLED_bcast_CUSTOM TO ENABLED_bcast_CUSTOM_[i] IN RENAME ENABLED_send_ACK TO ENABLED_send_ACK_[i] IN RENAME ENABLED_timeout TO ENABLED_timeout_[i] IN RENAME ERROR_new_intr_inst_unavailable TO ERROR_new_intr_inst_unavailable_[i] IN RENAME ERROR_new_time_nonce_unavailable TO ERROR_new_time_nonce_unavailable_[i] IN RENAME ERROR_new_time_stamp_unavailable TO ERROR_new_time_stamp_unavailable_[i] IN RENAME ERROR_timeout_update_inconsistent TO ERROR_timeout_update_inconsistent_[i] IN RENAME receiving_msgs TO receiving_msgs_RED[i] IN RED_Process[i]) || (|| (i: BLUE_ID): RENAME pc TO proc_pc[i] IN RENAME timeout_time TO to_vec_out[i] IN RENAME tvs TO tv_vec_out[i] IN RENAME intr_insts TO intr_inst_vec_out[i] IN RENAME sending_msg TO sending_msg_vec[i] IN RENAME sending_target TO sending_target_vec[i] IN RENAME bcast_target TO bcast_target_vec[i] IN RENAME ENABLED_bcast_CONST TO ENABLED_bcast_CONST_[i] IN RENAME ENABLED_bcast_CUSTOM TO ENABLED_bcast_CUSTOM_[i] IN RENAME ENABLED_send_ACK TO ENABLED_send_ACK_[i] IN RENAME ENABLED_timeout TO ENABLED_timeout_[i] IN RENAME ERROR_new_intr_inst_unavailable TO ERROR_new_intr_inst_unavailable_[i] IN RENAME ERROR_new_time_nonce_unavailable TO ERROR_new_time_nonce_unavailable_[i] IN RENAME ERROR_new_time_stamp_unavailable TO ERROR_new_time_stamp_unavailable_[i] IN RENAME ERROR_timeout_update_inconsistent TO ERROR_timeout_update_inconsistent_[i] IN RENAME receiving_msgs TO receiving_msgs_BLUE[i] IN BLUE_Process[i]); %% Composition of Channels RED_BLUE: TYPE = [# red_id: RED_ID, blue_id: BLUE_ID #]; RED2BLUE_Channels: MODULE = WITH OUTPUT r2b_buff: R2B_BUFFERS WITH OUTPUT r2b_bps: R2B_BPS WITH OUTPUT receiving_msgs_BLUE: ARRAY BLUE_ID OF ARRAY RED_ID OF MESSAGE WITH OUTPUT ENABLED_rcv_CONST_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_CUSTOM_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_BROKEN_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_ACK_RED2BLUE: ARRAY RED_ID OF ARRAY BLUE_ID OF BOOLEAN WITH INPUT sending_msg_vec: ARRAY PROCESS_ID OF MESSAGE (|| (rb: RED_BLUE): RENAME buffer TO r2b_buff[rb.red_id][rb.blue_id] IN RENAME pointer TO r2b_bps[rb.red_id][rb.blue_id] IN RENAME head TO receiving_msgs_BLUE[rb.blue_id][rb.red_id] IN RENAME ENABLED_rcv_CONST TO ENABLED_rcv_CONST_RED2BLUE[rb.red_id][rb.blue_id] IN RENAME ENABLED_rcv_CUSTOM TO ENABLED_rcv_CUSTOM_RED2BLUE[rb.red_id][rb.blue_id] IN RENAME ENABLED_rcv_BROKEN TO ENABLED_rcv_BROKEN_RED2BLUE[rb.red_id][rb.blue_id] IN RENAME ENABLED_rcv_ACK TO ENABLED_rcv_ACK_RED2BLUE[rb.red_id][rb.blue_id] IN RENAME sending_msg TO sending_msg_vec[rb.red_id] IN Channel[rb.red_id, rb.blue_id]); BLUE2RED_Channels: MODULE = WITH OUTPUT b2r_buff: B2R_BUFFERS WITH OUTPUT b2r_bps: B2R_BPS WITH OUTPUT receiving_msgs_RED: ARRAY RED_ID OF ARRAY BLUE_ID OF MESSAGE WITH OUTPUT ENABLED_rcv_CONST_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_CUSTOM_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_BROKEN_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN WITH OUTPUT ENABLED_rcv_ACK_BLUE2RED: ARRAY BLUE_ID OF ARRAY RED_ID OF BOOLEAN WITH INPUT sending_msg_vec: ARRAY PROCESS_ID OF MESSAGE (|| (rb: RED_BLUE): RENAME buffer TO b2r_buff[rb.blue_id][rb.red_id] IN RENAME pointer TO b2r_bps[rb.blue_id][rb.red_id] IN RENAME head TO receiving_msgs_RED[rb.red_id][rb.blue_id] IN RENAME ENABLED_rcv_CONST TO ENABLED_rcv_CONST_BLUE2RED[rb.blue_id][rb.red_id] IN RENAME ENABLED_rcv_CUSTOM TO ENABLED_rcv_CUSTOM_BLUE2RED[rb.blue_id][rb.red_id] IN RENAME ENABLED_rcv_BROKEN TO ENABLED_rcv_BROKEN_BLUE2RED[rb.blue_id][rb.red_id] IN RENAME ENABLED_rcv_ACK TO ENABLED_rcv_ACK_BLUE2RED[rb.blue_id][rb.red_id] IN RENAME sending_msg TO sending_msg_vec[rb.blue_id] IN Channel[rb.blue_id, rb.red_id]); ComposedSystem: MODULE = Processes || RED2BLUE_Channels || BLUE2RED_Channels || Scheduler; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Property to be verified %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% mutual_exclusion_and_correct_time_data_intr_inst_timeout_update: THEOREM ComposedSystem |- G((FORALL (red_id: RED_ID, blue_id: BLUE_ID): NOT (proc_pc[red_id] = crit AND proc_pc[blue_id] = crit)) AND (FORALL (id: PROCESS_ID): NOT ERROR_new_intr_inst_unavailable_[id] AND NOT ERROR_new_time_nonce_unavailable_[id] AND NOT ERROR_new_time_stamp_unavailable_[id] AND NOT ERROR_timeout_update_inconsistent_[id])); END