module Test {
	import from GSM_Types all;
	import from Osmocom_Types all;
	import from GSM_SystemInformation all;
	import from GSMTAP_Types all;
	import from GSMTAP_PortType all;
	import from IPL4_GSMTAP_CtrlFunct all;
	import from TELNETasp_PortType all;

	const octetstring si1 := '5506198fb38000000000000000000000000000e504002b'O;
	const octetstring si2 := '59061a00000000000000000000000000000000ffe50400'O;
	const octetstring si3 := '49061b000062f22404d2490301275d40e50400392b2b2b'O;
	const octetstring si4 := '31061c62f22404d25d40e504002b2b2b2b2b2b2b2b2b2b'O;
	const octetstring c_si2bis := '550602bfe809b3ff00000000000000000000007900002b'O;
	const octetstring c_si2ter := '010603bf66b0aa0a00000002000000000000002b2b2b2b'O;
	const octetstring c_si2quater := '050607a8a0364aa698d72ff424feee0506d5e7fff02043'O;

	type component dummy_CT {
		port GSMTAP_PT GSMTAP;
		port TELNETasp_PT BSCVTY;
		var boolean initialized := false;
		var SystemInformationConfig si_cfg := {
			bcch_extended := false,
			si1_present := true,
			si2bis_present := false,
			si2ter_present := false,
			si2quater_present := false,
			si7_present := false,
			si8_present := false,
			si9_present := false,
			si13_present := false,
			si13alt_present := false,
			si15_present := false,
			si16_present := false,
			si17_present := false,
			si2n_present := false,
			si21_present := false,
			si22_present := false
		};
	};

	testcase TC_si1() runs on dummy_CT {
		log("SI: ", dec_SystemInformation(si1));
		log("SI: ", dec_SystemInformation(si2));
		log("SI: ", dec_SystemInformation(si3));
		log("SI: ", dec_SystemInformation(si4));
		setverdict(pass);
	}

	template GsmtapHeader t_GsmtapHeader := {
		version := GSMTAP_VERSION,
		hdr_len := 4,
		msg_type := ?,
		timeslot := ?,
		arfcn := ?,
		signal_dbm := ?,
		snr_db := ?,
		frame_number := ?,
		sub_type := ?,
		antenna_nr := ?,
		sub_slot := ?,
		res := ?
	}

	template GsmtapHeader t_GsmtapHeaderUm(template GsmtapChannel ch) modifies t_GsmtapHeader := {
		msg_type := GSMTAP_TYPE_UM,
		sub_type := ch
	}

	template GsmtapMessage t_bcch := {
		header := t_GsmtapHeaderUm(GSMTAP_CHANNEL_BCCH),
		payload := ?
	}

	template GSMTAP_RecvFrom t_recvfrom(template GsmtapChannel ch) := {
		connId := ?,
		remName := ?,
		remPort := ?,
		locName := ?,
		locPort := GSMTAP_PORT,
		proto := {udp:={}},
		userData := ?,
		msg := { header := t_GsmtapHeaderUm(ch), payload := ?}
	}

	/* tuple of gsmtap header + decoded SI */
	type record SystemInformationGsmtap {
		GsmtapHeader gsmtap,
		SystemInformation si
	}

	/* an arbitrary-length vector of decoded SI + gsmtap header */
	type record of SystemInformationGsmtap SystemInformationVector;

	/* an array of SI-vectors indexed by TC value */
	type SystemInformationVector SystemInformationVectorPerTc[8];

	type record of integer IntegerRecord;

	function int2bool(integer int) return boolean {
		if (int != 0) {
			return true;
		} else {
			return false;
		}
	}

	function f_array_contains(IntegerRecord arr, integer key) return boolean {
		for (var integer i:= 0; i< sizeof(arr); i := i + 1) {
			if (arr[i] == key) {
				return true;
			}
		}
		return false;
	}


	/* compute TC as per 45.002 6.3.1.3 */
	function f_gsm_compute_tc(integer fn) return integer {
		return (fn / 51) mod 8;
	}

	/* determine if a given SI vector contains given SI type at least once */
	function f_si_vecslot_contains(SystemInformationVector arr, RrMessageType key, boolean bcch_ext := false) return boolean {
		for (var integer i:= 0; i< sizeof(arr); i := i + 1) {
			var integer fn_mod51 := arr[i].gsmtap.frame_number mod 51;
			if (not bcch_ext and fn_mod51 == 2 or
			        bcch_ext and fn_mod51 == 6) {
				if (arr[i].si.header.message_type == key) {
					return true;
				}
			}
		}
		return false;
	}

