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 lpsconfcheck komutudur.
Program:
ADI
lpsconfcheck - bir LPS'nin birleşik tau toplamlarını işaretleyin
SİNOPSİS
lpsconfcheck [SEÇENEK] ... [DOSYADA [ÇIKIŞ DOSYASI]]
AÇIKLAMA
INFILE'daki mCRL2 LPS'nin hangi tau-toplamlarının birleşik olduğunu kontrol eder, bunları yeniden adlandırarak işaretler
bunları ctau'ya yazın ve sonucu OUTFILE'a yazın. INFILE yoksa stdin kullanılır. Eğer
OUTFILE mevcut değil, stdout kullanılıyor.
SEÇENEKLER
SEÇENEK aşağıdakilerden herhangi biri olabilir:
-a, --hepsini kontrol et
yerine diğer tüm toplantılara ilişkin tau toplamlarının birleşimini kontrol edin
bir toplamla karşılaşıldığı anda bir sonraki tau-toplamıyla devam etmek
mevcut tau toplamı ile uyumlu değil
-c, --karşı-örnek
durumunda, birleşme koşulunun geçerli olmadığı bir değerleme görüntüler.
Karşılaşılan durum ne bir çelişki ne de bir totolojidir
-g, --değişmezler oluştur
azaltılmış kesişme koşulunun LPS'nin değişmezi olduğunu kanıtlamaya çalışın,
kesişme koşulunun bir totoloji olmaması durumunda
-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
kesişmeyi kontrol etmeden önce değişmezin geçerli olup olmadığını kontrol etmeyin
-m, --işaretleme yok
birleşik tau toplamlarını işaretlemeyin; LPS'de herhangi bir değişiklik yapılmadığından,
OUTFILE'a hiçbir şey yazılmıyor
-pÖNEK, --baskı-nokta=ÖNEK
İki toplamın kanıtlanamaması durumunda ortaya çıkan BDD'nin bir .dot dosyasını kaydedin
birleşik; ÖNEK, çı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
-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
-sNUM, --toplam=NUM
yalnızca NUM numaralı toplamı ortadan kaldırın veya basitleştirin
-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 lpsconfcheck'i çevrimiçi kullanın
