lpsconfcheck - 云端在线

程序：

您的姓名

lpsconfcheck - 标记 LPS 的融合 tau-summands

概要

lpsconf检查 [OPTION]……[文件 [输出文件]]

商品描述

检查 INFILE 中 mCRL2 LPS 的哪些 tau-summands 是融合的，通过重命名来标记它们
将它们写入 ctau，并将结果写入 OUTFILE。 如果 INFILE 不存在，则使用标准输入。 如果
OUTFILE 不存在，使用标准输出。

配置

OPTION 可以是以下任何一种：

-a, - 选择所有
检查关于所有其他被加数的 tau-summands 的汇合，而不是
一旦遇到被加数，就继续下一个 tau-被加数
与当前的 tau-summand 不融合

-c, --反例
显示汇合条件不成立的估值，以防万一
遇到的条件既不是矛盾也不是同义反复

-g, --生成不变量
尝试证明减少汇合条件是 LPS 的不变量，在
如果汇合条件不是同义反复

-o, - 就职
对列表应用归纳法

-i文件, --不变的=文件
在 INVFILE 中使用布尔公式（排序 Bool 的 mCRL2 数据表达式）作为
不变的

-n, --不检查
在检查汇合之前不要检查不变量是否成立

-m, --无标记
不要标记汇合的 tau-summands； 由于没有对 LPS 进行任何更改，
没有任何内容写入 OUTFILE

-p字首, --打印点=字首
保存生成的 BDD 的 .dot 文件，以防无法证明两个被加数
汇合； PREFIX 将用作输出文件的前缀

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

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

-z求解器, --smt-求解器=求解器
使用 SOLVER 从内部使用的 BDD 中删除不一致的路径（默认情况下，
不应用路径消除）：'cvc' SMT 求解器 CVC3

-s民, --被加数=民
仅用数字 NUM 消除或简化被加数

-t极限, - 时限=极限
最多花费 LIMIT 秒来证明一个公式

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

标准选项：

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

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

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

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

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

- 版
显示版本信息

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