ltsconvert - En ligne dans le Cloud

PROGRAMME:

Nom

ltsconvert - convertir et éventuellement minimiser un LTS

SYNOPSIS

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

DESCRIPTION

Convertissez le système de transition étiqueté (LTS) de INFILE en OUTFILE dans le
format après avoir appliqué la méthode de minimisation sélectionnée (la valeur par défaut est aucune). Si OUTFILE est
non fourni, stdout est utilisé. Si INFILE n'est pas fourni, stdin est utilisé.

Le format de sortie est déterminé par l'extension de OUTFILE, tandis que le format d'entrée est
déterminé par le contenu de INFILE. Les options --in et --out peuvent être utilisées pour forcer la saisie
et les formats de sortie. 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 (par défaut)

OPTIONS

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

-D, --déterminer
déterminer LTS

-eNom, --équivalence=Nom
générer un LTS équivalent, en préservant l'équivalence NAME: 'none' identité
équivalence (par défaut) 'bisim' forte bissimilarité 'bisim-sig' forte bissimilarité
en utilisant le raffinement de signature 'branching-bisim' branching bisimilarity 'branching-
bisim-sig' bisimilarité de branchement utilisant le raffinement de signature 'dpbranching-bisim'
divergence préservant la bisimilarité de branchement 'dpbranching-bisim-sig' divergence
préservation de la bissimilarité de branchement à l'aide du raffinement de signature « faible-bisim » faible
bissimilarité 'weak-bisim-sig' faible bissimilarité utilisant le raffinement de signature 'dpweak-
divergence bisim' préservant une faible bisimilarité divergence 'dpweak-bisim-sig'
préservation de la faible bissimilarité à l'aide d'une simulation forte de raffinement de signature « sim »
équivalence 'trace' équivalence de trace forte 'trace faible' équivalence de trace faible
'tau-star' réduction d'étoiles tau

-iFormat, --dans=Format
utiliser FORMAT comme format d'entrée

-lDOSSIER, --lps=DOSSIER
utiliser FILE comme LPS à partir duquel le LTS d'entrée a été généré ; cela pourrait être nécessaire pour
stocker les noms de paramètres corrects des états lors de l'enregistrement au format fsm et à
convertir les LTS non mCRL2 en LTS mCRL2

--pas de portée
ne pas effectuer de contrôle d'accessibilité sur l'entrée LTS

-n, --pas d'état
omettre les informations d'état lors de l'enregistrement au format point

-oFormat, --dehors=Format
utiliser FORMAT comme format de sortie

--tau=ACTNAME
considérer les actions avec un nom dans la liste séparée par des virgules ACTNAMES comme internes
(tau) actions en plus de celles définies comme telles par l'entrée

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

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 ltsconvert en ligne à l'aide des services onworks.net