lpsinvelm - ອອນລາຍໃນຄລາວ

ໂຄງການ:

NAME

lpsinvelm - ກວດເບິ່ງ invariants ແລະນໍາໃຊ້ສິ່ງເຫຼົ່ານີ້ເພື່ອເຮັດໃຫ້ງ່າຍຫຼືລົບລ້າງການ summands ຂອງ LPS.

ສະຫຼຸບສັງລວມ

lpsinvelm [ທາງເລືອກ]... --invfile=INVFILE [INFILE [OUTFILE]]

ລາຍລະອຽດ

ກວດເບິ່ງວ່າສູດ boolean (ການສະແດງອອກຂໍ້ມູນ mCRL2 ຂອງການຈັດລຽງ Bool) ທີ່ສະຫນອງໃຫ້
invariant ແມ່ນ invariant ຂອງສະເພາະຂະບວນການເສັ້ນຊື່ (LPS) ໃນ INFILE. ຖ້ານີ້ແມ່ນ
ກໍລະນີ, ເຄື່ອງມືກໍາຈັດການສະຫຼຸບທັງຫມົດຂອງ LPS ທີ່ມີເງື່ອນໄຂການລະເມີດ
invariant, ແລະຂຽນຜົນໄດ້ຮັບໃສ່ OUTFILE. ຖ້າມີ INFILE, stdin ຖືກໃຊ້. ຖ້າ
ບໍ່ມີ OUTFILE, stdout ຖືກໃຊ້.

ເຄື່ອງມືດັ່ງກ່າວຍັງສາມາດຖືກນໍາໃຊ້ເພື່ອງ່າຍເງື່ອນໄຂຂອງ summands ຂອງ LPS ທີ່ໃຫ້.

OPTIONS

ທາງເລືອກ ສາມາດເປັນອັນໃດອັນໜຶ່ງຕໍ່ໄປນີ້:

-y, --ການ​ລະ​ເມີດ​ທັງ​ຫມົດ​
ຢ່າຢຸດເຊົາທັນທີທີ່ພົບເຫັນການລະເມີດດຽວຂອງ invariant, ແຕ່
ລາຍງານການລະເມີດທັງໝົດແທນ

-c, --ຕົວ​ຢ່າງ
ສະແດງການປະເມີນມູນຄ່າທີ່ຊີ້ບອກວ່າເປັນຫຍັງ invariant ອາດຈະຖືກລະເມີດຖ້າມັນ
ແມ່ນບໍ່ແນ່ໃຈວ່າ summand ລະເມີດ invariant

-o, -- induction
ໃຊ້ induction ໃນລາຍການ

-iINVFILE, -- invariant=INVFILE
ໃຊ້ສູດ boolean (ການສະແດງອອກຂໍ້ມູນ mCRL2 ຂອງການຈັດລຽງ Bool) ໃນ INVFILE ເປັນ
ບໍ່ປ່ຽນແປງ

-n, --ບໍ່ກວດ
ຢ່າກວດເບິ່ງວ່າ invariant ຖືກ່ອນທີ່ຈະກໍາຈັດ summands ທີ່ບໍ່ສາມາດບັນລຸໄດ້

-e, -- ບໍ່​ມີ​ການ​ລົບ​ລ້າງ​
ບໍ່ໄດ້ລົບລ້າງຫຼືເຮັດໃຫ້ງ່າຍດາຍ summands, ແຕ່ເພີ່ມ invariant ກັບແຕ່ລະເງື່ອນໄຂ

-pPREFIX, --print-dot=PREFIX
ບັນທຶກໄຟລ໌ .dot ຂອງ BDD ຜົນໄດ້ຮັບ ຖ້າມັນເປັນໄປບໍ່ໄດ້ທີ່ຈະກໍານົດວ່າ a
summand ລະເມີດ invariant; PREFIX ຈະຖືກນໍາໃຊ້ເປັນຄໍານໍາຫນ້າຂອງໄຟລ໌ຜົນຜະລິດ

-QNUMBER, --qlimit=NUMBER
ຈໍາ​ກັດ​ການ​ນັບ​ຈໍາ​ນວນ​ຂອງ​ປະ​ລິ​ມານ​ໃຫ້ NUM ຕົວ​ປ່ຽນ​ແປງ​. (ຄ່າເລີ່ມຕົ້ນ NUM=1000, NUM=0 ສຳລັບ
ບໍ່​ຈໍາ​ກັດ).

-rNAME, --rewriter=NAME
ໃຊ້ຍຸດທະສາດການຂຽນຄືນໃຫມ່ NAME: 'jitty' jitty rewriting (ຄ່າເລີ່ມຕົ້ນ) 'jittyc' compiled
jitty rewriting 'jittyp' jitty rewriting ກັບ prover

-l, --simplify-ທັງໝົດ
ປັບປຸງເງື່ອນໄຂຂອງ summands ທັງຫມົດ, ແທນທີ່ຈະພຽງແຕ່ລົບລ້າງ summands
ເງື່ອນໄຂທີ່ສອດຄ່ອງກັບ invariant ແມ່ນກົງກັນຂ້າມ

-zSOLVER, --smt-solver=SOLVER
ໃຊ້ SOLVER ເພື່ອເອົາເສັ້ນທາງທີ່ບໍ່ສອດຄ່ອງອອກຈາກ BDDs ທີ່ໃຊ້ພາຍໃນ (ໂດຍຄ່າເລີ່ມຕົ້ນ,
ບໍ່ມີການນໍາໃຊ້ການກໍາຈັດເສັ້ນທາງ): 'cvc' ຕົວແກ້ໄຂ SMT CVC3

-tຈຳ ກັດ, -- ຈຳກັດເວລາ=ຈຳ ກັດ
ໃຊ້ເວລາຫຼາຍທີ່ສຸດ LIMIT ວິນາທີເພື່ອພິສູດສູດດຽວ

--ເວລາ[=ເອກະສານ]
ຕື່ມການວັດແທກເວລາໃສ່ FILE. ການວັດແທກຖືກຂຽນເປັນຄວາມຜິດພາດມາດຕະຖານຖ້າ
ບໍ່ມີ FILE ສະຫນອງໃຫ້

ຕົວເລືອກມາດຕະຖານ:

-q, --ງຽບ
ບໍ່ສະແດງຂໍ້ຄວາມເຕືອນ

-v, -- verbose
ສະແດງຂໍ້ຄວາມປານກາງສັ້ນ

-d, --debug
ສະ​ແດງ​ຂໍ້​ຄວາມ​ລະ​ອຽດ​ປານ​ກາງ​

--log-level=LEVEL
ສະແດງຂໍ້ຄວາມລະດັບປານກາງເຖິງແລະລວມທັງລະດັບ

-h, - ຊ່ວຍ
ສະແດງຂໍ້ມູນການຊ່ວຍເຫຼືອ

- ການປ່ຽນແປງ
ສະແດງຂໍ້ມູນສະບັບ

ໃຊ້ lpsinvelm ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net