lps2lts - 云端在线

程序：

您的姓名

lps2lts - 从 LPS 生成 LTS

概要

LPS2LTS [OPTION]……[文件 [输出文件]]

商品描述

从 INFILE 中的 LPS 生成 LTS 并将结果保存到 OUTFILE。 如果 INFILE 不是
提供，使用标准输入。 如果未提供 OUTFILE，则不存储 LTS。

如果使用 'jittyc' 重写器，则 MCRL2_COMPILEREWRITER 环境变量
（默认值：'mcrl2compilerewriter'）确定编译重写器的脚本，
和 MCRL2_COMPILEDIR（默认值：'.'）确定临时文件的存储位置。

请注意，lps2lts 可以在任何对之间传递具有相同标签的多个转换
状态。 如果不希望这样，可以通过应用强
使用例如工具 ltsconvert 进行双模拟还原。

OUTFILE 的格式由它的扩展名决定（除非它由一个
选项）。 支持的格式有：

'aut' 代表 Aldebaran 格式 (CADP)，
GraphViz 格式的“点”（不再支持作为输入格式），
'fsm' 用于有限状态机格式，或
'lts' 用于 mCRL2 LTS 格式 如果使用 jittyc 重写器，则
MCRL2_COMPILEREWRITER 环境变量（默认值：mcrl2compilerewriter）
确定编译重写器的脚本和 MCRL2_COMPILEDIR（默认值：
'.') 确定临时文件的存储位置。 请注意，lps2lts 可以提供多个
任何一对状态之间具有相同标签的转换。 如果这不是所希望的，例如
可以通过使用例如
工具 ltsconvert。

配置

OPTION 可以是以下任何一种：

-a名字, - 行动=名字
检测并报告转换系统中具有动作名称的动作
NAMES，一个逗号分隔的列表。 例如，这对于查找（或证明
没有）动作错误。 每次出现以下信息时都会打印一条消息
这些动作名称。 使用 -t 标志生成对这些操作的跟踪

-b[民], --位哈希[=民]
使用位散列来存储状态并且最多存储 NUM 个状态。 这意味着
而不是保留所有已访问状态的完整记录，而是一个位数组
用于指示之前是否已经看到状态的散列。
虽然这意味着这个选项可能会导致状态被误认为是其他
（因为它们映射到相同的散列），探索非常大的
否则无法探索的 LTS。 NUM 的默认值约为
2*10^8（这对应约25MB内存）

--缓存
使用枚举缓存技术来加速状态空间的生成。

-c[您的姓名], - 合流[=您的姓名]
使用操作标签 NAME 应用转换的优先级。（当没有 NAME 时
提供（即'-c'）优先级被赋予动作'ctau'。 优先考虑
tau 使用标志 -ctau。 请注意，如果线性过程不是 tau-confluent，
生成的状态空间必然分支类似于状态空间
LP。 使用的生成算法不需要线性过程
tau 收敛。

-D, - 僵局
检测死锁（即对于每个死锁都会打印一条消息）

-F, --背离
检测分歧（即对于具有分歧（= tau 循环）的每个状态，消息是
打印）。 检测分歧的算法对于每个状态都是线性的，所以
启用此选项后，状态空间探索变为二次，导致状态
启用此选项后，太空探索会变慢。

-yBOOL, - 假的=BOOL
用基于 BOOL 的值的虚拟值替换 LPS 中的自由变量：
“是”（默认）或“否”

--错误跟踪
如果在探索过程中发生错误，则将跟踪保存到无法访问的状态
探讨

--init-tsize=民
设置内部使用的哈希表的初始大小（默认为 10000）

-l民, - 最大限度=民
最多探索 NUM 个州

-m名字, --多动作=名字
检测和报告来自 NAMES 的转换系统中的多操作，一个逗号
分隔列表。 像 -a 一样工作，除了多动作完全匹配，
包括数据参数。

--无信息
不要将状态信息添加到 OUTFILE 没有这个选项 lps2lts 添加状态
向量到 LTS。 此选项会导致此信息被丢弃并说明
仅由序列号表示。 显式状态信息对于
例如，可视化目的，但可能导致 OUTFILE 增长
相当。 请注意，以 AUT 格式写入时，此选项是隐式的。

-oFORMAT, - 出去=FORMAT
以指定的格式保存输出

- 修剪
使用 summand pruning 来加速状态空间的生成。

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

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

-s您的姓名, - 战略=您的姓名
使用策略 NAME: 'b', 'breadth' 广度优先搜索探索状态空间
(默认) 'd', 'depth' 深度优先搜索 'p', 'prioritized' 优先单个
其第一个参数上的操作属于 Nat 类型，其中只有那些带有
选择此参数的最低值。 例如，如果有动作 a（3）和
b（4） a(3) 残留物和 b(4) 被跳过。 没有第一个排序参数的操作
总是选择具有多个操作的 Nat 和多操作（选项是
实验) 'q', 'prioritized' 优先考虑它的第一个参数是
对 Nat 进行排序（请参阅选项 --prioritized），并随机选择其中之一以获得
优先随机模拟（选项是实验性的）“r”，“随机”随机
模拟。 从所有下一个状态中随机选择一个，与是否无关
已经观察到这种状态。 因此，仅随机模拟
当遇到死锁状态时终止。

- 压制
在详细模式下，不打印指示访问数量的进度消息
状态和转换。 对于大型状态空间，进度消息的数量可以
非常可怕。 此功能有助于抑制这些。 其他详细信息，
例如探索的状态总数，只是保持可见。

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

--todo-max=民
在待办事项列表中最多保留 NUM 个状态； 此选项仅与广度相关
第一次搜索，其中 NUM 是每个级别的最大状态数，以及深度
第一次搜索，其中 NUM 是最大深度

-t[民], - 痕迹[=民]
写一个最短的轨迹到每个状态，从 NAMES 的一个动作到达
选项 --action，是使用 --deadlock 检测到的死锁，还是发散
使用 --divergence 检测到文件。 不会写入超过 NUM 条轨迹。 如果
没有提供 NUM，跟踪的数量是无限的。对于每个要被跟踪的跟踪
将创建一个带有扩展名 .trc (trace) 的唯一文件，其中包含一个
从初始状态到死锁状态的最短轨迹。 痕迹可以
使用 tracepp 打印漂亮并转换为其他格式。

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

标准选项：

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

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

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

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

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

- 版
显示版本信息

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