Este es el comando ltscompare que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
ltscompare - comparar dos LTS
SINOPSIS
Comparar [OPCIÓN] ... [ARCHIVO1] ARCHIVO2
DESCRIPCIÓN
Determine si los sistemas de transición etiquetados (LTS) en INFILE1 e INFILE2 son
relacionados por alguna equivalencia o preorden. Si no se proporciona INFILE1, se utiliza stdin.
Los formatos de entrada están determinados por el contenido de INFILE1 e INFILE2. Opciones --in1
y --in2 se pueden usar para forzar el formato de entrada de INFILE1 e INFILE2, respectivamente. los
los formatos admitidos son:
'aut' para el formato Aldebarán (CADP),
'punto' para el formato GraphViz (ya no se admite como formato de entrada),
'fsm' para el formato de máquina de estados finitos, o
'lts' para el formato mCRL2 LTS
OPCIONES
OPCIÓN puede ser cualquiera de los siguientes:
-c, --contraejemplo
generar trazas de ejemplo de contador si los lts de entrada no son equivalentes
-eNOMBRE), --equivalencia=NOMBRE)
use equivalence NAME (no permitido en combinación con -p / - preorder): 'none'
equivalencia de identidad (predeterminado) 'bisim' bisimilaridad fuerte 'ramificación-bisim'
bisimilaridad de ramificación 'dpbranching-bisim' divergencia preservando la ramificación
bisimilaridad 'débil-bisim' débil bisimilaridad 'dpweak-bisim' preservación de la divergencia
bisimilaridad débil 'sim' fuerte equivalencia de simulación 'rastro' rastro fuerte
equivalencia 'traza débil' equivalencia traza débil
-iFORMATO, --En 1=FORMATO
use FORMAT como formato para INFILE1 (o stdin)
-jFORMATO, --En 2=FORMATO
use FORMAT como formato para INFILE2
-pNOMBRE, --hacer un pedido=NOMBRE
use preorder NAME (no permitido en combinación con -e / - equivalencia): 'desconocido'
preorden desconocido (predeterminado) 'sim' fuerte preorden de simulación 'rastro' rastro fuerte
preorder 'traza débil' preorden de traza débil
--tau=ACTOS
considerar las acciones con un nombre en la lista separada por comas ACTNAMES como internas
(tau) acciones además de las definidas como tales por la entrada
--tiempo[=ARCHIVO]
anexar medidas de tiempo a ARCHIVO. Las medidas se escriben con error estándar si
no se proporciona ningún ARCHIVO
Opciones estándar:
-q, --tranquilo
no mostrar mensajes de advertencia
-v, --verboso
mostrar mensajes intermedios breves
-d, --depurar
mostrar mensajes intermedios detallados
--nivel de registro=NIVEL
mostrar mensajes intermedios hasta el nivel inclusive
-h, --ayuda
mostrar información de ayuda
--versión
mostrar información de la versión
Utilice ltscompare en línea utilizando los servicios de onworks.net
