mcrl22lps - Online in de cloud

PROGRAMMA:

NAAM

mcrl22lps - vertaal een mCRL2-specificatie naar een LPS

KORTE INHOUD

mcrl22lps [OPTIE]... [IN BESTAND [UITBESTAND]]

PRODUCTBESCHRIJVING

Lineariseert de mCRL2-specificatie in INFILE en schrijft de resulterende LPS naar OUTFILE. Indien
OUTFILE is niet aanwezig, stdout wordt gebruikt. Als INFILE niet aanwezig is, wordt stdin gebruikt.

OPTIES

OPTIE kan een van de volgende zijn:

-b, --binair
gebruik bij clustering binaire hoofdletterfuncties in plaats van n-ary; in de aanwezigheid van
-w/--newstate, toestandsvariabelen worden gecodeerd door een vector van booleaanse variabelen

-e, --alleen-controleren
controleer syntaxis en statische semantiek; niet lineariseren

-c, --TROS
alle acties in de uiteindelijke LPS zijn geclusterd. Clustering houdt in dat sommaties met de
dezelfde actielabels zijn gegroepeerd. Bijvoorbeeld a(f1) . P(g1) + a(f2) .
P(g2) wordt vervangen door som b: Bool . a(if(b, f1, f2)) . P(if(b, f2, g2)). De
voordeel is dat het aantal dagvaardingen op deze manier aanzienlijk kan worden verminderd.
Het nadeel is dat som-operatoren worden geïntroduceerd en nieuwe gegevens worden gesorteerd met
hulpfuncties worden gegenereerd. Om het ontstaan ​​van nieuwe soorten te voorkomen,
de optie -b/--binary kan worden gebruikt.

-D, --delta
voeg een true->delta-som toe aan elke status in elk proces; deze delta's nemen alles onder
andere voorwaardelijke getimede delta's, waardoor het aantal delta-sommen effectief wordt verminderd
drastisch in het resulterende lineaire proces; versnelt linearisatie. Dit is de
standaard, maar het gaat niet correct om met tijd.

-lNAAM, --lin-methode=NAAM
gebruik linearisatiemethode NAAM: 'normaal' voor het genereren van een LPS in reguliere vorm
(specificatie moet normaal zijn) (standaard) 'regular2' voor een variant van 'regular'
die meer gegevensvariabelen gebruikt (handig als 'normaal' niet werkt) 'stack' for
met behulp van stack data types (handig wanneer 'regular' en 'regular2' niet werken)

-w, --nieuwstaat
toestandsvariabelen worden gecodeerd met behulp van opgesomde typen in plaats van positieve natuurlijke
nummers (Pos). Door deze optie te gebruiken, worden nieuwe eindige sorteringen met de naam Enumk gegenereerd
waarbij k de grootte van het domein is. Ook hulpgevalfuncties en gelijkheden
zijn gedefinieerd. In combinatie met de optie --binary worden de eindige sorteringen gecodeerd
door booleans. (vereist linearisatiemethode 'regular' of 'regular2').

-z, --geen-alfa
alfabet reducties worden niet toegepast. Standaard probeert mcrl22lps te distribueren
communicatie, verbergen en toestaan ​​van operators over de parallelle compositie-operator als
dit vermindert de grootte van intermediaire lineaire processen. Door deze optie te gebruiken,
stap kan worden vermeden. De naam komt van de alfabetaxioma's in procesalgebra.

-n, --geen-cluster
de acties in tussenliggende LPS'en worden niet geclusterd voordat ze parallel worden gezet.
Standaard zijn deze processen geclusterd om te voorkomen dat het aantal
summands bij het transformeren van twee parallelle lineaire processen in een enkele lineaire
Verwerken. Als een lineair proces met M summands parallel wordt gezet met een linear
proces met N optellingen het resulterende proces heeft M×N + M + N optellingen. Zowel M als
N kan aanzienlijk worden verminderd door clustering ten koste van de introductie van nieuwe soorten
en functies. Zie -c/--cluster, in het bijzonder. voor een korte uitleg van de clustering
proces.

--geen-constelm
probeer geen constante eliminatie toe te passen bij het genereren van een lineair proces.

-g, --geen-deltaelm
vermijd het verwijderen van valse delta-sommen. Vanwege het bestaan ​​van tijd, delta
aanmaningen kunnen niet ontbreken. Door de aanwezigheid van multi-acties is het aantal
sommen kunnen enorm zijn. Het algoritme voor het verwijderen van delta-sommen werkt gewoon door:
het vergelijken van elke delta summand met elkaar summand om te zien of de voorwaarde
van de een impliceert de toestand van de ander. Het is duidelijk dat dit kwadratisch is
complexiteit en kan lang duren.

-f, --geen-globvars
instantiëren don't care waarden met willekeurige constanten, in plaats van ze te modelleren
door globale variabelen. Dit heeft geen effect op globale variabelen die zijn gedeclareerd in de
specificatie.

-o, --niet-herschrijven
herschrijf datatermen niet tijdens het lineariseren; handig wanneer het herschrijfsysteem dat doet
niet beëindigen. Deze optie schakelt ook de toepassing van constant . uit
eliminatie.

-m, --geen-sumelm
vermijd het toepassen van som-eliminatie in parallelle compositie

-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

-a, --staatnamen
de namen van gegenereerde dataparameters worden uitgebreid met de naam van het proces in
die ze voorkomen. Dit maakt het gemakkelijker om te bepalen waar de parameter vandaan komt.

-T, --getimed
Vertaal het proces naar een lineaire vorm met behoud van alle getimede informatie. parallel
processen het aantal mogelijke tijdsbeperkingen kan groot zijn, vertragend
linearisatie. Verleen de --delta optie die een veel snellere vertaling oplevert die
bewaart de timing niet correct

--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 mcrl22lps online met onworks.net-services