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 komut maria'dır.
Program:
ADI
maria - Yüksek seviyeli Petri ağları için Modüler Ulaşılabilirlik Analizörü
SİNOPSİS
maria [seçenekleri] Dosyaları...
TANIM
Bu kılavuz sayfası kısaca şunları belgelemektedir: maria emretmek. Daha eksiksiz belgeler
GNU Bilgi formatında mevcuttur; aşağıya bakınız.
maria girdisinde açıklanan eşzamanlı sistem modellerini analiz eden bir programdır.
Cebirsel Sistem Ağlarına dayalı bir dil. Biçimcilik Ekkart tarafından sunuldu
Kindler ve Hagen Völzer, ICATPN'98'de, Esneklik in Cebirsel Ağlar.
Cebirsel Sistem Ağları, herhangi bir veri türü veya cebirsel tanımlama yapmayan bir çerçevedir.
operasyonlar. Maria'daki veri tipi sistemi ve işlemler üst düzey
akılda programlama ve spesifikasyon dilleri. Buna rağmen, her Maria modelinin bir
sonlu açılım
Düşük seviyeli Petri ağı araçlarıyla birlikte çalışabilirliği sağlamak için Maria, tanımlayıcıları
alfa sayısal karakter ve alt çizgi dizilerine katlanmamış ağlar. Filtre
katlama.pl tanımlayıcıların okunabilirliğini geliştirmek için kullanılabilir veya uyarlanabilir.
SEÇENEKLER
Maria, iki ile başlayan uzun seçeneklerle olağan GNU komut satırı sözdizimini takip eder.
tireler (`-'). Seçeneklerin bir özeti aşağıda yer almaktadır. Tam bir açıklama için bkz.
Bilgi dosyaları.
-a sınır, --dizi sınırı=sınır
Dizi dizin türlerinin boyutunu şu şekilde sınırlayın: sınır olası değerler. 0 sınırı
kontrolleri devre dışı bırakır.
-b model, --genişlik-ilk-arama=model
Şunun erişilebilirlik grafiğini oluşturun: model genişlik öncelikli aramayı kullanma.
-C rehber, --derlemek=rehber
içinde C kodu oluşturun rehber ifadeleri değerlendirmek ve düşük seviye için
geçiş örneği analiz algoritmasının rutinleri. Bu seçenek kullanıldığında,
değerlendirme hataları biraz farklı bir şekilde rapor edilir. Çevirmen
bir durumdaki ilk hataya neden olan değerlemeyi ve ifadeyi görüntüler; NS
derlenmiş kod, hata sayısını görüntüler. Performans nedenleriyle,
oluşturulan kod, çoklu kümelere öğe eklerken taşma hatalarını kontrol etmez.
-C, --no-derleme
Karşıtı -C. Yerleşik yorumlayıcıdaki tüm ifadeleri değerlendirin. Bu
varsayılan davranış.
-D sembol, --tanımla=sembol
Önişlemci sembolünü tanımlayın sembol.
-d model, --derinlik-ilk-arama=model
Şunun erişilebilirlik grafiğini oluşturun: model derinlik öncelikli aramayı kullanma.
-E aralık, --kenarlar=aralık
Erişilebilirlik grafiğini oluştururken, grafiğin boyutunu her
aralık oluşturulan kenarlar
-e dizi, --yürüt=dizi
Gerçekleştirmek dizi.
-g grafik dosyası, --grafik=grafik dosyası
Daha önce oluşturulmuş bir erişilebilirlik grafiğini şuradan yükleyin: grafik dosyası.rgh.
-H h[,f[,t]], --karmalar=h[,f[,t]]
Olasılık doğrulaması için parametreleri yapılandırın (-P). tahsis t evrensel
hash fonksiyonları f elemanları ve karşılık gelen hash tabloları h her biri bit. Her ikisi de h
ve f sonraki uygun değerlere yuvarlanacaktır.
-?, -H, --yardım et
Maria'ya komut satırı seçeneklerinin bir özetini yazdırın ve çıkın.
-I rehber, --içerir=rehber
eklemek rehber içerme dosyaları için aranan dizinler listesine.
-i sütunlar, --genişlik=sütunlar
Çıktının sağ kenar boşluğunu şu şekilde ayarlayın: sütunlar. Varsayılan 80'dir.
-j Süreçler, --işler=Süreçler
Güvenlik özelliklerini kontrol ederken (seçenekler -L, -M ve -P), bu kadar işçiyi kullan
çok işlemcili bir bilgisayarda analizi hızlandırmak için işlemler. Ayrıca bakınız -k ve
-Z.
-k Liman[/ev sahibi], --bağlantı=Liman[/ev sahibi]
Güvenlik modeli kontrolünü dağıtın (seçenekler -L, -M ve -P) bir TCP/IP ağında. İçin
sunucu, yalnızca Liman genellikle arasında, 16 bitlik işaretsiz bir tamsayı olarak belirtilir.
1024 ve 65535. Çalışan işlemler için, Liman/ev sahibi bağlantı noktasını belirtir ve
sunucunun adresi. Ayrıca bakınız -j.
-L model, --kayıpsız=model
Yük model ve bir dizi erişilebilir durum oluşturarak onu analiz etmeye hazırlanın
disk dosyalarında. Ayrıca bakınız -M, -P, -j ve -k.
-m model, --model=model
Yük model ve erişilebilirlik grafiğini temizleyin.
-M model, --md5-sıkıştırılmış=model
Yük model ve aşırı bir yaklaşım oluşturarak onu analiz etmeye hazırlanın.
ana bellekteki erişilebilir durumlar kümesi. Ayrıca bakınız -P, -L, -j ve -k.
-N Cregexp, --isim=Cregexp
Bağlamda izin verilen adları belirtin c genişletilmiş normal ifade olarak regexp.
Bağlam, parametre dizisinin ilk karakteriyle tanımlanır; NS
sonraki karakterler, izin verilen adların olması gereken normal ifadeyi oluşturur.
maç.
-n Cregexp, --no-isim=Cregexp
Bağlamda izin verilmeyen adları belirtin c genişletilmiş normal ifade olarak
regexp.
İkisi de olursa -N ve ve -n bir bağlam için belirtilir c, sonra izin veren eşleşme
öncelik. Örneğin, tüm kullanıcı tanımlı tür adlarının
ile sonlandırıldı _t, belirtin -Nt -Nt'_t$'. İkinci parametredeki tırnak işaretleri
özel anlamını kaldırmak için gerekli $ komut satırı kabuğunda
muhtemelen Maria'yı çağırmak için kullanıyor.
-P model, --olasılıklı=model
Yük model ve bir dizi erişilebilir durum oluşturarak onu analiz etmeye hazırlanın
adı verilen bir teknik kullanarak ana bellekte bit durumu karma.
-p komuta, --özellik-çevirmen=komuta
Özellik otomatlarını çevirmek için kullanılacak komutu belirtin. komut gerekir
standart girişten bir formül okuyun ve karşılık gelen bir otomat yazın
standart çıktının açıklaması. Tercüman lbt bununla uyumludur
seçeneği.
-q sınır, --nicelendirme-limit=sınır
Birden fazla türe sahip türlerin nicelleştirilmesini (çoklu küme toplamı) önleyin sınır mümkün
değerler. 0 sınırı, kontrolleri devre dışı bırakır.
-U sembol, --tanımsız=sembol
Önişlemci sembolünün tanımını kaldırın sembol.
-u [a][f[dış dosya]], --açılmak=[a][f[dış dosya]]
Algoritma kullanarak ağı açın a ve formatta yaz f için dış dosya. Eğer dış dosya
belirtilmemişse, katlanmamış ağı standart çıktıya boşaltın. Olası biçimler
vardır m (Maria (insan tarafından okunabilir), varsayılan), l (LoLA), p (PEP) ve r (PROD). Orası
iki algoritmadır: geleneksel (varsayılan) ve bir örtülebilir
işaretleme (M).
-V, --versiyon
Maria'nın sürüm numarasını yazdırın ve çıkın.
-içinde, --ayrıntılı
Analizin farklı aşamalarında ayrıntılı bilgileri görüntüleyin.
-W, --uyarılar
Şüpheli ağ yapıları hakkında uyarıları etkinleştirin. Bu varsayılan davranıştır.
-w, --no-uyarılar
Karşıtı -W. Tüm uyarıları devre dışı bırakın.
-x sayı tabanı, --radix=sayı tabanı
Tanılama çıktısı için sayı tabanını belirtin. için izin verilen değerler sayı tabanı vardır
Ekim, sekizli, 8, hex, onaltılık, 16, Aralık, ondalık ve 10. Varsayılan, kullanmaktır
ondalık sayılar.
-E, --sıkıştır-gizli
Ardıl durumlarını saklamayarak erişilebilir durumlar kümesini azaltın.
geçiş örnekleri için bir gizlemek koşul tutar. Gizli ardıllar
ayrı bir durum kümesine kaydedilir. Bu seçenek hafızadan tasarruf edebilir (-L or -m) veya azaltmak
durumların ihmal edilme olasılığı (-M or -P) ve iyileştirebilir
paralel analizin verimliliği (-j or -k), ancak aynı zamanda önemli ölçüde artabilir.
işlemci zaman gereksinimi. Seçenek, canlılık modeliyle de çalışır
kontrol, ancak canlılık özelliklerinin doğruluk değerlerinin garantisi yoktur.
değişmeden kalır. Bu seçenek ile birleştirilebilir -Z.
-y, --sıkıştırılamayan-gizli
Karşıtı -Y. Bu varsayılan davranıştır.
-Z, --sıkıştır-yollar
olan ara durumları saklamayarak erişilebilir durumlar kümesini azaltın.
çoğu halefi. Bu seçenek hafızadan tasarruf edebilir (-L or -m) veya azaltmak
durumların ihmal edilme olasılığı (-M or -P) ve verimliliği artırabilir
paralel analiz (-j or -k), ancak aynı zamanda önemli ölçüde artırabilir.
işlemci süresi gereksinimi. Seçenek, canlılık modeli kontrolü ile de çalışır,
ancak canlılık özelliklerinin doğruluk değerlerinin korunacağının garantisi yoktur.
değişmemiş. Bu seçenek ile birleştirilebilir -Y.
, -z --no-sıkıştırılmış-yollar
Karşıtı -Z. Bu varsayılan davranıştır.
onworks.net hizmetlerini kullanarak maria'yı çevrimiçi kullanın
