这是 pbesconstelm 命令,可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行,例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序:
您的姓名
pbesconstelm - 从 PBES 中删除常量参数
概要
普贝斯康斯特尔姆 [OPTION]……[文件 [输出文件]]
商品描述
读取包含 PBES 的文件,并对其应用常量参数消除。 如果
OUTFILE 不存在,使用标准输出。 如果 INFILE 不存在,则标准输入
用来。
配置
OPTION 可以是以下任何一种:
-c, --计算条件
计算传播条件
-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: 'pbes' PBES in 内部格式 'pbes_text' PBES in
文本 (mCRL2) 格式的内部文本格式“文本”PBES
-p您的姓名, --pbes-重写器=您的姓名
使用 pbes 重写策略 NAME: 'simplify' 进行简化(默认)
'quantifier-all' 用于消除所有量词 'quantifier-finite'
消除有限量词变量 'pfnf' 以重写为 PFNF 范式
'ppg' 用于重写为参数化奇偶游戏形式 'bqnf-quantifier'
将量词上的连词重写为量词的连词(实验性)
-Q民, --qlimit=民
将量词的枚举限制为 NUM 变量。 (默认 NUM=1000,NUM=0 表示
无限)。
-e, --删除方程
去除多余的方程
-r您的姓名, --重写器=您的姓名
使用重写策略名称:'jitty' jitty 重写(默认)'jittyc' 已编译
jitty 重写 'jittyp' 用证明器重写 jitty
--计时[=文件]
将计时测量附加到 FILE。 测量值写入标准误差,如果
没有提供文件
标准选项:
-q, - 安静的
不显示警告信息
-v, --详细
显示简短的中间消息
-d, -调试
显示详细的中间消息
--日志级别=LEVEL
显示达到并包括级别的中间消息
-h, - 帮帮我
显示帮助信息
- 版
显示版本信息
使用 onworks.net 服务在线使用 pbesconstelm