lps2lts - Dalam Talian di Awan

JADUAL:

NAMA

lps2lts - menjana LTS daripada LPS

SINOPSIS

lps2lts [OPTION]... [INFILE [FAIL LUAR]]

DESCRIPTION

Hasilkan LTS daripada LPS dalam INFILE dan simpan hasilnya ke OUTFILE. Jika INFILE tidak
dibekalkan, stdin digunakan. Jika OUTFILE tidak dibekalkan, LTS tidak disimpan.

Jika penulis semula 'jittyc' digunakan, maka pembolehubah persekitaran MCRL2_COMPILEREWRITER
(nilai lalai: 'mcrl2compilerewriter') menentukan skrip yang menyusun penulis semula,
dan MCRL2_COMPILEDIR (nilai lalai: '.') menentukan tempat fail sementara disimpan.

Ambil perhatian bahawa lps2lts boleh menyampaikan berbilang peralihan dengan label yang sama antara mana-mana pasangan
negeri. Jika ini tidak diingini, peralihan tersebut boleh dialih keluar dengan menggunakan yang kuat
pengurangan bisimulasi menggunakan contohnya alat ltsconvert.

Format OUTFILE ditentukan oleh sambungannya (melainkan ia ditentukan oleh
pilihan). Format yang disokong ialah:

'aut' untuk format Aldebaran (CADP),
'titik' untuk format GraphViz (tidak lagi disokong sebagai format input),
'fsm' untuk format Mesin Keadaan Terhad, atau
'lts' untuk format mCRL2 LTS Jika penulis semula jittyc digunakan, maka
MCRL2_COMPILEREWRITER pembolehubah persekitaran (nilai lalai: mcrl2compilerewriter)
menentukan skrip yang menyusun penulis semula, dan MCRL2_COMPILEDIR (nilai lalai:
'.') menentukan di mana fail sementara disimpan. Ambil perhatian bahawa lps2lts boleh menghantar berbilang
peralihan dengan label yang sama antara mana-mana pasangan keadaan. Jika ini tidak diingini, seperti
peralihan boleh dialih keluar dengan menggunakan redukton bisimulasi yang kuat menggunakan contohnya
alat itu menukar.

PILIHAN

OPTION boleh menjadi mana-mana yang berikut:

-aNAMA, --tindakan=NAMA
mengesan dan melaporkan tindakan dalam sistem peralihan yang mempunyai nama tindakan daripada
NAMES, senarai yang dipisahkan koma. Ini contohnya berguna untuk mencari (atau membuktikan
ketiadaan) ralat tindakan. Mesej dicetak untuk setiap kejadian salah satu daripada
nama tindakan ini. Dengan bendera -t jejak ke arah tindakan ini dijana

-b[NUM], --bit-hash[=NUM]
gunakan pencincangan bit untuk menyimpan keadaan dan menyimpan paling banyak NUM keadaan. Ini bermakna bahawa
daripada menyimpan rekod penuh semua negeri yang telah dilawati, sedikit tatasusunan
digunakan yang menunjukkan sama ada cincang keadaan telah dilihat atau tidak sebelum ini.
Walaupun ini bermakna bahawa pilihan ini boleh menyebabkan negeri disalah anggap sebagai negeri lain
(kerana ia dipetakan kepada cincang yang sama), ia boleh berguna untuk meneroka yang sangat besar
LTS yang sebaliknya tidak boleh diterokai. Nilai lalai untuk NUM ialah lebih kurang
2*10^8 (ini sepadan dengan kira-kira 25MB memori)

- dicache
gunakan teknik caching enumerasi untuk mempercepatkan penjanaan ruang negeri.

