เบเบตเปเปเบกเปเบเบเปเบฒเบชเบฑเปเบ lps2lts เบเบตเปเบชเบฒเบกเบฒเบเบเปเบฒเปเบเบตเบเบเบฒเบเปเบเปเปเบ OnWorks เบเบนเปเปเบซเปเบเปเบฅเบดเบเบฒเบเปเบฎเบเบเบดเปเบเบเบฃเบตเปเบเบเปเบเปเบซเบเบถเปเบเปเบเบซเบผเบฒเบเบเปเบญเบเปเบฎเบฑเบเบงเบฝเบเบญเบญเบเปเบฅเบเปเบเบญเบเบเบงเบเปเบฎเบปเบฒเปเบเบฑเปเบ Ubuntu Online, Fedora Online, Windows online emulator เบซเบผเบท MAC OS online emulator
เปเบเบเบเบฒเบ:
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