HealthcareDevice.vdmrt

class 「調停人」
types
	public 「イベント」 = 
	<進むボタン押下> | <戻るボタン押下> | <決定ボタン押下> | <USB接続> | <USB切断>;
	
operations
	public pure 年取得: () ==> nat
	年取得() == is subclass responsibility
	post 1 <= RESULT and RESULT <= 9999;
	public pure 月取得: () ==> nat
	月取得() ==  is subclass responsibility
	post 1 <= RESULT and RESULT <= 12;
	public pure 日取得: () ==> nat
	日取得() ==  is subclass responsibility
	post 1 <= RESULT and RESULT <= 31;
	async public 年更新: nat ==> ()
	年更新(a年) == is subclass responsibility
	pre 1 <= a年 and a年 <= 9999;
	async public 月更新: nat ==> ()
	月更新(a月) == is subclass responsibility
	pre 1 <= a月 and a月 <= 12;
	async public 日更新: nat ==> ()
	日更新(a日) == is subclass responsibility
	pre 1 <= a日 and a日 <= 31;
	
	
	public pure 時刻取得: () ==> 「観測」`「時刻」
	時刻取得() == is subclass responsibility
	post 1 <= RESULT and RESULT <= 99991231;
	async public 時間経過: () ==> ()
	時間経過() ==  is subclass responsibility;

	public pure 歩幅取得: () ==> nat
	歩幅取得() == is subclass responsibility
	post 1 <= RESULT and RESULT <= 9999;
	async public 歩幅更新: nat ==> ()
	歩幅更新(a歩幅) == is subclass responsibility
	pre 1 <= a歩幅 and a歩幅 <= 9999;

	public pure 体重取得: () ==> nat
	体重取得() == is subclass responsibility
	post 1 <= RESULT and RESULT <= 9999;
	async public 体重更新: nat ==> ()
	体重更新(a体重) == is subclass responsibility
	pre 1 <= a体重 and a体重 <= 9999;
	
	async public 本日画面描画: () ==> ()
	本日画面描画() == is subclass responsibility;
	async public 前日画面描画: () ==> ()
	前日画面描画() == is subclass responsibility;
	async public 前々日画面描画: () ==> ()
	前々日画面描画() == is subclass responsibility;
	async public 本日有酸素画面描画: () ==> ()
	本日有酸素画面描画() == is subclass responsibility;
	async public 前日有酸素画面描画: () ==> ()
	前日有酸素画面描画() == is subclass responsibility;
	async public 前々日有酸素画面描画: () ==> ()
	前々日有酸素画面描画() == is subclass responsibility;
	async public 設定開始画面描画: () ==> ()
	設定開始画面描画() == is subclass responsibility;
	async public 年設定画面描画: nat ==> ()
	年設定画面描画(a年) == is subclass responsibility
	pre 1 <= a年 and a年 <= 9999;
	async public 月設定画面描画: nat ==> ()
	月設定画面描画(a月) == is subclass responsibility
	pre 1 <= a月 and a月 <= 12;
	async public 日設定画面描画: nat ==> ()
	日設定画面描画(a日) == is subclass responsibility
	pre 1 <= a日 and a日 <= 31;
	async public 歩幅設定画面描画: nat ==> ()
	歩幅設定画面描画(a歩幅) == is subclass responsibility
	pre 1 <= a歩幅 and a歩幅 <= 9999;
	async public 体重設定画面描画: nat ==> ()
	体重設定画面描画(a体重) == is subclass responsibility
	pre 1 <= a体重 and a体重 <= 9999;
	async public USB接続中画面描画: () ==> ()
	USB接続中画面描画() == is subclass responsibility;

	async public USB接続中ロック取得: () ==> ()
	USB接続中ロック取得() == is subclass responsibility;

	async public USB接続中ロック解除: () ==> ()
	USB接続中ロック解除() == is subclass responsibility;
	
	public pure 本日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	本日画面情報() == is subclass responsibility;
	public pure 前日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前日画面情報() == is subclass responsibility;
	public pure 前々日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前々日画面情報() == is subclass responsibility;
	public pure 本日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	本日有酸素画面情報() == is subclass responsibility;
	public pure 前日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前日有酸素画面情報() == is subclass responsibility;
	public pure 前々日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前々日有酸素画面情報() == is subclass responsibility;

	async public 進むボタン押下: () ==> ()
	進むボタン押下() == is subclass responsibility;
	async public 戻るボタン押下: () ==> ()
	戻るボタン押下() == is subclass responsibility;
	async public 決定ボタン押下: () ==> ()
	決定ボタン押下() == is subclass responsibility;

	async public USB接続: () ==> ()
	USB接続() == is subclass responsibility;
	async public USB切断: () ==> ()
	USB切断() == is subclass responsibility;
	
	async public 観測値追加: 「加速度」 ==> ()
  観測値追加(a加速度) == is subclass responsibility;
  public pure 現在時刻取得: () ==> 「観測」`「時刻」
  現在時刻取得() == is subclass responsibility;
  
	async public 画面状態変更: 「イベント」 * 「画面状態」 ==> ()
	画面状態変更(aイベント, a状態) == is subclass responsibility
end 「調停人」


class 「同僚」
instance variables
	protected 調停人: 「調停人」;
end 「同僚」

