從DieHard分析TLA+是如何計算狀态的

TLC計算狀态的算法

TLC維護兩個變量：seen和sq。seen用來記錄已經處理過的狀态；sq記錄将要計算的狀态；

問題

描述兩個水壺所有可能的狀态，通過TLA+的寬度周遊機制，暴力搜尋所有的狀态序列（TLA+中稱為behavior）

- 給 3 加侖水壺灌滿水
- 給 5 加侖水壺灌滿水
- 清空 3 加侖水壺
- 清空 5 加侖水壺
- 将 3 加侖水壺的水倒到 5 加侖水壺
- 将 5 加侖水壺的水倒到 3 加侖水壺

TLA+代碼

為了友善調試，在每個子句開始時列印了狀态。

-------------------------- MODULE DieHard  --------------------------
EXTENDS Naturals, TLC
VARIABLES small,big
S == <<small, big>>
Init == /\ Print("Init", TRUE)
        /\ small = 0
        /\ big = 0
TypeOK == /\ Print("TypeOK", TRUE)   
          /\ Print(S, TRUE) 
          /\ small \in 0..3
          /\ big \in 0..5
FillSmall == /\ Print("FillSmall", TRUE) 
             /\ Print(S, TRUE) 
             /\ small' = 3
             /\ big' = big
             /\ Print(S, TRUE) 
FillBig == /\ Print("FillBig", TRUE)  
           /\ Print(S, TRUE) 
           /\ small' = small
           /\ big' = 5
           /\ Print(S, TRUE) 
EmptySmall == /\ Print("EmptySmall", TRUE)  
              /\ Print(S, TRUE) 
              /\ small' = 0
              /\ big' = big
              /\ Print(S, TRUE) 
EmptyBig ==  /\ Print("EmptyBig", TRUE)
             /\ Print(S, TRUE)   
             /\ big' = 0
             /\ small' = small
             /\ Print(S, TRUE) 
SmallToBig ==  /\ Print("SmallToBig", TRUE)
               /\ Print(S, TRUE)  
               /\ IF small + big < 5
                  THEN
                    /\ big' = small + big
                    /\ small' = 0
                    /\ Print(S, TRUE) 
                  ELSE
                    /\ big' = 5
                    /\ small' = small - (5 - big)
                    /\ Print(S, TRUE) 
BigToSmall == /\ Print("BigToSmall", TRUE)
              /\ Print(S, TRUE)  
              /\ IF small + big < 3
                  THEN
                    /\ small' = small + big
                    /\ big' = 0
                    /\ Print(S, TRUE) 
                  ELSE
                    /\ small' = 3
                    /\ big' = big - (3 - small)
                    /\ Print(S, TRUE) 
Next == \/ FillSmall
        \/ FillBig
        \/ SmallToBig
        \/ BigToSmall
        \/ EmptyBig
        \/ EmptySmall
=============================================================================
\* Modification History
\* Last modified Wed Jul 18 15:47:26 CST 2018 by max
\* Created Wed Apr 25 21:42:59 CST 2018 by max

運作結果分析

Init生成的狀态加入sq中；
從sq中取出一個狀态，一次執行Next的幾個子句，每執行一個子句就會得到一個新狀态，加入sq中；
每次得到新狀态都要進行invariant的校驗；
如果新狀态曾經被計算過（seen），直接丢掉，也不進行invariant的計算；

