mtype = { S_OFF, S_ON }
mtype = { S_OFF_T_NONE, S_OFF_T_ON }
mtype = { S_ON_T_NONE, S_ON_T_OFF, S_ON_T_ON, S_ON_T_OFF_ON }
mtype = { REQ_NONE, REQ_OFF, REQ_ON, REQ_CAN, REQ_SET }

#define OFF_TIM_MAX		2

#define ON_TIM_H_MAX	2 - 1
#define ON_TIM_M_MAX	2 - 1

/* 状態 */
mtype s  			= S_OFF;
mtype ss 			= S_OFF_T_NONE;
/* 前周期状態 */
mtype ps  			= S_OFF;
mtype pss 			= S_OFF_T_NONE;

/* 要求（電源） */
chan req_power = [1] of { mtype }

/* 要求（ONタイマ） */
chan req_on_tim = [1] of { mtype, byte, byte }
byte req_on_tim_val_h;
byte req_on_tim_val_m;

/* 要求（OFFタイマ） */
chan req_off_tim = [1] of { mtype, byte }
byte req_off_tim_val;

/* ONタイマ */
/* 有効フラグ */
bool enable_on_tim = false;
/* 現在時刻 */
byte cur_on_h = 0;
byte cur_on_m = 0;
/* 現在時刻 */
byte set_on_h = 0;
byte set_on_m = 0;
/* 発火通知 */
chan is_fire_on_tim = [1] of { bool }

/* OFFタイマ */
/* 有効フラグ */
bool enable_off_tim = false;
/* 設定時間 */
byte set_off_tim_val;
/* 経過時間 */
byte cur_off_tim_val = 0;
/* 発火通知 */
chan is_fire_off_tim = [1] of { bool }

/* ポート */

inline check_model()
{
	printf("STAT [%e\t:%e\t]\n", s, ss);
	if
		/* 電源OFF中 */
		:: s == S_OFF ->
			if
				/* タイマセット無し */
				:: ss == S_OFF_T_NONE ->
					assert(enable_on_tim == false);
					assert(enable_off_tim == false)
				/* ONタイマセット中 */
				:: ss == S_OFF_T_ON -> 
					assert(enable_on_tim == true);
					assert(enable_off_tim == false)
				:: else -> skip
			fi
		/* 電源ON中 */
		:: s == S_ON ->
			if
				/* タイマセット無し */
				:: ss == S_ON_T_NONE ->
					assert(enable_on_tim == false);
					assert(enable_off_tim == false)
				/* OFFタイマセット中 */
				:: ss == S_ON_T_OFF ->
					assert(enable_on_tim == false);
					assert(enable_off_tim == true)
				/* ONタイマセット中 */
				:: ss == S_ON_T_ON ->
					assert(enable_on_tim == true);
					assert(enable_off_tim == false)
				/* ONタイマOFFタイマセット中 */
				:: ss == S_ON_T_OFF_ON ->
					assert(enable_on_tim == true);
					assert(enable_off_tim == true)
				:: else -> skip
			fi
		:: else -> skip
	fi;
	/* タイマのカウント値 */
	assert(cur_on_h <= ON_TIM_H_MAX);
	assert(cur_on_m <= ON_TIM_M_MAX);
	assert(cur_off_tim_val <= OFF_TIM_MAX)
}


inline set_off_tim(val)
{
	cur_off_tim_val = 0;
	set_off_tim_val = val;
	enable_off_tim = true;
}

inline clr_off_tim()
{
	enable_off_tim = false;
}

inline tick_off_tim()
{
	if 
		:: enable_off_tim == true ->
			cur_off_tim_val++;
			if 
				:: cur_off_tim_val >= set_off_tim_val -> 
					if
						:: empty(is_fire_off_tim) -> is_fire_off_tim!true
						:: nempty(is_fire_off_tim) -> skip
					fi
				:: else -> skip
			fi
		:: else -> skip
	fi
}

inline set_on_tim(val_h, val_m)
{
	set_on_h = val_h;
	set_on_m = val_m;
	enable_on_tim = true;
}

