1

我正在尝试在 TLA+ 中模拟David Gries 的咖啡罐问题，但我被困在这一部分：

“你能说最后剩下的豆子的颜色与最初在罐头里的黑豆和白豆的数量有关吗？”

我不知道如何处理这个问题。您能否提供一些建议或提示？（也欢迎提供方法）

这是我在 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
4

1 回答 1

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 的数量单调减少（可以通过MonotonicDecreasetemporal 属性验证），因此该过程必须在有限数量的步骤内终止。第二个问题似乎涉及概率，因此不太适合 TLA+。TLC 确实具有在 TLA+ 中模拟基本随机系统的能力，但这太有限，无法直接将问题 2 的答案编码为系统不变量。有一种称为PRISM的正式规范语言用于处理概率系统，尽管它的语言比 TLA+ 更不符合人体工程学。

编辑：我为这个问题写了一个棱镜规范，发现了一些非常有趣的东西——我们根本不需要处理概率！这是规范 - 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]

你知道我发现了什么吗？当你从偶数个白豆开始时，概率为零，当你从奇数个白豆开始时，概率为一！我们可以将此断言编码为 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)
于 2021-02-21T17:12:52.627 回答