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

这篇文章设计一个宿主侧测试工具 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 步反例回放到界面；这样生成阶段不被动画与设备速度拖慢，最终仍能验证真实交互。

interface TaskModel {
  visible: boolean;
  foreground: boolean;
  activeJob: number;
  generation: number;
  lastAction: string;
}

interface UiSnapshot {
  page: 'CLOSED' | 'OPEN';
  lifecycle: 'FOREGROUND' | 'BACKGROUND';
  activeJob: number;
  generation: number;
}

interface UiPort {
  open(): Promise<void>;
  start(): Promise<void>;
  background(): Promise<void>;
  resume(): Promise<void>;
  cancel(): Promise<void>;
  snapshot(): Promise<UiSnapshot>;
  reset(): Promise<void>;
}

function assertInvariant(model: TaskModel, actual: UiSnapshot): void {
  if (actual.activeJob > 1) throw new Error('activeJob <= 1 violated');
  if (model.visible !== (actual.page === 'OPEN')) throw new Error('page mismatch');
  if (model.generation !== actual.generation) throw new Error('generation mismatch');
}

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

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

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

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

import fc from 'fast-check';

type Real = { port: UiPort };

class StartCommand implements fc.AsyncCommand<TaskModel, Real> {
  check = (m: Readonly<TaskModel>): boolean =>
    m.visible && m.foreground && m.activeJob === 0;

  async run(m: TaskModel, r: Real): Promise<void> {
    m.activeJob = 1;
    m.generation += 1;
    m.lastAction = 'START';
    await r.port.start();
    assertInvariant(m, await r.port.snapshot());
  }

  toString = (): string => 'START';
}

class CancelCommand implements fc.AsyncCommand<TaskModel, Real> {
  check = (m: Readonly<TaskModel>): boolean => m.visible && m.activeJob === 1;

  async run(m: TaskModel, r: Real): Promise<void> {
    m.activeJob = 0;
    m.lastAction = 'CANCEL';
    await r.port.cancel();
    assertInvariant(m, await r.port.snapshot());
  }

  toString = (): string => 'CANCEL';
}

const commandArbs = [
  fc.constant(new StartCommand()),
  fc.constant(new CancelCommand())
];

实际项目还应为 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，便于图文一致。

async function runProperty(port: UiPort) {
  const property = fc.asyncProperty(
    fc.commands(commandArbs, { maxCommands: 30 }),
    async commands => {
      await port.reset();
      const model: TaskModel = {
        visible: false, foreground: true, activeJob: 0,
        generation: 0, lastAction: 'RESET'
      };
      await fc.asyncModelRun(() => ({ model, real: { port } }), commands);
    }
  );

  const details = await fc.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 步，开发者终于可以把一次偶发状态错乱写成确定的工程任务：哪一代回调越界，哪条不变量被破坏，修复后用哪组参数复验。这样的失败报告，比“多点几次看看”更适合进入团队日常。