-- 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. 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 siz 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); b: (B_mem); c: (C_mem); -- The next predicates simply specify whether the active conference -- is 1 or 2 c1: (A_conf=1); c2: (A_conf=2); 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_to_A_1_PDU, join_B_to_A_2_PDU, join_C_to_A_1_PDU, join_C_to_A_2_PDU, answer_B_to_A_1_PDU, answer_B_to_A_2_PDU, answer_C_to_A_1_PDU, answer_C_to_A_2_PDU, data_B_to_A_PDU, data_C_to_A_PDU, leave_B_to_A_1_PDU, leave_B_to_A_2_PDU, leave_C_to_A_1_PDU, leave_C_to_A_2_PDU @ U_SAP_A; OUTPUTS dataind @ C_SAP_A; join_A_to_BC_1_PDU, join_A_to_BC_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_PDU, leave_A_to_C_PDU, leave_A_to_BC_PDU, data_A_to_B_PDU, data_A_to_C_PDU, data_A_to_BC_PDU @ U_SAP_A; CODES avoid, -- always avoid avoid_sync, -- avoid in sync. sequence avoid_ts, -- avoid in ts. sequence avoid_main, -- avoid in transition to be checked avoid_check; -- avoid in SIOS TRANSITIONS -- Pred. Input Output Action State Code STATE Idle; -- user A is not participating an any conference - join_A_1 join_A_to_BC_1_PDU (A_conf := 1) Connected; - join_A_2 join_A_to_BC_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_to_A_1_PDU - (B_mem:=TRUE) -; (A_conf=1) answer_C_to_A_1_PDU - (C_mem:=TRUE) -; (A_conf=1) join_B_to_A_1_PDU answer_A_to_B_1_PDU (B_mem:=TRUE) -; (A_conf=1) join_C_to_A_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_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c1notbc leave leave_A_to_C_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c1bc leave leave_A_to_BC_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_to_A_2_PDU - (B_mem:=TRUE) -; (A_conf=2) answer_C_to_A_2_PDU - (C_mem:=TRUE) -; (A_conf=2) join_B_to_A_2_PDU answer_A_to_B_2_PDU (B_mem:=TRUE) -; (A_conf=2) join_C_to_A_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_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c2notbc leave leave_A_to_C_PDU (A_conf:=0; B_mem:=FALSE; C_mem:=FALSE) Idle; c2bc leave leave_A_to_BC_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_A_to_B_PDU - -; notbc datareq data_A_to_C_PDU - -; bc datareq data_A_to_BC_PDU - -; b data_B_to_A_PDU dataind - -; c data_C_to_A_PDU dataind - -; c1 leave_B_to_A_1_PDU - (B_mem:=FALSE) -; c2 leave_B_to_A_2_PDU - (B_mem:=FALSE) -; c1 leave_C_to_A_1_PDU - (C_mem:=FALSE) -; c2 leave_C_to_A_2_PDU - (C_mem:=FALSE) -; END STATE *; -- all other transitions, avoid testing them - * - - - avoid_main; END