lps2lts - Bulutta Çevrimiçi

Program:

ADI

lps2lts - bir LPS'den bir LTS oluşturun

SİNOPSİS

lps2lt [SEÇENEK] ... [DOSYADA [ÇIKIŞ DOSYASI]]

TANIM

INFILE'da LPS'den bir LTS oluşturun ve sonucu OUTFILE'a kaydedin. INFILE değilse
sağlanır, stdin kullanılır. OUTFILE sağlanmazsa, LTS saklanmaz.

'jittyc' yeniden yazıcısı kullanılıyorsa, MCRL2_COMPILEREWRITER ortam değişkeni
(varsayılan değer: 'mcrl2compilerewriter') yeniden yazıcıyı derleyen komut dosyasını belirler,
ve MCRL2_COMPILEDIR (varsayılan değer: '.') geçici dosyaların nerede saklanacağını belirler.

lps2lts'nin herhangi bir çift arasında aynı etiketle birden fazla geçiş sağlayabileceğini unutmayın.
devletler. Bu istenmiyorsa, güçlü bir uygulama uygulanarak bu tür geçişler kaldırılabilir.
örneğin ltsconvert aracını kullanarak bisimülasyon azaltma.

OUTFILE formatı, uzantısı tarafından belirlenir (bir
seçenek). Desteklenen biçimler şunlardır:

Aldebaran formatı (CADP) için 'aut',
GraphViz formatı için 'nokta' (artık giriş formatı olarak desteklenmemektedir),
Sonlu Durum Makinesi biçimi için 'fsm' veya
mCRL2 LTS formatı için 'lts' jittyc yeniden yazıcısı kullanılıyorsa,
MCRL2_COMPILEREWRITER ortam değişkeni (varsayılan değer: mcrl2compilerewriter)
yeniden yazıcıyı derleyen komut dosyasını ve MCRL2_COMPILEDIR (varsayılan değer:
'.') geçici dosyaların nerede saklanacağını belirler. lps2lts'nin birden çok
herhangi bir durum çifti arasında aynı etikete sahip geçişler. Bu istenmiyorsa, bu tür
geçişler, örneğin kullanılarak güçlü bir bisimülasyon indirgemesi uygulanarak kaldırılabilir
aracı ltsconvert.

SEÇENEKLER

SEÇENEK aşağıdakilerden herhangi biri olabilir:

-aİSİMLER, --eylem=İSİMLER
eylem adlarına sahip geçiş sistemindeki eylemleri tespit edin ve raporlayın.
NAMES, virgülle ayrılmış bir liste. Bu örneğin bulmak (veya kanıtlamak için yararlıdır)
yokluğu) bir eylem hatası. Bunlardan birinin her oluşumu için bir mesaj yazdırılır.
bu eylem adları. -t bayrağı ile bu eylemlere yönelik izler oluşturulur

-b[NUM], --bit-karma[=NUM]
durumları depolamak ve çoğu NUM durumda depolamak için bit karma kullanın. Bunun anlamı şudur ki
ziyaret edilen tüm durumların tam kaydını tutmak yerine, bir bit dizisi
Bir durumun hash değerinin daha önce görülüp görülmediğini belirtmek için kullanılır.
Bu, bu seçeneğin durumların başkalarıyla karıştırılmasına neden olabileceği anlamına gelse de
(aynı hash ile eşleştirildikleri için), çok büyük
Aksi takdirde keşfedilemeyen LTS'ler. NUM için varsayılan değer yaklaşık olarak
2*10^8 (bu yaklaşık 25MB belleğe karşılık gelir)

--önbelleğe alınmış
durum alanı oluşumunu hızlandırmak için numaralandırma önbelleğe alma tekniklerini kullanın.

