lpsinvelm - 云端在线

程序：

您的姓名

lpsinvelm - 检查不变量并使用它们来简化或消除 LPS 的被加数

概要

风信子 [OPTION]... --invfile=INVFILE [文件 [输出文件]]

商品描述

检查布尔公式（sort Bool 的 mCRL2 数据表达式）是否提供为
invariant 是 INFILE 中线性过程规范 (LPS) 的不变量。 如果这是
在这种情况下，该工具会消除 LPS 的所有条件违反
不变，并将结果写入 OUTFILE。 如果存在 INFILE，则使用 stdin。 如果
OUTFILE 不存在，使用标准输出。

该工具还可用于简化给定 LPS 的被加数条件。

配置

OPTION 可以是以下任何一种：

-y, --所有违规
一旦发现不变量的单一违反，不要立即终止，但是
改为报告所有违规行为

-c, --反例
显示一个估价，表明为什么不变量可能会被违反，如果它
不确定一个被加数是否违反了不变量

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

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

-n, --不检查
在消除不可达的被加数之前不检查不变量是否成立

-e, --无消除
不消除或简化被加数，而是将不变量添加到每个条件

-p字首, --打印点=字首
如果无法确定是否存在 BDD，则保存结果 BDD 的 .dot 文件
求和违反不变量； PREFIX 将用作输出文件的前缀

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

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

-l, --简化所有
简化所有被加数的条件，而不是仅仅消除被加数
其条件与不变量相结合是矛盾的

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

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

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

标准选项：

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

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

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

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

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

- 版
显示版本信息

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