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

ໂຄງການ:

NAME

lps2lts - ສ້າງ LTS ຈາກ LPS

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

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

ລາຍລະອຽດ

ສ້າງ LTS ຈາກ LPS ໃນ INFILE ແລະບັນທຶກຜົນໄດ້ຮັບໃສ່ OUTFILE. ຖ້າ INFILE ບໍ່ແມ່ນ
ສະຫນອງໃຫ້, stdin ຖືກນໍາໃຊ້. ຖ້າ OUTFILE ບໍ່ໄດ້ຖືກສະຫນອງ, LTS ຈະບໍ່ຖືກເກັບໄວ້.

ຖ້າ 'jittyc' rewriter ຖືກໃຊ້, ຫຼັງຈາກນັ້ນຕົວແປສະພາບແວດລ້ອມ MCRL2_COMPILEREWRITER
(ຄ່າເລີ່ມຕົ້ນ: 'mcrl2compilerewriter') ກໍານົດ script ທີ່ລວບລວມ rewriter,
ແລະ MCRL2_COMPILEDIR (ຄ່າເລີ່ມຕົ້ນ: '.') ກໍານົດບ່ອນທີ່ໄຟລ໌ຊົ່ວຄາວຖືກເກັບໄວ້.

ຈື່ໄວ້ວ່າ lps2lts ສາມາດສົ່ງຫຼາຍໄລຍະທີ່ມີປ້າຍຊື່ດຽວກັນລະຫວ່າງຄູ່ຂອງ
ລັດ. ຖ້າອັນນີ້ບໍ່ເປັນທີ່ຕ້ອງການ, ການຫັນປ່ຽນດັ່ງກ່າວສາມາດຖືກໂຍກຍ້າຍອອກໂດຍການໃຊ້ທີ່ເຂັ້ມແຂງ
bisimulation reducton ໂດຍໃຊ້ຕົວຢ່າງເຄື່ອງມື ltsconvert.

ຮູບແບບຂອງ OUTFILE ຖືກກໍານົດໂດຍສ່ວນຂະຫຍາຍຂອງມັນ (ເວັ້ນເສຍແຕ່ວ່າມັນຖືກກໍານົດໂດຍ
ທາງ​ເລືອກ). ຮູບ​ແບບ​ທີ່​ສະ​ຫນັບ​ສະ​ຫນູນ​ແມ່ນ​:

'aut' ສໍາລັບຮູບແບບ Aldebaran (CADP),
'ຈຸດ' ສໍາລັບຮູບແບບ GraphViz (ບໍ່ຮອງຮັບຮູບແບບການປ້ອນຂໍ້ມູນ),
'fsm' ສໍາລັບຮູບແບບ Finite State Machine, ຫຼື
'lts' ສໍາລັບຮູບແບບ mCRL2 LTS ຖ້າ jittyc rewriter ຖືກໃຊ້, ຫຼັງຈາກນັ້ນ
ຕົວແປສະພາບແວດລ້ອມ MCRL2_COMPILEREWRITER (ຄ່າເລີ່ມຕົ້ນ: mcrl2compilerewriter)
ກຳນົດສະຄຣິບທີ່ລວບລວມຕົວຂຽນໃໝ່, ແລະ MCRL2_COMPILEDIR (ຄ່າເລີ່ມຕົ້ນ:
'.') ກໍານົດບ່ອນທີ່ໄຟລ໌ຊົ່ວຄາວຖືກເກັບໄວ້. ໃຫ້ສັງເກດວ່າ lps2lts ສາມາດຈັດສົ່ງໄດ້ຫຼາຍ
ການປ່ຽນແປງທີ່ມີປ້າຍຊື່ດຽວກັນລະຫວ່າງຄູ່ຂອງລັດໃດນຶ່ງ. ຖ້ານີ້ບໍ່ແມ່ນຄວາມປາຖະຫນາ, ເຊັ່ນ
ການຫັນປ່ຽນສາມາດຖືກເອົາອອກໄດ້ໂດຍການໃຊ້ reducton bisimulation ທີ່ເຂັ້ມແຂງໂດຍໃຊ້ຕົວຢ່າງ
ເຄື່ອງ​ມື ltsconvert.

