UPPAAL学习
UPPAAL过程的节点
1.初始位置
过程的开始。每个进程必须有一个初始位置。初始位置用一个双圆圈标记。
2.紧急位置
紧急位置冻结时间。该过程通过紧急节点进行转换，没有任何延迟。
3.已提交位置
与紧急位置类似，承诺位置冻结时间。此外，如果任何进程处于承诺位置，则下一个转换必须从其中一个承诺位置进行。
不变量
- 表达时钟和整数变量值的条件，这些条件必须为真才能保持在该位直。
- 它被评估为布尔值。
- 只能使用时钟变量、整数变量和常量(或此类数组)
边
- 两个控制节点(位置)之间的线。
- 边被注释/标记为选择、守卫、同步和更新。（selections,guards,synchronizations and updates）
1.选择
语法 lD ‘:’ Type
选择ID是一个非确定性标识符。这些标识符可以作为变量，出现在此边界的其他标签(如守卫、同步或更新)中。支持的类型包括有界整数和标量集合。
它可以用作数组索引来决定要同步的通道，并作为参数在后续调用函数时使用。
例如，i : int[0,3]
因此，将在范围[0,3]内有一个随机值可以作为通道a的索引(chan a[4];)
2.守卫
- 在必须满足的条件边缘表达，以进行转换。
- 它应该是正确的，并且是无副作用的(即不允许有赋值)布尔表达式
- 只允许时钟变量、整数变量和常量(或此类数组)
3.同步
同步意味着两个(或更多)进程在一步中进行转换(改变位置)。
为了同步进程，它们的边应标记一个通道变量(在前面声明，例如chan Push)，然后为其中一个变量加上"!“，为另一个变量加上”?"。(例如，Push! 和 Push?)。
4. 更新
当进行一个转换时，可以评估该边的更新(赋值)表达式。此表达式的副作用会改变系统的状态(例如: x=3;)。
注意，你也可以使用:=运算符。
正态位置的性质
是否可以在P0的S1位置等待(正常位置)
- E<> P0.S1 and P0.x>0 //真还是假?
Time in P0 always >=0
- A[] P0.x >= 0 //真还是假?
这个查询的结果是什么:
- A[] PO.S1 and P0.x >=0
- 它是FALSE，因为A[]意味着在所有状态下都适用，而不仅仅是P0.S1
UPPAAL中的查询类型
- E-存在一个路径
- A-对所有路径
- []-路径中的所有状态
- <>-路径中的某些状态
支持以下组合:
- 'A[]'表达式
- 'E<>'表达式
- 'E[]'表达式
- ‘A<>’ 表达式
- 表达式 -->表达式
可达性属性
E<>p-可以达到一个状态，使得p得到满足。
p在(至少)一个可达状态中为真。
安全性和活性
任何系统的正确性总是以以下术语来表达的：安全性和活性
安全性
保证坏事永远不会发生
表示永远不会发生坏事的属性
活性
保证好事最终会发生：
最终 ==并不意味着有时间限制，但如果你让系统运行足够长的时间，那么…
表示好事最终会发生。
例子
交叉路口的交通信号灯
- 安全性
只有一个方向应该有绿灯
- 活性
每个方向最终都应该有绿灯
不变性
A[]p - p 保持不变。
P 在所有可达状态中为真。
变体
E[]p存在一条路径使得 p总是为真
活性属性
在简单形式中，活体性表达为:
路径公式A<>p，表示p最终被满足。
活性检测
或者导致或响应属性，表示为 p -->q，读作当p 被满足时，最终q也会被满足。
例如：每当发送一条消息时，最终它会被接收。
整数（Integer）：
使用关键字 int 声明。
取值范围为 -32768 到 32767。
布尔型（Boolean）：
使用关键字 bool 声明。
布尔变量只有两个取值：
- true（真）
- false（假）
（注意：true 和 false 必须小写，UPPAAL 区分大小写）
Uppaal 中的声明语法：
UPPAAL 的声明语法与 C 语言类似。
整数（Integer）
int num1, num2;
两个默认取值范围的整型变量 num1 和 num2。
int[0,100] a;
一个取值范围为 0 到 100 的整型变量 a。
int a[100];
一个包含 100 个元素的整型数组。
int a[2][3];
一个二维整型数组。
int[0,5] b = 0;
一个取值范围为 0 到 5 的整型变量 b，并初始化为 0。
布尔型（Boolean）
bool yes = true;
一个布尔变量 yes，初始值为 true。
bool b[8], c[4];
两个布尔数组 b 和 c，分别包含 8 个和 4 个元素。
常量（Const）
const int a = 1;
一个整型常量 a，值为 1。
const bool No = false;
一个布尔常量 No，值为 false。
紧急通道（Urgent Channels）
当一个通道被声明为紧急通道时，通过该通道的同步优先于普通通道，并且该转换必须立刻执行，不允许延迟。
使用关键字 urgent chan 声明。
- 紧急同步的边上 不允许 使用时钟守卫（clock guard）。
- 允许 使用不变式（invariants）和数据变量守卫。
- 注意：如果需要在某个状态冻结时间，可以将该位置声明为 Urgent 或 Committed。
广播通道（Broadcast Channels）
广播通道允许一对多同步。
带同步标签 e! 的边会向通道 e 发送一个广播，任何带同步标签 e? 且处于可触发状态的边都会与之同步。
例子： 用户向智能灯控系统中的灯控器发送广播信号 Push!，多个组件上的 Push? 同时接收。
声明示例
clock x, y;
两个时钟 x 和 y。
chan d;
一个普通通道 d。
urgent chan a, b, c;
三个紧急通道。
broadcast chan c;
一个广播通道 c。
函数与过程（Functions & Procedures）
可以与其他声明一同书写。
Add（加法）
以下函数返回两个整数的和，参数为值传递（call by value）：
int add(int a, int b)
{return a + b;
}
Swap（交换）
以下过程交换两个整数引用参数的值（call by reference）：
void swap(int &a, int &b)
{int c = a;a = b;b = c;
}
函数可用于：
- 赋值（Assignment）
- 比较（Comparison）
- 位置（Locations）
- 边（Edges）
过程（Procedure）可用于除以下情况外的任意位置：
- 赋值（Assignment）
- 比较（Comparison）