ltsconvert - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

ltsconvert - chuyển đổi và tùy chọn thu nhỏ LTS

SYNOPSIS

chuyển đổi [TÙY CHỌN] ... [TRONG TẬP TIN [NGOÀI RA]]

MÔ TẢ

Chuyển đổi hệ thống chuyển tiếp có nhãn (LTS) từ INFILE sang OUTFILE trong yêu cầu
định dạng sau khi áp dụng phương pháp thu nhỏ đã chọn (mặc định là không có). Nếu OUTFILE là
không được cung cấp, stdout được sử dụng. Nếu INFILE không được cung cấp, stdin sẽ được sử dụng.

Định dạng đầu ra được xác định bởi phần mở rộng của OUTFILE, trong khi định dạng đầu vào là
được xác định bởi nội dung của INFILE. Tùy chọn --in và --out có thể được sử dụng để buộc đầu vào
và các định dạng đầu ra. Các định dạng được hỗ trợ là:
'aut' cho định dạng Aldebaran (CADP),
'dot' cho định dạng GraphViz (không còn được hỗ trợ làm định dạng đầu vào),
'fsm' cho định dạng Máy trạng thái hữu hạn, hoặc
'lts' cho định dạng mCRL2 LTS (mặc định)

LỰA CHỌN

TÙY CHỌN có thể là bất kỳ điều nào sau đây:

-D, --xác định
xác định LTS

-eTÊN, - tương đương=TÊN
tạo một LTS tương đương, duy trì danh tính tương đương NAME: 'none'
tính tương đương (mặc định) 'bisim' tính phân giác mạnh 'bisim-sig' tính phân giác mạnh
sử dụng sàng lọc chữ ký 'branching-bisim' branching bisimilarity 'phân nhánh-
bisim-sig 'tính phân nhánh phân nhánh sử dụng sàng lọc chữ ký' dpbranching-bisim '
phân kỳ bảo toàn sự phân biệt phân nhánh 'dpbranching-bisim-sig' phân kỳ
duy trì tính phân nhánh phân nhánh bằng cách sử dụng tính năng sàng lọc chữ ký 'yếu-bisim' yếu
tính lưỡng tính 'yếu-bisim-sig' tính phân giác yếu sử dụng sàng lọc chữ ký 'dpweak-
bisim 'phân kỳ bảo toàn phân kỳ yếu' dpweak-bisim-sig 'phân kỳ
duy trì độ phân giác yếu bằng cách sử dụng mô phỏng mạnh mẽ 'sim' sàng lọc chữ ký
tương đương 'dấu vết' tương đương dấu vết mạnh 'dấu vết yếu' tương đương dấu vết yếu
giảm sao 'tau-star'

-iFORMAT, --trong=FORMAT
sử dụng FORMAT làm định dạng đầu vào

-lFILE, --lps=FILE
sử dụng FILE làm LPS mà từ đó LTS đầu vào được tạo ra; điều này có thể cần thiết để
lưu trữ tên tham số chính xác của các trạng thái khi lưu ở định dạng fsm và
chuyển đổi các LTS không phải mCRL2 thành mCRL2 LTS

- không tiếp cận được
không thực hiện kiểm tra khả năng tiếp cận trên LTS đầu vào

-n, - không có trạng thái
để lại thông tin trạng thái khi lưu ở định dạng dấu chấm

-oFORMAT, --ngoài=FORMAT
sử dụng FORMAT làm định dạng đầu ra

--tau=TÊN DIỆN
coi các hành động có tên trong danh sách được phân tách bằng dấu phẩy ACTNAMES là nội bộ
(tau) các hành động ngoài những hành động được xác định bởi đầu vào

--thời gian[=FILE]
nối các phép đo thời gian vào FILE. Các phép đo được ghi vào lỗi tiêu chuẩn nếu
không có FILE nào được cung cấp

Các tùy chọn tiêu chuẩn:

-q, --Yên lặng
không hiển thị thông báo cảnh báo

-v, --dài dòng
hiển thị thông báo trung gian ngắn

-d, --gỡ lỗi
hiển thị thông báo trung gian chi tiết

--mức đăng nhập=LEVEL
hiển thị các thông báo trung gian lên đến và bao gồm cả cấp

-h, --Cứu giúp
hiển thị thông tin trợ giúp

--phiên bản
hiển thị thông tin phiên bản

Sử dụng ltsconvert trực tuyến bằng các dịch vụ onworks.net