HarmonyOS 7 fast-check：ArkUI异步状态机种子复现

异步页面最难复现的缺陷，经常不是某个按钮本身，而是一串操作的组合：打开页面、启动任务、切后台、恢复、立刻取消。开发者手工点十次没有问题，用户在一次特殊时序里却看到两个任务同时活跃。普通用例会把“常见路径”写得很完整，却很少探索命令排列、等待点和重复操作。

这篇文章设计一个宿主侧测试工具StateFuzzLab，用 fast-check 生成 ArkUI 任务页的命令序列，再把最小失败路径回放到确定性模型。演示任务FCT-1331-415，种子415731，250 个计划用例执行到 170 个时发现失败，进度 68%；原始反例 23 步，收缩为 5 步：OPEN → START → BACKGROUND → RESUME → CANCEL。当前状态REPLAYING_COUNTEREXAMPLE，被破坏的不变量是activeJob <= 1。

一、不是多写随机点击，而是先写可判断的模型

fast-check 的模型测试以 command 为单位。每个命令包含前置条件，以及同时更新简化模型和真实系统的执行逻辑。同步系统可用modelRun，异步命令可用asyncModelRun，需要调度异步完成顺序时还可以使用scheduledModelRun。本文不把这些能力伪装成 HarmonyOS 系统 API；它运行在 TypeScript 测试工具侧，ArkUI Demo 通过一个测试端口接收命令并回传状态。

模型不复制整个页面。它只保留判断不变量需要的字段：visible、foreground、activeJob、generation和lastAction。真实系统端口暴露相同的观测快照。每条命令执行后比较关键字段，发现偏差立即失败。模型越小，失败原因越容易解释；把页面所有文本和动画都放进去，只会让收缩被无关差异干扰。

演示中的缺陷假设是：页面恢复时旧 generation 的启动回调迟到，先把 activeJob 从 0 写成 1；随后 CANCEL 清理当前 generation，却没有识别旧回调，最终又出现第二个活跃任务。文章不声称这来自真实线上事故，而是用一个可验证的故障模型解释属性测试方法。

二、命令必须描述边界，而不是描述按钮坐标

第一段代码定义模型与测试端口。UiPort可以由 Hypium UI 自动化、测试版 RPC 或纯内存替身实现。本文的最小演示采用内存端口保证快速收缩，再用 Hypium 把已收缩的 5 步反例回放到界面；这样生成阶段不被动画与设备速度拖慢，最终仍能验证真实交互。

interfaceTaskModel{visible:boolean;foreground:boolean;activeJob:number;generation:number;lastAction:string;}interfaceUiSnapshot{page:'CLOSED'|'OPEN';lifecycle:'FOREGROUND'|'BACKGROUND';activeJob:number;generation:number;}interfaceUiPort{open():Promise<void>;start():Promise<void>;background():Promise<void>;resume():Promise<void>;cancel():Promise<void>;snapshot():Promise<UiSnapshot>;reset():Promise<void>;}functionassertInvariant(model:TaskModel,actual:UiSnapshot):void{if(actual.activeJob>1)thrownewError('activeJob <= 1 violated');if(model.visible!==(actual.page==='OPEN'))thrownewError('page mismatch');if(model.generation!==actual.generation)thrownewError('generation mismatch');}

端口一定要有reset()。属性测试会执行很多样本，前一个样本留下的任务、缓存或页面栈若未清理，下一次失败就无法由 seed 单独复现。reset 不只是把字段赋零，还要等待异步任务停止、取消订阅、恢复测试时钟。若做不到干净复位，就应每个样本启动独立 Ability 或进程，而不是接受污染。

三、让 fast-check 生成“合法但刁钻”的动作

fc.commands接收命令生成器，每个命令用check判断当前模型是否允许执行。OPEN 只在页面关闭时有效；START 需要页面可见且前台；BACKGROUND 需要前台；RESUME 需要后台；CANCEL 需要活跃任务。前置条件不是为了保护被测系统，而是让生成器集中探索业务允许的路径。

第二段代码示意异步 command。为了控制篇幅，只展开 START 与 CANCEL；其他命令结构相同。run先更新模型还是先调用真实系统，要按业务语义统一，关键是每条命令末尾读取快照并验证不变量。

