TLA+ 中的咖啡罐问题：无法表达任务

问题描述

我正在尝试在 TLA+ 中为 David Gries’ Coffee Can Problem 建模，但我被困在这部分：

“对于罐头中最初的黑豆和白豆的数量，最后剩下的豆的颜色有什么看法？”

我不知道如何解决这个问题。你能提供一些建议或提示吗？ （也欢迎方法论）

这是我在 TLA+ 中的代码：

------------------------------ MODULE CanBean ------------------------------
EXTENDS Naturals,FiniteSets,Sequences

\* filter <- 2 | max_can <- 5
CONSTANT filter,max_can

VARIABLES picked,Can,Whites,Blacks
vars == <<picked,Blacks>>

IsBlack(i) == i % filter = 0
IsWhite(i) == i % filter /= 0

GetWhite(a,b) == IF IsWhite(a) THEN a ELSE b
GetBlack(a,b) == IF IsBlack(a) THEN a ELSE b
 
AreBothWhite(a,b) == IsWhite(a) /\ IsWhite(b)

Pick == /\ picked = <<>>
        /\ \E a,b \in Can : a/= b /\ picked' = <<a,b>>
        /\ UNCHANGED <<Whites,Blacks,Can>>
             
Process == /\ picked /= <<>>
           /\ LET a == picked[1] b == picked[2] IN
               /\ \/ AreBothWhite(a,b) /\ Whites' = Whites \ {a,b} /\ \E m \in Nat \cap Can : Blacks' = Blacks \cup { filter * m }
                  \/ ~AreBothWhite(a,b) /\ Blacks' = Blacks \ { GetBlack(a,b) } /\ UNCHANGED Whites
               /\ picked' = <<>>
               /\ Can' = Blacks' \cup Whites'
               
Terminating == /\ Cardinality(Can) = 1
               /\ UNCHANGED vars

TypeInvariantOK == /\ \A n \in Can : n \in Nat
                   /\ LET length == Len(picked)
                        IN length = 2 \/ length = 0

Init == /\ picked = <<>>
        /\ Can = 1..max_can
        /\ Blacks = { n \in Can : n % filter = 0 }
        /\ Whites = { n \in Can : n % filter /= 0 }

Next == Pick \/ Process \/ Terminating

=============================================================================
\* Modification History
\* Last modified Sun Feb 21 14:53:34 CET 2021
\* Created Sat Feb 20 19:50:01 CET 2021

解决方法

我编写了一个简化的 TLA+ 规范，您可能会觉得有用：

---------------------------- MODULE CoffeeCan -------------------------------

EXTENDS Naturals

VARIABLES can

Can == [black : Nat,white : Nat]

\* Initialize can so it contains at least one bean.
Init == can \in {c \in Can : c.black + c.white >= 1}

BeanCount == can.black + can.white

PickSameColorBlack ==
    /\ BeanCount > 1
    /\ can.black >= 2
    /\ can' = [can EXCEPT !.black = @ - 1]

PickSameColorWhite ==
    /\ BeanCount > 1
    /\ can.white >= 2
    /\ can' = [can EXCEPT !.black = @ + 1,!.white = @ - 2]

PickDifferentColor ==
    /\ BeanCount > 1
    /\ can.black >= 1
    /\ can.white >= 1
    /\ can' = [can EXCEPT !.black = @ - 1]

Termination ==
    /\ BeanCount = 1
    /\ UNCHANGED can

Next ==
    \/ PickSameColorWhite
    \/ PickSameColorBlack
    \/ PickDifferentColor
    \/ Termination

MonotonicDecrease == [][BeanCount > 1 => BeanCount' < BeanCount]_<<can>>

EventuallyTerminates == <>(ENABLED Termination)

Spec ==
    /\ Init
    /\ [][Next]_<<can>>
    /\ WF_<<can>>(Next)

THEOREM Spec =>
    /\ MonotonicDecrease
    /\ EventuallyTerminates

=============================================================================

您可以通过覆盖 Nat 的定义对其进行模型检查。

正如您所注意到的，从该规范中很容易看出 bean 的数量单调减少（可以使用 MonotonicDecrease 时间属性进行验证），因此该过程必须在有限的步骤数内终止。第二个问题似乎涉及概率，因此它不太适合 TLA+。 TLC 确实具有在 TLA+ 中 simulate basic random systems 的能力，但这太有限了，无法将问题 2 的答案直接编码为系统不变量。有一种名为 PRISM 的正式规范语言被创建来处理概率系统，尽管它的语言远不如 TLA+ 符合人体工程学。

编辑：我为这个问题写了一个 PRISM 规范并发现了一些非常有趣的东西——我们根本不需要处理概率！这是规范 - 看似多余的 min() 和 max() 用法是因为 PRISM 非常挑剔不让变量越界的更新，即使该更新被采用的概率为 0：

dtmc

const int MAX_BEAN = 20;

formula total = black + white;
formula p_two_black = (black/total)*(max(0,black-1)/(total-1));
formula p_two_white = (white/total)*(max(0,white-1)/(total-1));
formula p_different = 1.0 - p_two_black - p_two_white;

init
    total >= 1 & total <= MAX_BEAN
endinit

module CoffeeCan
    black : [0..(2*MAX_BEAN)];
    white : [0..MAX_BEAN];

    [] total > 1 ->
        p_two_black : (black' = max(0,black - 1))
        + p_two_white : (black' = min(2*MAX_BEAN,black + 1)) & (white' = max(0,white - 2))
        + p_different : (black' = max(0,black - 1));
    [] total = 1 -> true;
endmodule

在插入一些测试初始值后，我使用 PRISM 来检查以下公式，它基本上是问“我们以单个白豆终止的概率是多少？”：

P=?[F black = 0 & white = 1]

你知道我发现了什么吗？当您开始使用偶数个白豆时，概率为零，而当您开始使用奇数个白豆时，概率为 1！我们可以将此断言编码为 PRISM 将验证为真的属性：

P>=1 [mod(white,2) = 1 => (F black = 0 & white = 1)]
P>=1 [mod(white,2) = 0 => (F black = 1 & white = 0)]

回想起来这是显而易见的，因为白豆的数量只会减少两个。因此，如果您从偶数个白豆开始，您将获得零个白豆，如果您从奇数个白豆开始，您将获得一个白豆。您可以将此时间属性添加到上述 TLA+ 模型中以进行检查：

WhiteBeanTermination ==
    IF can.white % 2 = 0
    THEN <>(can.black = 1 /\ can.white = 0)
    ELSE <>(can.black = 0 /\ can.white = 1)