========================   這是第1輪 ========================
==== 初始狀态是<<0, 0>>
"Init"  TRUE
"TypeOK"  TRUE
<<0, 0>>  TRUE
"FillSmall"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE
"TypeOK"  TRUE
<<3, 0>>  TRUE 得到新狀态<<3, 0>>
"FillBig"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE
"TypeOK"  TRUE
<<0, 5>>  TRUE  得到新狀态<<0, 5>>
"SmallToBig"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE
"BigToSmall"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE  \* <<0, 0>>這個狀态在INIT之後就已經在seen中了，被處理過了。是以這個地方直接丢掉這個狀态：不進入sq；不進行invariant校驗；
"EmptyBig"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE
"EmptySmall"  TRUE
<<0, 0>>  TRUE
<<0, 0>>  TRUE
第1輪總結：本輪新增狀态<<3, 0>> 和 <<0, 5>>
========================   開始第2輪 ========================
==== 2.1 從sq中取出第一個狀态<<3, 0>>，開始計算Next
"FillSmall"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
"FillBig"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
"TypeOK"  TRUE
<<3, 5>>  TRUE  得到新狀态<<3, 5>>
"SmallToBig"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
"TypeOK"  TRUE
<<0, 3>>  TRUE  得到新狀态<<0, 3>>
"BigToSmall"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
"EmptyBig"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
"EmptySmall"  TRUE
<<3, 0>>  TRUE
<<3, 0>>  TRUE
==== 2.2 從sq中取出第一個狀态<<0, 5>>，開始計算Next
"FillSmall"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"FillBig"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"SmallToBig"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"BigToSmall"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"TypeOK"  TRUE   
<<3, 2>>  TRUE  得到新狀态<<3,2>>
"EmptyBig"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"EmptySmall"  TRUE
<<0, 5>>  TRUE
<<0, 5>>  TRUE
"FillSmall"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
"FillBig"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
第2輪總結：本輪新增狀态 <<3, 5>>,  <<0, 3>>, <<3,2>>
========================   開始第3輪 ========================
==== 3.1 從sq中取出第一個狀态<<3, 5>>，開始計算Next
"SmallToBig"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
"BigToSmall"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
"EmptyBig"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
"EmptySmall"  TRUE
<<3, 5>>  TRUE
<<3, 5>>  TRUE
==== 3.2 從sq中取出第一個狀态<<0, 3>>，開始計算Next
"FillSmall"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
"TypeOK"  TRUE
<<3, 3>>  TRUE  得到新狀态<<3, 3>>
"FillBig"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
"SmallToBig"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
"BigToSmall"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
"EmptyBig"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
"EmptySmall"  TRUE
<<0, 3>>  TRUE
<<0, 3>>  TRUE
==== 3.3 從sq中取出第一個狀态<<3, 2>>，開始計算Next
"FillSmall"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"FillBig"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"SmallToBig"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"BigToSmall"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"EmptyBig"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"EmptySmall"  TRUE
<<3, 2>>  TRUE
<<3, 2>>  TRUE
"TypeOK"  TRUE
<<0, 2>>  TRUE  得到新狀态<<0, 2>>
第3輪總結：本輪新增狀态<<3, 3>>和<<0, 2>>
========================   開始第4輪 ========================
==== 4.1 從sq中取出第一個狀态<<3, 3>>，開始計算Next
"FillSmall"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
"FillBig"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
"SmallToBig"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
"TypeOK"  TRUE
<<1, 5>>  TRUE  得到新狀态<<1, 5>>
"BigToSmall"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
"EmptyBig"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
"EmptySmall"  TRUE
<<3, 3>>  TRUE
<<3, 3>>  TRUE
==== 4.2 從sq中取出第一個狀态<<0, 2>>，開始計算Next
"FillSmall"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
"FillBig"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
"SmallToBig"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
"BigToSmall"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
"TypeOK"  TRUE
<<2, 0>>  TRUE  得到新狀态<<2, 0>>
"EmptyBig"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
"EmptySmall"  TRUE
<<0, 2>>  TRUE
<<0, 2>>  TRUE
第4輪總結：本輪新增狀态<<1, 5>>和<<2, 0>>
========================   開始第5輪 ========================
==== 5.1 從sq中取出第一個狀态<<1, 5>>，開始計算Next
"FillSmall"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
"FillBig"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
"SmallToBig"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
"BigToSmall"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
"EmptyBig"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
"TypeOK"  TRUE
<<1, 0>>  TRUE   得到新狀态<<1, 0>>
"EmptySmall"  TRUE
<<1, 5>>  TRUE
<<1, 5>>  TRUE
==== 5.1 從sq中取出第一個狀态<<2, 0>>，開始計算Next
"FillSmall"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
"FillBig"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
"TypeOK"  TRUE
<<2, 5>>  TRUE  得到新狀态<<2, 5>>
"SmallToBig"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
"BigToSmall"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
"EmptyBig"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
"EmptySmall"  TRUE
<<2, 0>>  TRUE
<<2, 0>>  TRUE
第5輪總結：本輪新增狀态 得到新狀态<<1, 0>>和<<2, 5>>
========================   開始第6輪 ========================
==== 6.1 從sq中取出第一個狀态<<1, 0>>，開始計算Next
"FillSmall"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
"FillBig"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
"SmallToBig"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
"TypeOK"  TRUE
<<0, 1>>  TRUE   得到新狀态<<0, 1>>
"BigToSmall"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
"EmptyBig"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
"EmptySmall"  TRUE
<<1, 0>>  TRUE
<<1, 0>>  TRUE
==== 6.3 從sq中取出第一個狀态<<2, 5>>，開始計算Next
"FillSmall"  TRUE
<<2, 5>>  TRUE
<<2, 5>>  TRUE
"FillBig"  TRUE
<<2, 5>>  TRUE
<<2, 5>>  TRUE
"SmallToBig"  TRUE
<<2, 5>>  TRUE
<<2, 5>>  TRUE
"BigToSmall"  TRUE
<<2, 5>>  TRUE
<<2, 5>>  TRUE
"TypeOK"  TRUE
<<3, 4>>  TRUE 得到新狀态 <<3, 4>>

