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

Question

我正在尝试在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, Can, Whites, 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

Answer 1

我写了一个简化的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检查以下公式，该公式基本上是问“我们以一个白色bean终止的概率是多少？”：

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)