	/* ensure a given TC slot of the SI vector contains given SI type at least once at TC */
	function f_ensure_si_vec_contains(SystemInformationVectorPerTc arr, integer tc, RrMessageType key, boolean ext_bcch := false) {
		if (not f_si_vecslot_contains(arr[tc], key, ext_bcch)) {
			log("Fail: No ", key, " in TC=", tc, "!");
			setverdict(fail);
		}
	}

	/* check if a given SI vector contains given SI type at least once on any TC */
	function f_si_vec_contains(SystemInformationVectorPerTc arr, RrMessageType key) return boolean {
		for (var integer tc:= 0; tc < sizeof(arr); tc := tc + 1) {
			if (f_si_vecslot_contains(arr[tc], key) or
			    f_si_vecslot_contains(arr[tc], key, true)) {
				return true;
			}
		}
		return false;
	}

	/* determine if a given SI vector contains given SI type at least N of M times */
	function f_si_vecslot_contains_n_of_m(SystemInformationVector arr, RrMessageType key, boolean bcch_ext := false, integer n := 1, integer m := 4) return boolean {
		var integer count := 0;
		if (sizeof(arr) < m) {
			testcase.stop("Error: Insufficient SI in array");
		}
		for (var integer i:= 0; i < m; i := i + 1) {
			var integer fn_mod51 := arr[i].gsmtap.frame_number mod 51;
			if (not bcch_ext and fn_mod51 == 2 or
			        bcch_ext and fn_mod51 == 6) {
				if (arr[i].si.header.message_type == key) {
					count := count + 1;
				}
			}
		}
		if (count >= n) {
			return true;
		} else {
			return false;
		}
	}

	/* ensure a given TC slot of the SI vector contains given SI type at least N out of M times at TC */
	function f_ensure_si_vec_contains_n_of_m(SystemInformationVectorPerTc arr, integer tc, RrMessageType key, boolean ext_bcch := false, integer n, integer m) {
		if (not f_si_vecslot_contains_n_of_m(arr[tc], key, ext_bcch, n, m)) {
			log("Fail: Not ", n, "/", m, " of ", key, " in TC=", tc, "!");
			setverdict(fail);
		}
	}

	/* determine if a given SI vector contains given SI type at least once */
	function f_si_vecslot_contains_only(SystemInformationVector arr, RrMessageType key, boolean bcch_ext := false) return boolean {
		for (var integer i:= 0; i< sizeof(arr); i := i + 1) {
			var integer fn_mod51 := arr[i].gsmtap.frame_number mod 51;
			if (not bcch_ext and fn_mod51 == 2 or
			        bcch_ext and fn_mod51 == 6) {
				if (arr[i].si.header.message_type != key) {
					return false;
				}
			}
		}
		return true;
	}

	/* ensure a given TC slot of the SI vector contains only given SI type */
	function f_ensure_si_vec_contains_only(SystemInformationVectorPerTc arr, integer tc, RrMessageType key, boolean ext_bcch := false) {
		if (not f_si_vecslot_contains_only(arr[tc], key, ext_bcch)) {
			log("Fail: Not all ", key, " in TC=", tc, "!");
			setverdict(fail);
		}
	}

	/* SI configuration of cell, against which we validate actual SI messages */
	type set SystemInformationConfig {
		boolean bcch_extended,
		boolean si1_present,
		boolean si2bis_present,
		boolean si2ter_present,
		boolean si2quater_present,
		boolean si7_present,
		boolean si8_present,
		boolean si9_present,
		boolean si13_present,
		boolean si13alt_present,
		boolean si15_present,
		boolean si16_present,
		boolean si17_present,
		boolean si2n_present,
		boolean si21_present,
		boolean si22_present
	}

