Lustre/Scade/Swan 语义性质中的因果性分析介绍
在《同步反应式系统》的第一课中，简要讨论了同步语言的因果分析。在本篇中，将讨论对课件该部分的学习笔记。
循环的定义
对同步数据流语言，如Lustre/Scade/Swan等，所编写的程序在需要满足“不包含循环”的性质。这里的循环（Cyclic）特别指的是：
- 方程组无解
比如方程 x = x + 1 无解。
比如如下方程组
x = y + 1
y = x + 2
同样无解。
2）方程组有多个解
比如方程 x = x 有多个解。
而下面的方程组
y = x
x = y
同样有多个解。有多个解的方程组，就有“非确定性”的性质。
不论是对无解的方程组情况，还是有多个解的方程组的情况，在关键嵌入式系统中，只能接受方程组有唯一解的情形。并且方程组有唯一解的性质，需要在程序编译期就能够被保证。方程组有唯一解，则认为方程组中没有循环，没有因果错误。
语义的因果性质
对仅使用基本特性的Lustre/Scade程序，检查因果性质通过下面的方法就能够充分检查：
- 对程序生成依赖图。在依赖图的构造中，对
pre, 以及fby运算的右侧操作数，不增加依赖。即对需要依赖前序周期变量的情况，不增加依赖。 - 对构造的依赖图进行拓扑排序，检查是否存在环。如果没有环，则不存在因果性质的违反。
样例分析
对下面的Lustre程序
node regulator (cruise_speed, speed : float; rst : bool)
returns (throttle : float);
var delta, aux : float;
letdelta = cruise_speed − speed;throttle = delta ∗ 10.0 + aux ∗ 0.2;aux = if rst then delta else delta + aux;
tel
程序的依赖关系如下面描述
delta -> {cruise_speed, speed}
throttle -> {delta, aux}
aux -> {aux, delta, rst}
注意到 aux -> aux，产生了环。因此这段 Lustre 程序存在因果性质问题。
模块化因果分析
对下面的程序，是否符合因果性？
node direct(x : int)
returns (y : int);
lety = x;
telnode main1(w : int)
returns (z : int);
letz = direct(z);
tel
由于 z -> z 因此不符合因果性质。
那对下面的程序呢？
node delayed(x : int)
returns (y : int);
lety = 0 fby x;
telnode main2(w : int)
returns (z : int);
letz = delayed(z);
tel
由于delayed延迟了一个周期，因此符合因果性质。对验证这类情况程序的因果性，可通过专有的类型系统进行分析。
不过在 Scade One 工具中，仍然以因果性问题拒绝了这类程序。
那对下面的程序呢？
node plumbing(x, y : int)
returns (dx, dy : int);
letdx = x;dy = y;
telnode main3(w : int)
returns (z : int);
var v : int;
letz, v = plumbing(v, w);
tel
由于依赖关系可构造为 w -> y -> dy -> x -> dx -> z，没有生成环，所以符合因果性。
在Scade One 中，该程序能够通过因果分析检查。
程序是否能通过因果检查，也和具体的编译机制有关。详细内容可参考课件中引用的文献。