Este es el comando ltsconvert 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
ltsconvert: convierte y, opcionalmente, minimiza un LTS
SINOPSIS
convertir [OPCIÓN] ... [EN ARCHIVO [PERFIL]]
DESCRIPCIÓN
Convierta el sistema de transición etiquetado (LTS) de INFILE a OUTFILE en el pedido
formato después de aplicar el método de minimización seleccionado (el valor predeterminado es ninguno). Si OUTFILE es
no suministrado, se utiliza stdout. Si no se proporciona INFILE, se utiliza stdin.
El formato de salida está determinado por la extensión de OUTFILE, mientras que el formato de entrada es
determinado por el contenido de INFILE. Las opciones --in y --out se pueden usar para forzar la entrada
y formatos de salida. 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 (predeterminado)
CAMPUS
OPCIÓN puede ser cualquiera de los siguientes:
-D, - determinar
determinar LTS
-eNOMBRE, --equivalencia=NOMBRE
generar un LTS equivalente, conservando la equivalencia NOMBRE: identidad 'ninguna'
equivalencia (predeterminado) 'bisim' bisimilaridad fuerte 'bisim-sig' bisimilaridad fuerte
uso de refinamiento de firma 'ramificación-bisim' ramificación bisimilaridad 'ramificación-
bisim-sig 'bisimilaridad de ramificación utilizando el refinamiento de la firma' dpbranching-bisim '
divergencia preservando la bisimilaridad ramificada 'dpbranching-bisim-sig' divergencia
preservando la bisimilaridad de ramificación usando el refinamiento de la firma 'débil-bisim' débil
bisimilaridad 'débil-bisim-sig' bisimilaridad débil usando el refinamiento de la firma 'dpweak-
bisim 'divergencia preservando bisimilaridad débil' dpweak-bisim-sig 'divergencia
preservando la bisimilitud débil usando el refinamiento de la firma 'sim' simulación fuerte
equivalencia 'traza' equivalencia de traza fuerte 'traza débil' equivalencia de traza débil
reducción de estrellas tau 'tau-star'
-iFORMATO, --en=FORMATO
utilizar FORMAT como formato de entrada
-lARCHIVO, --lps=ARCHIVO
use FILE como el LPS a partir del cual se generó el LTS de entrada; esto podría ser necesario para
almacenar los nombres correctos de los parámetros de los estados al guardar en formato fsm y para
convertir LTS que no son mCRL2 en un LTS mCRL2
--no alcance
no realice una verificación de accesibilidad en el LTS de entrada
-n, --no-estado
omita la información del estado al guardar en formato de puntos
-oFORMATO, --fuera=FORMATO
utilizar FORMAT como formato de salida
--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
Use ltsconvert en línea usando los servicios de onworks.net