Il s'agit de la commande ltscompare qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
ltscompare - comparer deux LTS
SYNOPSIS
ltscomparer [OPTION]... [INFILE1] INFILE2
DESCRIPTION
Déterminez si les systèmes de transition étiquetés (LTS) dans INFILE1 et INFILE2 sont
liés par une équivalence ou un préordre. Si INFILE1 n'est pas fourni, stdin est utilisé.
Les formats d'entrée sont déterminés par le contenu de INFILE1 et INFILE2. Options --in1
et --in2 peuvent être utilisés pour forcer le format d'entrée de INFILE1 et INFILE2, respectivement. Les
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
OPTIONS
OPTION peut être l'un des éléments suivants :
-c, --contre-exemple
générer des contre-exemples de traces si les lts d'entrée ne sont pas équivalents
-eNOM), --équivalence=NOM)
utiliser l'équivalence NAME (non autorisé en combinaison avec -p/--preorder): 'none'
équivalence d'identité (par défaut) 'bisim' forte bissimilarité 'branching-bisim'
ramification bissimilarité 'dpbranching-bisim' divergence préservant la ramification
bissimilarité 'faible-bisim' faible bissimilarité 'dpweak-bisim' divergence préservant
faible bissimilarité 'sim' forte équivalence de simulation 'trace' forte trace
équivalence 'faible trace' équivalence faible trace
-iFormat, --en 1=Format
utilisez FORMAT comme format pour INFILE1 (ou stdin)
-jFormat, --en 2=Format
utiliser FORMAT comme format pour INFILE2
-pNom, --Pré-commander=Nom
utiliser la précommande NAME (non autorisé en combinaison avec -e/--equivalence): 'inconnu'
précommande inconnue (par défaut) 'sim' simulation forte précommande 'trace' trace forte
précommande 'faible trace' trace faible précommande
--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 ltscompare en ligne en utilisant les services onworks.net
