UPPAAL使用方法
由于剛開始學習時間自動機及其使用方法，對UPPAAL使用不太熟悉，網上能找到的教程很少，摸索了很久終于成功實現一個小例子，所以記錄一下詳細教程。
這里用到的例子參考【UPPAAL學習筆記】1：基本使用示例，詳細信息可自行有鏈接查看，本文重點手把手教學UPPAAL方法，本人也是剛開始學習，有不足或理解有誤的情況歡迎指出。
下面使用幾個小例子展示使用 UPPAAL建模，驗證的方法。
簡單遷移
建模
首先，打開UPPAAL 后，【文件】→【新建模型】
新建模型如下所示：
需要建的模型如下圖，為一個簡單的TS模型
在【編輯器】的模板（【Template】）中，右側通過添加位置、頂點（釘子）和邊進行建模。
位置用名稱和不變量標記。通過下面紅框修改位置類型
通過【編輯location】，在【名字】處為位置命名，在【Invariant】處編輯不變量
通過下圖添加位置
以相同的方法，將其命名為end，通過下圖添加邊，邊用守衛條件（Guard）（例如，e == id）、同步（Sync）（例如，go?）和賦值（Update）（例如，x:=0）標記。
創建模型如下，可以在紅框處修改模板名字，添加參數
在【模型聲明】處將模型實例化，得到Process，此處實例化Template()，名稱與模板名稱相同，由于此處模板沒有參數，故()內為空
// Place template instantiations here.
Process = Template();
// List one or more processes to be composed into a system.
system Process;
建模完成后，對模板進行語法檢查，點擊【工具】→【檢查語法】，若右下角沒有消息，則語法無誤，可繼續進行模擬或驗證。
模擬
在【模擬器】中可以看到這個模型
選中例化對象Process，點擊【下一步】，就可以往下走
當TS走到end狀態后就無路可走了，故【使能遷移】里也沒有選項了
驗證
在【驗證器】中，點擊【添加】，在【待驗證性質】中輸入待驗證性質
性質描述意義如下：
E<> p：存在一條路徑，其中最終成立p，可達屬性（）。A[] p：對于所有路徑，始終成立p，安全屬性（安全屬性的形式是：某些壞事永遠不會發生）。E[] p：存在一條路徑，其中始終成立p，安全屬性。A<> p：對于所有路徑，最終將成立p，活性屬性（活性屬性的形式是：某些事最終會發生）。p --> q：每當成立p時，最終將成立q，活性屬性。
此處驗證兩條性質：
E<> Process.end
A<> Process.end
依次對性質進行驗證，選中需驗證的性質，點擊【開始驗證】即可。驗證結果在下方【驗證進度與結果】中。
此處，E<> Process.end表示存在一條路徑，未來能讓實例Process到達end狀態，顯然，驗證結果通過；
A<> Process.end表示對所有路徑，都能在未來讓實例Process達到end狀態，驗證結果不通過。因為一個TS的Guard條件通過，只表示“這條遷移可以發生”，但不代表一定會發生，可能存在一直停留在start狀態的情況，而不發生這條唯一的遷移，因此不滿足這條性質。
若想讓遷移在一定條件下一定發生，可以為狀態設置不變性，一旦不變性不滿足，就無法停留在這個狀態，迫使其進行遷移。
互斥進入臨界區
新增內容為：
1. 邊用守衛條件（Guard）（例如，e == id）、同步（Sync）（例如，go?）和賦值（Update）（例如，x:=0）標記示例。
2. 模板參數設置及實例化
建模
同步通道和時鐘控制
新增內容：
- 邊的標記方法
- 模板參數設置及實例化
- 一個項目中使用兩個進程模板
- 為狀態添加不變性條件
建模
模型如下圖所示
需建立兩個模板，新建模板方法為：【編輯】【添加模板】
建模方法同上，對邊的標記方法為：右鍵需標記的邊，選擇【編輯edge】
依次填寫，Guard（守衛條件，如，x>=2，e == id），同步通信（Sync，如，go?，reset?），賦值（Update，如，x:=0，e:=id）
建立模型如下圖。
模板P1是一個自循環，Guard條件x>=2時進行Sync（同步通信），往通道reset上發送重置信號（!表示發送，?表示接收)
模板Obs（意為Observer，觀察者），行為就是接收到通道reset上的信號之后，就將全局變量x設置為0（其實是表示時鐘重置，要從后面聲明的地方看出這一點）：
這里要注意taken上有個C，因為它勾選了Commited，被標記Commited的狀態會凍結時間流逝，而且下一次轉移一定從某個Commited狀態開始（要把所有凍結時間的狀態走出去，才能考慮普通的狀態），如果多個狀態被標Commited，它們就按Interleaving算。
模型聲明部分，這里可以不去顯式做例化（為啥？），直接兩個模板拿來用：
// Place template instantiations here.
// Process = Template();
// List one or more processes to be composed into a system.
system P1, Obs;
設置全局變量（全局的【聲明】），其中，x是時鐘（clock），reset是通道（chan）：
// Place global declarations here.
clock x;
chan reset;
模擬
語法檢查通過就可以去模擬，就是P1發信號然后Obs重置然后再回來,因為taken狀態被標Commited，所以到必須使Obs走出這個狀態才能桀紂往下走，即圖中紅框部分：總是先讓Obs回到idle狀態。
驗證
此處驗證兩條性質：
A[] Obs.taken imply x>=2,即對所有路徑的所有狀態都有，如果Obs到達了taken狀態，一定有時鐘x滿足x>=2，驗證是通過的，因為x>=2才能發信號到reset通道上，讓Obs同步接收之后進到taken狀態。
E<> Obs.idle and x>3，即存在某個路徑上某個狀態，Obs在idle狀態閑置時就有x>3了，驗證也是通過的。這條性質直觀上可能讓人感覺不能通過（因為x>=2是P1遷移的條件），但是回想最開始學的，這些Guard條件滿足時只表示“遷移可以發生”，而不是一定會發生，所以P1完全可以x超過3了還不發生遷移，也就不會往reset發信號，所以Obs也就處在最開始的idle狀態了。
為狀態添加不變性條件
對上述E<> Obs.idle and x>3性質的驗證通過，是因為可以一直停留在某個狀態，要解決這個問題，可以為狀態添加一個有關時鐘的不變性條件，當時間流逝使得這個條件不滿足時，就不得不離開這個狀態，發生遷移。
在模板P1中編輯位置loop(雙擊或右鍵編輯)，在【Invariant】里添加x<=3，為P1的loop狀態添加了x<=3的限制，也就是說它最多可以在這里停留到時鐘流到3，就必須執行遷移到別的狀態去了.
驗證性質A[] Obs.taken imply (x>=2 and x<=3)，即只要Obs到了taken狀態，時鐘x一定在2和3之間，驗證通過。
驗證性質E<> Obs.idle and x>2，即可能Obs在idle狀態時，時鐘x是大于2的，驗證通過。因為這個也是滿足loop里x不超過3的不變性的，完全可以等到2.999...。
但是它對性質E<> Obs.idle and x>3就是不滿足的了，因為一旦x>3，P1就必須從loop遷移走，發出的信號讓Obs也同步離開idle。
參考文獻
【1】【UPPAAL學習筆記】1：基本使用示例
)
