ltsconvert - Online sa Cloud

PROGRAMA:

NAME

ltsconvert - i-convert at opsyonal na i-minimize ang isang LTS

SINOPSIS

ltsconvert [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

I-convert ang may label na transition system (LTS) mula INFILE patungong OUTFILE sa hiniling
format pagkatapos ilapat ang napiling paraan ng pagliit (default ay wala). Kung ang OUTFILE ay
hindi naibigay, ginagamit ang stdout. Kung hindi ibinigay ang INFILE, ginagamit ang stdin.

Ang format ng output ay tinutukoy ng extension ng OUTFILE, samantalang ang format ng input ay
tinutukoy ng nilalaman ng INFILE. Maaaring gamitin ang mga opsyon --in at --out upang pilitin ang input
at mga format ng output. Ang mga sinusuportahang format ay:
'aut' para sa Aldebaran format (CADP),
'tuldok' para sa GraphViz format (hindi na suportado bilang input format),
'fsm' para sa Finite State Machine na format, o
'lts' para sa mCRL2 LTS format (default)

Opsyon

OPTION maaaring alinman sa mga sumusunod:

-D, --tukuyin
tukuyin ang LTS

-eNAME, --katumbas=NAME
bumuo ng katumbas na LTS, pinapanatili ang katumbas NAME: 'wala' na pagkakakilanlan
equivalence (default) 'bisim' strong bisimilarity 'bisim-sig' strong bisimilarity
gamit ang signature refinement 'branching-bisim' branching bisimilarity 'branching-
bisim-sig' sumasanga bisimilarity gamit ang signature refinement 'dpbranching-bisim'
divergence pinapanatili ang sumasanga bisimilarity 'dpbranching-bisim-sig' divergence
pinapanatili ang sumasanga bisimilarity gamit ang signature refinement 'weak-bisim' mahina
bisimilarity 'weak-bisim-sig' mahina bisimilarity gamit ang signature refinement 'dpweak-
divergence ng bisim' pinapanatili ang mahinang bisimilarity 'dpweak-bisim-sig' divergence
pinapanatili ang mahinang bisimilarity gamit ang signature refinement na 'sim' na malakas na simulation
equivalence 'trace' strong trace equivalence 'weak-trace' weak trace equivalence
'tau-star' tau star pagbabawas

-iFORMAT, --sa=FORMAT
gamitin ang FORMAT bilang format ng pag-input

-lFILE, --lps=FILE
gamitin ang FILE bilang LPS kung saan nabuo ang input LTS; ito ay maaaring kailanganin upang
iimbak ang tamang mga pangalan ng parameter ng mga estado kapag nagse-save sa fsm format at sa
i-convert ang mga hindi mCRL2 LTS sa isang mCRL2 LTS

--hindi maabot
huwag magsagawa ng reachability check sa input LTS

-n, --walang-estado
iwanan ang impormasyon ng estado kapag nagse-save sa tuldok na format

-oFORMAT, --labas=FORMAT
gamitin ang FORMAT bilang format ng output

--tau=ACTNAMES
isaalang-alang ang mga aksyon na may pangalan sa comma separated list na ACTNAMES bilang panloob
(tau) na mga aksyon bilang karagdagan sa mga tinukoy bilang tulad ng input

--mga oras[=FILE]
magdagdag ng mga sukat ng timing sa FILE. Ang mga sukat ay isinusulat sa karaniwang error kung
walang FILE na ibinigay

Mga karaniwang opsyon:

-q, --tahimik
huwag magpakita ng mga mensahe ng babala

-v, --verbose
magpakita ng mga maikling intermediate na mensahe

-d, --debug
magpakita ng mga detalyadong intermediate na mensahe

--log-level=ANTAS
magpakita ng mga intermediate na mensahe hanggang sa at kabilang ang antas

-h, - Tumulong
ipakita ang impormasyon ng tulong

--bersyon
ipakita ang impormasyon ng bersyon

Gamitin ang ltsconvert online gamit ang mga serbisyo ng onworks.net