Jest to polecenie lpsinvelm, 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Ę
lpsinvelm - sprawdź niezmienniki i użyj ich do uproszczenia lub wyeliminowania sum LPS
STRESZCZENIE
lpsinvelm [OPCJA]... --invfile=INVPLIK [W PLIKU [PLIK WYJŚCIOWY]]
OPIS
Sprawdza, czy formuła logiczna (wyrażenie danych mCRL2 sortowania Bool) podana jako
niezmiennik jest niezmiennikiem specyfikacji procesu liniowego (LPS) w INFILE. Jeśli to jest
przypadku, narzędzie eliminuje wszystkie sumy LPS, których stan narusza
niezmienny i zapisuje wynik do pliku OUTFILE. Jeśli INFILE jest obecny, używane jest standardowe wejście. Gdyby
Brak OUTFILE, używane jest standardowe wyjście.
Narzędzie można również wykorzystać do uproszczenia warunków sum danego LPS.
OPCJE
OPCJA może być jednym z następujących:
-y, --wszystkie-naruszenia
nie przerywaj, gdy tylko zostanie stwierdzone pojedyncze naruszenie niezmiennika, ale
zamiast tego zgłoś wszystkie naruszenia
-c, --kontr-przykład
wyświetlić wycenę wskazującą, dlaczego niezmiennik mógłby zostać naruszony, jeśli
nie ma pewności, czy summand narusza niezmiennik
-o, --wprowadzenie
zastosować indukcję na listach
-iINVPLIK, --niezmienny=INVPLIK
użyj formuły logicznej (wyrażenie danych mCRL2 sortowania Bool) w INVFILE jako
niezmienny
-n, --bez sprawdzania
nie sprawdzaj, czy niezmiennik się trzyma przed wyeliminowaniem nieosiągalnych sum
-e, --brak eliminacji
nie eliminuj ani nie upraszczaj sum, ale dodaj niezmiennik do każdego warunku
-pPREFIKSÓW, --drukuj-kropkę=PREFIKSÓW
zapisać plik .dot powstałego BDD, jeśli nie można określić, czy a
summand narusza niezmiennik; PREFIX będzie używany jako przedrostek plików wyjściowych
-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
-l, --uprość-wszystko
uprościć warunki wszystkich sum, zamiast po prostu eliminować summand
których warunki w połączeniu z niezmiennikiem są sprzecznościami
-zROZWIĄZYWANIE, --smt-solver=ROZWIĄZYWANIE
użyj SOLVER, aby usunąć niespójne ścieżki z wewnętrznie używanych dysków BDD (domyślnie
nie stosuje się eliminacji ścieżki): „cvc” solwer SMT CVC3
-tLIMIT, --limit czasu=LIMIT
spędź najwyżej LIMIT sekund na udowodnieniu jednej formuły
--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
Korzystaj z lpsinvelm online za pomocą usług onworks.net