-c[NAMA], --pertemuan[=NAMA]
gunakan keutamaan peralihan dengan label tindakan NAME.(apabila tiada NAME
keutamaan yang dibekalkan (iaitu, '-c') diberikan kepada tindakan 'ctau'. Untuk memberi keutamaan kepada
ke tau guna bendera -ctau. Ambil perhatian bahawa jika proses linear tidak tau-confluent,
ruang keadaan yang dijana semestinya bercabang serupa dengan ruang keadaan
lps itu. Algoritma penjanaan yang digunakan tidak memerlukan proses linear
menjadi konvergen tau.

-D, --kebuntuan
mengesan kebuntuan (iaitu untuk setiap kebuntuan mesej dicetak)

-F, --perbezaan
mengesan perbezaan (iaitu untuk setiap keadaan dengan perbezaan (=tau gelung) mesej adalah
dicetak). Algoritma untuk mengesan perbezaan adalah linear untuk setiap keadaan, jadi
keadaan penerokaan angkasa lepas menjadi kuadratik dengan pilihan ini dihidupkan, menyebabkan keadaan
penerokaan angkasa lepas menjadi perlahan apabila pilihan ini didayakan.

-yBOOL, --bodoh=BOOL
gantikan pembolehubah bebas dalam LPS dengan nilai dummy berdasarkan nilai BOOL:
'ya' (lalai) atau 'tidak'

--ralat-jejak
jika ralat berlaku semasa penerokaan, simpan jejak ke keadaan yang tidak boleh berlaku
diterokai

--init-tsize=NUM
tetapkan saiz awal jadual cincang yang digunakan secara dalaman (lalai ialah 10000)

-lNUM, --maks=NUM
teroka di kebanyakan NUM negeri

-mNAMA, --pelbagaian=NAMA
mengesan dan melaporkan pelbagai tindakan dalam sistem peralihan daripada NAMES, koma-
senarai berasingan. Berfungsi seperti -a, kecuali berbilang tindakan dipadankan dengan tepat,
termasuk parameter data.

--tiada-maklumat
jangan tambah maklumat keadaan pada OUTFILETanpa pilihan ini lps2lts menambah keadaan
vektor kepada LTS. Pilihan ini menyebabkan maklumat ini dibuang dan dinyatakan
hanya ditunjukkan oleh nombor urutan. Maklumat keadaan eksplisit berguna untuk
tujuan visualisasi, misalnya, tetapi boleh menyebabkan OUTFILE berkembang
dengan ketara. Ambil perhatian bahawa pilihan ini tersirat apabila menulis dalam format AUT.

-oFORMAT, --keluar=FORMAT
simpan output dalam FORMAT yang ditentukan

--pangkas
gunakan pemangkasan summand untuk mempercepatkan penjanaan ruang negeri.

-QNUM, --qlimit=NUM
hadkan penghitungan pengkuantiti kepada NUM pembolehubah. (Lalai NUM=1000, NUM=0 untuk
tidak terhad).

-rNAMA, --penulis semula=NAMA
gunakan strategi tulis semula NAMA: 'jitty' jitty menulis semula (lalai) 'jittyc' disusun
jitty menulis semula 'jittyp' jitty menulis semula dengan prover

-sNAMA, --strategi=NAMA
terokai ruang keadaan menggunakan strategi NAME: 'b', 'keluasan' carian pertama keluasan
(lalai) 'd', 'depth' depth-first search 'p', 'prioritized' prioritize single
tindakan pada hujah pertamanya adalah jenis Nat di mana hanya tindakan tersebut dengan
nilai terendah untuk parameter ini dipilih. Cth jika ada tindakan a(3) dan
b(4), a(3) kekal dan b(4) dilangkau. Tindakan tanpa jenis parameter pertama
Nat dan multactions dengan lebih daripada satu tindakan sentiasa dipilih (pilihan ialah
eksperimen) 'q', 'diutamakan' mengutamakan tindakan pada hujah pertamanya ialah
susun Nat (lihat pilihan --prioritized), dan pilih secara rawak salah satu daripada ini untuk mendapatkan a
simulasi rawak diutamakan (pilihan adalah eksperimen) 'r', rawak 'rawak'
simulasi. Daripada semua negeri seterusnya, satu dipilih secara rawak secara bebas daripada sama ada
negeri ini telah pun diperhatikan. Akibatnya, simulasi rawak sahaja
tamat apabila keadaan buntu ditemui.

--menekan
dalam mod verbose, jangan cetak mesej kemajuan yang menunjukkan bilangan yang dilawati
negeri dan peralihan. Untuk ruang keadaan yang besar bilangan mesej kemajuan boleh
menjadi agak mengerikan. Ciri ini membantu menyekatnya. Mesej verbose lain,
seperti jumlah bilangan negeri yang diterokai, hanya kekal kelihatan.

--masa[=FAIL]
tambah ukuran pemasaan pada FILE. Pengukuran ditulis kepada ralat piawai jika
tiada FAIL disediakan

--todo-maks=NUM
simpan paling banyak NUM keadaan dalam senarai tugasan; pilihan ini hanya relevan untuk keluasan-
carian pertama, dengan NUM ialah bilangan maksimum keadaan bagi setiap tahap dan untuk kedalaman
carian pertama, dengan NUM ialah kedalaman maksimum

-t[NUM], --jejak[=NUM]
Tulis jejak terpendek untuk setiap keadaan yang dicapai dengan tindakan daripada NAMES daripada
option --action, ialah jalan buntu yang dikesan dengan --deadlock, atau merupakan perbezaan
dikesan dengan --divergence ke fail. Tidak lebih daripada NUM jejak akan ditulis. Jika
NUM tidak dibekalkan bilangan jejak tidak terhad. Untuk setiap jejak yang akan
menulis fail unik dengan sambungan .trc (jejak) akan dibuat mengandungi a
jejak terpendek dari keadaan awal ke keadaan kebuntuan. Jejak boleh
cantik dicetak dan ditukar kepada format lain menggunakan tracepp.

-u, --data-tidak digunakan
jangan keluarkan bahagian spesifikasi data yang tidak digunakan

Pilihan standard:

-q, --senyap
jangan paparkan mesej amaran

-v, --verbose
memaparkan mesej perantaraan pendek

-d, --nyahpepijat
memaparkan mesej perantaraan terperinci

--peringkat-log=LEVEL
memaparkan mesej perantaraan sehingga dan termasuk tahap

-h, - membantu
memaparkan maklumat bantuan

--versi
memaparkan maklumat versi

Gunakan lps2lts dalam talian menggunakan perkhidmatan onworks.net