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

ໂຄງການ:

NAME

pbes2bool - ສ້າງ BES ຈາກ PBES ແລະແກ້ໄຂມັນ.

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

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

ລາຍລະອຽດ

ແກ້ໄຂ (P)BES ຈາກ INFILE. ຖ້າ INFILE ບໍ່ຢູ່, stdin ຖືກນໍາໃຊ້.

OPTIONS

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

-c, -- ເຄົາເຕີ້
ພິມໃນຕອນທ້າຍຂອງຕົ້ນໄມ້ທີ່ຕິດສະຫຼາກທີ່ມີ instantiations ຂອງເບື້ອງຊ້າຍມືຂອງ
ສົມຜົນ; ຕົ້ນໄມ້ນີ້ແມ່ນຕົວຊີ້ບອກວິທີການ pbes2bool ມາຮອດຄວາມຖືກຕ້ອງຫຼື
ຄວາມບໍ່ຖືກຕ້ອງຂອງ PBES

-eLEVEL, --ລົບ=LEVEL
ໃຊ້ລົບລະດັບ LEVEL ເພື່ອເອົາຕົວແປ bes 'none' ບໍ່ໄດ້ເອົາ bes ທີ່ສ້າງຂຶ້ນ
ຕົວແປ. ນີ້ສາມາດນໍາໄປສູ່ການນໍາໃຊ້ຄວາມຊົງຈໍາຫຼາຍເກີນໄປ. (ຄ່າເລີ່ມຕົ້ນ) 'ບາງ' ເອົາອອກ
ສ້າງຕົວແປທີ່ບໍ່ໄດ້ໃຊ້, ເວັ້ນເສຍແຕ່ວ່າເບື້ອງຂວາຂອງມັນ
ສົມຜົນແມ່ນຖືກຕ້ອງ ຫຼືຜິດ. rhss ຂອງຕົວແປຈະຕ້ອງຖືກຄິດໄລ່ຄືນໃຫມ່, ຖ້າ
ໄດ້ພົບອີກເທື່ອຫນຶ່ງ, ຊຶ່ງເປັນເລື່ອງປົກກະຕິ. 'ທັງໝົດ' ເອົາທຸກຕົວແປທີ່ເປັນ
ບໍ່ໄດ້ໃຊ້ແລ້ວໃນສົມຜົນໃດໆ. ນີ້ແມ່ນຄວາມຊົງຈໍາທີ່ຂ້ອນຂ້າງປະສິດທິພາບ, ແຕ່ວ່າມັນສາມາດເປັນ
ໃຊ້ເວລາຫຼາຍຍ້ອນວ່າ rhss ຂອງຕົວແປອອກ bes ອາດຈະຕ້ອງມີ
ຂ້ອນຂ້າງມັກຈະຄິດໄລ່ຄືນໃຫມ່.

-H, --hashtables
ໃຊ້ hashtables ເມື່ອປ່ຽນແທນສົມຜົນ bes, ແລະແປພາຍໃນ
ການສະແດງອອກໃນແຜນວາດການຕັດສິນໃຈຄູ່ (ທໍ້ຖອຍໃຈ, ເນື່ອງຈາກການປະຕິບັດ)

-iຮູບແບບ, --ໃນ=ຮູບແບບ
ໃຊ້ຮູບແບບການປ້ອນຂໍ້ມູນ FORMAT: 'pbes' PBES ໃນຮູບແບບພາຍໃນ 'pbes_text' PBES ໃນ
ຮູບແບບຂໍ້ຄວາມພາຍໃນ 'ຂໍ້ຄວາມ' PBES ໃນຮູບແບບຂໍ້ຄວາມ (mCRL2) 'bes' BES ພາຍໃນ
ຮູບແບບ 'bes_text' BES ໃນຮູບແບບຂໍ້ຄວາມພາຍໃນ 'cwi' BES ໃນຮູບແບບ CWI 'pgsolver'
BES ໃນຮູບແບບ PGSolver

-oຮູບແບບ, -- ຜົນຜະລິດ=ຮູບແບບ
ໃຊ້ຮູບແບບຜົນຜະລິດ FORMAT (ຕົວເລືອກນີ້ຖືກຍົກເລີກ. ໃຊ້ເຄື່ອງມື pbes2bes
ແທນ).

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

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

