lps2lts - Online in de cloud

PROGRAMMA:

NAAM

lps2lts - genereer een LTS van een LPS

KORTE INHOUD

lps2lts [OPTIE]... [IN BESTAND [UITBESTAND]]

PRODUCTBESCHRIJVING

Genereer een LTS van de LPS in INFILE en sla het resultaat op in OUTFILE. Als INFILE dat niet is
geleverd, wordt stdin gebruikt. Als OUTFILE niet wordt geleverd, wordt de LTS niet opgeslagen.

Als de 'jittyc'-rewriter wordt gebruikt, dan de MCRL2_COMPILEREWRITER-omgevingsvariabele
(standaardwaarde: 'mcrl2compilerewriter') bepaalt het script dat de rewriter compileert,
en MCRL2_COMPILEDIR (standaardwaarde: '.') bepaalt waar tijdelijke bestanden worden opgeslagen.

Merk op dat lps2lts meerdere overgangen kan leveren met hetzelfde label tussen elk paar
staten. Indien dit niet gewenst is, kunnen dergelijke overgangen worden verwijderd door een sterk middel aan te brengen
bisimulatiereductie met bijvoorbeeld de tool ltsconvert.

Het formaat van OUTFILE wordt bepaald door de extensie (tenzij deze wordt gespecificeerd door een
keuze). 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 Als de jittyc rewriter wordt gebruikt, dan is de
Omgevingsvariabele MCRL2_COMPILEREWRITER (standaardwaarde: mcrl2compilerewriter)
bepaalt het script dat de rewriter compileert, en MCRL2_COMPILEDIR (standaardwaarde:
'.') bepaalt waar tijdelijke bestanden worden opgeslagen. Merk op dat lps2lts meerdere kan leveren
overgangen met hetzelfde label tussen elk paar toestanden. Indien dit niet gewenst is, bv
overgangen kunnen worden verwijderd door een sterke bisimulatiereductie toe te passen met bijvoorbeeld
de tool ltsconvert.

OPTIES

OPTIE kan een van de volgende zijn:

-aNAMEN, --actie=NAMEN
detecteer en rapporteer acties in het transitiesysteem die actienamen hebben van
NAMES, een door komma's gescheiden lijst. Dit is bijvoorbeeld handig om de
afwezigheid) van een actiefout. Er wordt een bericht afgedrukt voor elk voorkomen van een van
deze actienamen. Met de vlag -t worden sporen naar deze acties gegenereerd

-b[NUM], --bit-hash[=NUM]
gebruik bit-hashing om statussen op te slaan en sla maximaal NUM-statussen op. Dit betekent dat
in plaats van een volledig overzicht bij te houden van alle staten die zijn bezocht, een beetje array
wordt gebruikt die aangeven of een hash van een staat al dan niet eerder is gezien.
Hoewel dit betekent dat deze optie ervoor kan zorgen dat staten voor andere worden aangezien
(omdat ze zijn toegewezen aan dezelfde hash), kan het handig zijn om zeer groot te verkennen
LTS'en die anders niet verkenbaar zijn. De standaardwaarde voor NUM is ongeveer
2*10^8 (dit komt overeen met ongeveer 25 MB geheugen)

--gecached
gebruik cachingtechnieken voor opsomming om het genereren van toestandsruimte te versnellen.

