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

ໂຄງການ:

NAME

ltsconvert - ແປງແລະທາງເລືອກໃນການຫຼຸດຜ່ອນ LTS

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

lts ແປງ [ທາງເລືອກ]... [INFILE [OUTFILE]]

ລາຍລະອຽດ

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

ຮູບແບບຜົນຜະລິດແມ່ນຖືກກໍານົດໂດຍການຂະຫຍາຍ OUTFILE, ໃນຂະນະທີ່ຮູບແບບການປ້ອນຂໍ້ມູນແມ່ນ
ກໍານົດໂດຍເນື້ອໃນຂອງ INFILE. ຕົວເລືອກ --in ແລະ --out ສາມາດຖືກໃຊ້ເພື່ອບັງຄັບການປ້ອນຂໍ້ມູນ
ແລະຮູບແບບຜົນຜະລິດ. ຮູບ​ແບບ​ທີ່​ສະ​ຫນັບ​ສະ​ຫນູນ​ແມ່ນ​:
'aut' ສໍາລັບຮູບແບບ Aldebaran (CADP),
'ຈຸດ' ສໍາລັບຮູບແບບ GraphViz (ບໍ່ຮອງຮັບຮູບແບບການປ້ອນຂໍ້ມູນ),
'fsm' ສໍາລັບຮູບແບບ Finite State Machine, ຫຼື
'lts' ສໍາລັບຮູບແບບ mCRL2 LTS (ຄ່າເລີ່ມຕົ້ນ)

OPTIONS

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

-D, -- ກໍານົດ
ກໍານົດ LTS

-eNAME, -- ທຽບເທົ່າ=NAME
ສ້າງ LTS ທຽບເທົ່າ, ຮັກສາຊື່ທຽບເທົ່າ: 'none' ຕົວຕົນ
ຄວາມເທົ່າທຽມ (ຄ່າເລີ່ມຕົ້ນ) 'bisim' ຄວາມຄ້າຍຄືກັນທີ່ເຂັ້ມແຂງ 'bisim-sig' ຄວາມຄ້າຍຄືກັນທີ່ເຂັ້ມແຂງ
ການ​ນໍາ​ໃຊ້​ການ​ປັບ​ປຸງ​ລາຍ​ເຊັນ 'branching​-bisim​' ກິ່ງ​ງ່າ bisimilarity 'branching-
bisim-sig' ການແຕກງ່າ bisimilarity ໂດຍນໍາໃຊ້ການປັບປຸງລາຍເຊັນ 'dpbranching-bisim'
divergence ຮັກສາຄວາມແຕກງ່າ bisimilarity 'dpbranching-bisim-sig' divergence
ຮັກສາຄວາມຄ້າຍຄືກັນຂອງກິ່ງງ່າໂດຍໃຊ້ການປັບປຸງລາຍເຊັນ 'weak-bisim' ອ່ອນແອ
bisimilarity 'weak-bisim-sig' bisimilarity ອ່ອນແອໂດຍນໍາໃຊ້ການປັບປຸງລາຍເຊັນ 'dpweak-
bisim' divergence ຮັກສາ bisimilarity ອ່ອນແອ 'dpweak-bisim-sig' divergence
ຮັກສາຄວາມຄ້າຍຄືກັນທີ່ອ່ອນແອໂດຍໃຊ້ການປັບປ່ຽນລາຍເຊັນ 'sim' simulation ທີ່ເຂັ້ມແຂງ
ທຽບເທົ່າ 'ຕິດຕາມ' ຄວາມສົມດຸນຂອງຮອຍທີ່ແຂງແຮງ 'ຮ່ອງຮອຍທີ່ອ່ອນແອ' ຄວາມສົມດຸນຂອງຮອຍທີ່ອ່ອນແອ
'tau-star' ການຫຼຸດລົງດາວ

-iຮູບແບບ, --ໃນ=ຮູບແບບ
ໃຊ້ FORMAT ເປັນຮູບແບບການປ້ອນຂໍ້ມູນ

-lເອກະສານ, --lps=ເອກະສານ
ໃຊ້ FILE ເປັນ LPS ທີ່ວັດສະດຸປ້ອນ LTS ຖືກສ້າງຂຶ້ນ; ນີ້ອາດຈະຈໍາເປັນຕ້ອງໄດ້
ເກັບຮັກສາຊື່ພາລາມິເຕີທີ່ຖືກຕ້ອງຂອງລັດໃນເວລາທີ່ບັນທຶກໃນຮູບແບບ fsm ແລະ
ປ່ຽນ mCRL2 LTSs ທີ່ບໍ່ແມ່ນ mCRL2 LTS

-- ບໍ່​ສາ​ມາດ​ບັນ​ລຸ​ໄດ້​
ຢ່າເຮັດການກວດສອບຄວາມສາມາດໃນການເຂົ້າຫາໄດ້ໃນ LTS ຂາເຂົ້າ

-n, --ບໍ່ມີລັດ
ປ່ອຍຂໍ້ມູນສະຖານະອອກເມື່ອບັນທຶກໃນຮູບແບບຈຸດ

-oຮູບແບບ, --ອອກ=ຮູບແບບ
ໃຊ້ FORMAT ເປັນຮູບແບບຜົນຜະລິດ

--tau=ACTNAMES
ພິຈາລະນາການກະທຳທີ່ມີຊື່ຢູ່ໃນລາຍການທີ່ແຍກດ້ວຍເຄື່ອງໝາຍຈຸດ ACTNAMES ໃຫ້ເປັນພາຍໃນ
(tau) ການປະຕິບັດນອກເຫນືອໄປຈາກທີ່ກໍານົດເປັນດັ່ງກ່າວໂດຍການປ້ອນຂໍ້ມູນ

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

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

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

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

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

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

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

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

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