	/* validate the SI scheduling according to TS 45.002 version 14.1.0 Release 14, Section 6.3.1.3 */
	function f_validate_si_scheduling(SystemInformationConfig cfg, SystemInformationVectorPerTc si_per_tc) {
		var integer i;
		for (i := 0; i < sizeof(si_per_tc); i := i + 1) {
			if (sizeof(si_per_tc[i]) == 0) {
				setverdict(fail, "No SI messages for TC=0!");
			}
		}
		if (cfg.si1_present) {
			/* ii) System Information Type 1 needs to be sent if frequency hopping is in use or
			 * when the NCH is present in a cell. If the MS finds another message on BCCH Norm
			 * when TC = 0, it can assume that System Information Type 1 is not in use. */
			f_ensure_si_vec_contains(si_per_tc, 0, SYSTEM_INFORMATION_TYPE_1);
			/* make sure *ALL* contain SI1 */
			f_ensure_si_vec_contains_only(si_per_tc, 0, SYSTEM_INFORMATION_TYPE_1);
		}
		f_ensure_si_vec_contains(si_per_tc, 1, SYSTEM_INFORMATION_TYPE_2);
		/* iii) A SI 2 message will be sent at least every time TC = 1 */
		f_ensure_si_vec_contains(si_per_tc, 2, SYSTEM_INFORMATION_TYPE_3);
		f_ensure_si_vec_contains(si_per_tc, 6, SYSTEM_INFORMATION_TYPE_3);
		f_ensure_si_vec_contains(si_per_tc, 3, SYSTEM_INFORMATION_TYPE_4);
		f_ensure_si_vec_contains(si_per_tc, 7, SYSTEM_INFORMATION_TYPE_4);

		/*  iii) System information type 2 bis or 2 ter messages are sent if needed, as determined by the
		 *  system operator. If only one of them is needed, it is sent when TC = 5. If both are
		 *  needed, 2bis is sent when TC = 5 and 2ter is sent at least once within any of 4
		 *  consecutive occurrences of TC = 4. */
		if (cfg.si2bis_present and not cfg.si2ter_present) {
			f_ensure_si_vec_contains(si_per_tc, 5, SYSTEM_INFORMATION_TYPE_2bis);
		} else if (cfg.si2ter_present and not cfg.si2bis_present) {
			f_ensure_si_vec_contains(si_per_tc, 5, SYSTEM_INFORMATION_TYPE_2ter);
		} else if (cfg.si2ter_present and cfg.si2bis_present) {
			f_ensure_si_vec_contains(si_per_tc, 5, SYSTEM_INFORMATION_TYPE_2bis);
			f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_2ter, false, 1, 4);
		}

		if (cfg.si7_present or cfg.si8_present) {
			/* vi) Use of System Information type 7 and 8 is not always necessary. It is necessary
			 * if System Information type 4 does not contain all information needed for cell
			 * selection and reselection. */
			if (not cfg.bcch_extended) {
				testcase.stop("Error: SI7/SI8 require BCCH Extd.");
			}
			if (cfg.si7_present) {
				f_ensure_si_vec_contains(si_per_tc, 7, SYSTEM_INFORMATION_TYPE_7, true);
			}
			if (cfg.si8_present) {
				f_ensure_si_vec_contains(si_per_tc, 3, SYSTEM_INFORMATION_TYPE_8, true);
			}
		}

