Jest to polecenie ltsconvert, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
ltsconvert - konwertuje i opcjonalnie minimalizuje LTS
STRESZCZENIE
Konwertuj [OPCJA]... [W PLIKU [PLIK WYJŚCIOWY]]
OPIS
Przekonwertuj oznaczony system przejścia (LTS) z INFILE na OUTFILE w żądanym pliku
format po zastosowaniu wybranej metody minimalizacji (domyślnie brak). Jeśli OUTFILE jest
nie dostarczone, używane jest standardowe wyjście. Jeśli nie podano INFILE, używane jest stdin.
Format wyjściowy jest określony przez rozszerzenie OUTFILE, natomiast format wejściowy
określona przez zawartość INFILE. Opcje --in i --out mogą zostać użyte do wymuszenia wprowadzenia danych
i formaty wyjściowe. Obsługiwane formaty to:
„aut” dla formatu Aldebarana (CADP),
„kropka” dla formatu GraphViz (nie jest już obsługiwany jako format wejściowy),
„fsm” dla formatu skończonej maszyny stanowej, lub
„lts” dla formatu mCRL2 LTS (domyślnie)
OPCJE
OPCJA może być jednym z następujących:
-D, --określić
określić LTS
-eIMIĘ, --równorzędność=IMIĘ
wygeneruj równoważny LTS, zachowując równoważność NAZWA: tożsamość „none”.
równoważność (domyślnie) „bisim” silna dwupodobieństwo „bisim-sig” silna dwupodobieństwo
przy użyciu udoskonalenia podpisu „branching-bisim” rozgałęziająca bipodobieństwo „branching-
bisim-sig” bipodobieństwo rozgałęzień przy użyciu udoskonalenia sygnatury „dpbranching-bisim”
dywergencja zachowująca rozgałęzienie bipodobieństwa 'dpbranching-bisim-sig' dywergencja
zachowanie dwupodobieństwa rozgałęzień przy użyciu udoskonalenia sygnatury „weak-bisim” słaby
bipodobieństwo „weak-bisim-sig” słaba bipodobieństwo przy użyciu udoskonalenia sygnatury „dpweak-
rozbieżność bisim' zachowująca słabą bipodobieństwo rozbieżność 'dpweak-bisim-sig'
zachowanie słabej bipodobieństwa przy użyciu silnej symulacji „sim” udoskonalenia podpisu
równoważność „ślad” silna równoważność śladu „słaby ślad” słaba równoważność śladu
„gwiazda tau” redukcja gwiazdy tau
-iFORMAT, --w=FORMAT
użyj FORMAT jako formatu wejściowego
-lFILE, --lps=FILE
użyj PLIKU jako LPS, z którego wygenerowano wejściowy LTS; może to być konieczne
przechowuj prawidłowe nazwy parametrów stanów podczas zapisywania w formacie fsm i do
przekonwertować LTS inne niż mCRL2 na LTS mCRL2
--bez zasięgu
nie wykonuj sprawdzania osiągalności na wejściowym LTS
-n, --brak-stanu
pomiń informacje o stanie podczas zapisywania w formacie kropkowym
-oFORMAT, --na zewnątrz=FORMAT
użyj FORMAT jako formatu wyjściowego
--tau=NAZWY AKTU
uważaj akcje z nazwą na liście rozdzielonej przecinkami ACTNAMES za wewnętrzne
(tau) działania dodatkowe do tych zdefiniowanych jako takie na wejściu
--czasy[=FILE]
dołącz pomiary czasu do pliku FILE. Pomiary są zapisywane z błędem standardowym, jeśli
nie podano żadnego PLIKU
Opcje standardowe:
-q, --cichy
nie wyświetlaj komunikatów ostrzegawczych
-v, --gadatliwy
wyświetlaj krótkie komunikaty pośrednie
-d, --odpluskwić
wyświetlaj szczegółowe komunikaty pośrednie
--poziom-logarytmowania=POZIOM
wyświetlaj komunikaty pośrednie do poziomu włącznie
-h, --help
wyświetl informacje pomocy
--wersja
wyświetl informacje o wersji
Użyj ltsconvert online, korzystając z usług onworks.net