從時序的角度看TLA的實行過程

Next == A \/ B \/ C

TLC使用寬度周遊：

1. 第1層周遊後得到的時序是：T1 = A 或 B 或 C；

2. 第2層周遊是基于第1層時序的：T2 = T1 x (A B C)，也就是 T2 = AA 或 AB 或 AC 或 BA 或 BB 或 BC 或 CA 或 CB 或CC；

3. 第3層周遊是基于第2層時序的：T3 = T2 x (A B C)，也就是 T3 = AAA ABA ACA BAA BBA BCA CAA CBA CCA | AAB ABB ACB BAB BBB BCB CAB CBB CCB | AAC ABC ACC BAC BBC BCC CAC CBC CCC

可以看到，TLC會周遊所有可能出現的時序組合。對于一個子句來說，可以在任意時刻發生這個動作。

從DieHard分析TLA+是如何計算狀态的

TLC計算狀态的算法

問題

TLA+代碼

運作結果分析

從時序的角度看TLA的實行過程

繼續閱讀

Codeforces 1417 D. Make Them Equal(思維+構造)

查找算法之二分查找查找算法之二分查找

查找算法學習之二分查找（Python版本）——BinarySearch

CQ V1.0分詞bates(基于雙數組tire樹)—應該是目前最快的中文分詞算法

Command Network(POJ 3164)---定根最小樹形圖模闆題題目描述輸入格式輸出格式輸入樣例輸出樣例分析源程式

開源低帶寬語音編解碼器

241 Different Ways to Add Parentheses（C代碼版）

【趨高機器視覺】機器視覺技術原了解析及解決方案

CSMA/CD1． CSMA/CD的概述2． CSMA 的工作原理3． CSMA/CD控制規程及特點4． CSMA/CD協定5． CSMA/CD的優點6．結束語

極大似然法(ML)與最大期望法(EM)

C++ 第十五周報告1--《冒泡法排序》

筆試面試題目：滑動視窗(二)

資料結構與算法（27）——排序（二）

Dijkstra--簡易版（最短路徑）

GitHub連夜封殺！這份阿裡 10W 字内部 Java 字面試手冊到底有多強？

hdu7108哈希