pbes2bes – Online w chmurze

PROGRAM:

IMIĘ

pbes2bes - Wygeneruj BES z PBES.

STRESZCZENIE

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

OPIS

Odczytuje PBES z INFILE i zapisuje równoważny BES do OUTFILE. Jeśli INFILE nie jest
obecnie używane jest stdin. Jeśli OUTFILE nie jest obecny, używane jest standardowe wyjście.

OPCJE

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

-ePOZIOM, --usuwać=POZIOM
użyj opcji usuń poziom POZIOM, aby usunąć zmienne bes 'none' nie usuwaj wygenerowanych bes
zmienne. Może to prowadzić do nadmiernego wykorzystania pamięci. (domyślnie) „niektóre” usuń
generowane są zmienne, które nie są używane, z wyjątkiem prawej strony
równanie jest prawdziwe lub fałszywe. Należy ponownie obliczyć rhss zmiennych, jeśli
spotkałem ponownie, co jest całkiem normalne. „all” usuwa każdą zmienną bes
nie jest już używany w żadnym równaniu. Jest to dość wydajne rozwiązanie pod względem pamięci, ale może tak być
bardzo czasochłonne, ponieważ może być konieczne określenie rhss usuniętych zmiennych bes
przeliczane dość często.

-H, --tablice skrótów
używaj tablic haszujących podczas podstawiania równań besa i tłumacz wewnętrznie
wyrażenia do binarnych diagramów decyzyjnych (odradzane ze względu na wydajność)

-iFORMAT, --w=FORMAT
użyj formatu wejściowego FORMAT: 'pbes' PBES w formacie wewnętrznym 'pbes_text' PBES w
wewnętrzny format tekstowy 'text' PBES w formacie tekstowym (mCRL2) 'bes' BES w wewnętrznym
format 'bes_text' BES w wewnętrznym formacie tekstowym 'cwi' BES w formacie CWI 'pgsolver'
BES w formacie PGSolver

-oFORMAT, --na zewnątrz=FORMAT
użyj formatu wyjściowego FORMAT: 'pbes' PBES w formacie wewnętrznym 'pbes_text' PBES w
wewnętrzny format tekstowy 'text' PBES w formacie tekstowym (mCRL2) 'bes' BES w wewnętrznym
format 'bes_text' BES w wewnętrznym formacie tekstowym 'cwi' BES w formacie CWI 'pgsolver'
BES w formacie PGSolver

-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

-zSZUKAJ, --Szukaj=SZUKAJ
użyj strategii wyszukiwania SZUKAJ: „najpierw wszerz” Oblicz prawą stronę
zmienne logiczne, według kolejności zgłoszeń. Można to porównać z a
wyszukiwanie wszerz. Jest to dobre do generowania przykładów przeciwnych. (domyślny)
„najpierw głębokość” Oblicza prawą stronę zmiennych logicznych, gdzie ostatnia
wygenerowana zmienna jest badana w pierwszej kolejności. Odpowiada to pierwszemu podejściu w głąb
szukaj. Może to znacznie przewyższać wyszukiwanie wszerz, gdy ważność
formułę ustala się po większych głębokościach. „b” Krótka ręka oznaczająca „najpierw szerokość”.
„d” Krótka ręka oznaczająca głębokość.

-sSTRAT, --strategia=STRAT
użyj strategii podstawienia STRAT: '0' Oblicz wszystkie równania logiczne, jakie mogą być
osiągnięty od stanu początkowego, bez optymalizacji. To najwięcej danych
wydajna opcja na wygenerowane równanie. (domyślnie) '1' Optymalizuj natychmiast
zastępując prawą stronę już zbadanych zmiennych, które są prawdziwe
lub false podczas generowania wyrażenia. Efektywność pamięci wynosi 0 cala
oprócz 1 zamień także zmienne, które są prawdziwe lub fałszywe na już
wygenerowana prawa strona. Może to oznaczać, że pewne zmienne staną się nieosiągalne
(np. X0 w X0 i X1, gdy X1 staje się fałszywe, zakładając, że X0 nie występuje gdzie indziej.
Zostanie zachowane, które zmienne stały się nieosiągalne, ponieważ te nie mają
do zbadania. W zależności od PBES może to zmniejszyć rozmiar pliku
wygenerował BES w znacznym stopniu, ale wymaga większego zużycia pamięci. „3” w
oprócz 2 sprawdź, czy wygenerowane zmienne występują w pętli,
w taki sposób, że można je ustawić na wartość prawda lub fałsz, w zależności od symbolu punktu stałego.
Może to znacznie wydłużyć czas potrzebny do wygenerowania równania.

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

-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

Korzystaj z pbes2bes online, korzystając z usług onworks.net