TLA+でパズル (1) Lock Challenge

「Alloyでパズル (16)」でやった Lock Challenge を、 PlusCal でもやってみようと思った。
が、PlusCal での書き方がわからず、TLA+版の方が先にできてしまった。

問題

Alloyでパズル (16) Lock Challenge を参照。

TLA+版

まだ『Specifying Systems』をほとんど読んでいないので、TLA+の書き方がよくわからない。
IF-THEN-ELSE版はできたので、もっとうまく書けないものか調査中。
現段階では、Match()をSequences利用版に置き換えている。

LockChallenge.tla

---- MODULE LockChallenge ----
EXTENDS Naturals, TLC, Sequences
VARIABLES sol1, sol2, sol3

WellPlace(a,b,c) == (IF a=sol1 THEN 1 ELSE 0)
                  + (IF b=sol2 THEN 1 ELSE 0)
                  + (IF c=sol3 THEN 1 ELSE 0)
Match(a,b,c) == LET Mt(n) == n \in {sol1,sol2,sol3}
                IN Len(SelectSeq(<<a,b,c>>,Mt))
Hint(a,b,c,matched,wellPlaced) == Match(a,b,c)=matched 
                               /\ WellPlace(a,b,c)=wellPlaced

Init == /\ sol1 \in 0..9
        /\ sol2 \in 0..9
        /\ sol3 \in 0..9
     \* lock
        /\ Hint(6,8,2, 1,1)
        /\ Hint(6,1,4, 1,0)
        /\ Hint(2,0,6, 2,0)
        /\ Hint(7,3,8, 0,0)
        /\ Hint(7,8,0, 1,0)
     \* another lock
        \* /\ Hint(1,2,3, 0,0)
        \* /\ Hint(4,5,6, 0,0)
        \* /\ Hint(7,8,9, 1,0)
        \* /\ Hint(9,0,0, 3,1)
     \* result
        /\ PrintT(<<sol1,sol2,sol3>>)

vars == << sol1,sol2,sol3 >>
Next == UNCHANGED vars
Spec == Init /\ [][Next]_vars
====

LockChallenge.cfg

SPECIFICATION Spec

結果

Output
<<0, 4, 2>>

PlusCal版

別記事を起こすほどのことでもない気がするのでひっそり追記で。
今頃気づいたのですが、４つ目と５つ目のヒントは不要なんですね。

LockChallengePlusCal.tla

---- MODULE LockChallengePlusCal ----
EXTENDS Naturals, TLC, Sequences

(* --algorithm LockChallengePlusCal
variable sol1 \in 0..9,  sol2 \in 0..9,  sol3 \in 0..9;

define
WellPlace(a,b,c) == (IF a=sol1 THEN 1 ELSE 0)
                  + (IF b=sol2 THEN 1 ELSE 0)
                  + (IF c=sol3 THEN 1 ELSE 0)
Match(a,b,c) == LET Mt(n) == n \in {sol1,sol2,sol3}
                IN Len(SelectSeq(<<a,b,c>>,Mt))
Hint(a,b,c,matched,wellPlaced) == Match(a,b,c)=matched /\ WellPlace(a,b,c)=wellPlaced
end define;

begin
    if (Hint(6,8,2, 1,1)
     /\ Hint(6,1,4, 1,0)
     /\ Hint(2,0,6, 2,0)
     /\ Hint(7,3,8, 0,0)
     /\ Hint(7,8,0, 1,0)
    ) then
        print <<sol1,sol2,sol3>>;
    end if;
end algorithm *)
====