class 「画面状態」 is subclass of 「同僚」
operations
	async public 進むボタン押下遷移: () ==> ()
	進むボタン押下遷移() == (
		進むボタン押下();
		調停人.画面状態変更(<進むボタン押下>, self.get状態())
	);
	async public 戻るボタン押下遷移: () ==> ()
	戻るボタン押下遷移() == (
		戻るボタン押下();
		調停人.画面状態変更(<戻るボタン押下>, self.get状態())
	);
	async public 決定ボタン押下遷移: () ==> ()
	決定ボタン押下遷移() == (
		決定ボタン押下();
		調停人.画面状態変更(<決定ボタン押下>, self.get状態())
	);
	async public USB接続遷移: () ==> ()
	USB接続遷移() == (
		USB接続();
		調停人.画面状態変更(<USB接続>, self.get状態())
	);
	async public USB切断遷移: () ==> ()
	USB切断遷移() == (
		USB切断();
		調停人.画面状態変更(<USB切断>, self.get状態())
	);
	async public entry処理: () ==> ()
	entry処理() == skip;
	
	async public do処理: () ==> ()
	do処理() == is subclass responsibility;

	async public exit処理: () ==> ()
	exit処理() == skip;

	protected pure get状態: () ==> 「画面状態」
	get状態() == is subclass responsibility;
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == skip;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == skip;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == skip;
	async protected USB接続: () ==> ()
	USB接続() == skip;
	async protected USB切断: () ==> ()
	USB切断() == skip;

end 「画面状態」

class 「USB切断中」 is subclass of 「画面状態」
operations
	async protected USB切断: () ==> ()
	USB切断() == is not yet specified
	pre false post false;
end 「USB切断中」



class 「TOP画面状態」 is subclass of 「USB切断中」
end 「TOP画面状態」
class 「本日画面」 is subclass of 「TOP画面状態」
operations
	public 「本日画面」: 「調停人」 ==> 「本日画面」
	「本日画面」(a歩数計調停人) == 調停人 := a歩数計調停人;
	
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;
	
	async public do処理: () ==> ()
	do処理() == 調停人.本日画面描画();
end 「本日画面」
class 「前日画面」 is subclass of 「TOP画面状態」
operations
	public 「前日画面」: 「調停人」 ==> 「前日画面」
	「前日画面」(a歩数計調停人) == 調停人 := a歩数計調停人;
	
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.前日画面描画();
 
end 「前日画面」
class 「前々日画面」 is subclass of 「TOP画面状態」
operations
	public 「前々日画面」: 「調停人」 ==> 「前々日画面」
	「前々日画面」(a歩数計調停人) == 調停人 := a歩数計調停人;

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.前々日画面描画();
end 「前々日画面」

class 「本日有酸素画面」 is subclass of 「TOP画面状態」
operations
	public 「本日有酸素画面」: 「調停人」 ==> 「本日有酸素画面」
	「本日有酸素画面」(a調停人) == 調停人 := a調停人;

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.本日有酸素画面描画();
end 「本日有酸素画面」
class 「前日有酸素画面」 is subclass of 「TOP画面状態」
operations
	public 「前日有酸素画面」: 「調停人」 ==> 「前日有酸素画面」
	「前日有酸素画面」(a歩数計調停人) == 調停人 := a歩数計調停人;
	
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.前日有酸素画面描画();
end 「前日有酸素画面」

class 「前々日有酸素画面」 is subclass of 「TOP画面状態」
operations
	public 「前々日有酸素画面」: 「調停人」 ==> 「前々日有酸素画面」
	「前々日有酸素画面」(a調停人) == 調停人 := a調停人;

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.前々日有酸素画面描画();
end 「前々日有酸素画面」


class 「設定開始確認」 is subclass of 「USB切断中」
operations
	public 「設定開始確認」: 「調停人」 ==> 「設定開始確認」
	「設定開始確認」(a調停人) == 調停人 := a調停人;

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public do処理: () ==> ()
	do処理() == 調停人.設定開始画面描画();
 
end 「設定開始確認」


class 「時刻設定状態」 is subclass of 「USB切断中」
end 「時刻設定状態」

class 「年設定」 is subclass of 「時刻設定状態」
values
	最大設定値 = 9999
instance variables
	設定中値: nat;
	inv 設定中値 <= 最大設定値;
