Đây là ứng dụng Linux có tên VeriSiMPL có bản phát hành mới nhất có thể được tải xuống dưới tên VeriSiMPL_Version3-0.tar.gz. Nó có thể được chạy trực tuyến trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks cho máy trạm.
Tải xuống và chạy trực tuyến ứng dụng này có tên là VeriSiMPL với OnWorks miễn phí.
Làm theo các hướng dẫn sau để chạy ứng dụng này:
- 1. Đã tải ứng dụng này xuống PC của bạn.
- 2. Nhập vào trình quản lý tệp của chúng tôi https://www.onworks.net/myfiles.php?username=XXXXX với tên người dùng mà bạn muốn.
- 3. Tải lên ứng dụng này trong trình quản lý tệp như vậy.
- 4. Khởi động trình giả lập trực tuyến OnWorks Linux hoặc trình giả lập trực tuyến Windows hoặc trình mô phỏng trực tuyến MACOS từ trang web này.
- 5. Từ Hệ điều hành OnWorks Linux mà bạn vừa khởi động, hãy truy cập trình quản lý tệp của chúng tôi https://www.onworks.net/myfiles.php?username=XXXXX với tên người dùng mà bạn muốn.
- 6. Tải xuống ứng dụng, cài đặt và chạy nó.
MÀN HÌNH
Ad
VeriSiMPL
MÔ TẢ
Hộp công cụ này được sử dụng để tạo ra các bản tóm tắt hữu hạn của các hệ thống Max-Plus-Linear (MPL) tự trị trên R ^ n. Tính trừu tượng được đặc trưng như Hệ thống chuyển tiếp có nhãn trạng thái hữu hạn (LTS). Các phần trừu tượng hữu hạn của LTS được hiển thị để mô phỏng hoặc phân đôi hệ thống MPL ban đầu. Các mô hình LTS phải được xác minh dựa trên các thông số kỹ thuật nhất định được biểu thị dưới dạng công thức trong Logic thời gian tuyến tính (LTL) và Logic cây tính toán (CTL). Hộp công cụ dự định tận dụng trình kiểm tra mô hình NuSMV. Các mô hình sẽ được thể hiện bằng ngôn ngữ C ++. Thủ tục trừu tượng chạy trong C ++. LTS đã tạo được xuất sang ngôn ngữ NuSMV. Như vậy, nó có thể được cung cấp, cùng với một thông số kỹ thuật quan tâm, cho trình kiểm tra mô hình NuSMV.
Nếu bạn quen thuộc hơn với ngôn ngữ JAVA, chúng tôi khuyên bạn nên thử VeriSiMPL phiên bản 2.0 hoàn toàn dựa trên JAVA.
Nếu bạn quen thuộc hơn với ngôn ngữ MATLAB, chúng tôi khuyên bạn nên thử VeriSiMPL phiên bản 1.4 hoàn toàn dựa trên MATLAB.
Tính năng
- Tạo trừu tượng LTS trạng thái hữu hạn từ hệ thống MPL bằng cách sử dụng cấu trúc dữ liệu cây và danh sách
- Tạo đại diện Affine theo từng mảnh từ hệ thống MPL
- Xác minh hệ thống MPL dựa trên công thức LTL hoặc CTL
- Hình dung TS trong Graphviz (Phiên bản 1.4)
- Xuất mô hình tự trị sang hệ thống PWA trong cấu trúc MPT (Phiên bản 1.4)
- Phân tích khả năng tiếp cận của hệ thống MPL (Phiên bản 1.4)
- GUI để tóm tắt và xác minh các hệ thống MPL tự trị (Phiên bản 1.4)
- GUI cho khả năng truy cập chuyển tiếp của các hệ thống MPL tự trị (Phiên bản 1.4)
Khán giả
Khoa học / Nghiên cứu, Giáo dục, Kỹ thuật
Ngôn ngữ lập trình
MATLAB, Java
Danh Mục
Đây là một ứng dụng cũng có thể được tìm nạp từ https://sourceforge.net/projects/verisimpl/. Nó đã được lưu trữ trên OnWorks để có thể chạy trực tuyến một cách dễ dàng nhất từ một trong những Hệ thống hoạt động miễn phí của chúng tôi.