OPTIONS

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

-aຊື່, --ການ​ປະ​ຕິ​ບັດ​=ຊື່
ກວດ​ສອບ​ແລະ​ລາຍ​ງານ​ການ​ປະ​ຕິ​ບັດ​ໃນ​ລະ​ບົບ​ການ​ຫັນ​ປ່ຽນ​ທີ່​ມີ​ຊື່​ການ​ປະ​ຕິ​ບັດ​ຈາກ​
NAMES, ລາຍຊື່ທີ່ຂັ້ນດ້ວຍເຄື່ອງໝາຍຈຸດ. ນີ້ແມ່ນຕົວຢ່າງທີ່ເປັນປະໂຫຍດເພື່ອຊອກຫາ (ຫຼືພິສູດ
ບໍ່ມີ) ຄວາມຜິດພາດການປະຕິບັດ. ຂໍ້ຄວາມຖືກພິມອອກສໍາລັບທຸກໆການປະກົດຕົວຂອງຫນຶ່ງ
ຊື່ການປະຕິບັດເຫຼົ່ານີ້. ດ້ວຍທຸງ -t ຮ່ອງຮອຍຕໍ່ການປະຕິບັດເຫຼົ່ານີ້ຖືກສ້າງຂື້ນ

-b[NUMBER], --bit-hash[=NUMBER]
ໃຊ້ hashing ບິດເພື່ອເກັບຮັກສາລັດແລະເກັບຮັກສາຢູ່ໃນເກືອບ NUM ລັດ. ນີ້ຫມາຍຄວາມວ່າ
ແທນທີ່ຈະຮັກສາບັນທຶກອັນເຕັມທີ່ຂອງທຸກລັດທີ່ໄດ້ໄປຢ້ຽມຢາມ, array ນ້ອຍ
ຖືກນໍາໃຊ້ເພື່ອຊີ້ບອກເຖິງວ່າມີ hash ຂອງລັດໃດທີ່ເຄີຍເຫັນມາກ່ອນ.
ເຖິງແມ່ນວ່ານີ້ຫມາຍຄວາມວ່າທາງເລືອກນີ້ອາດຈະເຮັດໃຫ້ລັດຕ່າງໆຜິດພາດກັບຄົນອື່ນ
(ເນື່ອງຈາກວ່າພວກມັນຖືກສ້າງແຜນທີ່ເປັນ hash ດຽວກັນ), ມັນສາມາດເປັນປະໂຫຍດທີ່ຈະຄົ້ນຫາຂະຫນາດໃຫຍ່ຫຼາຍ
LTSs ທີ່ບໍ່ດັ່ງນັ້ນບໍ່ສາມາດຂຸດຄົ້ນໄດ້. ຄ່າເລີ່ມຕົ້ນຂອງ NUM ແມ່ນປະມານ
2*10^8 (ອັນນີ້ເທົ່າກັບຄວາມຈຳປະມານ 25MB)

--cached
ໃຊ້ເຕັກນິກການເກັບຂໍ້ມູນ enumeration ເພື່ອເລັ່ງການຜະລິດພື້ນທີ່ຂອງລັດ.

