Page 78 - 《软件学报》2021年第12期

3742 Journal of Software 软件学报 Vol.32, No.12, December 2021

4),依据缺省的事件筛选策略P default 判断该事件是否要排除掉,即:若 E 发生后Ψ 不成立,则需将 E
X
排除;

′
• 筛选后的事件集 E 与 Pairs 一并送至 EE 中间表示生成模块处理,该模块对 Pairs 中的每个元组(C j ,
X
X
A j )调用 SameActionRules( E ′ ,Ψ ,C ,A ,W )(见算法 5),产生动作序列为A j 的 EE 规则集;然后,经过规则
X j j
合并、可读性化简后(见算法 1 第 13 行),这些 EE 规则集再由 EE 规则集生成器汇总输出精简的 EE 规
则集,最终实现从 SS 规则得到对应的 EE 规则.
在转译过程中,有多个环节需要与 Z3 交互:在转译开始之前,转译器会根据实体-能力抽象构建 Z3 数据类型
和 Z3 常量,并将对应关系填入 Z3-Python 数据结构转换模块中的 Z3 常量映射表;在转译过程中,事件筛选模块
和 EE 中间表示生成模块通过 Z3 判定事件的可满足性;规则合并模块通过 Z3 判断等价的条件部分,合并触发事
件;可读性化简模块通过 Z3 进行表达式化简以减少条件表达式长度.
下面结合算法 2~算法 5 详细介绍动作序列信息生成、事件筛选以及 EE 中间表示生成这 3 个关键模块.
算法 2. “执行前提-动作序列”对集合的生成(ConditionalActionsPairs).
输入:实体 e,期望状态组X,系统实体-能力抽象 W;
输出:结构如{(C 1 ,A 1 ),…,(C n ,A n )}的 Pairs,表示实体 e 满足 C i 时要达到X需执行A i .
1. Pairs=∅, ^ X = X | //X| c 表示对X中的(c,v)二元组集合的 c 投影得到实体能力集合
c
2. if ∃∈c ^ , c 不是可控能力 then error
X
3. ^ ′ = X Reorder (^ X ,{M c | ∈ c ^ X })
′
4. for each c i in ^ , (c i ,v i )∈X (i=1,…,m) do
X
5. Sets = SplitRangeByAction (M i c , ) //将 c i 的状态值域V 根据T 和目标值 v i 划分为{ ,...,V 1 i V i i k }
v
i c
i
i c
i
6. end for
7. for Sets 1 ×Sets 2 ×…×Sets m 中的每一个组合 (V 1 ,...,V m ) do //考察每一种初始取值的组合
1 j m j
8. A = CheckedActionSteps (( ,Vc 1 1 1 j , ),...,(v 1 c m ,V m m j ,v m )) //返回动作序列或特殊值 IMPOSSIBLE
9. C = AsCond ( ,Vc 1 1 1 j ) and...and AsCond (c m ,V m m j ) //c 1 ~c m 的取值范围分别处于V 1 1 j ,...,V m m j 的条件
10. Pairs=Pairs∪{(C,A)}
11. end for
• 动作序列信息生成模块
S
该模块会针对期望状态组X相同的 SS 规则组 \ ,调用算法 2 产生可能的动作序列及其执行前提集合
X
Pairs = X {(C j ,A j ) | j ∈ {1, }}n ,并求出与 \ 不兼容的条件Ψ (见算法 1 第 5 行).算法 2 的第 2 行指出,X投影得到
S
X
X
的能力集合^ 中的每个能力都必须是可控的.如第 2.4 节所述,可控能力 c 的状态机 M c =(V c ,T c )中的转移函数
X
[]C J
T c : V ⎯⎯⎯→ V ,每个状态转移带有条件 C 以及要执行的命令J,C 中可能会涉及其他实体能力.考虑到实际需
c
c
求以及处理上的简便,假设^ 中各能力的状态转移条件 C 中依赖的其他能力遵循部分序关系,算法 2 的第 3
X
′
行调用 Reorder 函数将^ 中的能力按这种序关系重排得到^ ,这样在第 8 行就可以尝试按此顺序依次检查动
X
X
′
作转移的可行性.另外,对于 ^ 中的能力 c i ,其状态值域 V 可能是无限的实数,而 M 是有限的,故第 5 行的
i c
i c
X
SplitRangeByAction 函数会检查 M 中到达期望值 v i 的各个状态转移动作J和转移条件 C,将J,C 相同的状态转
i c
移的起始状态涉及的各状态值划分到同一个子集,从而形成V 的有限子集划分 Sets i ,进而可能减少第 7 行要处
i c
′
理的^ 初始状态情形的数目,也能够减少后续规则合并的运算次数.
X
下面结合图 4 的例子来解释.该例子的动作实体为“电扇”,有 3 条 SS 规则.这些规则按期望状态组X是否相
)
同分成两组 \ X S 1 (①③ )和\ X S 2 (② .以 \ S X 2 组为例,根据该组的X 2 “(开关,开)(风速,低)”和图 2 电扇的状态机,按照