ltsconvert - Online in de cloud

PROGRAMMA:

NAAM

ltsconvert - converteer en optioneel minimaliseer een LTS

KORTE INHOUD

ltsconverteren [OPTIE]... [IN BESTAND [UITBESTAND]]

PRODUCTBESCHRIJVING

Converteer het gelabelde transitiesysteem (LTS) van INFILE naar OUTFILE in het gevraagde bestand
formaat na het toepassen van de geselecteerde minimalisatiemethode (standaard is geen). Als OUTFILE dat is
niet meegeleverd, stdout wordt gebruikt. Als INFILE niet wordt opgegeven, wordt stdin gebruikt.

Het uitvoerformaat wordt bepaald door de extensie van OUTFILE, terwijl het invoerformaat dat is
bepaald door de inhoud van INFILE. Opties --in en --out kunnen worden gebruikt om de invoer te forceren
en uitvoerformaten. De ondersteunde formaten zijn:
'aut' voor het Aldebaran-formaat (CADP),
'punt' voor het GraphViz-formaat (niet langer ondersteund als invoerformaat),
'fsm' voor het Finite State Machine-formaat, of
'lts' voor het mCRL2 LTS-formaat (standaard)

OPTIES

OPTIE kan een van de volgende zijn:

-D, --bepaal
LTS bepalen

-eNAAM, --gelijkwaardigheid=NAAM
genereer een gelijkwaardige LTS, waarbij de gelijkwaardigheid behouden blijft. NAAM: 'geen' identiteit
gelijkwaardigheid (standaard) 'bisim' sterke bisimilariteit 'bisim-sig' sterke bisimilariteit
met behulp van kenmerkende verfijning 'branching-bisim' vertakking bisimilariteit 'branching-
bisim-sig' vertakkende bisimilariteit met behulp van handtekeningverfijning 'dpbranching-bisim'
divergentie behoud van vertakkende bisimilariteit 'dpbranching-bisim-sig' divergentie
behoud van vertakkende bisimilariteit met behulp van kenmerkende verfijning 'zwak-bisim' zwak
bisimilariteit 'zwak-bisim-sig' zwakke bisimilariteit met behulp van kenmerkende verfijning 'dpweak-
bisim'-divergentie met behoud van zwakke bisimilariteit 'dpweak-bisim-sig'-divergentie
behoud van zwakke bisimilariteit met behulp van kenmerkende verfijning 'sim' sterke simulatie
gelijkwaardigheid 'spoor' sterke spoor-equivalentie 'zwak-spoor' zwakke spoor-equivalentie
'tau-star' tau-sterreductie

-iFORMAT, --in=FORMAT
gebruik FORMAT als invoerformaat

-lFILE, --lps=FILE
gebruik FILE als de LPS waaruit de invoer-LTS is gegenereerd; dit kan nodig zijn
sla de juiste parameternamen van staten op bij het opslaan in fsm-indeling en naar
converteer niet-mCRL2 LTS's naar een mCRL2 LTS

--geen bereik
voer geen bereikbaarheidscontrole uit op de invoer-LTS

-n, --geen-staat
laat statusinformatie achterwege bij het opslaan in puntformaat

-oFORMAT, --uit=FORMAT
gebruik FORMAT als uitvoerformaat

--tau=HANDELSNAMEN
beschouw acties met een naam in de door komma's gescheiden lijst ACTNAMES als intern
(tau) acties naast degene die als zodanig zijn gedefinieerd door de input

--tijden[=FILE]
timingmetingen toevoegen aan FILE. Metingen worden naar de standaardfout geschreven als
er is geen BESTAND aanwezig

Standaard opties:

-q, --stil
geen waarschuwingsberichten weergeven

-v, --uitgebreid
korte tussenberichten weergeven

-d, --debuggen
gedetailleerde tussenberichten weergeven

--Log niveau=NIVEAU
tussenberichten weergeven tot en met niveau

-h, --help
help informatie weergeven

--versie
versie-informatie weergeven

Gebruik ltsconvert online met behulp van onworks.net-services