lps2lts - Online sa Cloud

PROGRAMA:

NAME

lps2lts - bumuo ng isang LTS mula sa isang LPS

SINOPSIS

lps2lts [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

Bumuo ng LTS mula sa LPS sa INFILE at i-save ang resulta sa OUTFILE. Kung ang INFILE ay hindi
ibinibigay, ginagamit ang stdin. Kung ang OUTFILE ay hindi ibinibigay, ang LTS ay hindi nakaimbak.

Kung ginamit ang 'jittyc' rewriter, ang MCRL2_COMPILEREWRITER environment variable
(default na halaga: 'mcrl2compilerewriter') ay tumutukoy sa script na nag-compile sa muling manunulat,
at tinutukoy ng MCRL2_COMPILEDIR (default na halaga: '.') kung saan iniimbak ang mga pansamantalang file.

Tandaan na ang lps2lts ay maaaring maghatid ng maraming transition na may parehong label sa pagitan ng alinmang pares ng
estado. Kung hindi ito ninanais, maaaring alisin ang mga naturang transition sa pamamagitan ng paglalapat ng malakas
bisimulation reducton gamit halimbawa ang tool na ltsconvert.

Ang format ng OUTFILE ay tinutukoy ng extension nito (maliban kung ito ay tinukoy ng isang
opsyon). 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 na format Kung ginamit ang jittyc rewriter, kung gayon ang
MCRL2_COMPILEREWRITER variable ng kapaligiran (default na halaga: mcrl2compilerewriter)
tinutukoy ang script na nag-compile sa rewriter, at MCRL2_COMPILEDIR (default na halaga:
Tinutukoy ng '.') kung saan iniimbak ang mga pansamantalang file. Tandaan na ang lps2lts ay maaaring maghatid ng marami
mga transition na may parehong label sa pagitan ng anumang pares ng mga estado. Kung ito ay hindi ninanais, tulad
Maaaring alisin ang mga transition sa pamamagitan ng paglalapat ng malakas na bisimulation reducton gamit ang halimbawa
ang tool ay ltsconvert.

Opsyon

OPTION maaaring alinman sa mga sumusunod:

-aNAMES, --aksyon=NAMES
tumukoy at mag-ulat ng mga aksyon sa system ng mga transition kung saan nagmula ang mga pangalan ng pagkilos
NAMES, isang listahang pinaghihiwalay ng kuwit. Ito ay halimbawa na kapaki-pakinabang upang mahanap (o patunayan ang
kawalan) ng isang error sa pagkilos. Ang isang mensahe ay naka-print para sa bawat paglitaw ng isa sa
mga pangalan ng aksyon na ito. Gamit ang -t flag na mga bakas patungo sa mga pagkilos na ito ay nabuo

-b[NUM], --bit-hash[=NUM]
gumamit ng bit hashing upang mag-imbak ng mga estado at mag-imbak ng hindi hihigit sa NUM na estado. Ibig sabihin nito
sa halip na panatilihin ang isang buong talaan ng lahat ng mga estado na binisita, isang bit array
ay ginagamit na nagsasaad kung nakita o hindi ang isang hash ng isang estado.
Bagama't nangangahulugan ito na ang opsyong ito ay maaaring maging sanhi ng pagkakamali ng mga estado para sa iba
(dahil ang mga ito ay nakamapa sa parehong hash), maaari itong maging kapaki-pakinabang upang galugarin ang napakalaking
Mga LTS na kung hindi man ay hindi ma-explore. Ang default na halaga para sa NUM ay tinatayang
2*10^8 (ito ay tumutugma sa humigit-kumulang 25MB ng memorya)

--naka-cache
gumamit ng enumeration caching techniques para mapabilis ang pagbuo ng espasyo ng estado.

-c[NAME], --tagpuan[=NAME]
ilapat ang priyoridad ng mga transition na may label ng pagkilos na NAME.(kapag walang NAME
ibinigay (ibig sabihin, '-c') priyoridad ay ibinibigay sa aksyon na 'ctau'. Upang bigyang-priyoridad ang
upang tau gamitin ang watawat -ctau. Tandaan na kung ang linear na proseso ay hindi tau-confluent,
ang nabuong espasyo ng estado ay kinakailangang sumasanga bisimilar sa espasyo ng estado ng
ang lps. Ang generation algorithm na ginagamit ay hindi nangangailangan ng linear na proseso
upang maging tau convergent.

-D, --deadlock
tuklasin ang mga deadlock (ibig sabihin, para sa bawat deadlock ay naka-print ang isang mensahe)

-F, --divergence
tuklasin ang mga divergence (ibig sabihin, para sa bawat estado na may divergence (=tau loop) ang isang mensahe ay
nakalimbag). Ang algorithm upang makita ang mga pagkakaiba ay linear para sa bawat estado, kaya
Nagiging quadratic ang exploration ng kalawakan ng estado kapag naka-on ang opsyong ito, na nagiging sanhi ng estado
magiging mabagal ang paggalugad sa kalawakan kapag pinagana ang opsyong ito.

-yBOOL, --dummy=BOOL
palitan ang mga libreng variable sa LPS ng mga dummy na halaga batay sa halaga ng BOOL:
'oo' (default) o 'hindi'

--error-trace
kung may naganap na error sa panahon ng paggalugad, mag-save ng bakas sa estado na hindi maaaring mangyari
ginalugad

--init-tsize=NUM
itakda ang paunang sukat ng mga panloob na ginamit na hash table (default ay 10000)

-lNUM, --max=NUM
galugarin ang halos NUM na estado

-mNAMES, --multiaction=NAMES
tuklasin at mag-ulat ng mga multiaction sa transition system mula sa NAMES, isang kuwit
hiwalay na listahan. Gumagana tulad ng -a, maliban na ang mga multi-aksyon ay eksaktong tugma,
kabilang ang mga parameter ng data.

--walang-impormasyon
huwag magdagdag ng impormasyon ng estado sa OUTFILEKung wala ang opsyong ito ay nagdaragdag ang lps2lts ng estado
vector sa LTS. Ang pagpipiliang ito ay nagiging sanhi ng impormasyong ito na itapon at ipahayag
ay ipinapahiwatig lamang ng isang sequence number. Ang tahasang impormasyon ng estado ay kapaki-pakinabang para sa
mga layunin ng visualization, halimbawa, ngunit maaaring maging sanhi ng paglaki ng OUTFILE
malaki. Tandaan na ang opsyong ito ay implicit kapag nagsusulat sa AUT na format.

-oFORMAT, --labas=FORMAT
i-save ang output sa tinukoy na FORMAT

--pugutan
gumamit ng summand pruning upang mapabilis ang pagbuo ng espasyo ng estado.

-QNUM, --qlimit=NUM
limitahan ang enumeration ng mga quantifier sa NUM variable. (Default na NUM=1000, NUM=0 para sa
walang limitasyon).

-rNAME, --rewriter=NAME
gumamit ng diskarte sa pagsulat muli NAME: 'jitty' jitty rewriting (default) 'jittyc' compiled
jitty rewriting 'jittyp' jitty rewriting with prover

-sNAME, --diskarte=NAME
galugarin ang espasyo ng estado gamit ang diskarteng NAME: 'b', 'breadth' breadth-first search
(default) 'd', 'depth' depth-first search 'p', 'prioritize' prioritize single
mga aksyon sa unang argumento nito ay ng uri Nat kung saan ang mga aksyon lamang na may
Pinili ang pinakamababang halaga para sa parameter na ito. Hal kung may mga aksyon a(3) at
bNa (4), a(3) nananatili at b(4) ay nilaktawan. Mga pagkilos na walang unang parameter ng pag-uuri
Ang Nat at mga multaction na may higit sa isang aksyon ay palaging pinipili (ang opsyon ay
pang-eksperimentong) 'q', 'pinunahin' ay inuuna ang mga aksyon sa una nitong argumento bilang ng
sort Nat (tingnan ang opsyon --prioritized), at random na pumili ng isa sa mga ito upang makakuha ng a
priyoridad na random simulation (ang opsyon ay experimental) 'r', 'random' random
kunwa. Sa lahat ng susunod na estado, ang isa ay pinili nang random nang independyente kung
ang estadong ito ay naobserbahan na. Dahil dito, random simultation lamang
nagtatapos kapag nakatagpo ang isang deadlocked na estado.

--sugpuin
sa verbose mode, huwag mag-print ng mga progress message na nagsasaad ng bilang ng binisita
estado at mga transition. Para sa malalaking puwang ng estado ang bilang ng mga mensahe ng pag-unlad ay maaaring
maging medyo kakila-kilabot. Nakakatulong ang feature na ito na sugpuin ang mga iyon. Iba pang mga verbose na mensahe,
gaya ng kabuuang bilang ng mga estadong na-explore, manatiling nakikita.

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

--todo-max=NUM
panatilihin ang hindi hihigit sa NUM na estado sa mga listahan ng todo; ang pagpipiliang ito ay may kaugnayan lamang para sa lawak-
unang paghahanap, kung saan ang NUM ay ang maximum na bilang ng mga estado bawat antas, at para sa lalim
unang paghahanap, kung saan ang NUM ay ang pinakamataas na lalim

-t[NUM], --bakas[=NUM]
Sumulat ng pinakamaikling bakas sa bawat estado na naabot ng isang aksyon mula sa NAMES mula sa
opsyon --action, ay isang deadlock na nakita sa --deadlock, o isang divergence
natukoy na may --divergence sa isang file. Hindi hihigit sa NUM na bakas ang isusulat. Kung
NUM ay hindi ibinigay ang bilang ng mga bakas ay walang hangganan. Para sa bawat bakas na dapat
nakasulat ng isang natatanging file na may extension na .trc (trace) ay malilikha na naglalaman ng a
pinakamaikling bakas mula sa paunang estado hanggang sa deadlock na estado. Ang mga bakas ay maaaring
medyo naka-print at na-convert sa iba pang mga format gamit ang tracepp.

-u, --hindi nagamit-data
huwag tanggalin ang mga hindi nagamit na bahagi ng detalye ng data

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

Gumamit ng lps2lts online gamit ang mga serbisyo ng onworks.net