網路協議分析與設計——Spin實驗（尚不完善）
參考教材：《網路協議工程》吳禮發，電子工業出版社，2011.4
實驗環境：Ubuntu 18.04.1 LTS，Windows 10，VMware 15.0.2。
（一）Spin入門（iSpin究竟是怎麼裝上去的？是tar.gz的install.sh還是sudo apt install spin？）
Ubuntu下直接一句sudo apt install spin，就不make了。基本就裝好Spin了，想要最新版Spin的話就手動下載：
Spin - Formal Verification
http://spinroot.com/spin/whatispin.html
點選下方download，進入介面後下載spin649_linux64.gz。
拷貝到虛擬機器桌面，gunzip解壓後滑鼠右鍵點選解壓後的檔案，將它重新命名為spin，複製到/usr/bin下：
檢視版本，回顯6.4.9說明一切順利：
其他需要安裝的：（有些可能裝過了，不管咋樣挨個試一遍都裝沒裝全）
sudo apt-get install byacc
sudo apt-get install tcl
sudo apt-get install tk8.5
sudo apt-get install graphviz //可以圖形化顯示執行結果
sudo apt-get install pan
（二）小試牛刀
開啟iSpin，先實驗個簡單的資料鏈路層RDT 1.0協議（書P152）
（這在裡面輸程式碼對齊不咋方便，不如在VS2017裡輸好了直接拷進來，再開啟）
點選選單欄的Simulate/Replay，設定maximum number of steps=300，點選“(Re)Run”開始模擬：
下面中間的黑色視窗是命令列形式，如果在shell裡執行iSpin右上角顯示的Background command executed，得到的結果就是中間窗口裡的樣子。
再看時序圖，SENDER和RECEIVER都是0→1→2→0→……不斷迴圈，這正是RDT 1.0協議：通道沒有誤碼，也不會丟失報文，接收方有無限接受能力，一方傳送，一方接收。這是個理想狀態下的協議。
接下來看看一般性驗證：點選選單欄Verification，選擇“safety”，點選Run，結果如下圖，結果基本與書中P154圖6-3一致。
無進展迴圈驗證則點選Liveness中的non-progress cycles，再點選一次Run，結果如下圖所示，與書中P154圖6-4一致：
（三）實驗一：思考題6-5
報文和應答均會出錯，且都丟失，接收方沒有無限接收能力——實用的停等協議。請用PROMELA進行描述，並用SPIN模擬執行、一般性驗證、無進展迴圈驗證和人為加入錯誤進行認證。
參考連結：
1.模型檢測工具spin在ubuntu下的安裝方法 - 泥瓦匠的專欄 - CSDN部落格
https://blog.csdn.net/tiefanhe/article/details/8176418