inline clr_on_tim()
{
	enable_on_tim = false;
}

inline tick_on_tim()
{
	do
		:: empty(is_fire_on_tim) -> break
		:: nempty(is_fire_on_tim) -> is_fire_on_tim?_
	od;
	cur_on_m++;
	if 
		:: cur_on_m < ON_TIM_M_MAX -> skip
		:: else -> 
			cur_on_m = 0;
			cur_on_h++;
			if 
				:: cur_on_h < ON_TIM_H_MAX -> skip
				:: else -> cur_on_h = 0
			fi
	fi;
	if 
		:: enable_on_tim == true ->
			if
				:: cur_on_h == set_on_h && cur_on_m == set_on_m ->
					is_fire_on_tim!true 
				:: else -> skip
			fi
		:: else -> skip
	fi
}

inline tv()
{
	do ::
		ps = s;
		pss = ss;
		if
			/* 電源OFF中 */
			:: (s == S_OFF) ->
				if	
					/* タイマセット無し */
					:: (ss == S_OFF_T_NONE) ->
						if 
							:: req_power?[REQ_ON] ->
							    req_power?_;
								printf("POWER ON\n");
								s = S_ON;
								ss = S_ON_T_NONE
							:: else -> skip
						fi
					/* ONタイマセット中 */
					:: (ss == S_OFF_T_ON) ->
						if
							:: is_fire_on_tim?[true] ->
								is_fire_on_tim?_;
								clr_on_tim();
								printf("ON TIMER FIRED\n");
								s = S_ON;
								ss = S_ON_T_NONE
							:: req_power?[REQ_ON] ->
								req_power?_;
								printf("POWER ON\n");
								s = S_ON;
								ss = S_ON_T_ON
							:: else -> skip
						fi
					:: else -> skip
				fi
			/* 電源ON中 */
			:: (s == S_ON) ->
				if	
					/* タイマセット無し */
					:: (ss == S_ON_T_NONE) ->
						if 
							:: req_power?[REQ_OFF] ->
								req_power?_;
								printf("POWER OFF\n");
								s = S_OFF;
								ss = S_OFF_T_NONE
							:: req_on_tim?[REQ_SET] ->
								req_on_tim?_, req_on_tim_val_h, req_on_tim_val_m;
								set_on_tim(req_on_tim_val_h, req_on_tim_val_m);
								printf("ON  TIMER SET[%d:%d]\n", req_on_tim_val_h, req_on_tim_val_m);
								ss = S_ON_T_ON
							:: req_off_tim?[REQ_SET] ->
								req_off_tim?_, req_off_tim_val;
								set_off_tim(req_off_tim_val);
								printf("OFF TIMER SET[%d]\n", req_off_tim_val);
								ss = S_ON_T_OFF
							:: else -> skip
						fi
					/* OFFタイマセット中 */
					:: (ss == S_ON_T_OFF) ->
						if
							:: is_fire_off_tim?[true] ->
								is_fire_off_tim?_;
								clr_off_tim();
								printf("OFF TIMER FIRED\n");
								s = S_OFF;
								ss = S_OFF_T_NONE
							:: req_power?[REQ_OFF] ->
								req_power?_;
								clr_off_tim();
								printf("POWER OFF\n");
								s = S_OFF;
								ss = S_OFF_T_NONE
							:: req_on_tim?[REQ_SET] ->
								req_on_tim?_, req_on_tim_val_h, req_on_tim_val_m;
								set_on_tim(req_on_tim_val_h, req_on_tim_val_m);
								printf("ON  TIMER SET[%d:%d]\n", req_on_tim_val_h, req_on_tim_val_m);
								ss = S_ON_T_OFF_ON
							:: req_off_tim?[REQ_CAN] ->
								req_off_tim?_, _;
								clr_off_tim();
								ss = S_ON_T_NONE
							:: else  -> skip
						fi
					/* ONタイマセット中 */
					:: (ss == S_ON_T_ON) ->
						if 
							:: is_fire_on_tim?[true] ->
								is_fire_on_tim?_;
								clr_on_tim();
								printf("ON TIMER FIRED\n");
								ss = S_ON_T_NONE
							:: req_power?[REQ_OFF] ->
								req_power?_;
								printf("POWER OFF\n");
								s = S_OFF;
								ss = S_OFF_T_ON
							:: req_off_tim?[REQ_SET] ->
								req_off_tim?_, req_off_tim_val;
								set_off_tim(req_off_tim_val);
								printf("OFF TIMER SET[%d]\n", req_off_tim_val);
								ss = S_ON_T_OFF_ON
							:: req_on_tim?[REQ_CAN] ->
								req_on_tim?_, _, _;
								clr_on_tim();
								printf("ON TIMER CANCEL\n");
								ss = S_ON_T_NONE
							:: else -> skip
						fi
					/* ONタイマOFFタイマセット中 */
					:: (ss == S_ON_T_OFF_ON) ->
						if 
							:: is_fire_off_tim?[true] ->
								is_fire_off_tim?_;
								clr_off_tim();
								printf("OFF TIMER FIRED\n");
								s = S_OFF;
								ss = S_OFF_T_ON
							:: is_fire_on_tim?[true] ->
								is_fire_on_tim?_;
								clr_on_tim();
								printf("ON TIMER FIRED\n");
								ss = S_ON_T_OFF
							:: req_power?[REQ_OFF] ->
								req_power?_;
								clr_off_tim();
								printf("POWER OFF\n");
								s = S_OFF;
								ss = S_OFF_T_ON
							:: req_off_tim?[REQ_CAN] ->
								req_off_tim?_, _;
								clr_off_tim();
								printf("OFF TIMER CANCEL\n");
								ss = S_ON_T_ON
							:: req_on_tim?[REQ_CAN] ->
								req_on_tim?_, _, _;
								clr_on_tim();
								printf("ON TIMER CANCEL\n");
								ss = S_ON_T_OFF
							:: else -> skip
						fi
					:: else -> skip
				fi
			:: else -> skip
		fi;
		if
			:: (ps == s && pss == ss) -> break
			:: else -> skip
		fi
	od
}