		if (cfg.si2quater_present) {
			/*  iii) System information type 2 quater is sent if needed, as determined by the system
			 *  operator.  If sent on BCCH Norm, it shall be sent when TC = 5 if neither of 2bis
			 *  and 2ter are used, otherwise it shall be sent at least once within any of 4
			 *  consecutive occurrences of TC = 4. If sent on BCCH Ext, it is sent at least once
			 *  within any of 4 consecutive occurrences of TC = 5. */
			if (not (cfg.bcch_extended)) {
				if (not (cfg.si2bis_present or cfg.si2ter_present)) {
					f_ensure_si_vec_contains(si_per_tc, 5, SYSTEM_INFORMATION_TYPE_2quater);
				} else {
					f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_2quater, false, 1, 4);
				}
			} else {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 5, SYSTEM_INFORMATION_TYPE_2quater, true, 1, 4);
			}
		}
		if (cfg.si9_present) {
			/* vi) System Information type 9 is sent in those blocks with TC = 4 which are specified
			 * in system information type 3 as defined in 3GPP TS 44.018. */
			f_ensure_si_vec_contains(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_9); // FIXME SI3
		}
		if (cfg.si13_present) {
			/* vii) System Information type 13 is only related to the GPRS service. System Information
			 * Type 13 need only be sent if GPRS support is indicated in one or more of System
			 * Information Type 3 or 4 or 7 or 8 messages. These messages also indicate if the
			 * message is sent on the BCCH Norm or if the message is transmitted on the BCCH Ext.
			 * In the case that the message is sent on the BCCH Norm, it is sent at least once
			 * within any of 4 consecutive occurrences of TC=4. */
			if (not cfg.bcch_extended) {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_13, false, 1, 4);
			} else {
				f_ensure_si_vec_contains(si_per_tc, 0, SYSTEM_INFORMATION_TYPE_13, true);
			}
			if (f_si_vec_contains(si_per_tc, SYSTEM_INFORMATION_TYPE_13alt)) {
				setverdict(fail, "Cannot have SI13alt and SI13");
			}
		}
		if (cfg.si16_present or cfg.si17_present) {
			/* viii) System Information type 16 and 17 are only related to the SoLSA service. They
			 * should not be sent in a cell where network sharing is used (see rule xv). */
			if (cfg.si22_present) {
				testcase.stop("Error: Cannot have SI16/SI17 and SI22!");
			}
			if (f_si_vec_contains(si_per_tc, SYSTEM_INFORMATION_TYPE_22)) {
				setverdict(fail, "Cannot have SI16/SI17 and SI22!");
			}
			if (not cfg.bcch_extended) {
				testcase.stop("Error: SI16/SI17 requires BCCH Extd!");
			}
			if (cfg.si16_present) {
				f_ensure_si_vec_contains(si_per_tc, 6, SYSTEM_INFORMATION_TYPE_16, true);
			}
			if (cfg.si17_present) {
				f_ensure_si_vec_contains(si_per_tc, 2, SYSTEM_INFORMATION_TYPE_17, true);
			}
		}

			/* ix) System Information type 18 and 20 are sent in order to transmit non-GSM
			 * broadcast information. The frequency with which they are sent is determined by the
			 * system operator. System Information type 9 identifies the scheduling of System
			 * Information type 18 and 20 messages. */

			/* x) System Information Type 19 is sent if COMPACT neighbours exist. If System
			 * Information Type 19 is present, then its scheduling shall be indicated in System
			 * Information Type 9. */

		if (cfg.si15_present) {
			/* xi) System Information Type 15 is broadcast if dynamic ARFCN mapping is used in the
			 * PLMN. If sent on BCCH Norm, it is sent at least once within any of 4 consecutive
			 * occurrences of TC = 4. If sent on BCCH Ext, it is sent at least once within any of
			 * 4 consecutive occurrences of TC = 1. */
			if (not cfg.bcch_extended) {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_15, false, 1, 4);
			} else {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 1, SYSTEM_INFORMATION_TYPE_15, true, 1, 4);
			}
		}
		if (cfg.si13alt_present) {
			/* xii) System Information type 13 alt is only related to the GERAN Iu mode. System
			 * Information Type 13 alt need only be sent if GERAN Iu mode support is indicated in
			 * one or more of System Information Type 3 or 4 or 7 or 8 messages and SI 13 is not
			 * broadcast. These messages also indicate if the message is sent on the BCCH Norm or
			 * if the message is transmitted on the BCCH Ext. In the case that the message is sent
			 * on the BCCH Norm, it is sent at least once within any of 4 consecutive occurrences
			 * of TC = 4. */
			if (cfg.si13_present) {
				testcase.stop("Error: Cannot have SI13alt and SI13");
			}
			if (f_si_vec_contains(si_per_tc, SYSTEM_INFORMATION_TYPE_13)) {
				setverdict(fail, "Cannot have SI13alt and SI13");
			}
			if (not cfg.bcch_extended) {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_13alt, false, 1, 4);
			} else {
				f_ensure_si_vec_contains(si_per_tc, 0, SYSTEM_INFORMATION_TYPE_13alt, true);
			}
		}
		if (cfg.si2n_present) {
			/* xiii) System Information Type 2n is optionally sent on BCCH Norm or BCCH Ext if needed,
			 * as determined by the system operator. In the case that the message is sent on the
			 * BCCH Norm, it is sent at least once within any of 4 consecutive occurrences of TC =
			 * 4. If the message is sent on BCCH Ext, it is sent at least once within any of 2
			 * consecutive occurrences of TC = 4. */
			if (not cfg.bcch_extended) {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_2n, false, 1, 4);
			} else {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_2n, true, 2, 4);
			}
		}
		if (cfg.si21_present) {
			/* xiv) System Information Type 21 is optionally sent on BCCH Norm or BCCH Ext, as
			 * determined by the system operator. If Extended Access Barring is in use in the cell
			 * then this message is sent at least once within any of 4 consecutive occurrences of
			 * TC = 4 regardless if it is sent on BCCH Norm or BCCH Ext. If BCCH Ext is used in a
			 * cell then this message shall only be sent on BCCH Ext. */
			if (not cfg.bcch_extended) {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_21, false, 1, 4);
			} else {
				f_ensure_si_vec_contains_n_of_m(si_per_tc, 4, SYSTEM_INFORMATION_TYPE_21, true, 1, 4);
				if (f_si_vecslot_contains(si_per_tc[4], SYSTEM_INFORMATION_TYPE_21)) {
					setverdict(fail, "Cannot have SI21 on BCCH Norm if BCCH Extd enabled!");
				}
			}
		}
		if (cfg.si22_present) {
			/* xv) System Information Type 22 is sent if network sharing is in use in the cell. It
			 * should not be sent in a cell where SoLSA is used (see rule viii). System
			 * Information Type 22 instances shall be sent on BCCH Ext within any occurrence of TC
			 * =2 and TC=6. */
			if (cfg.si16_present or cfg.si17_present) {
				testcase.stop("Error: Cannot have SI16/SI17 and SI22!");
			}
			if (f_si_vec_contains(si_per_tc, SYSTEM_INFORMATION_TYPE_16) or
			    f_si_vec_contains(si_per_tc, SYSTEM_INFORMATION_TYPE_17)) {
				setverdict(fail, "Cannot have SI16/SI17 and SI22!");
			}
			if (not cfg.bcch_extended) {
				testcase.stop("Error: SI22 requires BCCH Extd!");
			} else {
				f_ensure_si_vec_contains_only(si_per_tc, 2, SYSTEM_INFORMATION_TYPE_22, true);
				f_ensure_si_vec_contains_only(si_per_tc, 6, SYSTEM_INFORMATION_TYPE_22, true);
			}
		}
	}


	function f_gsmtap_sample_si(GSMTAP_PT pt, float duration := 8.0) return SystemInformationVectorPerTc {
		timer T := duration;
		var SystemInformationVectorPerTc si_per_tc;
		var GSMTAP_RecvFrom rf;

		/* initialize all per-TC vectors empty */
		for (var integer i := 0; i < sizeof(si_per_tc); i := i + 1) {
			si_per_tc[i] := {};
		}

		/* flush all previous/buffered elements */
		pt.clear

		T.start;
		alt {
			[] pt.receive(t_recvfrom(GSMTAP_CHANNEL_BCCH)) -> value rf {
					var SystemInformation si := dec_SystemInformation(rf.msg.payload);
					var SystemInformationGsmtap sig := { rf.msg.header, si };
					var integer tc := f_gsm_compute_tc(rf.msg.header.frame_number);
					log("SI received at TC=", tc, ": ", si);
					/* append to the per-TC bucket */
					si_per_tc[tc] := si_per_tc[tc] & { sig };
					repeat;
				}
			[] pt.receive { repeat; };
			[] T.timeout { };
		}
		for (var integer i := 0; i < sizeof(si_per_tc); i := i + 1) {
			log(testcasename(), ": TC=", i, " has #of SI=", sizeof(si_per_tc[i]));
		}
		return si_per_tc;
	}

	function f_gsmtap_get_si(GSMTAP_PT pt, RrMessageType msg_type) return SystemInformation {
		timer T := 10.0;
		var GSMTAP_RecvFrom rf;
		var SystemInformation si;

		/* flush all previous/buffered elements */
		pt.clear

		T.start;
		alt {
			[] pt.receive(t_recvfrom(GSMTAP_CHANNEL_BCCH)) -> value rf {
					si := dec_SystemInformation(rf.msg.payload);
					if (si.header.message_type == msg_type) {
						return si;
					}
					repeat;
				}
			[] pt.receive { repeat; };
			[] T.timeout { testcase.stop("Error waiting for SI on GSMTAP"); };
		}
		return si;
	}

	function f_gsmtap_match_si(GSMTAP_PT pt, RrMessageType msg_type, template SystemInformation t) {
		var SystemInformation si := f_gsmtap_get_si(pt, msg_type);
		if (not match(si, t)) {
			setverdict(fail, "SI ", si, " doesn't match ", t);
		} else {
			setverdict(pass);
		}
	}

	function f_init() runs on dummy_CT {
		if (initialized) {
			return;
		}
		/* GSMTAP initialization */
		map(self:GSMTAP, system:GSMTAP);
		IPL4_GSMTAP_CtrlFunct.f_IPL4_listen(GSMTAP, "0.0.0.0", GSMTAP_PORT, {udp := {}});

		/* VTY initialization */
		map(self:BSCVTY, system:BSCVTY);
		f_vty_set_prompts(BSCVTY)
		f_vty_transceive(BSCVTY, "enable");

		initialized := true;
	}

	testcase TC_si_default() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;

		f_init();

		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		setverdict(pass);
	}

	testcase TC_si_sched_2bis() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		/* Enable SI2bis + validate scheduling */
		si_cfg.si2bis_present := true;
		f_si_cfg_to_vty();
		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		/* cleanup */
		si_cfg.si2bis_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	testcase TC_si_sched_2ter() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		/* Enable SI2ter + validate scheduling */
		si_cfg.si2ter_present := true;
		f_si_cfg_to_vty();
		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		/* cleanup */
		si_cfg.si2ter_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	testcase TC_si_sched_2ter_2bis() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		/* Enable SI2bis + SI2ter + validate scheduling */
		si_cfg.si2bis_present := true;
		si_cfg.si2ter_present := true;
		f_si_cfg_to_vty();
		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		/* cleanup */
		si_cfg.si2bis_present := false;
		si_cfg.si2ter_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	testcase TC_si_sched_2quater() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		/* Enable SI2quater + validate scheduling */
		si_cfg.si2quater_present := true;
		f_si_cfg_to_vty();

		/* cleanup */
		si_cfg.si2quater_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	testcase TC_si_sched_13() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		/* Enable SI2ter + validate scheduling */
		si_cfg.si13_present := true;
		f_si_cfg_to_vty();
		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		/* cleanup */
		si_cfg.si13_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	testcase TC_si_sched_13_2bis_2ter_2quater() runs on dummy_CT {
		var SystemInformationVectorPerTc si_per_tc;
		f_init();

		si_cfg.si2bis_present := true;
		si_cfg.si2ter_present := true;
		si_cfg.si2quater_present := true;
		si_cfg.si13_present := true;
		f_si_cfg_to_vty();
		si_per_tc := f_gsmtap_sample_si(GSMTAP);
		f_validate_si_scheduling(si_cfg, si_per_tc);

		/* cleanup */
		si_cfg.si2bis_present := false;
		si_cfg.si2ter_present := false;
		si_cfg.si2quater_present := false;
		si_cfg.si13_present := false;
		f_si_cfg_to_vty();

		setverdict(pass);
	}

	function f_si_cfg_to_vty() runs on dummy_CT {
		if (si_cfg.si2bis_present) {
			f_vty_si_static(BSCVTY, 0, "2bis", c_si2bis);
		} else {
			f_vty_si_computed(BSCVTY, 0, "2bis");
		}
		if (si_cfg.si2ter_present) {
			f_vty_si_static(BSCVTY, 0, "2ter", c_si2ter);
		} else {
			f_vty_si_computed(BSCVTY, 0, "2ter");
		}
		if (si_cfg.si13_present) {
			f_vty_gprs_mode(BSCVTY, 0, "gprs");
		} else {
			f_vty_gprs_mode(BSCVTY, 0, "none");
		}
		if (si_cfg.si2quater_present) {
			f_vty_si2q_add_uarfcn(BSCVTY, 0, 23, 42);
		} else {
			f_vty_si2q_del_uarfcn(BSCVTY, 0, 23, 42);
		}
		/* for debugging */
		f_vty_transceive(BSCVTY, "write terminal");
		/* actually commit the changes from BSC -> BTS */
		f_vty_si_resend(BSCVTY, 0);
	}

	/* permitted prompts on VTY */
	const charstring NORMAL_PROMPT := "OpenBSC> ";
	const charstring ENABLE_PROMPT := "OpenBSC# ";
	const charstring CONFIG_PROMPT := "OpenBSC(*)\#";
	template charstring t_vty_unknown := pattern "*% Unknown command.";

	const ASP_TelnetDynamicConfig vty_prompt[3] := {
		{
			prompt := {
				id := 1,
				prompt := NORMAL_PROMPT,
				has_wildcards := false
			}
		}, {
			prompt := {
				id := 2,
				prompt := ENABLE_PROMPT,
				has_wildcards := false
			}
		}, {
			prompt := {
				id := 3,
				prompt := CONFIG_PROMPT,
				has_wildcards := true
			}
		}
	};

	/* configure prompts in TELNETasp module */
	function f_vty_set_prompts(TELNETasp_PT pt) {
		/* set some configuration that isn't possible to express
		 * in the config file due to syntactic restrictions (Who invents config
		 * files that don't permit regular expressions? */
		for (var integer i := 0; i < sizeof(vty_prompt); i:= i + 1) {
			pt.send(vty_prompt[i])
		}
	}

	/* wait for any of the permitted prompts; buffer + return all intermediate output */
	function f_vty_wait_for_prompt(TELNETasp_PT pt) return charstring {
		template charstring config_pattern := pattern CONFIG_PROMPT;
		var charstring rx, buf := "";
		timer T := 2.0;

		T.start;
		alt {
			[] pt.receive(NORMAL_PROMPT) { };
			[] pt.receive(ENABLE_PROMPT) { };
			[] pt.receive(config_pattern) { };
			[] pt.receive(t_vty_unknown) { testcase.stop(fail, "VTY: Unknown Command") };
			[] pt.receive(charstring:?) -> value rx { buf := buf & rx; repeat };
			[] T.timeout { setverdict(fail, "VTY Timeout for prompt"); return ""};
		}
		T.stop;
		return buf;
	}

	/* send a VTY command and obtain response until prompt is received */
	function f_vty_transceive_ret(TELNETasp_PT pt, charstring tx) return charstring {
		pt.send(tx);
		return f_vty_wait_for_prompt(pt);
	}

	/* send a VTY command and obtain response until prompt is received */
	function f_vty_transceive(TELNETasp_PT pt, charstring tx) {
		f_vty_transceive_ret(pt, tx);
	}

	type integer BtsNr (0..255);
	type integer BtsTrxNr (0..255);
	type integer BtsTimeslotNr (0..7);

	type charstring BtsGprsMode ("none", "gprs", "egrps");

	/* enter the'confiugration' mode of the VTY */
	function f_vty_enter_config(TELNETasp_PT pt) {
		f_vty_transceive(pt, "configure terminal")
	}

	function f_vty_enter_cfg_network(TELNETasp_PT pt) {
		f_vty_enter_config(pt);
		f_vty_transceive(pt, "network")
	}

	function f_vty_enter_cfg_bts(TELNETasp_PT pt, BtsNr bts := 0) {
		f_vty_enter_cfg_network(pt);
		f_vty_transceive(pt, "bts " & int2str(bts));
	}

	function f_vty_enter_cfg_trx(TELNETasp_PT pt, BtsNr bts := 0, BtsTrxNr trx := 0) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "trx " & int2str(trx));
	}

	function f_vty_enter_cfg_ts(TELNETasp_PT pt, BtsNr bts := 0, BtsTrxNr trx := 0, BtsTimeslotNr ts) {
		f_vty_enter_cfg_trx(pt, bts, trx);
		f_vty_transceive(pt, "timeslot " & int2str(ts));
	}

	function f_vty_si_static(TELNETasp_PT pt, BtsNr bts, charstring si, octetstring bytes) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "system-information " & si & " mode static");
		f_vty_transceive(pt, "system-information " & si & " static " & hex2str(oct2hex(bytes)));
		f_vty_transceive(pt, "end");
	}

	function f_vty_si_computed(TELNETasp_PT pt, BtsNr bts, charstring si) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "system-information " & si & " mode computed");
		f_vty_transceive(pt, "end");
	}

	function f_vty_si_resend(TELNETasp_PT pt, BtsNr bts := 0) {
		f_vty_transceive(pt, "bts " & int2str(bts) & " resend-system-information");
		/* wait for 1s until changes propagate */
		timer T := 1.0;
		T.start;
		T.timeout;
	}

	function f_vty_gprs_mode(TELNETasp_PT pt, integer bts, BtsGprsMode mode) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "gprs mode " & mode);
		f_vty_transceive(pt, "end");
	}

	function f_vty_si2q_add_uarfcn(TELNETasp_PT pt, BtsNr bts, UmtsArfcn uarfcn, UmtsScramblingCode sc, integer diversity := 0) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "si2quater neighbor-list add uarfcn " & int2str(uarfcn) & " " & int2str(sc) & " " & int2str(diversity));
		f_vty_transceive(pt, "end");
	}

	function f_vty_si2q_del_uarfcn(TELNETasp_PT pt, BtsNr bts, UmtsArfcn uarfcn, UmtsScramblingCode sc) {
		f_vty_enter_cfg_bts(pt, bts);
		f_vty_transceive(pt, "si2quater neighbor-list del uarfcn " & int2str(uarfcn) & " " & int2str(sc));
		f_vty_transceive(pt, "end");
	}

	testcase TC_telnet() runs on dummy_CT {
		f_init();
		f_vty_enter_config(BSCVTY);
		f_vty_transceive(BSCVTY, "show network")
		f_vty_transceive(BSCVTY, "network")
		f_vty_transceive(BSCVTY, "bts 0")
		f_vty_transceive(BSCVTY, "end")
		setverdict(pass);
	}

	template SystemInformation t_SI_SI3 := {
		header := t_SiHeader(SYSTEM_INFORMATION_TYPE_3, ?),
		payload := { si3 := t_SI3 }
	}

	testcase TC_cellid() runs on dummy_CT {
		var CellIdentity cid := float2int(rnd() * 65535.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_id := cid;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "cell_identity " & int2str(cid));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_lac() runs on dummy_CT {
		var uint16_t lac := float2int(rnd() * 65535.0);

		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.lai.lac := lac;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "location_area_code " & int2str(lac));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_rach_tx_int() runs on dummy_CT {
		var uint16_t rach_tx_int := float2int(rnd() * 15.0);

		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.rach_control.tx_integer := int2bit(rach_tx_int, 4);

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "rach tx integer " & int2str(rach_tx_int));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_rach_max_tx() runs on dummy_CT {
		var uint16_t r := float2int(rnd() * 3.0);
		const integer max_tx_map[4] := { 1, 2, 4, 7 };
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.rach_control.max_retrans := int2bit(r, 2);

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "rach max transmission " & int2str(max_tx_map[r]));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_dtx_ul() runs on dummy_CT {
		var integer i := float2int(rnd() * 2.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_options.dtx := int2bit(i, 2);

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		if (i == 0) {
			f_vty_transceive(BSCVTY, "dtx uplink");
		} else if (i == 1) {
			f_vty_transceive(BSCVTY, "dtx uplink force");
		} else {
			f_vty_transceive(BSCVTY, "no dtx uplink");
		}

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_attach() runs on dummy_CT {
		var integer i := float2int(rnd());
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.ctrl_chan_desc.att := int2bool(i);

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "channel-descrption attach " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_bs_pa_mfrms() runs on dummy_CT {
		var integer i := 2 + float2int(rnd() * 7.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.ctrl_chan_desc.bs_pa_mfrms := i - 2;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "channel-descrption bs-pa-mfrms " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_bs_ag_blks_res() runs on dummy_CT {
		var integer i := float2int(rnd() * 7.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.ctrl_chan_desc.bs_ag_blks_res := i;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "channel-descrption bs-ag-blks-res " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_radio_link_timeout() runs on dummy_CT {
		var integer i := float2int(rnd() * 15.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_options.radio_link_timeout := int2bit(i, 4);

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "radio-link-timeout " & int2str(4 + i*4));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_cell_resel_hyst() runs on dummy_CT {
		var integer i := float2int(rnd() * 7.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_sel_par.cell_resel_hyst := i;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "cell reselection hysteresis " & int2str(i*2));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_rxlev_acc_min() runs on dummy_CT {
		var integer i := float2int(rnd() * 63.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_sel_par.rxlev_access_min := i;

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "rxlev access min " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_neci() runs on dummy_CT {
		var integer i := float2int(rnd() * 1.0);
		var template SystemInformation t := t_SI_SI3;
		t.payload.si3.cell_sel_par.neci := int2bool(i);

		f_init();
		f_vty_enter_cfg_network(BSCVTY);
		f_vty_transceive(BSCVTY, "neci " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	testcase TC_emerg_allowed() runs on dummy_CT {
		var integer i := float2int(rnd());
		var template SystemInformation t := t_SI_SI3;
		if (i == 1) {
			t.payload.si3.rach_control.ac := '?????0??????????'B;
		} else {
			t.payload.si3.rach_control.ac := '?????1??????????'B;
		}

		f_init();
		f_vty_enter_cfg_bts(BSCVTY, 0);
		f_vty_transceive(BSCVTY, "rach emergency call allowed " & int2str(i));
		f_vty_transceive(BSCVTY, "end")
		f_vty_si_resend(BSCVTY, 0);

		f_gsmtap_match_si(GSMTAP, SYSTEM_INFORMATION_TYPE_3, t);
	}

	/* TODO:
	* 	* don't only validate SI3 but check all other SI with same IE?
	*	* parse + validate rest octets somehow
	*	* validate contents/encoding of neighbor channel lists
	*	* validate si2quater sub-mux scheduling
	*/


	control {
		execute(TC_si1());
		execute(TC_telnet());
		execute(TC_si_default());
		execute(TC_si_sched_2bis());
		execute(TC_si_sched_2ter());
		execute(TC_si_sched_2ter_2bis());
		execute(TC_si_sched_2quater());
		execute(TC_si_sched_13());
		execute(TC_si_sched_13_2bis_2ter_2quater());
		execute(TC_neci());
		execute(TC_cell_resel_hyst());
		execute(TC_rxlev_acc_min());
		execute(TC_cellid());
		execute(TC_lac());
		execute(TC_rach_tx_int());
		execute(TC_rach_max_tx());
		execute(TC_attach());
		execute(TC_dtx_ul());
		execute(TC_emerg_allowed());
		execute(TC_bs_pa_mfrms());
		execute(TC_bs_ag_blks_res());
		execute(TC_radio_link_timeout());
	}
}