-c[NAME], -- ຂົວ​ເຊື່ອມ​ຕໍ່​[=NAME]
ນຳໃຊ້ການຈັດລຳດັບຄວາມສຳຄັນຂອງການຫັນປ່ຽນດ້ວຍປ້າຍກຳກັບ NAME.(ເມື່ອບໍ່ມີ NAME
ສະໜອງໃຫ້ (ie, '-c') ບູລິມະສິດແມ່ນມອບໃຫ້ກັບການປະຕິບັດ 'ctau'. ໃຫ້ຄວາມສໍາຄັນກັບ
to tau ໃຊ້ທຸງ -ctau. ໃຫ້ສັງເກດວ່າຖ້າຫາກວ່າຂະບວນການ linear ບໍ່ແມ່ນ tau-confluent,
ພື້ນທີ່ຂອງລັດທີ່ສ້າງຂຶ້ນແມ່ນຈໍາເປັນຕ້ອງມີສາຂາ bisimilar ກັບພື້ນທີ່ຂອງລັດຂອງ
lps ໄດ້. ສູດການຄິດໄລ່ການຜະລິດທີ່ຖືກນໍາໃຊ້ບໍ່ຮຽກຮ້ອງໃຫ້ມີຂະບວນການເສັ້ນຊື່
ຈະ convergent.

-D, --deadlock
ກວດ​ພົບ deadlocks (ເຊັ່ນ​: ສໍາ​ລັບ​ການ deadlock ທຸກ​ຂໍ້​ຄວາມ​ໄດ້​ຖືກ​ພິມ​ອອກ​)

-F, --ຄວາມ​ແຕກ​ຕ່າງ
ກວດພົບຄວາມແຕກຕ່າງ (ເຊັ່ນ: ທຸກໆລັດທີ່ມີ divergence (=tau loop) ຂໍ້ຄວາມແມ່ນ
ພິມ). ສູດການຄິດໄລ່ໃນການກວດສອບຄວາມແຕກຕ່າງແມ່ນເສັ້ນຊື່ສໍາລັບທຸກໆລັດ, ດັ່ງນັ້ນ
ການສຳຫຼວດອາວະກາດຂອງລັດກາຍເປັນສີ່ຫຼ່ຽມດ້ວຍຕົວເລືອກນີ້ເປີດ, ເຊິ່ງກໍ່ໃຫ້ເກີດສະຖານະ
ການສຳຫຼວດອາວະກາດຈະຊ້າລົງເມື່ອຕົວເລືອກນີ້ຖືກເປີດໃຊ້.

-yBOOL, -- dummy=BOOL
ປ່ຽນແທນຕົວແປຟຣີໃນ LPS ດ້ວຍຄ່າ dummy ໂດຍອີງໃສ່ມູນຄ່າຂອງ BOOL:
'ແມ່ນ' (ຄ່າເລີ່ມຕົ້ນ) ຫຼື 'ບໍ່'

--error-trace
ຖ້າມີຂໍ້ຜິດພາດເກີດຂຶ້ນໃນລະຫວ່າງການຂຸດຄົ້ນ, ບັນທຶກການຕິດຕາມໄປຫາສະຖານະທີ່ບໍ່ສາມາດເປັນໄດ້
explored

--init-tsize=NUMBER
ກໍານົດຂະຫນາດເບື້ອງຕົ້ນຂອງຕາຕະລາງ hash ທີ່ໃຊ້ພາຍໃນ (ຄ່າເລີ່ມຕົ້ນແມ່ນ 10000)

-lNUMBER, --ສູງສຸດ=NUMBER
ສຳຫຼວດຢູ່ໃນເກືອບ NUM ລັດ

-mຊື່, --multiction=ຊື່
ກວດພົບ ແລະລາຍງານການກະທຳຫຼາຍອັນໃນລະບົບການຫັນປ່ຽນຈາກ NAMES, ເຄື່ອງໝາຍຈຸດ-
ບັນຊີລາຍຊື່ທີ່ແຍກອອກ. ເຮັດວຽກຄ້າຍຄື -a, ຍົກເວັ້ນການດໍາເນີນການຫຼາຍແມ່ນກົງກັນແທ້,
ລວມທັງຕົວກໍານົດການຂໍ້ມູນ.

-- ບໍ່ມີຂໍ້ມູນ
ຢ່າເພີ່ມຂໍ້ມູນລັດໃສ່ OUTFILE ໂດຍບໍ່ມີທາງເລືອກນີ້ lps2lts ເພີ່ມສະຖານະ
vector ກັບ LTS. ທາງເລືອກນີ້ເຮັດໃຫ້ຂໍ້ມູນນີ້ຖືກຍົກເລີກແລະລະບຸ
ຖືກລະບຸໂດຍຕົວເລກລໍາດັບເທົ່ານັ້ນ. ຂໍ້ມູນຂອງລັດທີ່ຊັດເຈນແມ່ນເປັນປະໂຫຍດສໍາລັບ
ສໍາລັບຕົວຢ່າງ, ຈຸດປະສົງຂອງການເບິ່ງເຫັນ, ແຕ່ສາມາດເຮັດໃຫ້ OUTFILE ຂະຫຍາຍຕົວ
ຢ່າງຫຼວງຫຼາຍ. ຈົ່ງຈື່ໄວ້ວ່າທາງເລືອກນີ້ແມ່ນ implicit ໃນເວລາທີ່ຂຽນໃນຮູບແບບ AUT.

-oຮູບແບບ, --ອອກ=ຮູບແບບ
ບັນທຶກຜົນຜະລິດໃນຮູບແບບທີ່ລະບຸ

--prune
ໃຊ້ pruning summand ເພື່ອເລັ່ງການຜະລິດພື້ນທີ່ຂອງລັດ.

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

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

-sNAME, --ຍຸດ​ທະ​ສາດ=NAME
ສຳຫຼວດພື້ນທີ່ຂອງລັດໂດຍໃຊ້ຍຸດທະສາດ NAME: 'b', 'broadth' width-first search
(ຄ່າເລີ່ມຕົ້ນ) 'd', 'depth' depth-first search 'p', 'prioritized' ບຸລິມະສິດອັນດຽວ
ການກະທໍາກ່ຽວກັບການໂຕ້ຖຽງຄັ້ງທໍາອິດຂອງຕົນເປັນການຈັດລຽງ Nat ບ່ອນທີ່ມີພຽງແຕ່ການກະທໍາເຫຼົ່ານັ້ນກັບ
ຄ່າຕໍ່າສຸດສໍາລັບພາລາມິເຕີນີ້ຖືກເລືອກ. ຕົວຢ່າງ: ຖ້າມີການກະທຳ a(3) ແລະ
b(4) a(3) ຍັງຄົງແລະ b(4) ຖືກຂ້າມ. ການປະຕິບັດທີ່ບໍ່ມີຕົວກໍານົດການທໍາອິດຂອງການຈັດລຽງ
Nat ແລະ multctions ທີ່ມີຫຼາຍກ່ວາຫນຶ່ງປະຕິບັດແມ່ນເລືອກສະເຫມີ (ທາງເລືອກແມ່ນ
ການທົດລອງ) 'q', 'rprioritized' ຈັດລໍາດັບຄວາມສໍາຄັນຂອງການປະຕິບັດການໂຕ້ຖຽງທໍາອິດຂອງມັນ.
ຄັດ​ເລືອກ Nat (ເບິ່ງ​ທາງ​ເລືອກ --prioritized), ແລະ​ສຸ່ມ​ເລືອກ​ເອົາ​ຫນຶ່ງ​ໃນ​ເຫຼົ່າ​ນີ້​ເພື່ອ​ໃຫ້​ໄດ້​ຮັບ a
ການຈຳລອງແບບສຸ່ມຈັດລຳດັບຄວາມສຳຄັນ (ທາງເລືອກແມ່ນການທົດລອງ) 'r', 'ສຸ່ມ' ແບບສຸ່ມ
ການຈຳລອງ. ອອກຈາກລັດຕໍ່ໄປທັງຫມົດ, ຫນຶ່ງຈະຖືກເລືອກໂດຍສຸ່ມເປັນເອກະລາດບໍ່ວ່າຈະເປັນ
ລັດນີ້ໄດ້ຖືກສັງເກດເຫັນແລ້ວ. ດັ່ງນັ້ນ, ການຈໍາລອງແບບສຸ່ມເທົ່ານັ້ນ
ສິ້ນສຸດເມື່ອພົບສະຖານະການປິດກັ້ນ.

-- ສະກັດກັ້ນ
ໃນຮູບແບບ verbose, ຢ່າພິມຂໍ້ຄວາມຄວາມຄືບຫນ້າທີ່ຊີ້ບອກຈໍານວນຂອງການຢ້ຽມຢາມ
ລັດ​ແລະ​ການ​ຫັນ​ປ່ຽນ​. ສໍາລັບພື້ນທີ່ລັດຂະຫນາດໃຫຍ່, ຈໍານວນຂໍ້ຄວາມກ້າວຫນ້າສາມາດ
ເປັນຕາຢ້ານຫຼາຍ. ຄຸນນະສົມບັດນີ້ຊ່ວຍສະກັດກັ້ນສິ່ງເຫຼົ່ານັ້ນ. ຂໍ້​ຄວາມ​ຄໍາ​ເວົ້າ​ອື່ນໆ​,
ເຊັ່ນ: ຈໍານວນທັງຫມົດຂອງລັດທີ່ຂຸດຄົ້ນ, ພຽງແຕ່ຍັງຄົງເຫັນໄດ້.

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

--todo-ສູງສຸດ=NUMBER
ຮັກສາຢູ່ໃນເກືອບ NUM ລັດໃນລາຍການທີ່ຕ້ອງເຮັດ; ທາງ​ເລືອກ​ນີ້​ແມ່ນ​ກ່ຽວ​ຂ້ອງ​ພຽງ​ແຕ່​ສໍາ​ລັບ​ຄວາມ​ກວ້າງ -
ການຄົ້ນຫາຄັ້ງທໍາອິດ, ບ່ອນທີ່ NUM ເປັນຈໍານວນສູງສຸດຂອງລັດຕໍ່ລະດັບ, ແລະສໍາລັບຄວາມເລິກ
ການຄົ້ນຫາຄັ້ງທໍາອິດ, ບ່ອນທີ່ NUM ແມ່ນຄວາມເລິກສູງສຸດ

-t[NUMBER], -- ຕິດຕາມ[=NUMBER]
ຂຽນຮ່ອງຮອຍທີ່ສັ້ນທີ່ສຸດໄປຫາແຕ່ລະລັດທີ່ບັນລຸໄດ້ດ້ວຍການດໍາເນີນການຈາກ NAMES ຈາກ
ທາງ​ເລືອກ --action, ແມ່ນ​ການ​ຢຸດ​ເຊົາ​ການ​ກວດ​ພົບ​ດ້ວຍ --deadlock, ຫຼື​ເປັນ divergence
ກວດພົບດ້ວຍ --divergence ກັບໄຟລ໌. ບໍ່ເກີນ NUM ຮອຍຈະຖືກຂຽນ. ຖ້າ
NUM ບໍ່ໄດ້ຖືກສະໜອງໃຫ້ຈໍານວນການຕິດຕາມແມ່ນບໍ່ມີຂອບເຂດ. ສໍາລັບແຕ່ລະການຕິດຕາມທີ່ຈະເປັນ
ຂຽນໄຟລ໌ທີ່ເປັນເອກະລັກທີ່ມີນາມສະກຸນ .trc (ຕິດຕາມ) ຈະຖືກສ້າງຂື້ນທີ່ປະກອບດ້ວຍ a
ຮ່ອງຮອຍທີ່ສັ້ນທີ່ສຸດຈາກສະຖານະເບື້ອງຕົ້ນໄປຫາສະຖານະປິດກັ້ນ. ຮ່ອງຮອຍສາມາດເປັນ
ພິມທີ່ສວຍງາມແລະປ່ຽນເປັນຮູບແບບອື່ນໆໂດຍໃຊ້ tracepp.

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

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

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

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

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

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

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

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

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