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

CHƯƠNG TRÌNH:

TÊN

maria - Trình phân tích khả năng tiếp cận mô-đun cho mạng Petri cấp cao

SYNOPSIS

maria [lựa chọn] các tập tinhữu ích. Cảm ơn !

MÔ TẢ

Trang hướng dẫn sử dụng này tài liệu ngắn gọn về maria yêu cầu. Tài liệu đầy đủ hơn là
có sẵn ở định dạng Thông tin GNU; xem bên dưới.

maria là một chương trình phân tích các mô hình của các hệ thống đồng thời, được mô tả trong phần đầu vào của nó
ngôn ngữ dựa trên Mạng hệ thống đại số. Chủ nghĩa hình thức được trình bày bởi Ekkart
Kindler và Hagen Völzer tại ICATPN'98, Linh hoạt in Đại số Lưới.
Mạng hệ thống đại số là một khung không xác định bất kỳ loại dữ liệu hoặc đại số nào
hoạt động. Hệ thống kiểu dữ liệu và các thao tác trong Maria được thiết kế ở mức độ cao
ngôn ngữ lập trình và đặc tả trong tâm trí. Mặc dù vậy, mỗi mô hình Maria đều có một
sự mở ra hữu hạn.
Để đảm bảo khả năng tương tác với các công cụ mạng Petri cấp thấp, Maria dịch các mã định danh sang
các lưới được mở ra thành các chuỗi ký tự chữ và số và dấu gạch dưới. Bộ lọc
tên gấp.pl có thể được sử dụng hoặc điều chỉnh để cải thiện khả năng đọc của mã định danh.

LỰA CHỌN

