maria - Online w chmurze

PROGRAM:

IMIĘ

maria — modułowy analizator osiągalności dla wysokopoziomowych sieci Petriego

STRESZCZENIE

maria [Opcje] pliki...

OPIS

Ta strona podręcznika opisuje pokrótce maria Komenda. Bardziej kompletna dokumentacja to
dostępne w formacie GNU Info; patrz poniżej.

maria to program, który analizuje modele systemów współbieżnych, opisane na jego wejściu
język oparty na algebraicznych sieciach systemowych. Formalizm przedstawił Ekkart
Kindler i Hagen Völzer na ICATPN'98, Elastyczność in Algebraiczny Sieci.
Algebraic System Nets to framework, który nie definiuje żadnych typów danych ani algebraicznych
operacje. System typów danych i operacje w Maria są zaprojektowane z wysokim poziomem
mając na uwadze języki programowania i specyfikacji. Mimo to każdy model Marii ma
skończone rozwijanie.
Aby zapewnić interoperacyjność z narzędziami sieci Petriego niskiego poziomu, Maria tłumaczy identyfikatory na:
rozwinięte sieci do ciągów znaków alfanumerycznych i podkreśleń. Filtr
nazwa_folderu.pl mogą być używane lub dostosowywane w celu poprawy czytelności identyfikatorów.

OPCJE

