lps2lts - En ligne dans le cloud

PROGRAMME:

Nom

lps2lts - générer un LTS à partir d'un LPS

SYNOPSIS

lps2lts [OPTION]... [DANS LE FICHIER [FICHIERS]]

DESCRIPTION

Générez un LTS à partir du LPS dans INFILE et enregistrez le résultat dans OUTFILE. Si INFILE n'est pas
fourni, stdin est utilisé. Si OUTFILE n’est pas fourni, le LTS n’est pas stocké.

Si le réécrivain 'jittyc' est utilisé, alors la variable d'environnement MCRL2_COMPILEREWRITER
(valeur par défaut : 'mcrl2compilerewriter') détermine le script qui compile le rewriter,
et MCRL2_COMPILEDIR (valeur par défaut : '.') détermine où les fichiers temporaires sont stockés.

Notez que lps2lts peut fournir plusieurs transitions avec la même étiquette entre n'importe quelle paire de
États. Si cela n'est pas souhaité, ces transitions peuvent être supprimées en appliquant une forte
Réduction par bisimulation en utilisant par exemple l'outil ltsconvert.

Le format de OUTFILE est déterminé par son extension (sauf s'il est spécifié par un
option). Les formats pris en charge sont :

'aut' pour le format Aldebaran (CADP),
'dot' pour le format GraphViz (n'est plus pris en charge comme format d'entrée),
'fsm' pour le format de la machine à états finis, ou
'lts' pour le format mCRL2 LTS Si le réécrivain jittyc est utilisé, alors le
Variable d'environnement MCRL2_COMPILEREWRITER (valeur par défaut : mcrl2compilerewriter)
détermine le script qui compile le rewriter, et MCRL2_COMPILEDIR (valeur par défaut :
'.') détermine l'emplacement de stockage des fichiers temporaires. Notez que lps2lts peut fournir plusieurs
transitions avec la même étiquette entre n’importe quelle paire d’états. Si cela n'est pas souhaité, tel
les transitions peuvent être supprimées en appliquant une forte réduction de bisimulation en utilisant par exemple
l'outil ltsconvert.

OPTIONS

OPTION peut être l'un des éléments suivants :

-aDES NOMS, --action=DES NOMS
détecter et signaler les actions dans le système de transitions dont les noms d'action proviennent de
NOMS, une liste séparée par des virgules. Ceci est par exemple utile pour trouver (ou prouver le
absence) d’une erreur d’action. Un message est imprimé pour chaque occurrence de l'un des
ces noms d'action. Avec l'option -t, des traces vers ces actions sont générées

