ltsconvert - 云端在线

程序：

您的姓名

ltsconvert - 转换并可选择最小化 LTS

概要

转换 [OPTION]……[文件 [输出文件]]

商品描述

在请求中将标记转换系统 (LTS) 从 INFILE 转换为 OUTFILE
应用选定的最小化方法后的格式（默认为无）。 如果 OUTFILE 是
未提供，使用标准输出。 如果未提供 INFILE，则使用 stdin。

输出格式由 OUTFILE 的扩展名决定，而输入格式是
由 INFILE 的内容决定。 选项 --in 和 --out 可用于强制输入
和输出格式。 支持的格式有：
'aut' 代表 Aldebaran 格式 (CADP)，
GraphViz 格式的“点”（不再支持作为输入格式），
'fsm' 用于有限状态机格式，或
'lts' 用于 mCRL2 LTS 格式（默认）

配置

OPTION 可以是以下任何一种：

-D, --确定
确定 LTS

-e您的姓名, - 等价=您的姓名
生成等效的 LTS，保留等效性 NAME: 'none' identity
等价（默认） 'bisim' 强双相似性 'bisim-sig' 强双相似性
使用签名细化 'branching-bisim' 分支双相似性 'branching-
bisim-sig' 使用签名细化'dpbranching-bisim'的分支双相似性
分歧保持分支双相似性 'dpbranching-bisim-sig' 分歧
使用签名细化 'weak-bisim' 保持分支双相似性
双相似性 'weak-bisim-sig' 使用签名细化 'dpweak- 的弱双相似性
bisim' 分歧保留弱双相似性 'dpweak-bisim-sig' 分歧
使用签名细化“sim”强模拟保持弱双相似性
等价 'trace' 强跟踪等价 'weak-trace' 弱跟踪等价
'tau-star' tau 星减少

-iFORMAT, - 在=FORMAT
使用 FORMAT 作为输入格式

-l文件, --lps=文件
使用 FILE 作为生成输入 LTS 的 LPS； 这可能需要
以 fsm 格式保存时存储正确的状态参数名称并保存到
将非 mCRL2 LTS 转换为 mCRL2 LTS

--无法到达
不对输入 LTS 执行可达性检查

-n, --无状态
以点格式保存时省略状态信息

-oFORMAT, - 出去=FORMAT
使用 FORMAT 作为输出格式

--tau=行为名称
将具有逗号分隔列表 ACTNAMES 名称的操作视为内部操作
(tau) 除了输入定义的动作之外的动作

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

标准选项：

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

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

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

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

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

- 版
显示版本信息

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