-zຄົ້ນຫາ, --ຄົ້ນຫາ=ຄົ້ນຫາ
ໃຊ້ຍຸດທະສາດການຄົ້ນຫາ SEARCH: 'breadth-first' ຄິດໄລ່ດ້ານຂວາມືຂອງ
ຕົວແປ boolean ຢູ່ໃນພື້ນຖານທໍາອິດມາທໍາອິດ. ນີ້ແມ່ນປຽບທຽບກັບ a
ການ​ຊອກ​ຫາ​ຄວາມ​ກວ້າງ​ຂວາງ​ຄັ້ງ​ທໍາ​ອິດ​. ນີ້ແມ່ນດີສໍາລັບການສ້າງຕົວຢ່າງຕ້ານ. (ຄ່າເລີ່ມຕົ້ນ)
'depth-first' ຄິດໄລ່ດ້ານຂວາມືຂອງຕົວແປ boolean ບ່ອນທີ່ສຸດທ້າຍ
ຕົວແປທີ່ສ້າງຂຶ້ນແມ່ນໄດ້ຖືກສືບສວນກ່ອນ. ນີ້ເທົ່າກັບຄວາມເລິກກ່ອນ
ຄົ້ນຫາ. ນີ້​ສາ​ມາດ​ປະ​ຕິ​ບັດ​ຢ່າງ​ຫຼວງ​ຫຼາຍ​ການ​ຄົ້ນ​ຫາ​ຄວາມ​ກວ້າງ​ຂວາງ​ທໍາ​ອິດ​ໃນ​ເວ​ລາ​ທີ່​ຄວາມ​ຖືກ​ຕ້ອງ​ຂອງ
ສູດຖືກກໍານົດຫຼັງຈາກຄວາມເລິກໃຫຍ່ກວ່າ. 'b' ມືສັ້ນສໍາລັບຄວາມກວ້າງ - ທໍາອິດ.
'd' ມືສັ້ນສໍາລັບຄວາມເລິກກ່ອນ.

-sຕອກ, --ຍຸດ​ທະ​ສາດ=ຕອກ
ໃຊ້ຍຸດທະສາດການທົດແທນ STRAT: '0' ຄິດໄລ່ສົມຜົນ boolean ທັງໝົດທີ່ສາມາດເປັນ
ບັນລຸໄດ້ຈາກສະຖານະເບື້ອງຕົ້ນ, ໂດຍບໍ່ມີການເພີ່ມປະສິດທິພາບ. ນີ້ແມ່ນຂໍ້ມູນຫຼາຍທີ່ສຸດ
ທາງເລືອກທີ່ມີປະສິດທິພາບຕໍ່ສົມຜົນທີ່ສ້າງຂຶ້ນ. (ຄ່າເລີ່ມຕົ້ນ) '1' ເພີ່ມປະສິດທິພາບໂດຍທັນທີ
ການທົດແທນດ້ານຂວາມືສໍາລັບຕົວແປທີ່ສືບສວນແລ້ວທີ່ເປັນຄວາມຈິງ
ຫຼືຜິດໃນເວລາສ້າງການສະແດງອອກ. ນີ້ແມ່ນຄວາມຊົງຈໍາທີ່ມີປະສິດທິພາບເທົ່າກັບ 0. '2' ໃນ
ນອກເໜືອໄປຈາກ 1, ຍັງປ່ຽນຕົວແປທີ່ເປັນຈິງ ຫຼື false ເປັນແລ້ວ
ສ້າງ​ເບື້ອງ​ຂວາ​. ນີ້ສາມາດຫມາຍຄວາມວ່າຕົວແປທີ່ແນ່ນອນກາຍເປັນບໍ່ສາມາດເຂົ້າຫາໄດ້
(ເຊັ່ນ: X0 ໃນ X0 ແລະ X1, ເມື່ອ X1 ກາຍເປັນຜິດ, ສົມມຸດວ່າ X0 ບໍ່ໄດ້ເກີດຂຶ້ນຢູ່ບ່ອນອື່ນ.
ມັນຈະຖືກຮັກສາໄວ້ວ່າຕົວແປໃດທີ່ບໍ່ສາມາດເຂົ້າຫາໄດ້ຍ້ອນວ່າສິ່ງເຫຼົ່ານີ້ບໍ່ມີ
ຈະຖືກສືບສວນ. ອີງຕາມ PBES, ນີ້ສາມາດຫຼຸດຜ່ອນຂະຫນາດຂອງ
ຜະລິດ BES ຢ່າງຫຼວງຫຼາຍແຕ່ຕ້ອງການຄວາມຊົງຈໍາທີ່ໃຫຍ່ກວ່າ. '3' ໃນ
ນອກເໜືອໄປຈາກ 2, ສືບສວນຕົວແປທີ່ສ້າງຂຶ້ນ ບໍ່ວ່າຈະເກີດຂຶ້ນໃນວົງແຫວນ,
ເຊັ່ນວ່າພວກເຂົາສາມາດຖືກຕັ້ງຄ່າເປັນຈິງຫຼືຜິດ, ຂຶ້ນກັບສັນຍາລັກຈຸດຄົງທີ່.
ນີ້ສາມາດເພີ່ມເວລາທີ່ຈໍາເປັນເພື່ອສ້າງສົມຜົນຢ່າງຫຼວງຫຼາຍ.

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

-u, --unused_data
ຢ່າເອົາສ່ວນທີ່ບໍ່ໄດ້ໃຊ້ຂອງຂໍ້ມູນສະເພາະ

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

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

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

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

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

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

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

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