pbes2bool - 云端在线

程序：

您的姓名

pbes2bool - 从 PBES 生成 BES 并解决它。

概要

pbes2布尔 [OPTION]...[文件]

商品描述

从 INFILE 解决 (P)BES。 如果 INFILE 不存在，则使用 stdin。

配置

OPTION 可以是以下任何一种：

-c, - 柜台
最后打印一棵树，标有左侧的实例化
方程； 这棵树表明 pbes2bool 如何有效或
PBES 的无效性

-eLEVEL, --擦除=LEVEL
使用删除级别 LEVEL 删除 bes 变量 'none' 不删除生成的 bes
变量。 这会导致过度使用内存。 （默认） 'some' 删除
生成的是未使用的变量，除非它的右侧
等式是真还是假。 必须重新计算变量的 rhss，如果
又遇到了，很正常。 'all' 删除每个 bes 变量
不再用于任何方程。 这是非常有效的内存效率，但它可以
非常耗时，因为移除的 bes 变量的 rhss 可能必须是
经常重新计算。

-H, --哈希表
代入 bes 方程时使用哈希表，并翻译内部
二元决策图的表达式（不鼓励，由于性能）

-iFORMAT, - 在=FORMAT
使用输入格式 FORMAT: 'pbes' PBES in 内部格式 'pbes_text' PBES in
内部文本格式 'text' PBES 文本 (mCRL2) 格式 'bes' BES 内部
格式 'bes_text' BES 内部文本格式 'cwi' BES CWI 格式 'pgsolver'
PGSolver 格式的 BES

-oFORMAT, - 输出=FORMAT
使用输出格式 FORMAT（不推荐使用此选项。使用工具 pbes2bes
代替）。

-Q民, --qlimit=民
将量词的枚举限制为 NUM 变量。 （默认 NUM=1000，NUM=0 表示
无限）。

-r您的姓名, --重写器=您的姓名
使用重写策略名称：'jitty' jitty 重写（默认）'jittyc' 已编译
jitty 重写 'jittyp' 用证明器重写 jitty

-z搜索, - 搜索=搜索
使用搜索策略 SEARCH: 'breadth-first' 计算右侧
布尔变量先到先得。 这与一个
广度优先搜索。 这有利于生成反例。 （默认）
'depth-first' 计算布尔变量的右侧，其中最后一个
首先研究生成的变量。 这对应于深度优先
搜索。 这可以大大优于广度优先搜索时的有效性
一个公式是在更大的深度后确定的。 'b' 广度优先的简写。
'd' 深度优先的简写。

-sSTRAT, - 战略=STRAT
使用替换策略 STRAT: '0' 计算所有可以为的布尔方程
从初始状态到达，没有优化。 这是最多的数据
每个生成的方程的有效选项。 (默认) '1' 立即优化
用右手边代替已经研究过的变量是真的
或在生成表达式时为 false。 这与 0 的内存效率一样。 '2' In
除 1 外，还将为真或为假的变量代入已经
生成右手边。 这可能意味着某些变量变得无法访问
（例如 X0 和 X0 中的 X1，当 X1 变为假时，假设 X0 不在其他地方出现。
将维护哪些变量变得不可访问，因为这些变量没有
进行调查。 根据 PBES，这可以减少
大量生成 BES，但需要更大的内存占用。 '3' 输入
除了 2，调查生成的变量是否出现在循环中，
这样它们就可以设置为真或假，具体取决于定点符号。
这会显着增加生成方程所需的时间。

--计时[=文件]
将计时测量附加到 FILE。 测量值写入标准误差，如果
没有提供文件

-u, --未使用的数据
不要删除数据规范中未使用的部分

标准选项：

-q, - 安静的
不显示警告信息

-v, --详细
显示简短的中间消息

-d, -调试
显示详细的中间消息

--日志级别=LEVEL
显示达到并包括级别的中间消息

-h, - 帮帮我
显示帮助信息

- 版
显示版本信息

使用 onworks.net 服务在线使用 pbes2bool