-- An EFSM specification (Kit format) of the conference protocol -- as described in the paper: -- Testing Theory in Practice: A simple Experiment -- -- In this specification, the CPE is specified that is used by one user, -- named A, which can participate in two conferences, named 1 and 2. -- Furthermore, the existance of two other remote users, named B and C, -- is modeled. -- In this specification the implicite presence of a party (B or C) -- is assumed if a dataPDU is received without having received a (lost) -- answerPDU. EFSM conference_protocol; VARIABLES A_conf: 0..2; -- A's active conference, 0 means not active B_mem: BOOL; -- B is member of A's active conference C_mem: BOOL; -- C is member of A's active conference PREDICATES -- The predicates are introduced for notational convenience. -- The first eight predicate names indicate A's active conference -- followed by a specification of B resp. C's presence in that same -- conference. c1notbnotc: (A_conf=1) AND (NOT B_mem) AND (NOT C_mem); c1bnotc: (A_conf=1) AND (B_mem) AND (NOT C_mem); c1notbc: (A_conf=1) AND (NOT B_mem) AND (C_mem); c1bc: (A_conf=1) AND (B_mem) AND (C_mem); c2notbnotc: (A_conf=2) AND (NOT B_mem) AND (NOT C_mem); c2bnotc: (A_conf=2) AND (B_mem) AND (NOT C_mem); c2notbc: (A_conf=2) AND (NOT B_mem) AND (C_mem); c2bc: (A_conf=2) AND (B_mem) AND (C_mem); -- The following four predicates simply specify whether B and C -- participation in the same conference as A or not. notbnotc: (NOT B_mem) AND (NOT C_mem); bnotc: (B_mem) AND (NOT C_mem); notbc: (NOT B_mem) AND (C_mem); bc: (B_mem) AND (C_mem); START Idle: (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE); GATES C_SAP_A, U_SAP_A; INPUTS join_A_1, join_A_2, datareq, leave @ C_SAP_A; join_B_1_PDU, join_B_2_PDU, join_C_1_PDU, join_C_2_PDU, answer_B_1_PDU, answer_B_2_PDU, answer_C_1_PDU, answer_C_2_PDU, data_PDU_from_B, data_PDU_from_C, leave_B_PDU, leave_C_PDU, leave_BC_PDU @ U_SAP_A; OUTPUTS dataind_from_B, dataind_from_C @ C_SAP_A; join_A_1_PDU, join_A_2_PDU, answer_A_to_B_1_PDU, answer_A_to_B_2_PDU, answer_A_to_C_1_PDU, answer_A_to_C_2_PDU, leave_A_to_B_1_PDU, leave_A_to_B_2_PDU, leave_A_to_C_1_PDU, leave_A_to_C_2_PDU, leave_A_to_BC_1_PDU, leave_A_to_BC_2_PDU, data_to_B_PDU, data_to_C_PDU, data_to_BC_PDU @ U_SAP_A; CODES code; -- a code TRANSITIONS -- Pred. Input Output Action State Code STATE Idle; -- user A is not participating an any conference - join_A_1 join_A_1_PDU (A_conf := 1) Connected; - join_A_2 join_A_2_PDU (A_conf := 2) Connected; END STATE Connected; -- user A is participating in a conference -- Transitions that are possible when A participates in conference 1 (A_conf=1) answer_B_1_PDU - (B_mem:=TRUE) -; (A_conf=1) answer_C_1_PDU - (C_mem:=TRUE) -; (A_conf=1) join_B_1_PDU answer_A_to_B_1_PDU (B_mem:=TRUE) -; (A_conf=1) join_C_1_PDU answer_A_to_C_1_PDU (C_mem:=TRUE) -; c1notbnotc leave - (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c1bnotc leave leave_A_to_B_1_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c1notbc leave leave_A_to_C_1_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c1bc leave leave_A_to_BC_1_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; -- Transitions that are possible when A participates in conference 2 (A_conf=2) answer_B_2_PDU - (B_mem:=TRUE) -; (A_conf=2) answer_C_2_PDU - (C_mem:=TRUE) -; (A_conf=2) join_B_2_PDU answer_A_to_B_2_PDU (B_mem:=TRUE) -; (A_conf=2) join_C_2_PDU answer_A_to_C_2_PDU (C_mem:=TRUE) -; c2notbnotc leave - (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c2bnotc leave leave_A_to_B_2_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c2notbc leave leave_A_to_C_2_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c2bc leave leave_A_to_BC_2_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; -- Transitions that are independent of A's active conference notbnotc datareq - - -; bnotc datareq data_to_B_PDU - -; notbc datareq data_to_C_PDU - -; bc datareq data_to_BC_PDU - -; c1bnotc data_PDU_from_B dataind_from_B (B_mem:=TRUE) -; c1bc data_PDU_from_B dataind_from_B (B_mem:=TRUE) -; c2bnotc data_PDU_from_B dataind_from_B (B_mem:=TRUE) -; c2bc data_PDU_from_B dataind_from_B (B_mem:=TRUE) -; c1notbc data_PDU_from_B join_A_to_B_1_PDU - -; c1notbnotc data_PDU_from_B join_A_to_B_1_PDU - -; c2notbc data_PDU_from_B join_A_to_B_2_PDU - -; c2notbnotc data_PDU_from_B join_A_to_B_2_PDU - -; - data_PDU_from_C dataind_from_C (C_mem:=TRUE) -; - leave_B_PDU - (B_mem:=FALSE) -; - leave_C_PDU - (C_mem:=FALSE) -; END STATE *; -- all other transitions - * - - -; END