PlusCal で ダイ・ハード３ ジャグ問題 

PlusCalを使えるようになるにあたって、手近な目標と設定していたことがある。
TLA+版があり、[Alloyでも試してみた](https://qiita.com/jpwgad/items/3bdf4fd6cd7e36619e06)「ダイ・ハード３ ジャグ問題」のPlusCal版を作ることだ。

# TLA+版はどうだったか

参考記事[[TLA+] ダイ・ハードジャグ問題から仕様を考える](https://dev.classmethod.jp/articles/tlaplus-diehard-jug-problem-spec/) より引用。
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+](https://learntla.com/concurrency/procedures-and-macros/) を読もう。

```pluscal:DieHard3Jug.tla（assert版）
------------------------------ 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ファイルも必要だ。

```tla:DieHard3Jug.cfg
SPECIFICATION Spec

CONSTANTS 
    BigCapacity = 5
    SmallCapacity = 3
```
<img width="1455" alt="DH3assert.png" src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/4d675989-f9f3-a513-0c6f-d593f59cff55.png">
無事`assert`に引っかかり、Error Trace に手順が出た。

# PlusCal版を作る (不変条件版)

しかしせっかくTLA+には不変チェックがあるのだから、使いたい。
`.tla`と`.cfg`にどう書いたらいいのか試してみたら、こうだった。
PlusCal外から見えるように`define`内に式を書き、`.cfg`でそれが`INVARIANT`であると宣言する。

しかし、初期値を割り当てる瞬間に不成立となってしまう事態を避けるため、bigとsmallの取り得る範囲を明記できなくなってしまった。
変数の宣言は`var = 初期値`か`var \in MIN..MAX`形式しか書けないからだ。
範囲の宣言もINVARIANTに書けるだろうが、今回は単に外した。
これで無事、式が成り立たなくなった瞬間（今回の例では最後のジャグ操作をした瞬間）に止まるようになった。

```pluscal:DieHard3Jug.tla（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
*)
====
```

```tla:DieHard3Jug.cfg
SPECIFICATION Spec

CONSTANTS 
    BigCapacity = 5
    SmallCapacity = 3

INVARIANT NotSolved
```

# モヤっとする

正直なところ、`assert`や`INVARIANT`で止まったから最短手順が求められたと言う手法はあまり気に入らない。
それが「最短」手順だと言う保証も今のところマニュアル等で見つけられていないし。

この手法は「どれだけ手順を組み合わせても解はない（キリッ」と言っておいて「いやこんな反例があるよ」と指摘させるものだ。
解を求めるアルゴリズムを書かないのは、アルゴリズム言語たるTLA+/PlusCalの正しい使い方でなく、裏ワザ的なものと考えるべきだろう。

... とはいえ、正しい解を求めるアルゴリズムを考えるのは難しそうなのでパスしておこう。