-c[NAAM], --samenvloeiing[=NAAM]
prioritering van overgangen toepassen met het actielabel NAME. (wanneer er geen NAME is
geleverde (dwz '-c') prioriteit wordt gegeven aan de actie 'ctau'. Voorrang geven aan
om tau te gebruiken, gebruik je de vlag -ctau. Merk op dat als het lineaire proces niet tau-confluent is,
de gegenereerde toestandsruimte is noodzakelijkerwijs vergelijkbaar met de toestandsruimte van
de lp's. Het gebruikte generatiealgoritme vereist geen lineair proces
tau convergent zijn.

-D, --impasse
deadlocks detecteren (dwz voor elke deadlock wordt een bericht afgedrukt)

-F, -- divergentie
divergenties detecteren (dwz voor elke toestand met een divergentie (= tau-lus) is een bericht
afgedrukt). Het algoritme om de verschillen te detecteren is lineair voor elke toestand, dus
toestandsruimteverkenning wordt kwadratisch met deze optie aan, waardoor een toestand ontstaat
ruimteverkenning wordt langzaam als deze optie is ingeschakeld.

-yBOOL, --dummie=BOOL
vervang vrije variabelen in de LPS door dummy-waarden op basis van de waarde van BOOL:
'ja' (standaard) of 'nee'

--fout-trace
als er een fout optreedt tijdens de verkenning, sla dan een trace op naar de staat die niet kon zijn
nagegaan

--init-tgrootte=NUM
stel de initiële grootte in van de intern gebruikte hashtabellen (standaard is 10000)

-lNUM, --max=NUM
verkennen in de meeste NUM-staten

-mNAMEN, --multiactie=NAMEN
multiacties detecteren en rapporteren in het transitiesysteem van NAMES, een komma-
gescheiden lijst. Werkt als -a, behalve dat multi-acties exact overeenkomen,
inclusief gegevensparameters.

--geen informatie
voeg geen statusinformatie toe aan OUTFILEZonder deze optie voegt lps2lts state toe
vector naar de LTS. Deze optie zorgt ervoor dat deze informatie wordt weggegooid en vermeldt
worden alleen aangegeven door een volgnummer. Expliciete statusinformatie is nuttig voor
visualisatiedoeleinden, maar kan ervoor zorgen dat het OUTFILE groeit
aanzienlijk. Merk op dat deze optie impliciet is bij het schrijven in het AUT-formaat.

-oFORMAT, --uit=FORMAT
sla de uitvoer op in het opgegeven FORMAAT

--gedroogde pruim
gebruik summand pruning om het genereren van toestandsruimte te versnellen.

-QNUM, --qlimiet=NUM
beperk de opsomming van kwantoren tot NUM variabelen. (Standaard NUM=1000, NUM=0 voor
onbeperkt).

-rNAAM, --herschrijver=NAAM
gebruik herschrijfstrategie NAAM: 'jitty' jitty herschrijven (standaard) 'jittyc' gecompileerd
jitty herschrijven 'jittyp' jitty herschrijven met spreekwoord

-sNAAM, --strategie=NAAM
verken de toestandsruimte met strategie NAME: 'b', 'breedte' breedte-eerst zoeken
(standaard) 'd', 'depth' diepte-eerst zoeken 'p', 'prioriteit' prioriteit single
acties op het eerste argument zijn van soort Nat waar alleen die acties met de
laagste waarde voor deze parameter zijn geselecteerd. Bijvoorbeeld als er acties zijn a(3) en
b(4) a(3) blijft en b(4) wordt overgeslagen. Acties zonder een eerste soort parameter
Nat en multacties met meer dan één actie worden altijd gekozen (optie is
experimenteel) 'q', 'rprioritized' prioriteren acties op basis van het eerste argument dat van is
sorteer Nat (zie optie --prioritized), en selecteer willekeurig een van deze om een
willekeurige simulatie met prioriteit (optie is experimenteel) 'r', 'willekeurig' willekeurig
simulatie. Van alle volgende toestanden wordt er willekeurig één gekozen, ongeacht of
deze toestand is al waargenomen. Bijgevolg alleen willekeurige simulatie
eindigt wanneer een impasse wordt aangetroffen.

--onderdrukken
druk in uitgebreide modus geen voortgangsberichten af ​​die het aantal bezoeken aangeven
staten en overgangen. Voor grote statusruimten kan het aantal voortgangsberichten
behoorlijk afschuwelijk zijn. Deze functie helpt deze te onderdrukken. Andere uitgebreide berichten,
zoals het totale aantal onderzochte staten, gewoon zichtbaar blijven.

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

--todo-max=NUM
houd maximaal NUM-statussen in todo-lijsten bij; deze optie is alleen relevant voor breedte-
eerste zoekopdracht, waarbij NUM het maximale aantal staten per niveau is, en voor diepte
eerste zoekopdracht, waarbij NUM de maximale diepte is

-t[NUM], --spoor[=NUM]
Schrijf een kortste tracering naar elke status die wordt bereikt met een actie van NAMES from
optie --action, is een deadlock gedetecteerd met --deadlock, of is een divergentie
gedetecteerd met --divergentie naar een bestand. Er worden niet meer dan NUM sporen geschreven. Als
NUM wordt niet opgegeven, het aantal sporen is onbegrensd. Voor elk spoor dat moet zijn
Er wordt een uniek bestand met de extensie .trc (trace) gemaakt met daarin een
kortste spoor van de begintoestand naar de deadlock-toestand. De sporen kunnen zijn
mooi afgedrukt en geconverteerd naar andere formaten met tracepp.

-u, --ongebruikte gegevens
verwijder geen ongebruikte delen van de gegevensspecificatie

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 lps2lts online met behulp van onworks.net-services