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 确实有能力 simulate basic random systems in TLA+, but this is too limited to directly encode the answer to question two as a system invariant. There's a formal specification language called 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)

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

Coffee Can Problem in TLA+ : cannot express a task

formal-verification

formal-methods

language-specifications

tla+