-c[ADI], --birleşme[=ADI]
NAME eylem etiketine sahip geçişlerin önceliklendirilmesini uygulayın.(Hiçbir NAME olmadığında
sağlanan (yani, '-c') öncelik 'ctau' eylemine verilir. Öncelik vermek
tau için -ctau bayrağını kullanın. Doğrusal süreç tau-birleşik değilse,
üretilen durum uzayı zorunlu olarak durum uzayına benzer şekilde dallanır.
lps. Kullanılan üretim algoritması doğrusal işlem gerektirmez
tau yakınsak olmak.

-D, -- kilitlenme
kilitlenmeleri algılama (yani her kilitlenme için bir mesaj yazdırılır)

-F, --uyuşmazlık
sapmaları tespit et (yani bir sapma (=tau döngüsü) olan her durum için bir mesaj
basılı). Sapmaları saptamak için algoritma her durum için doğrusaldır, bu nedenle
durum uzayı araştırması, bu seçenek açıkken ikinci dereceden hale gelir ve bir duruma neden olur
Bu seçenek etkinleştirildiğinde uzay keşfi yavaşlar.

-yBOOL, --kukla=BOOL
LPS'deki boş değişkenleri BOOL değerine dayalı kukla değerlerle değiştirin:
'evet' (varsayılan) veya 'hayır'

--hata-izi
keşif sırasında bir hata oluşursa, olamayacak duruma bir iz kaydedin.
araştırdı

--init-tsize=NUM
dahili olarak kullanılan karma tabloların başlangıç ​​boyutunu ayarlayın (varsayılan 10000'dir)

-lNUM, --maks=NUM
en fazla NUM eyaleti keşfedin

-mİSİMLER, --çoklu eylem=İSİMLER
bir virgül olan NAMES'ten geçiş sistemindeki çoklu eylemleri tespit edin ve raporlayın.
ayrılmış liste Çoklu eylemlerin tam olarak eşleşmesi dışında -a gibi çalışır,
veri parametreleri dahil.

--bilgi yok
OUTFILE'a durum bilgisi ekleme Bu seçenek olmadan lps2lts durum ekler
LTS'ye vektör. Bu seçenek, bu bilgilerin atılmasına neden olur ve
yalnızca bir sıra numarası ile belirtilir. Açık durum bilgisi aşağıdakiler için yararlıdır:
örneğin görselleştirme amaçlıdır, ancak OUTFILE'ın büyümesine neden olabilir
önemli ölçüde. AUT biçiminde yazarken bu seçeneğin örtük olduğunu unutmayın.

-oFORMAT, --dışarı=FORMAT
çıktıyı belirtilen FORMAT'ta kaydedin

--kuru erik
durum alanı oluşumunu hızlandırmak için toplama budama kullanın.

-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

-sADI, --strateji=ADI
NAME stratejisini kullanarak durum uzayını keşfedin: 'b', 'genişlik' genişlik öncelikli arama
(varsayılan) 'd', 'derinlik' öncelikli arama 'p', 'öncelikli' tek önceliklendirme
ilk argümanındaki eylemler, yalnızca
bu parametre için en düşük değer seçilir. Örneğin eylemler varsa a(3) ve
b(4) a(3) kalır ve b(4) atlanır. İlk sıralama parametresi olmayan eylemler
Birden fazla eyleme sahip nat ve çoklu eylemler her zaman seçilir (seçenek
deneysel) 'q', 'önceliklendirilmiş', ilk argümanı olan eylemlere öncelik verir
Nat'ı sıralayın (--öncelikli seçeneğe bakın) ve bunlardan birini rastgele seçerek bir
öncelikli rastgele simülasyon (seçenek deneyseldir) 'r', 'rastgele' rastgele
simülasyon. Sonraki tüm durumlardan biri, aşağıdakilerden bağımsız olarak rastgele seçilir:
bu durum zaten gözlemlendi. Sonuç olarak, yalnızca rastgele simülasyon
bir kilitlenme durumuyla karşılaşıldığında sona erer.

--bastırmak
ayrıntılı modda, ziyaret edilenlerin sayısını belirten ilerleme mesajlarını yazdırmayın.
durumlar ve geçişler. Büyük durum uzayları için ilerleme mesajlarının sayısı
oldukça korkunç olmak. Bu özellik, bunları bastırmaya yardımcı olur. Diğer ayrıntılı mesajlar,
Keşfedilen toplam durum sayısı gibi, sadece görünür kalır.

--zamanlamalar[=DOSYA]
DOSYA'ya zamanlama ölçümlerini ekleyin. Ölçümler, aşağıdaki durumlarda standart hataya yazılır:
DOSYA sağlanmadı

--todo-max=NUM
en fazla NUM durumu yapılacaklar listesinde tut; bu seçenek yalnızca genişlik için geçerlidir.
NUM, seviye başına maksimum durum sayısı ve derinlik için ilk arama
NUM'un maksimum derinlik olduğu ilk arama

-t[NUM], --iz[=NUM]
NAMES'ten bir eylemle ulaşılan her duruma en kısa bir iz yazın.
--action seçeneği, --deadlock ile tespit edilen bir kilitlenme mi yoksa bir sapma mı
bir dosyaya --divergence ile tespit edildi. NUM adetten fazla iz yazılmayacak. Eğer
NUM sağlanmaz, izleme sayısı sınırsızdır. Alınacak her izleme için
.trc (izleme) uzantılı benzersiz bir dosya yazıldığında, bir
başlangıç ​​durumundan kilitlenme durumuna kadar en kısa iz. izler olabilir
oldukça yazdırılır ve tracepp kullanılarak diğer biçimlere dönüştürülür.

-u, --kullanılmayan-veri
veri spesifikasyonunun kullanılmayan kısımlarını çıkarmayın

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 lps2lts'yi çevrimiçi kullanın