importfcfrom'fast-check';typeReal={port:UiPort};classStartCommandimplementsfc.AsyncCommand<TaskModel,Real>{check=(m:Readonly<TaskModel>):boolean=>m.visible&&m.foreground&&m.activeJob===0;asyncrun(m:TaskModel,r:Real):Promise<void>{m.activeJob=1;m.generation+=1;m.lastAction='START';awaitr.port.start();assertInvariant(m,awaitr.port.snapshot());}toString=():string=>'START';}classCancelCommandimplementsfc.AsyncCommand<TaskModel,Real>{check=(m:Readonly<TaskModel>):boolean=>m.visible&&m.activeJob===1;asyncrun(m:TaskModel,r:Real):Promise<void>{m.activeJob=0;m.lastAction='CANCEL';awaitr.port.cancel();assertInvariant(m,awaitr.port.snapshot());}toString=():string=>'CANCEL';}constcommandArbs=[fc.constant(newStartCommand()),fc.constant(newCancelCommand())];

实际项目还应为 OPEN、BACKGROUND、RESUME 和页面销毁分别建命令，并把对象做成无共享可变状态。不要在 command 实例字段里累积上一次运行结果，否则 shrink 重放会受到旧数据影响。命令的toString()也很重要，它决定报告中的反例是否能被人读懂。

项目演示图中，左侧目录包含model.ts、commands.ts、property.test.ts与ReplayPage.ets；中间显示AsyncCommand和不变量；右侧模拟器展示 68%、170/250 与 seed；底部日志固定为FCT-1331-415、23→5、activeJob=2。这是一张配套演示图，不是测试已在真机完成的证明。

四、seed 只能定位生成，path 才能直达反例

fast-check 失败报告会给出 seed 与 path。对 command 模型测试，还可能需要replayPath记录哪些命令实际通过前置条件并执行。只保存 seed 不够：同一 seed 在属性、任意值或版本变化后可能经过不同收缩过程；只保存最终五步文字也不够，因为参数化命令可能丢失具体值。

第三段代码使用fc.check而非直接assert，目的是把 RunDetails 转成应用自己的 JSON 证据。失败时保存seed、counterexamplePath、错误、不变量、工具版本和 command replayPath；通过时也记录 numRuns。示例固定 seed 415731，便于图文一致。

asyncfunctionrunProperty(port:UiPort){constproperty=fc.asyncProperty(fc.commands(commandArbs,{maxCommands:30}),asynccommands=>{awaitport.reset();constmodel:TaskModel={visible:false,foreground:true,activeJob:0,generation:0,lastAction:'RESET'};awaitfc.asyncModelRun(()=>({model,real:{port}}),commands);});constdetails=awaitfc.check(property,{seed:415731,numRuns:250,endOnFailure:true,verbose:2});return{failed:details.failed,seed:details.seed,path:details.counterexamplePath,counterexample:details.counterexample,error:details.error,numRuns:details.numRuns};}

check与assert的差别是前者把结果交给调用方处理，后者失败时直接抛出格式化异常。证据工具适合 check，普通测试套件适合 assert。无论哪种，都不要在失败后自动换 seed 直到绿色；那会把缺陷藏起来。CI 应保留第一次失败的完整参数，再用 seed、path 与 replayPath单独重放。

五、收缩后的五步才适合接入 UI 自动化

生成阶段可以运行 250 组模型命令，但没有必要把所有随机序列都驱动真机。演示策略分两层：内存端口负责大规模发现和收缩，收缩得到 5 步后，生成一个 Hypium 用例按OPEN → START → BACKGROUND → RESUME → CANCEL操作测试页面，并在每步后读取页面诊断字段。

这种分层不会证明内存模型等于真实应用，所以契约测试不可缺。每个端口方法至少有一组对照用例，确认 START、CANCEL 与生命周期事件在模型和应用中产生相同状态。若契约不一致，属性测试只是证明了替身正确。

运行页在 13:31 显示 170/250、68%，状态REPLAYING_COUNTEREXAMPLE，seed 415731，原始 23 步、最小 5 步，不变量activeJob <= 1。顶部有 Wi‑Fi、5G、信号和 84% 电量，页面没有手机外框。

