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状态的情况，而不发生这条唯一的迁移，因此不满足这条性质。
若想让迁移在一定条件下一定发生，可以为状态设置不变性，一旦不变性不满足，就无法停留在这个状态，迫使其进行迁移。
互斥进入临界区
新增内容为：
- 边的标记方法
- 模板参数设置及实例化
建模
模型如下图
同步通道和时钟控制
新增内容：
- 模板参数设置及实例化
- 一个项目中使用两个进程模板
- 为状态添加不变性条件
建模
模型如下图所示
需建立两个模板，新建模板方法为：【编辑】【添加模板】
建模方法同上，对边的标记方法为：右键需标记的边，选择【编辑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：基本使用示例
