这是可以使用我们的多个免费在线工作站之一（例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器）在 OnWorks 免费托管服务提供商中运行的命令 sparksimp
程序：
您的姓名
sparksimp - 分析所有生成的 SPARK 证明工件（并行）
概要
火花简化 [选项] [-sargs SIMPLIFIER_OPTIONS] [-zargs ZOMBIESCOPE_OPTIONS] [-vargs
VICTOR_OPTIONS]
商品描述
火花简化, 分析所有验证条件和由
SPARK 的检查员并尝试使用 Simplifier、ZombieScope 和
胜利者。 如果需要，这可以并行完成。
本手册页仅总结了 火花简化 命令行标志，请参考
完整的 SPARKSimp 手册以获取更多信息。
配置
这些选项并不完全遵循通常的 GNU 命令行语法，因为选项以
一个破折号而不是通常的两个。
-a 处理所有文件，即使它们的时间戳表明它们已被
之前分析过。
-v 显示版本信息。
-V 详细输出。
-n 试运行 - 这仅打印要分析的文件列表，然后停止。
-ns 不要运行简化程序。
-nz 不要运行 ZombieScope。
-胜利者
在未经 Simplifier 验证的 VC 上运行 ViCToR/Alt-Ergo。 如果 -ns 然后指定
这将在所有 VC 上运行 ViCToR。
-t, -r 按大小对 vcg 文件进行排序，并首先分析最大的文件。 如果 -r 被指定为
首先分析最小的。
-l 将分析的每个单元的 spadesimp 和僵尸范围输出记录到 UNIT.log 和
UNIT.zsl 分别。
-e 将所有输出回显到屏幕； 此选项不能与 -p.
-p =N 使用 N 个并发进程。
-x=PATH
指定替代的简化程序可执行文件。
-z=PATH
指定替代 ZombieScope 可执行文件。
-sargs 配置, -zargs 配置, -变量 配置
其中之一之后的任何选项都将直接传递给简化程序，
ZombieScope 或 ViCToR 分别。 请参阅他们的手册页或文档
获取更多信息。
使用 onworks.net 服务在线使用 sparksimp
