Đây là lệnh ltscompare có thể chạy trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks bằng cách sử dụng một trong nhiều máy trạm trực tuyến miễn phí của chúng tôi như Ubuntu Online, Fedora Online, trình giả lập trực tuyến Windows hoặc trình giả lập trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
ltscompare - so sánh hai LTS
SYNOPSIS
so sánh [TÙY CHỌN] ... [INFILE1] INFILE2
MÔ TẢ
Xác định xem các hệ thống chuyển tiếp được dán nhãn (LTS) trong INFILE1 và INFILE2 có
liên quan bởi một số tương đương hoặc đặt hàng trước. Nếu INFILE1 không được cung cấp, stdin sẽ được sử dụng.
Các định dạng đầu vào được xác định bởi nội dung của INFILE1 và INFILE2. Tùy chọn --in1
và --in2 có thể được sử dụng để buộc định dạng đầu vào của INFILE1 và INFILE2 tương ứng. Các
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
LỰA CHỌN
TÙY CHỌN có thể là bất kỳ điều nào sau đây:
-c, --counter-ví dụ
tạo dấu vết ví dụ bộ đếm nếu lts đầu vào không tương đương
-eTÊN), - tương đương=TÊN)
sử dụng NAME tương đương (không được phép kết hợp với -p / - preorder): 'none'
tương đương danh tính (mặc định) 'bisim' tính phân giác mạnh 'branching-bisim'
sự phân biệt phân nhánh phân nhánh 'dpbranching-bisim' bảo tồn sự phân nhánh
tính phân giác 'yếu-bisim' tính phân giác yếu 'dpweak-bisim' bảo toàn
tính lưỡng tính yếu 'sim' tương đương mô phỏng mạnh 'dấu vết' dấu vết mạnh
tương đương 'dấu vết yếu' tương đương dấu vết yếu
-iFORMAT, --trong 1=FORMAT
sử dụng FORMAT làm định dạng cho INFILE1 (hoặc stdin)
-jFORMAT, --trong 2=FORMAT
sử dụng FORMAT làm định dạng cho INFILE2
-pTÊN, --đặt hàng trước=TÊN
sử dụng NAME đặt hàng trước (không được phép kết hợp với -e / - tương đương): 'không xác định'
đặt hàng trước không xác định (mặc định) 'sim' đặt trước mô phỏng mạnh mẽ 'theo dõi' dấu vết mạnh mẽ
đặt hàng trước theo dõi yếu 'dấu vết yếu'
--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 ltscompare trực tuyến bằng các dịch vụ onworks.net
