异步页面最难复现的缺陷经常不是某个按钮本身而是一串操作的组合打开页面、启动任务、切后台、恢复、立刻取消。开发者手工点十次没有问题用户在一次特殊时序里却看到两个任务同时活跃。普通用例会把“常见路径”写得很完整却很少探索命令排列、等待点和重复操作。这篇文章设计一个宿主侧测试工具StateFuzzLab用 fast-check 生成 ArkUI 任务页的命令序列再把最小失败路径回放到确定性模型。演示任务FCT-1331-415种子415731250 个计划用例执行到 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():Promisevoid;start():Promisevoid;background():Promisevoid;resume():Promisevoid;cancel():Promisevoid;snapshot():PromiseUiSnapshot;reset():Promisevoid;}functionassertInvariant(model:TaskModel,actual:UiSnapshot):void{if(actual.activeJob1)thrownewError(activeJob 1 violated);if(model.visible!(actual.pageOPEN))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先更新模型还是先调用真实系统要按业务语义统一关键是每条命令末尾读取快照并验证不变量。importfcfromfast-check;typeReal{port:UiPort};classStartCommandimplementsfc.AsyncCommandTaskModel,Real{check(m:ReadonlyTaskModel):booleanm.visiblem.foregroundm.activeJob0;asyncrun(m:TaskModel,r:Real):Promisevoid{m.activeJob1;m.generation1;m.lastActionSTART;awaitr.port.start();assertInvariant(m,awaitr.port.snapshot());}toString():stringSTART;}classCancelCommandimplementsfc.AsyncCommandTaskModel,Real{check(m:ReadonlyTaskModel):booleanm.visiblem.activeJob1;asyncrun(m:TaskModel,r:Real):Promisevoid{m.activeJob0;m.lastActionCANCEL;awaitr.port.cancel();assertInvariant(m,awaitr.port.snapshot());}toString():stringCANCEL;}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、activeJob2。这是一张配套演示图不是测试已在真机完成的证明。四、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){constpropertyfc.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);});constdetailsawaitfc.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_COUNTEREXAMPLEseed 415731原始 23 步、最小 5 步不变量activeJob 1。顶部有 Wi‑Fi、5G、信号和 84% 电量页面没有手机外框。详情页不重复进度环而是展开五步时间线并在 RESUME 后标出旧 generation 回调在 CANCEL 后显示activeJob2。红圈强调失败点底部列出 seed 与 path方便复制到测试参数。六、最小失败序列仍然需要工程判断收缩得到五步不代表第五步一定有 bug。它只说明在当前模型、命令前置条件和调度方式下这是仍能触发不变量破坏的较小反例。真正修复时要看日志中的 generation、回调来源和资源所有权。演示的修复方向是RESUME 产生新 generation旧 generation 的启动回调只能记录lateDropped不得写 activeJob。不变量也不能写成空泛的“页面不崩”。适合属性测试的判断通常具备明确状态activeJob 不大于 1页面关闭后监听数为 0CANCEL 后最终状态不是 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 与 pathcommand 模型测试还要处理 replayPath。华为测试服务资料确认 Hypium 可用于 HarmonyOS UI 自动化CI 可通过命令行执行相关用例。属性测试的价值不是随机而是“发现之后还能准确重放”。当 23 步被收缩成 5 步开发者终于可以把一次偶发状态错乱写成确定的工程任务哪一代回调越界哪条不变量被破坏修复后用哪组参数复验。这样的失败报告比“多点几次看看”更适合进入团队日常。
HarmonyOS 7 fast-check：ArkUI异步状态机种子复现
异步页面最难复现的缺陷经常不是某个按钮本身而是一串操作的组合打开页面、启动任务、切后台、恢复、立刻取消。开发者手工点十次没有问题用户在一次特殊时序里却看到两个任务同时活跃。普通用例会把“常见路径”写得很完整却很少探索命令排列、等待点和重复操作。这篇文章设计一个宿主侧测试工具StateFuzzLab用 fast-check 生成 ArkUI 任务页的命令序列再把最小失败路径回放到确定性模型。演示任务FCT-1331-415种子415731250 个计划用例执行到 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():Promisevoid;start():Promisevoid;background():Promisevoid;resume():Promisevoid;cancel():Promisevoid;snapshot():PromiseUiSnapshot;reset():Promisevoid;}functionassertInvariant(model:TaskModel,actual:UiSnapshot):void{if(actual.activeJob1)thrownewError(activeJob 1 violated);if(model.visible!(actual.pageOPEN))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先更新模型还是先调用真实系统要按业务语义统一关键是每条命令末尾读取快照并验证不变量。importfcfromfast-check;typeReal{port:UiPort};classStartCommandimplementsfc.AsyncCommandTaskModel,Real{check(m:ReadonlyTaskModel):booleanm.visiblem.foregroundm.activeJob0;asyncrun(m:TaskModel,r:Real):Promisevoid{m.activeJob1;m.generation1;m.lastActionSTART;awaitr.port.start();assertInvariant(m,awaitr.port.snapshot());}toString():stringSTART;}classCancelCommandimplementsfc.AsyncCommandTaskModel,Real{check(m:ReadonlyTaskModel):booleanm.visiblem.activeJob1;asyncrun(m:TaskModel,r:Real):Promisevoid{m.activeJob0;m.lastActionCANCEL;awaitr.port.cancel();assertInvariant(m,awaitr.port.snapshot());}toString():stringCANCEL;}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、activeJob2。这是一张配套演示图不是测试已在真机完成的证明。四、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){constpropertyfc.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);});constdetailsawaitfc.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_COUNTEREXAMPLEseed 415731原始 23 步、最小 5 步不变量activeJob 1。顶部有 Wi‑Fi、5G、信号和 84% 电量页面没有手机外框。详情页不重复进度环而是展开五步时间线并在 RESUME 后标出旧 generation 回调在 CANCEL 后显示activeJob2。红圈强调失败点底部列出 seed 与 path方便复制到测试参数。六、最小失败序列仍然需要工程判断收缩得到五步不代表第五步一定有 bug。它只说明在当前模型、命令前置条件和调度方式下这是仍能触发不变量破坏的较小反例。真正修复时要看日志中的 generation、回调来源和资源所有权。演示的修复方向是RESUME 产生新 generation旧 generation 的启动回调只能记录lateDropped不得写 activeJob。不变量也不能写成空泛的“页面不崩”。适合属性测试的判断通常具备明确状态activeJob 不大于 1页面关闭后监听数为 0CANCEL 后最终状态不是 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 与 pathcommand 模型测试还要处理 replayPath。华为测试服务资料确认 Hypium 可用于 HarmonyOS UI 自动化CI 可通过命令行执行相关用例。属性测试的价值不是随机而是“发现之后还能准确重放”。当 23 步被收缩成 5 步开发者终于可以把一次偶发状态错乱写成确定的工程任务哪一代回调越界哪条不变量被破坏修复后用哪组参数复验。这样的失败报告比“多点几次看看”更适合进入团队日常。