Ini ialah arahan ltsconvert yang boleh dijalankan dalam penyedia pengehosan percuma OnWorks menggunakan salah satu daripada berbilang stesen kerja dalam talian percuma kami seperti Ubuntu Online, Fedora Online, emulator dalam talian Windows atau emulator dalam talian MAC OS.
JADUAL:
NAMA
ltsconvert - tukar dan secara pilihan meminimumkan LTS
SINOPSIS
ltsconvert [OPTION]... [INFILE [FAIL LUAR]]
DESCRIPTION
Tukar sistem peralihan berlabel (LTS) daripada INFILE kepada OUTFILE dalam yang diminta
format selepas menggunakan kaedah pengecilan yang dipilih (lalai adalah tiada). Jika OUTFILE adalah
tidak dibekalkan, stdout digunakan. Jika INFILE tidak dibekalkan, stdin digunakan.
Format output ditentukan oleh sambungan OUTFILE, manakala format input adalah
ditentukan oleh kandungan INFILE. Pilihan --masuk dan --keluar boleh digunakan untuk memaksa input
dan format output. 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 (lalai)
PILIHAN
OPTION boleh menjadi mana-mana yang berikut:
-D, --menentukan
tentukan LTS
-eNAMA, --kesetaraan=NAMA
menjana LTS yang setara, mengekalkan kesetaraan NAME: identiti 'tiada'
kesetaraan (lalai) 'bisim' kesamaan kuat 'bisim-sig' kesamaan kuat
menggunakan penambahbaikan tandatangan 'percabangan-bisim' bercabang bisimilarity 'percabangan-
bisim-sig' bercabang bisimilarity menggunakan tandatangan penghalusan 'dpbranching-bisim'
perbezaan mengekalkan percabangan kemiripan 'dpbranching-bisim-sig' divergence
memelihara kemiripan percabangan menggunakan tandatangan penghalusan 'lemah-bisim' lemah
kemiripan 'weak-bisim-sig' kemiripan lemah menggunakan penghalusan tandatangan 'dpweak-
penyimpangan bisim' mengekalkan kemiripan yang lemah penyimpangan 'dpweak-bisim-sig'
mengekalkan kesamarataan yang lemah menggunakan simulasi kuat 'sim' penambahbaikan tandatangan
kesetaraan 'jejak' kesetaraan jejak kuat 'jejak-lemah' kesetaraan jejak lemah
'tau-star' tau pengurangan bintang
-iFORMAT, --dalam=FORMAT
gunakan FORMAT sebagai format input
-lFAIL, --lps=FAIL
gunakan FILE sebagai LPS dari mana input LTS dijana; ini mungkin diperlukan untuk
simpan nama parameter yang betul bagi keadaan apabila menyimpan dalam format fsm dan ke
menukar LTS bukan mCRL2 kepada mCRL2 LTS
--tidak-sampai
jangan lakukan semakan kebolehcapaian pada input LTS
-n, --tiada-negara
tinggalkan maklumat nyata apabila menyimpan dalam format titik
-oFORMAT, --keluar=FORMAT
gunakan FORMAT sebagai format output
--tau=ACTNAMES
pertimbangkan tindakan dengan nama dalam senarai dipisahkan koma ACTNAMES sebagai dalaman
(tau) sebagai tambahan kepada tindakan yang ditakrifkan sedemikian oleh input
--masa[=FAIL]
tambah ukuran pemasaan pada FILE. Pengukuran ditulis kepada ralat piawai jika
tiada FAIL disediakan
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 ltsconvert dalam talian menggunakan perkhidmatan onworks.net