薬飲み過ぎ防止アルゴリズムの検証
概要
「数字であそぼ。」という数学を学ぶ大学生の漫画があります。 この34話(コミックス6巻)にて、認知症が進み始めた主人公の祖父に確実に1日1個だけ薬を飲ませるためのアルゴリズムを考案する話があります。このアルゴリズムを形式手法のツールであるTLA+で記述し主人公たちの意図どおり動くのか検証してみました。
環境
| 名前 | バージョン |
|---|---|
| OS | Ubuntu 20.04 |
| CPU | AMD Ryzen 9 3900XT |
| TLA+ Toolbox | 1.7.1 |
問題
主人公たちが挑んだ問題は以下です。
祖父はある薬を毎日1錠のみ飲まなければならない。毎日必ず数回薬を飲むことを思い出すが飲んだかどうかを忘れることがあり、結果1日に2錠以上飲んでしまう。シンプルな対策方法を求めよ。ピルケースなどは祖父のプライドの問題で使用不可。
主人公たちが提案したアルゴリズム
'飲む瓶'と'備蓄瓶'を用意し、祖父がアルゴリズム(手順書として)に従ってそれらに入っている薬の個数をコントロールして今飲んで良いのかどうかを'飲む瓶'内の個数で表現するというのが主人公たちの答えでした。
まず、開始時点では1個飲んだこととして補充を行います。
この補充方法は以下のとおり。
なお、'飲む瓶'の量の調整のために'備蓄瓶'に戻すマイナスの補充は発生しないことが後の検証で分かります。
以下は薬を思い出した時に行う、飲んで良いかの判断と補充の一連のメインのアルゴリズムです。補充方法は上記と同一です。
例えば、9月29日に'飲む瓶'に1個入っていたとします。その場合飲んで良い数なので1錠飲み、'備蓄瓶'から'飲む瓶'に2錠を補充します。同日にもう一度アルゴリズムを作動させても'飲む瓶'の薬は2錠であり、飲んで良い個数ではないので飲まないし補充もしません。次の9月30日になると、'飲む瓶'の薬は2錠であり飲んで良い数ですので1錠'飲む瓶'から取り出して飲み、月末日なので3個になるように補充、、、となります。
検証
以下は上記アルゴリズムのTLA+による表現です。日数が28〜31日の月を定義し、それらの月内での日付進行、月間での月の進行をシミュレートしています。3月などの31日の月から4月などの30日の月という普通の月間の進行やうるう月発生時の29日の月から31日の月への進行などです。現実に存在しない月の進行の組み合わせなども含んでいます。
medicine.tla
EXTENDS Integers, Naturals, TLC
CONSTANT MonthLens, BuyNum
VARIABLE bottle, \* 飲む瓶
stock, \* 備蓄瓶
drunkMedInDayNum, \* その日に飲んだ薬の数
d, \* その月内の日
mlen, \* その月の日数 28~31日
triedNum, \* その日に薬のことを思い出して飲んで良いのか一連の判断を下した回数。
goodMed \* 1日1錠のみ薬を飲み続けているか
vars == <<bottle, stock, drunkMedInDayNum, d, mlen, triedNum, goodMed>>
\* 飲む瓶に補充後に、飲む瓶に在るべき薬の総数
getMedNumShouldBe == CASE d = mlen -> 3 \* 月末
[] (d /= mlen /\ d % 2 = 0) -> 1 \* 月末以外の偶数日
[] (d /= mlen /\ d % 2 /= 0) -> 2 \* 月末以外の奇数日
\* 現時点で飲んで良いと判断する'飲む瓶'内の個数
getNumToDrink == CASE d = 1 -> 3 \* 1日
[] (d /= 1 /\ d % 2 /= 0) -> 1 \* 1日以外の奇数日
[] (d % 2 = 0) -> 2 \* 偶数日
\* 初期値。すでに1個飲んでいることとしている。
Init == /\ drunkMedInDayNum = 1
/\ mlen \in MonthLens
/\ d \in 1..mlen
/\ stock = BuyNum - getMedNumShouldBe
/\ bottle = getMedNumShouldBe
/\ triedNum = 1
/\ goodMed = TRUE
\* 型チェック
TypeOK == /\ bottle \in Nat
/\ stock \in Nat
/\ drunkMedInDayNum \in Nat
/\ mlen \in MonthLens
/\ d \in 1..mlen
/\ triedNum \in Nat
/\ goodMed \in BOOLEAN
\* 次の日に移る行動
NextDate == /\ drunkMedInDayNum' = 0 \* 飲んだ個数のリセット
/\ triedNum' = 0 \* 飲もうとした回数のリセット
/\ goodMed' = (goodMed /\ (drunkMedInDayNum = 1)) \* 毎日1錠のみ飲み続けているかの更新
/\ \/ /\ d < mlen \* 月末ではない場合に日付を加算して次の日へ
/\ d' = d + 1
/\ UNCHANGED <<bottle, stock, mlen>>
\/ /\ d >= mlen \* 月末は次の月の日数を更新し1日へ
/\ d' = 1
/\ mlen' \in MonthLens
/\ UNCHANGED <<bottle, stock>>
\* '備蓄瓶'から'飲む瓶'への補充行動
suppliedNumFromStock == getMedNumShouldBe - (bottle -1)
SupplyFromStock == /\ \/ /\ 0 > (stock - suppliedNumFromStock) \* 補充が'備蓄瓶'の薬で足りない場合はBuyNum分を購入し'備蓄瓶'へ
/\ stock' = stock + BuyNum - suppliedNumFromStock
\/ /\ 0 <= (stock - suppliedNumFromStock) \* 補充が可能な分'備蓄瓶'に残っている場合は取り出す
/\ stock' = stock - suppliedNumFromStock
/\ bottle' = (bottle - 1) + suppliedNumFromStock \* '飲む瓶'へ補充
\* 飲む行動
TryDrink == /\ bottle = getNumToDrink \* '飲む瓶'の数が、飲むことが許可されている数か判定する条件
/\ drunkMedInDayNum' = drunkMedInDayNum + 1 \* その日に飲んだ数を加算
/\ SupplyFromStock \* 飲んだ分の補充行動
/\ UNCHANGED <<d, mlen, goodMed>>
\* 統合行動
Next == \/ /\ triedNum > 0 \* 1回以上薬を飲もうとしたら次の日に進むことを許可する
/\ NextDate
\/ /\ TryDrink \* 薬を飲もうとする行動
/\ triedNum' = triedNum + 1
\* 時相仕様
Spec == /\ Init \* 初期化
/\ WF_vars(NextDate) \* NextDateにWeakly fairness設定
/\ [][Next]_vars \* Nextが呼ばれるか変化しないか
Inv == /\ TypeOK
/\ goodMed \* 毎日一回のみ飲み続けているか
/\ suppliedNumFromStock >= 0 \* '飲む瓶'への補充量は常に0以上か。即ちマイナスの補充は無いか。
Liveness == /\ []<>(d = 1) \* 日付が回り続けているか
/\ []<>(d = 15)
モデルは以下のように設定しました。
結果
以下のようにエラー無しで検証に成功しました。
考察
この作品で示された問題は分散サービスなどで求められるようなベキ等性を暗に要求するものであり、主人公たちの提示したアルゴリズムはそれを満たすものでした。アルゴリズムは'その日にまだ飲んでいないか否か'の状態と'飲む瓶内の個数'との対応を設定するものであり、その対応は日によって変化するものでした。面白いことに'飲む瓶内の個数'は対応を取れる限りの能力が備わっていれば良いために、例えば個数を以下のように変化させてもTLA+の検証は通過します。単なるタグとして整数が機能しているわけなのでタグ間で重複しなければよいのです。※マイナスの補充が発生しますが。
\* 飲む瓶に補充後に、飲む瓶に在るべき薬の総数
getMedNumShouldBe == CASE d = mlen -> 5 \* 月末
[] (d /= mlen /\ d % 2 = 0) -> 6 \* 月末以外の偶数日
[] (d /= mlen /\ d % 2 /= 0) -> 22 \* 月末以外の奇数日
\* 現時点で飲んで良いと判断する'飲む瓶'内の個数
getNumToDrink == CASE d = 1 -> 5 \* 1日
[] (d /= 1 /\ d % 2 /= 0) -> 6 \* 1日以外の奇数日
[] (d % 2 = 0) -> 22 \* 偶数日
ピルケースなどを使う方法と比べて確かに手順は面倒ですが、格納リソースは効率良く使えていてなんと言うか数学的に圧縮された手法のように見えます。
終わりに
漫画「数字であそぼ。」は割と日常系なのですが込み入った内容が時々でてきて毎回読み飛ばしてしまいます。しかし、ふとしたときにちゃんと内容を理解するために再読したくなるんですよね。その読ませるところがこの漫画の魅力と感じています。他にも読み飛ばしてしまって理解/検証しきっていない話もあるので検証してブログ書いてみます。
TLA+の記述途中ではクリティカルな考慮漏れが1つあったのですが、ChatGPT5が見つけてくれて修正できました。設計時点でのモデルに基づく記述なので、この時点で考慮漏れがあったら見つけづらいです。目で見て判断できるまでにチェックするか、ChatGPTを活用するのが良いのでしょうか。検討する余地があります。LivenessやInvariantの記述をより頑強にするというのが良いのかもしれません。
Discussion