PlusCalを使えるようになるにあたって、手近な目標と設定していたことがある。
TLA+版があり、Alloyでも試してみた「ダイ・ハード３ ジャグ問題」のPlusCal版を作ることだ。
TLA+版はどうだったか
参考記事[TLA+] ダイ・ハードジャグ問題から仕様を考える より引用。
TLA+でこれだけであり、無駄なくシンプルだ。
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small, big
TypeOK == /\ small \in 0..3
/\ big \in 0..5
Init == /\ big = 0
/\ small = 0
FillSmall == /\ small' = 3
/\ big' = big \* thats a bad idea. It's not math
FillBig == /\ big' = 5
/\ small' = small \* thats a bad idea. It's not math
EmptySmall == /\ small' = 0
/\ big' = big
EmptyBig == /\ big' = 0
/\ small' = small
SmallToBig == IF big + small =< 5
THEN /\ big' = big + small
/\ small' = 0
ELSE /\ big' = 5
/\ small' = big + small - 5
BigToSmall == IF big + small <= 3
THEN /\ small' = big + small
/\ big' = 0
ELSE /\ small' = 3
/\ big' = big + small - 3
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
NotSolved == big /= 4
=============================================================================
\* Modification History
\* Last modified Fri Feb 22 22:10:06 JST 2019 by komurohiraku
\* Created Sat Jan 05 23:43:04 JST 2019 by komurohiraku
PlusCal版を作る (assert版)
これをPlusCalで書くとどうなるだろう。
短くなるか？（プログラマー的に）読みやすくなるか？
やってみた。
短くはない。読みやすいかの判断はまかせよう。
なぜprocedureでなくmacroにするのかは、Learn TLA+ を読もう。
------------------------------ MODULE DieHard3Jug -------------------------------
EXTENDS Naturals, TLC
CONSTANTS BigCapacity, SmallCapacity
(* --algorithm DieHard3Jug
variables
big \in 0..BigCapacity ;
small \in 0..SmallCapacity ;
define
bigCapacity == BigCapacity - big
smallCapacity == SmallCapacity - small
end define
macro smallToBig() begin
if small > bigCapacity then
big := BigCapacity ;
small := small - bigCapacity
else
big := big + small ;
small := 0
end if ;
end macro;
macro bigToSmall() begin
if big > smallCapacity then
small := SmallCapacity ;
big := big - smallCapacity
else
small := small + big ;
big := 0
end if ;
end macro;
begin start:
big:=0 || small:=0 ;
w: while TRUE do
assert big # 4 /\ big + small # 4 ;
either FillBig: big:=BigCapacity
or FillSmall: small:=SmallCapacity
or EmptyBig: big:=0
or EmptySmall: small:=0
or SmallToBig: smallToBig()
or BigToSmall: bigToSmall()
end either
end while
end algorithm
*)
====
まずは assert をループ内に置いた。
whileにはラベルが必要だが、長いと結果が見辛くなるので短くwとした。
VSCodeで試すので、Modelファイルも必要だ。
SPECIFICATION Spec
CONSTANTS
BigCapacity = 5
SmallCapacity = 3
無事assertに引っかかり、Error Trace に手順が出た。
PlusCal版を作る (不変条件版)
しかしせっかくTLA+には不変チェックがあるのだから、使いたい。
.tlaと.cfgにどう書いたらいいのか試してみたら、こうだった。
PlusCal外から見えるようにdefine内に式を書き、.cfgでそれがINVARIANTであると宣言する。
しかし、初期値を割り当てる瞬間に不成立となってしまう事態を避けるため、bigとsmallの取り得る範囲を明記できなくなってしまった。
変数の宣言はvar = 初期値かvar \in MIN..MAX形式しか書けないからだ。
範囲の宣言もINVARIANTに書けるだろうが、今回は単に外した。
これで無事、式が成り立たなくなった瞬間（今回の例では最後のジャグ操作をした瞬間）に止まるようになった。
------------------------------ MODULE DieHard3Jug -------------------------------
EXTENDS Naturals, TLC
CONSTANTS BigCapacity, SmallCapacity
(* --algorithm DieHard3Jug
variables
big = 0 ;
small = 0 ;
define
\* invariant
NotSolved == big # 4 /\ big + small # 4
\* other
bigCapacity == BigCapacity - big
smallCapacity == SmallCapacity - small
end define
macro smallToBig() begin
if small > bigCapacity then
big := BigCapacity ;
small := small - bigCapacity
else
big := big + small ;
small := 0
end if ;
end macro;
macro bigToSmall() begin
if big > smallCapacity then
small := SmallCapacity ;
big := big - smallCapacity
else
small := small + big ;
big := 0
end if ;
end macro;
begin
w: while TRUE do
either FillBig: big:=BigCapacity
or FillSmall: small:=SmallCapacity
or EmptyBig: big:=0
or EmptySmall: small:=0
or SmallToBig: smallToBig()
or BigToSmall: bigToSmall()
end either
end while
end algorithm
*)
====
SPECIFICATION Spec
CONSTANTS
BigCapacity = 5
SmallCapacity = 3
INVARIANT NotSolved
モヤっとする
正直なところ、assertやINVARIANTで止まったから最短手順が求められたと言う手法はあまり気に入らない。
それが「最短」手順だと言う保証も今のところマニュアル等で見つけられていないし。
この手法は「どれだけ手順を組み合わせても解はない（キリッ」と言っておいて「いやこんな反例があるよ」と指摘させるものだ。
解を求めるアルゴリズムを書かないのは、アルゴリズム言語たるTLA+/PlusCalの正しい使い方でなく、裏ワザ的なものと考えるべきだろう。
... とはいえ、正しい解を求めるアルゴリズムを考えるのは難しそうなのでパスしておこう。