lps2lts - Online w chmurze

PROGRAM:

IMIĘ

lps2lts - wygeneruj LTS z LPS

STRESZCZENIE

lps2lts [OPCJA]... [W PLIKU [PLIK WYJŚCIOWY]]

OPIS

Wygeneruj LTS z LPS w INFILE i zapisz wynik w OUTFILE. Jeśli INFILE nie jest
dostarczone, używane jest stdin. Jeżeli OUTFILE nie zostanie podany, LTS nie zostanie zapisany.

Jeśli używany jest moduł zapisujący „jittyc”, wówczas zmienna środowiskowa MCRL2_COMPILEREWRITER
(wartość domyślna: 'mcrl2compilerewriter') określa skrypt, który kompiluje moduł rewriterski,
i MCRL2_COMPILEDIR (wartość domyślna: '.') określa, gdzie przechowywane są pliki tymczasowe.

Należy pamiętać, że lps2lts może dostarczyć wiele przejść z tą samą etykietą pomiędzy dowolną parą
stwierdza. Jeśli nie jest to pożądane, takie przejścia można usunąć, stosując mocny
Redukcja bisymulacyjna za pomocą na przykład narzędzia ltsconvert.

Format pliku OUTFILE jest określony przez jego rozszerzenie (chyba że jest ono określone przez rozszerzenie
opcja). 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 Jeśli używany jest moduł zapisujący jittyc, wówczas plik
Zmienna środowiskowa MCRL2_COMPILEREWRITER (wartość domyślna: mcrl2compilerewriter)
określa skrypt, który kompiluje moduł zapisujący, oraz MCRL2_COMPILEDIR (wartość domyślna:
„.”) określa, gdzie przechowywane są pliki tymczasowe. Należy pamiętać, że lps2lts może dostarczyć wiele plików
przejścia o tej samej etykiecie pomiędzy dowolną parą stanów. Jeśli nie jest to pożądane, np
przejścia można usunąć stosując silną redukcję bisymulacyjną za pomocą np
narzędzie ltsconvert.

OPCJE

OPCJA może być jednym z następujących:

-aNAZWY, --akcja=NAZWY
wykrywa i raportuje akcje w systemie przejść, które mają nazwy akcji
NAZWY, lista rozdzielona przecinkami. Jest to na przykład przydatne do znalezienia (lub udowodnienia
brak) błędu działania. Przy każdym wystąpieniu jednego z nich drukowany jest komunikat
te nazwy akcji. Z flagą -t generowane są ślady tych działań

-b[NUM], --bit-hash[=NUM]
użyj skrótu bitowego do przechowywania stanów i przechowuj co najwyżej stany NUM. To znaczy że
zamiast prowadzić pełny zapis wszystkich odwiedzonych stanów, tablicę bitów
służy do wskazania, czy skrót stanu był już widziany, czy nie.
Chociaż oznacza to, że ta opcja może powodować mylenie stanów z innymi
(ponieważ są mapowane na ten sam skrót), przydatne może być eksplorowanie bardzo dużych obiektów
LTS, których w innym przypadku nie można eksplorować. Domyślna wartość NUM to w przybliżeniu
2*10^8 (odpowiada to około 25 MB pamięci)

-- w pamięci podręcznej
użyj technik buforowania wyliczeń, aby przyspieszyć generowanie przestrzeni stanów.

