Bu, Ubuntu Online, Fedora Online, Windows çevrimiçi emülatörü veya MAC OS çevrimiçi emülatörü gibi birden fazla ücretsiz çevrimiçi iş istasyonumuzdan birini kullanarak OnWorks ücretsiz barındırma sağlayıcısında çalıştırılabilen lpsinvelm komutudur.
Program:
ADI
lpsinvelm - değişmezleri kontrol edin ve bunları bir LPS'nin toplamlarını basitleştirmek veya ortadan kaldırmak için kullanın
SİNOPSİS
lpsinvelm [SEÇENEK]... --invfile=INVDOSYASI [DOSYADA [ÇIKIŞ DOSYASI]]
TANIM
Boole formülünün (Bool sıralamalı bir mCRL2 veri ifadesi) olarak sağlanıp sağlanmadığını kontrol eder.
değişmez, INFILE'deki doğrusal işlem belirtiminin (LPS) değişmezidir. eğer bu
durumda, araç, koşulu ihlal eden LPS'nin tüm toplamlarını ortadan kaldırır.
değişmez ve sonucu OUTFILE'a yazar. INFILE varsa, stdin kullanılır. Eğer
OUTFILE mevcut değil, stdout kullanılıyor.
Araç, verilen LPS'nin toplamlarının koşullarını basitleştirmek için de kullanılabilir.
SEÇENEKLER
SEÇENEK aşağıdakilerden herhangi biri olabilir:
-y, --tüm-ihlaller
değişmezin tek bir ihlali bulunur bulunmaz sonlandırmayın, ancak
bunun yerine tüm ihlalleri rapor et
-c, --karşı-örnek
değişmezse neden ihlal edilebileceğini gösteren bir değerleme göster
bir toplamın değişmezi ihlal edip etmediğinden emin değil
-o, --indüksiyon
listelerde tümevarım uygula
-iINVDOSYA, --değişmez=INVDOSYA
INVFILE'de boole formülünü (Bool sıralamanın bir mCRL2 veri ifadesi) şu şekilde kullanın:
değişmez
-n, --kontrol yok
ulaşılamayan toplamları ortadan kaldırmadan önce değişmezin geçerli olup olmadığını kontrol etmeyin
-e, --yo-eliminasyon
toplamları ortadan kaldırmayın veya basitleştirmeyin, ancak değişmezi her koşula ekleyin
-pÖNEK, --baskı-nokta=ÖNEK
olup olmadığını belirlemek mümkün değilse, elde edilen BDD'nin bir .dot dosyasını kaydedin.
summand değişmezi ihlal ediyor; ÖN EK, çıktı dosyalarının öneki olarak kullanılacaktır.
-QNUM, --qlimit=NUM
niceleyicilerin numaralandırmasını NUM değişkenle sınırlayın. (Varsayılan NUM=1000, NUM=0 için
sınırsız).
-rADI, --yeniden yazan=ADI
yeniden yazma stratejisini kullan NAME: 'jitty' jitty yeniden yazma (varsayılan) 'jittyc' derlendi
jitty yeniden yazma 'jittyp' atasözü ile jitty yeniden yazma
-l, --basitleştir-hepsini
sadece toplamları ortadan kaldırmak yerine, tüm toplamların koşullarını basitleştirin
değişmez ile birlikte koşulları çelişkiler olan
-zÇÖZÜCÜ, --smt-çözücü=ÇÖZÜCÜ
dahili olarak kullanılan BDD'lerden tutarsız yolları kaldırmak için SOLVER'ı kullanın (varsayılan olarak,
yol eleme uygulanmaz): 'cvc' SMT çözücü CVC3
-tLİMİT, --zaman sınırı=LİMİT
tek bir formülü kanıtlamak için en fazla LIMIT saniye harcayın
--zamanlamalar[=DOSYA]
DOSYA'ya zamanlama ölçümlerini ekleyin. Ölçümler, aşağıdaki durumlarda standart hataya yazılır:
DOSYA sağlanmadı
Standart seçenekler:
-q, --sessizlik
uyarı mesajlarını gösterme
-v, --ayrıntılı
kısa ara mesajları göster
-d, - hata ayıklama
ayrıntılı ara mesajları göster
--log-seviyesi=SEVİYE
seviyeye kadar ara mesajları göster
-h, --yardım et
yardım bilgilerini göster
--versiyon
sürüm bilgilerini göster
onworks.net hizmetlerini kullanarak lpsinvelm'i çevrimiçi kullanın