Maria stosuje zwykłą składnię wiersza poleceń GNU, z długimi opcjami zaczynającymi się od dwóch
myślniki (`-'). Podsumowanie opcji znajduje się poniżej. Aby uzyskać pełny opis, zobacz
pliki informacyjne.

-a ograniczenie, --limit-tablicy=ograniczenie
Ogranicz rozmiar typów indeksów tablicy do ograniczenie możliwa wartość. Limit 0
wyłącza kontrole.

-b model, --wszerz-najpierw-szukaj=model
Wygeneruj wykres osiągalności model przy użyciu wyszukiwania wszerz.

-C katalog, --kompilacja=katalog
Generuj kod C w katalog do oceny wyrażeń i dla niskiego poziomu
procedury algorytmu analizy instancji przejścia. Gdy ta opcja jest używana,
błędy oceny zgłaszane są w nieco inny sposób. Tłumacz
wyświetla wycenę i wyrażenie, które spowodowało pierwszy błąd w stanie; ten
skompilowany kod wyświetla liczbę błędów. Ze względu na wydajność,
wygenerowany kod nie sprawdza błędów przepełnienia podczas dodawania elementów do wielu zestawów.

-C, --no-kompilacja
Przeciwieństwo -C. Oceń wszystkie wyrażenia we wbudowanym interpreterze. To jest
zachowanie domyślne.

-D symbol, --definiuj=symbol
Zdefiniuj symbol preprocesora symbol.

-d model, ---najpierw-wyszukiwanie w głąb=model
Wygeneruj wykres osiągalności model za pomocą wyszukiwania w głąb.

-E interwał, --krawędzie=interwał
Podczas generowania wykresu osiągalności zgłaszaj rozmiar wykresu po każdym
interwał wygenerowane krawędzie.

-e ciąg, --wykonaj=ciąg
Wykonać ciąg.

-g plik graficzny, --graf=plik graficzny
Załaduj wcześniej wygenerowany wykres osiągalności z plik graficznyrgh.

-H h[,f[,t]], --hash=h[,f[,t]]
Skonfiguruj parametry weryfikacji probabilistycznej (-P). Przeznaczyć t uniwersalny
funkcje haszujące f elementy i odpowiadające im tablice haszujące h bity każdy. Obie h
i f zostanie zaokrąglona w górę do kolejnych odpowiednich wartości.

-?, -H, --help
Wydrukuj podsumowanie opcji wiersza poleceń do Marii i zakończ.

-I katalog, --włącz=katalog
Dodać katalog do listy katalogów wyszukiwanych plików dołączanych.

-i kolumny, --szerokość=kolumny
Ustaw prawy margines wyjścia na kolumny. Wartość domyślna to 80.

-j procesów, --praca=procesów
Podczas sprawdzania właściwości bezpieczeństwa (opcje -L, -M i -P), użyj tego wielu pracowników
procesy przyspieszające analizę na komputerze wieloprocesorowym. Zobacz też -k i
-Z.

-k Port[/gospodarz], --połącz=Port[/gospodarz]
Dystrybucja sprawdzania modelu bezpieczeństwa (opcje -L, -M i -P) w sieci TCP/IP. Do
tylko serwer Port jest określony jako 16-bitowa liczba całkowita bez znaku, zwykle między
1024 i 65535. Dla procesów pracowniczych Port/gospodarz określa port i
adres serwera. Zobacz też -j.

-L model, --bezstratny=model
Załadować model i przygotować się do jego analizy, konstruując zbiór stanów osiągalnych
w plikach dyskowych. Zobacz też -M, -P, -j i -k.

-m model, --model=model
Załadować model i wyczyść jego wykres osiągalności.

-M model, --md5-skompaktowany=model
Załadować model i przygotuj się do analizy, konstruując nadmierne przybliżenie
zestaw stanów osiągalnych w pamięci głównej. Zobacz też -P, -L, -j i -k.

-N kregexp, --nazwa=kregexp
Określ nazwy dozwolone w kontekście c jako rozszerzone wyrażenie regularne regexp.
Kontekst jest identyfikowany przez pierwszy znak ciągu parametru; ten
kolejne znaki stanowią wyrażenie regularne, którego dozwolone nazwy muszą
mecz.

-n kregexp, --no-name=kregexp
Określ nazwy niedozwolone w kontekście c jako rozszerzone wyrażenie regularne
regexp.
Jeśli oba -N i i -n są określone dla kontekstu c, wtedy trwa mecz zezwalający
precedens. Na przykład, aby wymagać, aby wszystkie nazwy typów zdefiniowane przez użytkownika były:
zakończone z _t, podaj -nie -Nt'_t$'. Cytaty w drugim parametrze to
wymagane do usunięcia specjalnego znaczenia z $ w powłoce wiersza poleceń jesteś
prawdopodobnie używając do przywołania Marii.

-P model, --probabilistyczne=model
Załadować model i przygotować się do jego analizy, konstruując zbiór stanów osiągalnych
w pamięci głównej za pomocą techniki zwanej stan bitów mieszanie.

-p komenda, --właściwość-tłumacz=komenda
Określ polecenie, które będzie używane do tłumaczenia automatów właściwości. Polecenie powinno:
odczytaj wzór ze standardowego wejścia i napisz odpowiedni automat
opis na standardowe wyjście. Tłumacz funt jest z tym kompatybilny
opcja.

-q ograniczenie, --limit-ilości=ograniczenie
Zapobiegaj kwantyfikacji (suma wielozestawowa) typów mających więcej niż ograniczenie możliwy
wartości. Limit równy 0 wyłącza kontrole.

-U symbol, --niedefiniuj=symbol
Cofnij zdefiniowanie symbolu preprocesora symbol.

-u [a][f[plik wyjściowy]], --rozwiń=[a][f[plik wyjściowy]]
Rozłóż siatkę za pomocą algorytmu a i napisz to w formacie f do plik wyjściowy. Jeśli plik wyjściowy
nie jest określony, zrzuć rozłożoną siatkę na standardowe wyjście. Możliwe formaty
jest m (Maria (czytelna dla człowieka), domyślnie), l (LoLA), p (PEP) i r (SZTURCHAĆ). Tam
są dwa algorytmy: tradycyjny (domyślny) i zredukowany przez skonstruowanie a możliwy do pokrycia
Oznakowanie (M).

-V, --wersja
Wydrukuj numer wersji Marii i wyjdź.

-v, --gadatliwy
Wyświetlaj szczegółowe informacje na różnych etapach analizy.

-W, --ostrzeżenia
Włącz ostrzeżenia o podejrzanych konstrukcjach sieciowych. To jest zachowanie domyślne.

-w, --bez ostrzeżeń
Przeciwieństwo -W. Wyłącz wszystkie ostrzeżenia.

-x podstawa liczb, --radix=podstawa liczb
Określ podstawę liczbową dla danych wyjściowych diagnostyki. Dozwolone wartości dla podstawa liczb jest
październik, ósemkowy, 8, hex, szesnastkowy, 16, grudzień, dziesiętny i 10. Domyślnie jest używać
liczby dziesiętne.

-T, --skompresuj-ukryte
Zmniejsz zbiór stanów osiągalnych, nie przechowując stanów następczych
instancje przejść, dla których a ukryć warunek jest spełniony. Ukryci następcy to
przechowywane w oddzielnym zestawie stanów. Ta opcja może oszczędzać pamięć (-L or -m) lub zmniejsz
prawdopodobieństwo pominięcia stanów (-M or -P) i może poprawić
efektywność analizy równoległej (-j or -k), ale może też znacznie wzrosnąć
wymagania dotyczące czasu procesora. Opcja działa również z modelem na żywo
sprawdzanie, ale nie ma gwarancji, że prawdziwe wartości właściwości żywotności
pozostają bez zmian. Ta opcja może być łączona z -Z.

-y, --bez kompresji ukrytej
Przeciwieństwo -Y. To jest zachowanie domyślne.

-Z, --kompresuj-ścieżki
Zmniejsz zestaw stanów osiągalnych, nie przechowując stanów pośrednich, które mają
większość jeden następca. Ta opcja może oszczędzać pamięć (-L or -m) lub zmniejsz
prawdopodobieństwo pominięcia stanów (-M or -P) i może poprawić wydajność
analizy równoległej (-j or -k), ale może też znacznie zwiększyć
wymagania dotyczące czasu procesora. Opcja działa również przy sprawdzaniu modelu na żywo,
ale nie ma gwarancji, że prawdziwe wartości właściwości życiowych pozostaną
bez zmian. Ta opcja może być łączona z -Y.

-z, --no-compress-paths
Przeciwieństwo -Z. To jest zachowanie domyślne.

Korzystaj z marii online za pomocą usług onworks.net