lpsinvelm - Online di Cloud

PROGRAM:

NAMA

lpsinvelm - periksa invarian dan gunakan ini untuk menyederhanakan atau menghilangkan jumlah LPS

RINGKASAN

lpsinvelm [PILIHAN]... --invfile=INVFILE [INFILE [FILE KELUAR]]

DESKRIPSI

Memeriksa apakah rumus boolean (ekspresi data mCRL2 semacam Bool) disediakan sebagai
invariant adalah invarian dari spesifikasi proses linier (LPS) di INFILE. Jika ini adalah
kasus, alat tersebut menghilangkan semua perintah LPS yang kondisinya melanggar
invarian, dan menulis hasilnya ke OUTFILE. Jika INFILE ada, stdin digunakan. Jika
OUTFILE tidak ada, stdout digunakan.

Alat tersebut juga dapat digunakan untuk menyederhanakan kondisi summand dari LPS yang diberikan.

PILIHAN

PILIHAN dapat berupa salah satu dari berikut ini:

-y, --semua-pelanggaran
tidak menghentikan segera setelah satu pelanggaran invarian ditemukan, tetapi
laporkan semua pelanggaran sebagai gantinya

-c, --kontra-contoh
menampilkan penilaian yang menunjukkan mengapa invarian mungkin dapat dilanggar jika itu
tidak pasti apakah suatu pemanggilan melanggar invarian

-o, --induksi
terapkan induksi pada daftar

-iFILE INV, --invarian=FILE INV
gunakan rumus boolean (ekspresi data mCRL2 semacam Bool) di INVFILE sebagai
invarian

-n, --tidak memeriksa
jangan periksa apakah invarian berlaku sebelum menghilangkan summand yang tidak terjangkau

-e, --tidak ada eliminasi
jangan menghilangkan atau menyederhanakan penjumlahan, tetapi tambahkan invarian ke setiap kondisi

-pAWALAN, --cetak-titik=AWALAN
simpan file .dot dari BDD yang dihasilkan jika tidak mungkin untuk menentukan apakah a
summand melanggar invarian; PREFIX akan digunakan sebagai awalan dari file output

-QNUM, --qbatas=NUM
membatasi enumerasi quantifiers ke variabel NUM. (Default NUM=1000, NUM=0 untuk
tak terbatas).

-rNAMA, --penulis ulang=NAMA
gunakan strategi penulisan ulang NAMA: 'jitty' jitty rewriting (default) 'jittyc' dikompilasi
gelisah menulis ulang 'jittyp' gelisah menulis ulang dengan pepatah

-l, --sederhanakan-semua
sederhanakan kondisi semua pemanggilan, bukan hanya menghilangkan pemanggilan
yang kondisinya dalam hubungannya dengan invarian adalah kontradiksi

-zPEMECAH, --smt-solver=PEMECAH
gunakan SOLVER untuk menghapus jalur yang tidak konsisten dari BDD yang digunakan secara internal (secara default,
tidak ada eliminasi jalur yang diterapkan): 'cvc' pemecah SMT CVC3

-tMEMBATASI, --batas waktu=MEMBATASI
habiskan paling banyak LIMIT detik untuk membuktikan satu formula

--waktu[=FILE]
menambahkan pengukuran waktu ke FILE. Pengukuran ditulis ke kesalahan standar jika
tidak ada FILE yang disediakan

Opsi standar:

-q, --diam
jangan tampilkan pesan peringatan

-v, --bertele-tele
tampilkan pesan perantara pendek

-d, --debug
tampilkan pesan perantara yang terperinci

--tingkat log=TINGKAT
tampilkan pesan perantara hingga dan termasuk level

-h, --membantu
tampilkan informasi bantuan

--Versi: kapan
menampilkan informasi versi

Gunakan lpsinvelm online menggunakan layanan onworks.net