详情页不重复进度环，而是展开五步时间线，并在 RESUME 后标出旧 generation 回调，在 CANCEL 后显示activeJob=2。红圈强调失败点，底部列出 seed 与 path，方便复制到测试参数。

六、最小失败序列仍然需要工程判断

收缩得到五步，不代表第五步一定有 bug。它只说明在当前模型、命令前置条件和调度方式下，这是仍能触发不变量破坏的较小反例。真正修复时要看日志中的 generation、回调来源和资源所有权。演示的修复方向是：RESUME 产生新 generation，旧 generation 的启动回调只能记录lateDropped，不得写 activeJob。

不变量也不能写成空泛的“页面不崩”。适合属性测试的判断通常具备明确状态：activeJob 不大于 1；页面关闭后监听数为 0；CANCEL 后最终状态不是 RUNNING；同一 generation 只能完成一次；后台期间不会创建新 UI 资源。这些条件既能在模型里表达，也能从诊断端口读取。

测试时钟要可控。真实 setTimeout、网络和后台调度会让同一 seed 仍然不稳定。端口应支持虚拟时钟或显式flush()，把“异步何时完成”变成命令的一部分。如果使用 fast-check 的 scheduler 探索竞态，也要保存调度报告；不能只保留操作序列。

依赖版本同样要进证据。fast-check 的收缩与报告格式可能随版本演进，HarmonyOS 页面生命周期行为也与目标 SDK 和设备相关。证据文件至少写入 fast-check 版本、Node 版本、应用 commit、SDK、设备型号与 Hypium 用例版本。本文不虚构具体最新版本号，只要求项目锁文件成为证据附件。

七、把失败变成可以交接的资产

StateFuzzLab最终输出三份文件：原始 RunDetails 摘要、最小命令序列、可执行回放配置。回放配置不包含账号、令牌或真实用户数据；参数化输入先做脱敏。若失败涉及图片或文件路径，报告保存 fixture ID，而不是设备上的真实路径。

团队评审时先看不变量，再看五步序列，最后看页面日志。不要先盯着 seed 猜随机数。seed 是定位工具，不是原因。修复后，同一个反例要进入常规回归，同时属性测试继续运行新的 seed；否则这里只修了一个样本，没有保留探索能力。

命令集合也需要版本评审。新增一个RETRY或NAVIGATE_BACK命令，会改变可探索空间，旧 seed 未必仍生成相同路径。提交命令变更时应附带“新增状态、前置条件、影响的不变量”，并保留上一版工具运行记录。若大量旧反例失去重放能力，先迁移固定回归用例，再升级生成模型。

覆盖率不应只写“跑了 250 次”。更有用的是状态与转移覆盖：是否到达 BACKGROUND、是否执行 RESUME 后 CANCEL、是否出现连续 START 被前置条件拒绝、每条不变量被检查多少次。演示的 170/250 表示样本进度，不代表覆盖率 68%。把这两个概念混在同一进度条，会让报告显得精确，实际却无法回答探索了什么。

失败截图也只能当辅助证据。动画帧、文字或系统状态栏可能因设备不同而变化，像素比较很容易产生噪声。真正的断言应来自稳定语义字段，例如诊断页的 generation、activeJob 和生命周期。截图用于帮助人理解当时页面，不用于替代状态日志。

最后要给属性测试设置成本上限。CI 中可以固定 numRuns 与时间预算，夜间任务再扩大探索；出现失败后停止继续消耗设备，优先保存证据。若收缩时间过长，可利用框架的时间限制与后续 replay 恢复，但必须标记“收缩未完成”，不能把当前反例称为最小反例。本文的 23→5 是演示设定，实际报告应以框架输出为准。

八、参考边界

• fast-check 官方文档确认commands的模型测试结构，以及asyncModelRun、scheduledModelRun的用途。
• 官方回放说明要求保存 seed 与 path；command 模型测试还要处理 replayPath。
• 华为测试服务资料确认 Hypium 可用于 HarmonyOS UI 自动化，CI 可通过命令行执行相关用例。

属性测试的价值不是随机，而是“发现之后还能准确重放”。当 23 步被收缩成 5 步，开发者终于可以把一次偶发状态错乱写成确定的工程任务：哪一代回调越界，哪条不变量被破坏，修复后用哪组参数复验。这样的失败报告，比“多点几次看看”更适合进入团队日常。