operations
	public 「年設定」: 「調停人」 ==> 「年設定」
	「年設定」(a調停人) == atomic(
		調停人 := a調停人;
		設定中値 := a調停人.年取得();
	);
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public entry処理: () ==> ()
	entry処理() == 設定中値 := 調停人.年取得();

	async public do処理: () ==> ()
	do処理() == 調停人.年設定画面描画(設定中値);
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == atomic(設定中値 := 設定中値 + 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == atomic(設定中値 := 設定中値 - 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == 調停人.年更新(設定中値);
end 「年設定」
class 「月設定」 is subclass of 「時刻設定状態」
values
	最大設定値 = 12
instance variables
	設定中値: nat;
	inv 1 <= 設定中値 and 設定中値 <= 最大設定値;
operations
	public 「月設定」: 「調停人」 ==> 「月設定」
	「月設定」(a調停人) == atomic(
		調停人 := a調停人;
		設定中値 := a調停人.月取得();
	);
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;
 
	async public entry処理: () ==> ()
	entry処理() == 設定中値 := 調停人.月取得();

	async public do処理: () ==> ()
	do処理() == 調停人.月設定画面描画(設定中値);
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == atomic(設定中値 := 設定中値 + 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == atomic(設定中値 := 設定中値 - 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == 調停人.月更新(設定中値);
end 「月設定」

class 「日設定」 is subclass of 「時刻設定状態」
values
	最大設定値 = 31
instance variables
	設定中値: nat;
	inv 1 <= 設定中値 and 設定中値 <= 最大設定値;
operations
	public 「日設定」: 「調停人」 ==> 「日設定」
	「日設定」(a調停人) == atomic(
		調停人 := a調停人;
		設定中値 := a調停人.日取得();
	);
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;
 
	async public entry処理: () ==> ()
	entry処理() == 設定中値 := 調停人.日取得();

	async public do処理: () ==> ()
	do処理() == 調停人.日設定画面描画(設定中値);
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == atomic(設定中値 := 設定中値 + 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == atomic(設定中値 := 設定中値 - 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == 調停人.日更新(設定中値);
end 「日設定」


class 「歩幅設定」 is subclass of 「USB切断中」
values
	最大設定値 = 999
instance variables
	設定中値: nat;
	inv 1 <= 設定中値 and 設定中値 <= 最大設定値;
operations
	public 「歩幅設定」: 「調停人」 ==> 「歩幅設定」
	「歩幅設定」(a調停人) == atomic(
		調停人 := a調停人;
		設定中値 := a調停人.歩幅取得();
	);

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public entry処理: () ==> ()
	entry処理() == 設定中値 := 調停人.歩幅取得();
	
	async public do処理: () ==> ()
	do処理() == 調停人.歩幅設定画面描画(設定中値);
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == atomic(設定中値 := 設定中値 + 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == atomic(設定中値 := 設定中値 - 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == 調停人.歩幅更新(設定中値);
end 「歩幅設定」

class 「体重設定」 is subclass of 「USB切断中」
values
	最大設定値 = 9999
instance variables
	設定中値: nat;
	inv 1 <= 設定中値 and 設定中値 <= 最大設定値;
operations
	public 「体重設定」: 「調停人」 ==> 「体重設定」
	「体重設定」(a調停人) == atomic(
		調停人 := a調停人;
		設定中値 := a調停人.体重取得();
	);
	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public entry処理: () ==> ()
	entry処理() == 設定中値 := 調停人.体重取得();

	async public do処理: () ==> ()
	do処理() == 調停人.体重設定画面描画(設定中値);
 
	async protected 進むボタン押下: () ==> ()
	進むボタン押下() == atomic(設定中値 := 設定中値 + 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 戻るボタン押下: () ==> ()
	戻るボタン押下() == atomic(設定中値 := 設定中値 - 1; 設定中値 := (設定中値 + 1) mod (最大設定値 + 1))
	post 設定中値 <> 設定中値~;
	async protected 決定ボタン押下: () ==> ()
	決定ボタン押下() == 調停人.体重更新(設定中値);
end 「体重設定」


class 「USB接続中」 is subclass of 「画面状態」
operations
	public 「USB接続中」: 「調停人」 ==> 「USB接続中」
	「USB接続中」(a調停人) == 調停人 := a調停人;

	protected pure get状態: () ==> 「画面状態」
	get状態() == return self;

	async public entry処理: () ==> ()
	entry処理() == 調停人.USB接続中ロック取得();

	async public do処理: () ==> ()
	do処理() == 調停人.USB接続中画面描画();
	
	async public exit処理: () ==> ()
	exit処理() == 調停人.USB接続中ロック解除();
 
	async protected USB接続: () ==> ()
	USB接続() == is not yet specified
	pre false post false;
end 「USB接続中」


class 「IMU」 is subclass of 「同僚」
operations
	public 「IMU」: 「調停人」 ==> 「IMU」
	「IMU」(a調停人) == 調停人 := a調停人;
	public 観測: () ==> ()
	観測() == 調停人.観測値追加(
		new 「加速度」(
			new 「量」(MATH`rand(10), <M>),
			new 「量」(MATH`rand(10), <M>),
			new 「量」(MATH`rand(10), <M>)
		)
	);
end 「IMU」

class 「量」
types
	public 「単位」 = <KG> | <時間> | <速度> | <歩数> | <KCAL> | <M>
instance variables
	値: real;
	単位: 「単位」;
operations
	public 「量」: real * 「単位」 ==> 「量」
	「量」(a値, a単位) == atomic(値 := a値; 単位 := a単位);
	public pure get値: () ==> real
	get値() == return 値;
	public pure 掛ける: real ==> 「量」
	掛ける(a係数) == return new 「量」(値 * a係数, 単位);
	public pure 足す: 「量」 ==> 「量」
	足す(a量) == return new 「量」(値 + a量.get値(), 単位)
	pre a量.単位 = 単位;
end 「量」

class 「加速度」
instance variables
	x: 「量」;
	y: 「量」;
	z: 「量」;
operations
	public 「加速度」: 「量」 * 「量」 * 「量」 ==> 「加速度」
	 「加速度」(aX, aY, aZ) == atomic(x := aX; y := aY; z := aZ);
	public pure 距離: () ==> 「量」
	距離() == return new 「量」(abs x.get値() + abs y.get値() + abs z.get値(), <M>);
end 「加速度」

class 「観測」
types
	public 「時刻」 = nat
instance variables
	量: 「量」;
	時刻: 「時刻」;
operations
	public 「観測」: 「加速度」 * 「時刻」 ==> 「観測」
	「観測」(a加速度, a時刻) == atomic(量 := a加速度.距離(); 時刻 := a時刻);
	public 「観測」: 「量」 * 「時刻」 ==> 「観測」
	「観測」(a量, a時刻) == atomic(量 := a量; 時刻 := a時刻);
	public pure get距離: () ==> 「量」
	get距離() == return 量;
	public pure get時刻: () ==> 「時刻」
	get時刻() == return 時刻;
end 「観測」

class 「期間」
instance variables
	開始: 「観測」`「時刻」;
	終了: 「観測」`「時刻」;
operations
	public 「期間」: 「観測」`「時刻」 * 「観測」`「時刻」 ==> 「期間」
	「期間」(a開始, a終了) == atomic(開始 := a開始; 終了 := a終了);
	public pure 内: 「観測」`「時刻」 ==> bool
	内(a時刻) == return 開始 <= a時刻 and a時刻 <= 終了;
end 「期間」

class 「観測履歴」
values
	protected 歩行中判定閾値: real = 0.1;
	protected 時間間隔閾値: nat = 3;
operations
	protected pure 平滑化: () ==>　seq of 「観測」
	平滑化() == is subclass responsibility;
	protected pure 歩行中: () ==>　seq of 「観測」
	歩行中() == return [ 観測 | 観測 in seq 平滑化() & 観測.get距離().get値() > 歩行中判定閾値 ];

	protected pure 期間内観測取得: 「期間」 ==> seq of 「観測」
	期間内観測取得(a期間) ==
		return [ 観測 | 観測 in seq 平滑化() & a期間.内(観測.get時刻()) ];
	public pure 消費カロリー計算: 「量」 * 「期間」 * 「量」 ==> 「量」
	消費カロリー計算(a体重, a期間, a歩幅) == 
		return new 「量」(
			3.0 * ((a歩幅.get値() * 歩数計算(a期間, a歩幅).get値() / 100000.0) / 4.0) * a体重.get値(),
			<KCAL>);
	public pure 歩数計算: 「期間」 * 「量」 ==> 「量」
	歩数計算(a期間, a歩幅) == 
		return new 「量」(歩行距離(a期間).get値() / a歩幅.get値(), <歩数>);
	public pure 歩行距離: 「期間」 ==> 「量」
	歩行距離(a期間) == (
		dcl 総距離: real := 0;
		for 観測 in 歩行中() do
			if a期間.内(観測.get時刻()) then
				総距離 := 総距離 + 観測.get距離().get値();
		return new 「量」(総距離, <M>)
	);
	public pure 歩行時間: 「期間」 ==> 「量」
	歩行時間(a期間) ==  (
		dcl 総時間: real := 0;
		dcl 前回歩行時間: nat := 0;
		for 観測 in 歩行中() do
			if a期間.内(観測.get時刻()) then (
				if 前回歩行時間 < 観測.get時刻() and  観測.get時刻() <= 前回歩行時間 + 時間間隔閾値 then
					総時間 := 総時間 + (観測.get時刻() - 前回歩行時間);
				前回歩行時間 := 観測.get時刻();
			);
		return new 「量」(総時間, <時間>)
	);
	public pure 平均速度: 「期間」 ==> 「量」
	平均速度(a期間) == 
		return new 「量」(歩行距離(a期間).get値() / 歩行時間(a期間).get値(), <速度>);
	async public 追加: 「観測」 ==> ()
	追加(a観測) == is subclass responsibility;
end 「観測履歴」


class 「通常観測履歴」 is subclass of 「観測履歴」
values
	平滑化係数: real = 0.8;
instance variables
	private 観測履歴: seq of 「観測」 := [];
operations
	protected pure 平滑化: () ==>　seq of 「観測」
	平滑化() == (
		dcl 前回観測値: 「観測」 := 観測履歴(1);
		dcl 計算結果: seq of 「観測」 := [前回観測値];
		for 観測 in 観測履歴(2, ..., len(観測履歴)) do (
			計算結果 := [
				new 「観測」(
					前回観測値.get距離().掛ける(1.0 - 平滑化係数).足す(観測.get距離().掛ける(平滑化係数)),
					観測.get時刻())
			] ^ 計算結果;
		);
		return 計算結果;
	);
	protected pure 歩行中: () ==>　seq of 「観測」
	歩行中() == return [ 観測 | 観測 in seq 平滑化() & 観測.get距離().get値() > 歩行中判定閾値 ];
	async public 追加: 「観測」 ==> ()
	追加(a観測) == 観測履歴 := 観測履歴 ^ [a観測];
end 「通常観測履歴」

class 「有酸素運動観測履歴」 is subclass of 「観測履歴」
instance variables
	観測履歴: 「観測履歴」;
functions
	有酸素判定:　seq of 「観測」 -> bool
	有酸素判定(a観測履歴) == true;
operations
	protected pure 平滑化: () ==>　seq of 「観測」
	平滑化() == return 観測履歴.平滑化();
	public 「有酸素運動観測履歴」: 「観測履歴」 ==> 「有酸素運動観測履歴」
	「有酸素運動観測履歴」(a観測履歴) == (観測履歴 := a観測履歴);
	protected pure 歩行中: () ==>　seq of 「観測」
	歩行中() ==  (
		dcl 全有酸素観測: seq of seq of 「観測」 := [];
		dcl 前回歩行時間: nat := 0;
		dcl 有酸素観測: seq of 「観測」 := [];
		for 観測 in 観測履歴.歩行中() do
			if 前回歩行時間 < 観測.get時刻() and  観測.get時刻() <= 前回歩行時間 + 時間間隔閾値 then
				有酸素観測 := 有酸素観測 ^ [観測]
			else (
				if 有酸素判定(有酸素観測) then (
					全有酸素観測 := 全有酸素観測 ^ [有酸素観測]
				);
				有酸素観測 := []
			);
		return conc 全有酸素観測;
	);
	async public 追加: 「観測」 ==> ()
	追加(a観測) == 観測履歴.追加(a観測);
end 「有酸素運動観測履歴」


class 「ボタン」 is subclass of 「同僚」
operations
	async public ボタン押下: () ==> ()
	ボタン押下() == is subclass responsibility;
end 「ボタン」

class 「進むボタン」 is subclass of 「ボタン」
operations
	public 「進むボタン」: 「調停人」 ==> 「進むボタン」
	「進むボタン」(a調停人) == 調停人 := a調停人;
	
	async public ボタン押下: () ==> ()
	ボタン押下() == 調停人.進むボタン押下();
end 「進むボタン」

class 「戻るボタン」 is subclass of 「ボタン」
operations
	public 「戻るボタン」: 「調停人」 ==> 「戻るボタン」
	「戻るボタン」(a調停人) == 調停人 := a調停人;

	async public ボタン押下: () ==> ()
	ボタン押下() == 調停人.戻るボタン押下();
end 「戻るボタン」

class 「決定ボタン」 is subclass of 「ボタン」
operations
	public 「決定ボタン」: 「調停人」 ==> 「決定ボタン」
	「決定ボタン」(a調停人) == 調停人 := a調停人;

	async public ボタン押下: () ==> ()
	ボタン押下() == 調停人.戻るボタン押下();
end 「決定ボタン」

class 「液晶パネル」 is subclass of 「同僚」
operations
	public 「液晶パネル」: 「調停人」 ==> 「液晶パネル」
	「液晶パネル」(a調停人) == 調停人 := a調停人;
	
	async private 画面表示指示: token ==> ()
	画面表示指示(-) == cycles(100) skip;
	
	async public 本日画面描画: () ==> ()
	本日画面描画() == 画面表示指示(mk_token(調停人.本日画面情報()));
	async public 前日画面描画: () ==> ()
	前日画面描画() == 画面表示指示(mk_token(調停人.前日画面情報()));
	async public 前々日画面描画: () ==> ()
	前々日画面描画() == 画面表示指示(mk_token(調停人.前々日画面情報()));
	async public 本日有酸素画面描画: () ==> ()
	本日有酸素画面描画() == 画面表示指示(mk_token(調停人.本日有酸素画面情報()));
	async public 前日有酸素画面描画: () ==> ()
	前日有酸素画面描画() == 画面表示指示(mk_token(調停人.前日有酸素画面情報()));
	async public 前々日有酸素画面描画: () ==> ()
	前々日有酸素画面描画() == 画面表示指示(mk_token(調停人.前々日有酸素画面情報()));
	async public 設定開始画面描画: () ==> ()
	設定開始画面描画() == 画面表示指示(mk_token("設定開始"));
	async public 年設定画面描画: nat ==> ()
	年設定画面描画(a年) == 画面表示指示(mk_token(mk_(a年, 調停人.時刻取得())));
	async public 月設定画面描画: nat ==> ()
	月設定画面描画(a月) == 画面表示指示(mk_token(mk_(a月, 調停人.時刻取得())));
	async public 日設定画面描画: nat ==> ()
	日設定画面描画(a日) == 画面表示指示(mk_token(mk_(a日, 調停人.時刻取得())));
	async public 歩幅設定画面描画: nat ==> ()
	歩幅設定画面描画(a歩幅) == 画面表示指示(mk_token(a歩幅));
	async public 体重設定画面描画: nat ==> ()
	体重設定画面描画(a体重) == 画面表示指示(mk_token(a体重));
	async public USB接続中画面描画: () ==> ()
	USB接続中画面描画() == 画面表示指示(mk_token("USB接続中"));
end 「液晶パネル」

class 「USB端子」 is subclass of 「同僚」
operations
	public 「USB端子」: 「調停人」 ==> 「USB端子」
	「USB端子」(a調停人) == 調停人 := a調停人;
	
	async public USB接続: () ==> ()
	USB接続() == 調停人.USB接続();

	async public USB切断: () ==> ()
	USB切断() == 調停人.USB切断();
	
end 「USB端子」

class 「歩数計調停人」 is subclass of 「調停人」
instance variables
	private 本日画面: 「画面状態」;
	private 前日画面: 「画面状態」;
	private 前々日画面:　「画面状態」;
	private 本日有酸素画面: 「画面状態」;
	private 前日有酸素画面: 「画面状態」;
	private 前々日有酸素画面: 「画面状態」;
	private 設定開始確認: 「画面状態」;
	private 年設定: 「画面状態」;
	private 月設定: 「画面状態」;
	private 日設定: 「画面状態」;
	private 歩幅設定: 「画面状態」;
	private 体重設定: 「画面状態」;
	private USB接続中: 「画面状態」;
	private 現在状態: 「画面状態」;
	private USB接続OFF最終状態: 「画面状態」;

	private 次状態: map 「イベント」 * 「画面状態」 to 「画面状態」;
	private 初回起動: bool := true;
	private 観測履歴: 「観測履歴」 := new 「通常観測履歴」();
	private 歩幅: 「量」 := new 「量」(1, <M>);
	private 体重: 「量」 := new 「量」(50, <KG>);
	private 現在時刻:　「観測」`「時刻」;
	private 液晶パネル: 「液晶パネル」;
	private 進むボタン: 「進むボタン」;
	private 戻るボタン: 「戻るボタン」;
	private 決定ボタン: 「決定ボタン」;
	private USB端子: 「USB端子」;
operations
	public 「歩数計調停人」: () ==> 「歩数計調停人」
	「歩数計調停人」() == (
		現在時刻 := 20210131;
		本日画面 := new 「本日画面」(self);
		前日画面 := new 「前日画面」(self);
		前々日画面 := new 「前々日画面」(self);
		本日有酸素画面 := new 「本日有酸素画面」(self);
		前日有酸素画面 := new 「前日有酸素画面」(self);
		前々日有酸素画面 := new 「前々日有酸素画面」(self);
		設定開始確認 := new 「設定開始確認」(self);
		年設定 := new 「年設定」(self);
		月設定 := new 「月設定」(self);
		日設定 := new 「日設定」(self);
		歩幅設定 := new 「歩幅設定」(self);
		体重設定 := new 「体重設定」(self);
		USB接続中 := new 「USB接続中」(self);
		液晶パネル := new 「液晶パネル」(self);
		進むボタン := new 「進むボタン」(self);
		戻るボタン := new 「戻るボタン」(self);
		決定ボタン := new 「決定ボタン」(self);
		USB端子 := new 「USB端子」(self);
		現在状態 := 年設定;
		USB接続OFF最終状態 := 現在状態;
		次状態 := {
			mk_(<進むボタン押下>, 本日画面) |-> 前日画面,
			mk_(<戻るボタン押下>, 本日画面) |-> 本日画面,
			mk_(<決定ボタン押下>, 本日画面) |-> 本日有酸素画面,
			mk_(<USB接続>,     本日画面) |-> USB接続中,
			
			mk_(<進むボタン押下>, 前日画面) |-> 前々日画面,
			mk_(<戻るボタン押下>, 前日画面) |-> 本日画面,
			mk_(<決定ボタン押下>, 前日画面) |-> 前日有酸素画面,
			mk_(<USB接続>,     前日画面) |-> USB接続中,
	
			mk_(<進むボタン押下>, 前々日画面) |-> 設定開始確認,
			mk_(<戻るボタン押下>, 前々日画面) |-> 前日画面,
			mk_(<決定ボタン押下>, 前々日画面) |-> 前々日有酸素画面,
			mk_(<USB接続>,     前々日画面) |-> USB接続中,
	
			mk_(<進むボタン押下>, 本日有酸素画面) |-> 前日有酸素画面,
			mk_(<戻るボタン押下>, 本日有酸素画面) |-> 本日有酸素画面,
			mk_(<決定ボタン押下>, 本日有酸素画面) |-> 本日画面,
			mk_(<USB接続>,     本日有酸素画面) |-> USB接続中,
	
			mk_(<進むボタン押下>, 前日有酸素画面) |-> 前々日有酸素画面,
			mk_(<戻るボタン押下>, 前日有酸素画面) |-> 本日有酸素画面,
			mk_(<決定ボタン押下>, 前日有酸素画面) |-> 前日画面,
			mk_(<USB接続>,     前日有酸素画面) |-> USB接続中,
	
			mk_(<進むボタン押下>, 前々日有酸素画面) |-> 設定開始確認,
			mk_(<戻るボタン押下>, 前々日有酸素画面) |-> 前日有酸素画面,
			mk_(<決定ボタン押下>, 前々日有酸素画面) |-> 前々日画面,
			mk_(<USB接続>,     前々日有酸素画面) |-> USB接続中,
	
			mk_(<進むボタン押下>, 設定開始確認) |-> 設定開始確認,
			mk_(<戻るボタン押下>, 設定開始確認) |-> 本日画面,
			mk_(<決定ボタン押下>, 設定開始確認) |-> 年設定,
			mk_(<USB接続>,     設定開始確認) |-> USB接続中,
	
			mk_(<進むボタン押下>, 年設定) |-> 年設定,
			mk_(<戻るボタン押下>, 年設定) |-> 年設定,
			mk_(<決定ボタン押下>, 年設定) |-> 月設定,
			mk_(<USB接続>,     年設定) |-> USB接続中,
	
			mk_(<進むボタン押下>, 月設定) |-> 月設定,
			mk_(<戻るボタン押下>, 月設定) |-> 月設定,
			mk_(<決定ボタン押下>, 月設定) |-> 日設定,
			mk_(<USB接続>,     月設定) |-> USB接続中,
	
			mk_(<進むボタン押下>, 日設定) |-> 日設定,
			mk_(<戻るボタン押下>, 日設定) |-> 日設定,
			mk_(<決定ボタン押下>, 日設定) |-> 歩幅設定,
			mk_(<USB接続>,     日設定) |-> USB接続中,
	
			mk_(<進むボタン押下>, 歩幅設定) |-> 歩幅設定,
			mk_(<戻るボタン押下>, 歩幅設定) |-> 歩幅設定,
			mk_(<決定ボタン押下>, 歩幅設定) |-> 体重設定,
			mk_(<USB接続>,     歩幅設定) |-> USB接続中,
	
			mk_(<進むボタン押下>, 体重設定) |-> 体重設定,
			mk_(<戻るボタン押下>, 体重設定) |-> 体重設定,
			mk_(<決定ボタン押下>, 体重設定) |-> 本日画面,
			mk_(<USB接続>,     体重設定) |-> USB接続中,
	
			mk_(<進むボタン押下>, USB接続中) |-> USB接続中,
			mk_(<戻るボタン押下>, USB接続中) |-> USB接続中,
			mk_(<決定ボタン押下>, USB接続中) |-> USB接続中,
			mk_(<USB切断>,     USB接続中) |-> USB接続OFF最終状態
		};		
	);
	public pure 年取得: () ==> nat
	年取得() == return floor(現在時刻 / 10000);
	public pure 月取得: () ==> nat
	月取得() == return floor(現在時刻 / 100) mod 100;
	public pure 日取得: () ==> nat
	日取得() == return 現在時刻 mod 100;
	async public 年更新: nat ==> ()
	年更新(a年) == 現在時刻 := a年 * 10000;
	async public 月更新: nat ==> ()
	月更新(a月) == atomic(
		現在時刻 := 現在時刻 - 月取得() * 100;
		現在時刻 := a月 * 100);
	async public 日更新: nat ==> ()
	日更新(a日) == atomic(
		現在時刻 := 現在時刻 - 日取得();
		現在時刻 := a日 * 10000);
	
	public pure 時刻取得: () ==> 「観測」`「時刻」
	時刻取得() == return 現在時刻;
	async public 時間経過: () ==> ()
	時間経過() == 現在時刻 := 現在時刻 + 1;

	public pure 歩幅取得: () ==> nat
	歩幅取得() == return 歩幅.get値();
	async public 歩幅更新: nat ==> ()
	歩幅更新(a歩幅) == 歩幅 := new 「量」(a歩幅, <M>);

	public pure 体重取得: () ==> nat
	体重取得() == return 体重.get値();
	async public 体重更新: nat ==> ()
	体重更新(a体重) == 体重 := new 「量」(a体重, <KG>);
	
	async public 本日画面描画: () ==> ()
	本日画面描画() == 液晶パネル.本日画面描画();
	async public 前日画面描画: () ==> ()
	前日画面描画() == 液晶パネル.前日画面描画();
	async public 前々日画面描画: () ==> ()
	前々日画面描画() == 液晶パネル.前々日画面描画();
	async public 本日有酸素画面描画: () ==> ()
	本日有酸素画面描画() == 液晶パネル.本日有酸素画面描画();
	async public 前日有酸素画面描画: () ==> ()
	前日有酸素画面描画() == 液晶パネル.前日有酸素画面描画();
	async public 前々日有酸素画面描画: () ==> ()
	前々日有酸素画面描画() == 液晶パネル.前々日有酸素画面描画();
	async public 設定開始画面描画: () ==> ()
	設定開始画面描画() == 液晶パネル.設定開始画面描画();
	async public 年設定画面描画: nat ==> ()
	年設定画面描画(a年) == 液晶パネル.年設定画面描画(a年);
	async public 月設定画面描画: nat ==> ()
	月設定画面描画(a月) == 液晶パネル.年設定画面描画(a月);
	async public 日設定画面描画: nat ==> ()
	日設定画面描画(a日) == 液晶パネル.年設定画面描画(a日);
	async public 歩幅設定画面描画: nat ==> ()
	歩幅設定画面描画(a歩幅) == 液晶パネル.年設定画面描画(a歩幅);
	async public 体重設定画面描画: nat ==> ()
	体重設定画面描画(a体重) == 液晶パネル.年設定画面描画(a体重);
	async public USB接続中画面描画: () ==> ()
	USB接続中画面描画() == 液晶パネル.USB接続中画面描画();

	async public USB接続中ロック取得: () ==> ()
	USB接続中ロック取得() == skip;

	async public USB接続中ロック解除: () ==> ()
	USB接続中ロック解除() == skip;
	
	private pure TOP画面情報: nat * bool ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	TOP画面情報(a過去, a有酸素) == 
		let a観測履歴 = 
			if a有酸素 then 
				new 「有酸素運動観測履歴」(観測履歴) 
			else 
				観測履歴 in
		let a期間 = new 「期間」(a過去, 現在時刻) in
		let a歩数 = a観測履歴.歩数計算(a期間, 歩幅) in
		let a消費カロリー = a観測履歴.消費カロリー計算(体重, a期間, 歩幅) in
		let a歩行距離 = a観測履歴.歩行距離(a期間) in
		let a歩行時間 = a観測履歴.歩行時間(a期間) in
		let a平均速度 = a観測履歴.平均速度(a期間) in
		return mk_(a歩数, a消費カロリー, a歩行距離, a歩行時間, a平均速度);
	public pure 本日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	本日画面情報() == TOP画面情報(0, false);
	public pure 前日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前日画面情報() == TOP画面情報(2, false);
	public pure 前々日画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前々日画面情報() == TOP画面情報(2, false);
	public pure 本日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	本日有酸素画面情報() == TOP画面情報(0, true);
	public pure 前日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前日有酸素画面情報() == TOP画面情報(2, true);
	public pure 前々日有酸素画面情報: () ==> 「量」 * 「量」 * 「量」 * 「量」 * 「量」
	前々日有酸素画面情報() == TOP画面情報(2, true);

	async public 進むボタン押下: () ==> ()
	進むボタン押下() == 現在状態.進むボタン押下遷移();
	async public 戻るボタン押下: () ==> ()
	戻るボタン押下() == 現在状態.進むボタン押下遷移();
	async public 決定ボタン押下: () ==> ()
	決定ボタン押下() == 現在状態.進むボタン押下遷移();

	async public USB接続: () ==> ()
	USB接続() == 現在状態.USB接続遷移();
	async public USB切断: () ==> ()
	USB切断() == 現在状態.USB切断遷移();
	
	async public 観測値追加: 「加速度」 ==> ()
  観測値追加(a加速度) == (
  	観測履歴.追加(new 「観測」(a加速度, 現在時刻取得()))
  );
  public pure 現在時刻取得: () ==> 「観測」`「時刻」
  現在時刻取得() == return 現在時刻;
  
	async public 画面状態変更: 「イベント」 * 「画面状態」 ==> ()
	画面状態変更(aイベント, a状態) == (
		a状態.exit処理();
		現在状態 := 次状態(mk_(aイベント, a状態));
		現在状態.entry処理();
		if aイベント = <USB切断> and a状態 <> USB接続中 then
			USB接続OFF最終状態 := 現在状態
	)
	pre mk_(aイベント, a状態) in set dom 次状態;

sync
	mutex(
		年更新,
		月更新,
		日更新,
		時間経過,
		歩幅更新,
		体重更新,
		USB接続中ロック取得,
		観測値追加);

end 「歩数計調停人」

class 「タイマー」 is subclass of 「同僚」
operations
	public 「タイマー」: 「調停人」 ==> 「タイマー」
	「タイマー」(a調停人) == 調停人 := a調停人;
  async public 時間経過: () ==> ()
  時間経過() == 調停人.時間経過();
end 「タイマー」

class 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == is subclass responsibility;
	async public 実行: () ==> ()
	実行() == is subclass responsibility;
sync
end 「環境タスク」

class 「進むボタン押下タスク」 is subclass of 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == 「歩数計」`調停人.進むボタン押下();
	async public 実行: () ==> ()
	実行() == start(self);
thread
	periodic (1000, 50, 500, 0)(シグナル生成)
end 「進むボタン押下タスク」

class 「戻るボタン押下タスク」 is subclass of 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == 「歩数計」`調停人.戻るボタン押下();
	async public 実行: () ==> ()
	実行() == start(self);
thread
	periodic (1000, 50, 500, 0)(シグナル生成)
end 「戻るボタン押下タスク」

class 「決定ボタン押下タスク」 is subclass of 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == 「歩数計」`調停人.決定ボタン押下();
	async public 実行: () ==> ()
	実行() == start(self);
thread
	periodic (1000, 50, 500, 0)(シグナル生成)
end 「決定ボタン押下タスク」

class 「USB接続タスク」 is subclass of 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == 「歩数計」`調停人.USB接続();
	async public 実行: () ==> ()
	実行() == start(self);
thread
	periodic (1000, 50, 500, 0)(シグナル生成)
end 「USB接続タスク」

class 「USB切断タスク」 is subclass of 「環境タスク」
operations
	async public シグナル生成: () ==> ()
	シグナル生成() == 「歩数計」`調停人.USB切断();
	async public 実行: () ==> ()
	実行() == start(self);
thread
	periodic (1000, 50, 500, 0)(シグナル生成)
end 「USB切断タスク」


system 「歩数計」
instance variables
	public static 調停人: 「調停人」 := new 「歩数計調停人」();
	public static タイマー: 「タイマー」 := new 「タイマー」(調停人);
	public static IMU: 「IMU」 := new 「IMU」(調停人);
	CPU1: CPU := new CPU(<FP>,22E6);
	CPU2: CPU := new CPU(<FP>,22E6);
	CPU3: CPU := new CPU(<FP>,22E6);
	BUS1: BUS := new BUS(<CSMACD>, 72E3, {CPU1, CPU2, CPU3});
operations
	public 「歩数計」: () ==> 「歩数計」
	「歩数計」() == (
		CPU1.deploy(調停人, "歩数計調停人");
		CPU1.setPriority(「歩数計調停人」`進むボタン押下, 60);
		CPU1.setPriority(「歩数計調停人」`戻るボタン押下, 70);
		CPU1.setPriority(「歩数計調停人」`決定ボタン押下, 80);
		CPU1.setPriority(「歩数計調停人」`USB切断, 100);
		CPU1.setPriority(「歩数計調停人」`USB接続, 90);
		CPU2.deploy(タイマー, "タイマー");
		CPU2.setPriority(「タイマー」`時間経過, 100);
		CPU3.deploy(IMU, "IMU");
		CPU3.setPriority(「IMU」`観測, 100);
	);
end 「歩数計」

class Test
traces
	TT: let x in set {1,2,3} in (
		「歩数計」`調停人.進むボタン押下() |
		「歩数計」`調停人.戻るボタン押下() |
		「歩数計」`調停人.決定ボタン押下() |
		「歩数計」`調停人.USB切断() |
		「歩数計」`調停人.USB接続()
	);
end Test