Maria tuân theo cú pháp dòng lệnh GNU thông thường, với các tùy chọn dài bắt đầu bằng hai
dấu gạch ngang (`-'). Một bản tóm tắt các tùy chọn được bao gồm dưới đây. Để có mô tả đầy đủ, hãy xem
các tệp Thông tin.

-a hạn chế, --array-giới hạn=hạn chế
Giới hạn kích thước của các loại chỉ mục mảng ở mức hạn chế những giá trị khả thi. Giới hạn 0
vô hiệu hóa việc kiểm tra.

-b kiểu mẫu, --breadth-first-search=kiểu mẫu
Tạo biểu đồ khả năng tiếp cận của kiểu mẫu sử dụng tìm kiếm theo chiều rộng.

-C thư mục, --biên dịch=thư mục
Tạo mã C trong thư mục để đánh giá các biểu thức và cho mức độ thấp
các thủ tục của thuật toán phân tích cá thể chuyển tiếp. Khi tùy chọn này được sử dụng,
lỗi đánh giá được báo cáo theo một cách hơi khác. Thông dịch viên
hiển thị giá trị và biểu thức gây ra lỗi đầu tiên ở một trạng thái; các
mã được biên dịch hiển thị số lượng lỗi. Vì lý do hiệu suất,
mã được tạo không kiểm tra lỗi tràn khi thêm các mục vào nhiều bộ.

-NS, - không biên dịch
Sự đối lập của -C. Đánh giá tất cả các biểu thức trong trình thông dịch tích hợp. Đây là
hành vi mặc định.

-D biểu tượng, --define =biểu tượng
Xác định ký hiệu tiền xử lý biểu tượng.

-d kiểu mẫu, --độ sâu-tìm kiếm đầu tiên=kiểu mẫu
Tạo biểu đồ khả năng tiếp cận của kiểu mẫu sử dụng tìm kiếm theo chiều sâu.

-E khoảng thời gian, --edge=khoảng thời gian
Khi tạo biểu đồ khả năng tiếp cận, hãy báo cáo kích thước của biểu đồ sau mỗi lần
khoảng thời gian các cạnh được tạo ra.

-e chuỗi, --execute =chuỗi
Thực hiện chuỗi.

-g tệp đồ thị, --graph =tệp đồ thị
Tải biểu đồ khả năng tiếp cận được tạo trước đó từ tệp đồ thị.rgh.

-H h[,f[,t]], --băm=h[,f[,t]]
Định cấu hình các tham số để xác minh xác suất (-P). Chỉ định t phổ quát
hàm băm của f các phần tử và bảng băm tương ứng của h mỗi bit. Cả hai h
và f sẽ được làm tròn đến các giá trị phù hợp tiếp theo.

- ?, -NS, --Cứu giúp
In bản tóm tắt các tùy chọn dòng lệnh tới Maria và thoát.

-I thư mục, --bao gồm =thư mục
Nối thư mục vào danh sách các thư mục được tìm kiếm bao gồm các tệp.

-i cột, - width =cột
Đặt lề phải của đầu ra thành cột. Giá trị mặc định là 80.

-j Quy trình, --jobs =Quy trình
Khi kiểm tra các đặc tính an toàn (tùy chọn -L, -M và -P), sử dụng nhiều công nhân này
các quy trình để tăng tốc độ phân tích trên máy tính đa bộ xử lý. Xem thêm -k và
-Z.

-k cổng[/chủ nhà], --connect =cổng[/chủ nhà]
Phân phối kiểm tra mô hình an toàn (tùy chọn -L, -M và -P) trong mạng TCP/IP. Vì
máy chủ, chỉ cổng được chỉ định là số nguyên không dấu 16 bit, thường nằm trong khoảng
1024 và 65535. Đối với các quy trình công nhân, cổng/chủ nhà chỉ định cổng và
địa chỉ của máy chủ. Xem thêm -j.

-L kiểu mẫu, --không mất mát=kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị phân tích nó bằng cách xây dựng một tập hợp các trạng thái có thể tiếp cận
trong các tập tin đĩa. Xem thêm -M, -P, -j và -k.

-m kiểu mẫu, --mẫu =kiểu mẫu
Phụ tải kiểu mẫu và xóa biểu đồ khả năng tiếp cận của nó.

-M kiểu mẫu, --md5-compact=kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị phân tích nó bằng cách xây dựng một xấp xỉ quá mức
tập hợp các trạng thái có thể truy cập được trong bộ nhớ chính. Xem thêm -P, -L, -j và -k.

-N cregexp, --name =cregexp
Chỉ định tên được phép trong ngữ cảnh c như biểu thức chính quy mở rộng regexp.
Ngữ cảnh được xác định bằng ký tự đầu tiên của chuỗi tham số; các
các ký tự tiếp theo tạo thành biểu thức chính quy mà các tên được phép phải
phù hợp.

-n cregexp, --không tên=cregexp
Chỉ định tên không được phép trong ngữ cảnh c như biểu thức chính quy mở rộng
regexp.
Nếu cả hai -N và và -n được chỉ định cho một bối cảnh c, sau đó trận đấu cho phép diễn ra
quyền ưu tiên. Ví dụ: để yêu cầu tất cả các tên loại do người dùng xác định phải
chấm dứt với _t, chỉ định -nt -Nt'_t$'. Các trích dẫn trong tham số sau là
cần phải loại bỏ ý nghĩa đặc biệt khỏi $ trong shell dòng lệnh bạn là
có lẽ dùng để gọi Maria.

-P kiểu mẫu, --xác suất=kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị phân tích nó bằng cách xây dựng một tập hợp các trạng thái có thể tiếp cận
trong bộ nhớ chính bằng cách sử dụng một kỹ thuật gọi là trạng thái bit băm.

-p lệnh, --property-dịch=lệnh
Chỉ định lệnh sẽ sử dụng để dịch automata thuộc tính. Lệnh nên
đọc công thức từ đầu vào tiêu chuẩn và viết máy tự động tương ứng
mô tả thành đầu ra tiêu chuẩn. Người dịch LBT tương thích với cái này
tùy chọn.

-q hạn chế, --giới hạn định lượng=hạn chế
Ngăn chặn việc định lượng (tổng nhiều tập hợp) của các loại có nhiều hơn hạn chế có thể
các giá trị. Giới hạn 0 sẽ vô hiệu hóa việc kiểm tra.

-U biểu tượng, --undefine =biểu tượng
Không xác định ký hiệu tiền xử lý biểu tượng.

-u [a][f[ô uế]], --mở ra=[a][f[ô uế]]
Mở rộng mạng bằng thuật toán a và viết nó ở định dạng f đến ô uế. Nếu ô uế
không được chỉ định, hãy chuyển mạng chưa mở sang đầu ra tiêu chuẩn. Các định dạng có thể có
đang m (Maria (người có thể đọc được), mặc định), l (LoLA), p (PEP) và r (SẢN PHẨM). Ở đó
là hai thuật toán: truyền thống (mặc định) và rút gọn bằng cách xây dựng một có thể che phủ được
đánh dấu (M).

-V, --phiên bản
In số phiên bản của Maria và thoát.

-v, --dài dòng
Hiển thị thông tin chi tiết về các giai đoạn phân tích khác nhau.

-À, - cảnh báo
Bật cảnh báo về các cấu trúc mạng đáng ngờ. Đây là hành vi mặc định.

-w, --không cảnh báo
Sự đối lập của -W. Vô hiệu hóa tất cả các cảnh báo.

-x cơ sở số, --radix =cơ sở số
Chỉ định cơ sở số cho đầu ra chẩn đoán. Giá trị được phép cho cơ sở số đang
Tháng Mười, bát phân, 8, hex, thập lục phân, 16, Tháng mười hai, số thập phân và 10. Mặc định là sử dụng
số thập phân.

-Ừ, --nén-ẩn
Giảm tập hợp các trạng thái có thể truy cập bằng cách không lưu trữ các trạng thái kế tiếp của
các trường hợp chuyển tiếp trong đó một ẩn điều kiện giữ. Những người kế vị ẩn giấu là
được lưu trữ vào một tập trạng thái riêng biệt. Tùy chọn này có thể tiết kiệm bộ nhớ (-L or -m) hoặc giảm
xác suất các trạng thái bị bỏ qua (-M or -P) và nó có thể cải thiện
hiệu quả của phân tích song song (-j or -k), nhưng nó cũng có thể tăng đáng kể
yêu cầu về thời gian của bộ xử lý. Tùy chọn này cũng hoạt động với mô hình sống động
đang kiểm tra, nhưng không có gì đảm bảo rằng giá trị thực của các đặc tính sống động
vẫn không thay đổi. Tùy chọn này có thể được kết hợp với -Z.

-y, --no-nén-ẩn
Sự đối lập của -Y. Đây là hành vi mặc định.

-Z, --nén-đường dẫn
Giảm tập hợp các trạng thái có thể truy cập bằng cách không lưu trữ các trạng thái trung gian có tại
hầu hết đều là người kế vị. Tùy chọn này có thể tiết kiệm bộ nhớ (-L or -m) hoặc giảm
xác suất các trạng thái bị bỏ qua (-M or -P) và nó có thể cải thiện hiệu quả
phân tích song song (-j or -k), nhưng nó cũng có thể làm tăng đáng kể
yêu cầu về thời gian của bộ xử lý. Tùy chọn này cũng hoạt động với việc kiểm tra mô hình hoạt động,
nhưng không có gì đảm bảo rằng giá trị thực của các đặc tính sống động vẫn còn
không thay đổi. Tùy chọn này có thể được kết hợp với -Y.

-z, --no-nén-đường dẫn
Sự đối lập của -Z. Đây là hành vi mặc định.

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