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

ໂຄງການ:

NAME

lpsconfcheck - ຫມາຍ confluent tau-summands ຂອງ LPS

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

lpsconfcheck [ທາງເລືອກ]... [INFILE [OUTFILE]]

ລາຍລະອຽດ

ກວດເບິ່ງວ່າ tau-summands ຂອງ mCRL2 LPS ໃນ INFILE ແມ່ນ confluent, ຫມາຍໃຫ້ເຂົາເຈົ້າໂດຍການປ່ຽນຊື່.
ເຂົາເຈົ້າໃສ່ ctau, ແລະຂຽນຜົນໄດ້ຮັບໃສ່ OUTFILE. ຖ້າ INFILE ບໍ່ແມ່ນປະຈຸບັນ stdin ຖືກນໍາໃຊ້. ຖ້າ
ບໍ່ມີ OUTFILE, stdout ຖືກໃຊ້.

OPTIONS

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

-a, --ກວດເບິ່ງທັງໝົດ
ກວດເບິ່ງຄວາມສົມດຸນຂອງ tau-summands ກ່ຽວກັບ summands ອື່ນໆທັງຫມົດ, ແທນທີ່ຈະ
ສືບຕໍ່ກັບ tau-summand ຕໍ່ໄປທັນທີທີ່ summand ຖືກພົບ
ບໍ່ confluent ກັບ tau-summand ໃນປັດຈຸບັນ

-c, --ຕົວ​ຢ່າງ
ສະແດງການປະເມີນມູນຄ່າທີ່ເງື່ອນໄຂ confluence ບໍ່ຖື, ໃນກໍລະນີທີ່
ເງື່ອນໄຂທີ່ພົບບໍ່ແມ່ນຄວາມຂັດແຍ້ງຫຼືຄວາມເຄັ່ງຕຶງ

-g, --generate-invariants
ພະຍາຍາມພິສູດວ່າເງື່ອນໄຂ confluence ຫຼຸດລົງແມ່ນ invariant ຂອງ LPS, ໃນ
ກໍ​ລະ​ນີ​ທີ່​ສະ​ພາບ​ການ confluence ບໍ່​ແມ່ນ tautology​

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

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

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

-m, --ບໍ່ມີເຄື່ອງໝາຍ
ຫ້າມໝາຍເຖິງ tau-summands confluent; ເນື່ອງຈາກບໍ່ມີການປ່ຽນແປງໃດໆຕໍ່ LPS,
ບໍ່ມີຫຍັງຖືກຂຽນໃສ່ OUTFILE

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

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

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

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

-sNUMBER, --summand=NUMBER
ລົບລ້າງຫຼືເຮັດໃຫ້ຄວາມງ່າຍດາຍຂອງ summand ດ້ວຍຕົວເລກ NUM ເທົ່ານັ້ນ

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

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

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

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

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

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

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

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

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

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