lpsinvelm - Trực tuyến trên Đám mây

CHƯƠNG TRÌNH:

TÊN

lpsinvelm - kiểm tra các bất biến và sử dụng chúng để đơn giản hóa hoặc loại bỏ các triệu hồi của một LPS

SYNOPSIS

lpsinvelm [TÙY CHỌN] ... --invfile = INVFILE [TRONG TẬP TIN [NGOÀI RA]]

MÔ TẢ

Kiểm tra xem công thức boolean (một biểu thức dữ liệu mCRL2 của sắp xếp Bool) có được cung cấp dưới dạng không
invariant là một bất biến của đặc tả quy trình tuyến tính (LPS) trong INFILE. Nêu Đây la
trường hợp này, công cụ loại bỏ tất cả các lệnh triệu hồi của LPS có điều kiện vi phạm
bất biến, và ghi kết quả vào OUTFILE. Nếu có INFILE, stdin được sử dụng. Nếu như
OUTFILE không có, stdout được sử dụng.

Công cụ này cũng có thể được sử dụng để đơn giản hóa các điều kiện của các triệu hồi và LPS đã cho.

LỰA CHỌN

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

-y, - tất cả các vi phạm
không chấm dứt ngay khi phát hiện thấy một vi phạm duy nhất của bất biến, nhưng
báo cáo tất cả các vi phạm thay thế

-c, --counter-ví dụ
hiển thị một định giá cho biết lý do tại sao điều bất biến có thể bị vi phạm nếu nó
không chắc liệu một triệu hồi có vi phạm điều bất biến

-o, --hướng dẫn
áp dụng giới thiệu trên danh sách

-iTUYỂN DỤNG, --bất biến=TUYỂN DỤNG
sử dụng công thức boolean (một biểu thức dữ liệu mCRL2 của sắp xếp Bool) trong INVFILE dưới dạng
bất biến

-n, --Không kiểm tra
không kiểm tra xem bất biến có giữ được không trước khi loại bỏ các triệu hồi không thể truy cập

-e, --không loại bỏ
không loại bỏ hoặc đơn giản hóa các triệu hồi, nhưng thêm bất biến vào mỗi điều kiện

-pTIẾP ĐẦU NGỮ, - dấu chấm=TIẾP ĐẦU NGỮ
lưu tệp .dot của BDD kết quả nếu không thể xác định xem
summand vi phạm bất biến; PREFIX sẽ được sử dụng làm tiền tố của các tệp đầu ra

-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

-l, --đơn giản hóa-tất cả
đơn giản hóa các điều kiện của tất cả các summand, thay vì chỉ loại bỏ các summand
mà điều kiện kết hợp với điều kiện bất biến là mâu thuẫn

-zGIẢI, --smt-bộ giải quyết=GIẢI
sử dụng SOLVER để xóa các đường dẫn không nhất quán khỏi các BDD được sử dụng nội bộ (theo mặc định,
không áp dụng loại bỏ đường dẫn): 'cvc' trình giải quyết SMT CVC3

-tLIMIT, --thời gian giới hạn=LIMIT
dành nhiều nhất LIMIT giây để chứng minh một công thức

--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 lpsinvelm trực tuyến bằng các dịch vụ onworks.net