Đây là lệnh pbesrewr 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 mô phỏng trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
pbesrewr - viết lại và đơn giản hóa PBES
SYNOPSIS
pbesrewr [TÙY CHỌN] ... [TRONG TẬP TIN [NGOÀI RA]]
MÔ TẢ
Viết lại PBES trong INFILE, xóa các biến đã định lượng và viết PBES kết quả vào
NGOÀI RA. Nếu không có INFILE, stdin sẽ được sử dụng. Nếu OUTFILE không có, stdout là
đã sử dụng.
LỰA CHỌN
TÙY CHỌN có thể là bất kỳ điều nào sau đây:
-iFORMAT, --trong=FORMAT
sử dụng định dạng đầu vào FORMAT: 'pbes' PBES ở định dạng nội bộ 'pbes_text' PBES trong
định dạng văn bản nội bộ 'văn bản' PBES ở định dạng văn bản (mCRL2) 'bes' BES trong nội bộ
định dạng 'bes_text' BES ở định dạng văn bản nội bộ 'cwi' BES ở định dạng CWI 'pgsolver'
BES ở định dạng PGSolver
-oFORMAT, --ngoài=FORMAT
sử dụng định dạng đầu ra FORMAT: 'pbes' PBES ở định dạng nội bộ 'pbes_text' PBES trong
định dạng văn bản nội bộ 'văn bản' PBES ở định dạng văn bản (mCRL2)
-pTÊN, --pbes-viết lại=TÊN
sử dụng chiến lược viết lại pbes TÊN: 'simple' để đơn giản hóa (mặc định)
'quantifier-all' để loại bỏ tất cả các định lượng 'quantifier-finite' cho
loại bỏ các biến định lượng hữu hạn 'định lượng-một-điểm' cho quy tắc một điểm
loại bỏ định lượng 'pfnf' để viết lại thành PFNF dạng bình thường 'ppg' cho
viết lại thành dạng Trò chơi chẵn lẻ được tham số 'bqnf-quantifier' để viết lại
bộ định lượng trên liên hợp đến liên hợp của bộ định lượng (thực nghiệm)
-QNUM, --qlimit=NUM
giới hạn việc liệt kê các định lượng đến NUM biến. (Mặc định NUM = 1000, NUM = 0 cho
vô hạn).
-rTÊN, - nhà văn=TÊN
sử dụng chiến lược viết lại TÊN: 'jitty' jitty viết lại (mặc định) 'jittyc' được biên dịch
jitty viết lại 'jittyp' jitty viết lại với câu châm ngôn
--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 pbesrewr trực tuyến bằng các dịch vụ onworks.net
