To jest aplikacja Linux o nazwie VeriSiMPL, której najnowszą wersję można pobrać jako VeriSiMPL_Version3-0.tar.gz. Można ją uruchomić online w darmowym dostawcy hostingu OnWorks dla stacji roboczych.
Pobierz i uruchom online tę aplikację o nazwie VeriSiMPL z OnWorks za darmo.
Postępuj zgodnie z tymi instrukcjami, aby uruchomić tę aplikację:
- 1. Pobrałem tę aplikację na swój komputer.
- 2. Wpisz w naszym menedżerze plików https://www.onworks.net/myfiles.php?username=XXXXX z wybraną nazwą użytkownika.
- 3. Prześlij tę aplikację w takim menedżerze plików.
- 4. Uruchom emulator online OnWorks Linux lub Windows online lub emulator online MACOS z tej witryny.
- 5. W systemie operacyjnym OnWorks Linux, który właśnie uruchomiłeś, przejdź do naszego menedżera plików https://www.onworks.net/myfiles.php?username=XXXXX z wybraną nazwą użytkownika.
- 6. Pobierz aplikację, zainstaluj ją i uruchom.
ZRZUTY EKRANU
Ad
VeriSiMPL
OPIS
Ten zestaw narzędzi służy do generowania skończonych abstrakcji autonomicznych systemów Max-Plus-Linear (MPL) w oparciu o R^n. Abstrakcje charakteryzują się skończonymi znakowanymi systemami przejściowymi (LTS). Pokazano, że skończone abstrakcje LTS symulują lub bisymulują oryginalny system MPL. Modele LTS należy weryfikować pod kątem podanych specyfikacji wyrażonych we wzorach w Liniowej Logice Temporalnej (LTL) i Logice Drzewa Obliczeniowego (CTL). Zestaw narzędzi ma na celu wykorzystanie modułu sprawdzania modelu NuSMV. Modele mają być wyrażone w języku C++. Procedura abstrakcji działa w języku C++. Wygenerowany LTS jest eksportowany do języka NuSMV. Jako taki może zostać wprowadzony wraz z interesującą nas specyfikacją do modułu sprawdzającego model NuSMV.
Jeśli znasz lepiej język JAVA, sugerujemy wypróbowanie wersji 2.0 VeriSiMPL, która jest w pełni oparta na JAVA.
Jeśli jesteś bardziej zaznajomiony z językiem MATLAB, sugerujemy wypróbowanie VeriSiMPL w wersji 1.4, która jest w pełni oparta na MATLAB-ie.
Funkcjonalności
- Wygeneruj abstrakcję LTS o skończonych stanach z systemu MPL przy użyciu listy i struktury danych drzewa
- Wygeneruj fragmentaryczną reprezentację afiniczną z systemu MPL
- Zweryfikuj system MPL pod kątem formuły LTL lub CTL
- Wizualizuj TS w Graphviz (wersja 1.4)
- Eksport modelu autonomicznego do systemu PWA w strukturze MPT (wersja 1.4)
- Analiza osiągalności systemów MPL (wersja 1.4)
- GUI do abstrakcji i weryfikacji autonomicznych systemów MPL (wersja 1.4)
- GUI dla osiągalności w przód autonomicznych systemów MPL (wersja 1.4)
Publiczność
Nauka/badania, edukacja, inżynieria
Język programowania
MATLAB, Jawa
Kategorie
Jest to aplikacja, którą można również pobrać ze strony https://sourceforge.net/projects/verisimpl/. Został on hostowany w OnWorks, aby można go było uruchomić online w najprostszy sposób z jednego z naszych bezpłatnych systemów operacyjnych.