inline arch_mec()
{
	tick_off_tim();
	tick_on_tim()
}




inline req_sim_power()
{
	do
		:: empty(req_power) -> break
		:: nempty(req_power) -> req_power?_
	od;
	if
		:: req_power!REQ_OFF
		:: req_power!REQ_ON
		:: skip
	fi
}

inline req_sim_on_tim()
{
	byte on_set_h = 0;
	byte on_set_m = 0;

	do
		:: empty(req_on_tim) -> break
		:: nempty(req_on_tim) -> req_on_tim?_, _, _
	od;
	if
		:: req_on_tim!REQ_CAN, 0, 0
		::
			do
				:: on_set_h < ON_TIM_H_MAX -> on_set_h++
				:: on_set_h >= ON_TIM_H_MAX -> break
				:: break
			od;
			do
				:: on_set_m < ON_TIM_M_MAX -> on_set_m++
				:: on_set_m >= ON_TIM_M_MAX -> break
				:: break
			od;
			req_on_tim!REQ_SET, on_set_h, on_set_m
		:: skip
	fi
}

inline req_sim_off_tim()
{
	byte off_set = 1;

	do
		:: empty(req_off_tim) -> break
		:: nempty(req_off_tim) -> req_off_tim?_, _
	od;
	if
		:: req_off_tim!REQ_CAN, 0
		::
			do
				:: off_set < OFF_TIM_MAX -> off_set++
				:: off_set >= OFF_TIM_MAX -> break
				:: break
			od;
			req_off_tim!REQ_SET, off_set
		:: skip
	fi
}

inline req_sim()
{
	req_sim_power();	/* 電源要求 */
	req_sim_on_tim();	/* オンタイマ要求 */
	req_sim_off_tim()	/* オフタイマ要求 */
}

active proctype main()
{
	do ::
		/* 検証モデル動作 */
		tv();

		/* 検証 */
		check_model();

		/* アーキテクチャメカニズム動作 */
		arch_mec();
		
		/* 要求シミュレーション */
		req_sim();
	od
}