-b[NUM], --bit-hachage[=NUM]
utilisez le hachage de bits pour stocker les états et stocker au plus NUM états. Cela signifie que
au lieu de conserver un enregistrement complet de tous les états visités, un tableau de bits
est utilisé pour indiquer si un hachage d'un état a déjà été vu ou non.
Bien que cela signifie que cette option peut conduire à confondre des États avec d’autres
(parce qu'ils sont mappés sur le même hachage), il peut être utile d'explorer de très grandes
Des LTS qui autrement ne seraient pas explorables. La valeur par défaut de NUM est d'environ
2*10^8 (cela correspond à environ 25 Mo de mémoire)

--caché
utiliser des techniques de mise en cache d’énumération pour accélérer la génération de l’espace d’état.

-c[Nom], --confluence[=Nom]
appliquer la priorisation des transitions avec le label d'action NOM. (quand aucun NOM n'est
fourni (c'est-à-dire '-c') la priorité est donnée à l'action 'ctau'. Donner la priorité à
pour tau, utilisez le drapeau -ctau. Notez que si le processus linéaire n'est pas tau-confluent,
l'espace d'état généré se ramifie nécessairement de manière bisimilaire à l'espace d'état de
les lps. L'algorithme de génération utilisé ne nécessite pas le processus linéaire
être tau convergent.

-D, --impasse
détecter les blocages (c'est-à-dire que pour chaque blocage, un message est imprimé)

-F, --divergence
détecter les divergences (c'est-à-dire pour chaque état avec une divergence (= boucle tau) un message est
imprimé). L'algorithme pour détecter les divergences est linéaire pour chaque état, donc
L'exploration de l'espace d'état devient quadratique avec cette option activée, provoquant un état
l'exploration spatiale devient lente lorsque cette option est activée.

-yBOOL, --factice=BOOL
remplacez les variables libres dans le LPS par des valeurs factices basées sur la valeur de BOOL :
'oui' (par défaut) ou 'non'

--erreur-trace
si une erreur survient lors de l'exploration, enregistrez une trace vers l'état qui n'a pas pu être
exploré

--init-tsize=NUM
définir la taille initiale des tables de hachage utilisées en interne (la valeur par défaut est 10000 XNUMX)

-lNUM, --maximum=NUM
explorer au plus NUM états

-mDES NOMS, --multiaction=DES NOMS
détecter et signaler les multiactions dans le système de transitions à partir de NAMES, une virgule
liste séparée. Fonctionne comme -a, sauf que les actions multiples correspondent exactement,
y compris les paramètres de données.

--pas d'information
n'ajoutez pas d'informations d'état à OUTFILE Sans cette option, lps2lts ajoute l'état
vecteur vers le LTS. Cette option entraîne la suppression de ces informations et indique
sont uniquement indiqués par un numéro de séquence. Les informations d'état explicites sont utiles pour
à des fins de visualisation, par exemple, mais peut entraîner la croissance du OUTFILE
considérablement. Notez que cette option est implicite lors de l'écriture au format AUT.

-oFormat, --dehors=Format
enregistrer la sortie dans le FORMAT spécifié

--prune
utilisez l'élagage par somme pour accélérer la génération de l'espace d'état.

-QNUM, --qlimite=NUM
limiter l'énumération des quantificateurs à NUM variables. (Par défaut NUM=1000, NUM=0 pour
illimité).

-rNom, --réscripteur=Nom
utiliser la stratégie de réécriture NOM : 'jitty' réécriture jitty (par défaut) 'jittyc' compilé
réécriture jitty 'jittyp' réécriture jitty avec prouveur

-sNom, --stratégie=Nom
explorer l'espace d'état à l'aide de la stratégie NOM : 'b', 'breadth', recherche en largeur d'abord
(par défaut) 'd', 'profondeur' recherche en profondeur d'abord 'p', 'priorisé' priorité unique
les actions sur son premier argument étant de type Nat où seules les actions avec le
la valeur la plus basse pour ce paramètre est sélectionnée. Par exemple, s'il y a des actions ade Géographie (3) et avec la
b(4), a(3) reste et b(4) est ignoré. Actions sans premier paramètre de tri
Nat et les multiactions avec plus d'une action sont toujours choisies (l'option est
expérimental) 'q', 'priorisé' priorise les actions sur son premier argument étant de
triez Nat (voir l'option --prioritized), et sélectionnez-en un au hasard pour obtenir un
simulation aléatoire prioritaire (l'option est expérimentale) 'r', 'random' aléatoire
simulation. Parmi tous les états suivants, un est choisi au hasard, indépendamment du fait que
cet état a déjà été observé. Par conséquent, la simulation aléatoire uniquement
se termine lorsqu'un état de blocage est rencontré.

--réprimer
en mode verbeux, n'imprimez pas les messages de progression indiquant le nombre de sites visités
états et transitions. Pour les grands espaces d'états, le nombre de messages de progression peut
être assez horrible. Cette fonctionnalité permet de les supprimer. Autres messages verbeux,
comme le nombre total d'États explorés, restent simplement visibles.

--horaires[=DOSSIER]
ajouter des mesures de synchronisation à FILE. Les mesures sont écrites avec l'erreur standard si
aucun FICHIER n'est fourni

--todo-max=NUM
conserver au plus NUM états dans les listes de tâches ; cette option n'est pertinente que pour l'étendue-
première recherche, où NUM est le nombre maximum d'états par niveau, et pour la profondeur
première recherche, où NUM est la profondeur maximale

-t[NUM], --tracer[=NUM]
Écrivez une trace la plus courte vers chaque état atteint avec une action de NAMES de
option --action, est-ce qu'un blocage est détecté avec --deadlock, ou est-ce une divergence
détecté avec --divergence dans un fichier. Pas plus de NUM traces seront écrites. Si
NUM n'est pas fourni, le nombre de traces est illimité. Pour chaque trace à être
écrit un fichier unique avec l'extension .trc (trace) sera créé contenant un
trace la plus courte de l’état initial à l’état de blocage. Les traces peuvent être
joliment imprimé et converti dans d'autres formats à l'aide de tracepp.

-u, --données-inutilisées
ne supprimez pas les parties inutilisées de la spécification des données

Options standards :

-q, --silencieux
ne pas afficher les messages d'avertissement

-v, --verbeux
afficher de courts messages intermédiaires

-d, --déboguer
afficher des messages intermédiaires détaillés

--niveau de journal=NIVEAU
afficher des messages intermédiaires jusqu'au niveau inclus

-h, --Aidez-moi
afficher les informations d'aide

--version
afficher les informations de version

Utilisez lps2lts en ligne à l'aide des services onworks.net