-c[IMIĘ], --zbieg[=IMIĘ]
zastosuj priorytetyzację przejść za pomocą etykiety akcji NAZWA. (gdy nie ma NAZWY
dostarczone (tj. „-c”) priorytet ma akcja „ctau”. Aby dać pierwszeństwo
aby tau użyć flagi -ctau. Należy zauważyć, że jeśli proces liniowy nie jest zbieżny z tau,
wygenerowana przestrzeń stanów jest z konieczności rozgałęziona w sposób bipodobny do przestrzeni stanów
lps. Zastosowany algorytm generacji nie wymaga procesu liniowego
być zbieżny tau.

-D, --impas
wykrywać zakleszczenia (tj. dla każdego zakleszczenia drukowany jest komunikat)

-F, --rozbieżność
wykryć rozbieżności (tj. dla każdego stanu z rozbieżnością (= pętla tau) jest to wiadomość
drukowane). Algorytm wykrywania rozbieżności jest liniowy dla każdego stanu, tj
eksploracja przestrzeni stanów staje się kwadratowa, gdy ta opcja jest włączona, powodując stan
eksploracja kosmosu staje się powolna, gdy ta opcja jest włączona.

-yBOOL, --atrapa=BOOL
zamień wolne zmienne w LPS na wartości fikcyjne oparte na wartości BOOL:
„tak” (domyślnie) lub „nie”

--śledzenie błędów
jeśli podczas eksploracji wystąpi błąd, zapisz ślad do stanu, w którym nie mogło być
zbadane

--init-tsize=NUM
ustaw początkowy rozmiar wewnętrznie używanych tabel skrótów (domyślnie jest to 10000)

-lNUM, --maks=NUM
eksploruj co najwyżej NUM stanów

-mNAZWY, --multikcja=NAZWY
wykrywać i raportować multiakcje w systemie przejść z NAZW, przecinka
oddzielna lista. Działa jak -a, z tą różnicą, że wiele akcji jest dokładnie dopasowywanych,
łącznie z parametrami danych.

--brak informacji
nie dodawaj informacji o stanie do OUTFILEBez tej opcji lps2lts dodaje stan
wektor do LTS. Ta opcja powoduje odrzucenie tych informacji i stanów
są oznaczone jedynie numerem porządkowym. Jawne informacje o stanie są przydatne w przypadku
na przykład do celów wizualizacji, ale może spowodować wzrost pliku OUTFILE
wydatnie. Należy pamiętać, że ta opcja jest niejawna podczas zapisu w formacie AUT.

-oFORMAT, --na zewnątrz=FORMAT
zapisz wynik w określonym FORMACIE

--suszona śliwka
użyj czyszczenia sumarycznego, aby przyspieszyć generowanie przestrzeni stanów.

-QNUM, --qlimit=NUM
ograniczyć wyliczanie kwantyfikatorów do NUM zmiennych. (Domyślnie NUM=1000, NUM=0 dla
Nieograniczony).

-rIMIĘ, --przepisujący=IMIĘ
użyj strategii przepisywania NAZWA: 'jitty' jitty przepisywanie (domyślnie) 'jittyc' skompilowane
jitty przepisywanie 'jittyp' jitty przepisywanie z prover

-sIMIĘ, --strategia=IMIĘ
eksploruj przestrzeń stanów, używając strategii NAZWA: „b”, „szerokość” przeszukiwanie wszerz
(domyślnie) „d”, „głębokość” wyszukiwanie w głąb „p”, „z priorytetem” priorytetyzacja pojedynczego
akcje, których pierwszym argumentem jest rodzaj Nat, gdzie tylko te akcje z
wybierana jest najniższa wartość tego parametru. Np. jeśli są jakieś działania a(3) i
b(4) a(3) pozostaje i b(4) zostaje pominięty. Akcje bez pierwszego parametru sortowania
Zawsze wybierane są nat i multiakcje z więcej niż jedną akcją (opcja to
eksperymentalne) „q”, „priorytetyzowane” nadają priorytet działaniom na podstawie pierwszego argumentu
sortuj Nat (patrz opcja --priorytet) i losowo wybierz jedną z nich, aby uzyskać
symulacja losowa z priorytetem (opcja jest eksperymentalna) 'r', 'losowa' losowa
symulacja. Ze wszystkich kolejnych stanów jeden jest wybierany losowo, niezależnie od tego, czy
stan ten został już zaobserwowany. W związku z tym tylko losowa symulacja
kończy się w przypadku napotkania stanu zakleszczenia.

--stłumić
w trybie szczegółowym nie drukuj komunikatów o postępie wskazujących liczbę odwiedzin
stany i przejścia. W przypadku dużych przestrzeni stanów liczba komunikatów postępu może być większa
być dość okropne. Ta funkcja pomaga je stłumić. Inne szczegółowe wiadomości,
takie jak całkowita liczba zbadanych stanów, po prostu pozostają widoczne.

--czasy[=FILE]
dołącz pomiary czasu do pliku FILE. Pomiary są zapisywane z błędem standardowym, jeśli
nie podano żadnego PLIKU

--do-maks=NUM
przechowuj na listach rzeczy do zrobienia maksymalnie NUM stanów; ta opcja ma zastosowanie tylko w przypadku szerokości
pierwsze wyszukiwanie, gdzie NUM to maksymalna liczba stanów na poziom oraz głębokość
pierwsze wyszukiwanie, gdzie NUM to maksymalna głębokość

-t[NUM], --namierzać[=NUM]
Zapisz najkrótszy ślad do każdego stanu, który zostanie osiągnięty dzięki akcji z NAMES
opcja --action, oznacza zakleszczenie wykryte za pomocą opcji --deadlock lub jest rozbieżnością
wykryte z opcją --divergence do pliku. Zostanie zapisanych nie więcej niż NUM śladów. Jeśli
Nie podano liczby NUM, liczba śladów jest nieograniczona. Dla każdego śladu, który ma być
zapisany zostanie unikalny plik z rozszerzeniem .trc (trace) zawierający plik
najkrótszy ślad od stanu początkowego do stanu zakleszczenia. Ślady mogą być
ładnie wydrukowane i przekonwertowane na inne formaty za pomocą programu Trapp.

-u, --nieużywane-dane
nie usuwaj niewykorzystanych części specyfikacji danych

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 lps2lts online, korzystając z usług onworks.net