Tiếng AnhTiếng PhápTiếng ĐứcTiếng ÝBồ Đào NhaTiếng NgaTiếng Tây Ban Nha

Biểu tượng yêu thích OnWorks

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

Chạy maria trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks trên 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

Đây là maria lệnh có thể được 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


maria - Máy phân tích khả năng tiếp cận mô-đun cho lưới 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 chỉ huy. 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 đầu vào của nó
ngôn ngữ dựa trên Hệ thống Đại số Nets. Chủ nghĩa hình thức được trình bày bởi Ekkart
Kindler và Hagen Völzer tại ICATPN'98, Mềm dẻo in Đại số Lưới.
Nets hệ thống đại số là một khung không xác định bất kỳ kiểu dữ liệu hoặc đại số nào
các hoạt động. Hệ thống kiểu dữ liệu và các hoạt động trong Maria được thiết kế ở cấp độ cao
ngôn ngữ lập trình và đặc điểm kỹ thuật. Mặc dù vậy, mỗi người mẫu Maria 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 số nhận dạng trong
mở lưới thành các chuỗi ký tự chữ số và dấu gạch dưới. Bộ lọc
foldname.pl có thể được sử dụng hoặc điều chỉnh để cải thiện khả năng đọc của các số nhận dạng.

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 (`-'). Dưới đây là một bản tóm tắt các tùy chọn. Để có một mô tả đầy đủ, hãy xem
các tệp Thông tin.

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

-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-ưu tiên.

-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 quy trình của thuật toán phân tích phiên bản chuyển tiếp. Khi tùy chọn này được sử dụng,
các 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 trong một trạng thái; NS
mã biên dịch hiển thị số 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 cài sẵn. Đâ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, --depth-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 sâu.

-E khoảng thời gian, --edges =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
khoảng thời gian các cạnh 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]], --hashes =h[,f[,t]]
Định cấu hình các thông số để xác minh theo 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 từng bit. Cả hai h
f sẽ được làm tròn đến các giá trị phù hợp tiếp theo.

- ?, -NS, --Cứu giúp
In tóm tắt các tùy chọn dòng lệnh cho 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 (các tùy chọn -L, -M-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 xử lý. Xem thêm -k
-Z.

-k cổng[/chủ nhà], --connect =cổng[/chủ nhà]
Phân phối kiểm tra mô hình an toàn (các tùy chọn -L, -M-P) trong mạng TCP / IP. Vì
máy chủ, chỉ cổng được chỉ định dưới dạng số nguyên không dấu 16 bit, thường nằm giữa
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, --lossless =kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị cho việc 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ể truy cập
trong các tệp đĩa. Xem thêm -M, -P, -j-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-compacted =kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị cho việc phân tích nó bằng cách xây dựng một giá trị xấp xỉ cao hơn
tập hợp các trạng thái có thể truy cập trong bộ nhớ chính. Xem thêm -P, -L, -j-k.

-N cregexp, --name =cregexp
Chỉ định các tên được phép trong ngữ cảnh c dưới dạng biểu thức chính quy mở rộng regexp.
Bối cảnh được xác định bởi ký tự đầu tiên của chuỗi tham số; NS
các ký tự kế tiếp 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, --no-name =cregexp
Chỉ định những tên không được phép trong ngữ cảnh c dưới dạng 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 ngữ cảnh c, thì 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 -T'_t $ '. Các dấu ngoặc kép trong tham số sau là
bắt buộc phải loại bỏ ý nghĩa đặc biệt khỏi $ trong trình bao dòng lệnh, bạn là
có lẽ đang sử dụng để gọi Maria.

-P kiểu mẫu, --probabilistic =kiểu mẫu
Phụ tải kiểu mẫu và chuẩn bị cho việc 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ể truy cập
trong bộ nhớ chính bằng cách sử dụng một kỹ thuật được gọi là bitstate băm.

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

-q hạn chế, --quantification-limit =hạn chế
Ngăn chặn việc định lượng (tổng nhiều bộ) 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 các séc.

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

-u [a][f[ô uế]], --unfold =[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, kết xuất lưới mở ra đầu ra tiêu chuẩn. Các định dạng có thể
đang m (Maria (con người có thể đọc được), mặc định), l (LoLA), p (PEP), và r (PROD). Ở đó
là hai thuật toán: truyền thống (mặc định) và giảm bớt bằng cách xây dựng có thể che giấu được
đánh dấu (M).

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

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

-À, - cảnh báo
Bật cảnh báo về 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. Tắt 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. Các 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ân10. Mặc định là sử dụng
số thập phân.

-Y, - máy 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 đổi mà một ẩn điều kiện giữ. Những người kế vị ẩn là
được lưu trữ vào một tập hợ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 mà 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 lên đá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 liveness
kiểm tra, nhưng không có gì đảm bảo rằng các giá trị trung thực của các thuộ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, - đường dẫ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 trung gian có tại
nhất một kế. 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 rằng 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 sống động,
nhưng không có gì đảm bảo rằng các giá trị trung thực của các thuộ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, - không-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 các dịch vụ onworks.net


Ad


Ad

Các chương trình trực tuyến Linux & Windows mới nhất