lps2lts: en línea en la nube

PROGRAMA:

NOMBRE

lps2lts: genera un LTS a partir de un LPS

SINOPSIS

lps2lts [OPCIÓN] ... [EN ARCHIVO [PERFIL]]

DESCRIPCIÓN

Genere un LTS a partir del LPS en INFILE y guarde el resultado en OUTFILE. Si INFILE no es
suministrado, se utiliza stdin. Si no se suministra OUTFILE, el LTS no se almacena.

Si se usa el reescritor 'jittyc', entonces la variable de entorno MCRL2_COMPILEREWRITER
(valor predeterminado: 'mcrl2compilerewriter') determina el script que compila el reescritor,
y MCRL2_COMPILEDIR (valor predeterminado: '.') determina dónde se almacenan los archivos temporales.

Tenga en cuenta que lps2lts puede ofrecer varias transiciones con la misma etiqueta entre cualquier par de
estados. Si esto no se desea, dichas transiciones se pueden eliminar aplicando un fuerte
reducción de bisimulación utilizando, por ejemplo, la herramienta ltsconvert.

El formato de OUTFILE está determinado por su extensión (a menos que esté especificado por un
opción). 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 Si se usa el reescritor jittyc, entonces el
Variable de entorno MCRL2_COMPILEREWRITER (valor predeterminado: mcrl2compilerewriter)
determina el script que compila el reescritor y MCRL2_COMPILEDIR (valor predeterminado:
'.') determina dónde se almacenan los archivos temporales. Tenga en cuenta que lps2lts puede ofrecer múltiples
transiciones con la misma etiqueta entre cualquier par de estados. Si esto no se desea, tal
las transiciones se pueden eliminar aplicando una fuerte reducción de bisimulación utilizando, por ejemplo,
la herramienta ltsconvert.

CAMPUS

OPCIÓN puede ser cualquiera de los siguientes:

-aNOMBRES, --acción=NOMBRES
detectar e informar acciones en el sistema de transiciones que tienen nombres de acción de
NAMES, una lista separada por comas. Esto es, por ejemplo, útil para encontrar (o probar la
ausencia) de un error de acción. Se imprime un mensaje para cada ocurrencia de uno de
estos nombres de acciones. Con la bandera -t se generan trazos hacia estas acciones

-b[NUM], - bit-hash[=NUM]
utilice bit hash para almacenar estados y almacenar en la mayoría de NUM estados. Esto significa que
en lugar de mantener un registro completo de todos los estados que se han visitado, una matriz de bits
se utiliza para indicar si se ha visto antes o no un hash de un estado.
Aunque esto significa que esta opción puede hacer que los estados se confundan con otros
(porque se asignan al mismo hash), puede resultar útil explorar
LTS que de otro modo no serían explorables. El valor predeterminado de NUM es aproximadamente
2 * 10 ^ 8 (esto corresponde a unos 25 MB de memoria)

- en caché
Utilice técnicas de almacenamiento en caché de enumeración para acelerar la generación de espacios de estado.

-c[NOMBRE], --confluencia[=NOMBRE]
aplicar la priorización de las transiciones con la etiqueta de acción NAME. (cuando no hay NAME
suministrado (es decir, '-c') se da prioridad a la acción 'ctau'. Dar prioridad a
para tau usa la bandera -ctau. Tenga en cuenta que si el proceso lineal no es tau-confluente,
el espacio de estado generado es necesariamente bisimilar al espacio de estado de
los lps. El algoritmo de generación que se utiliza no requiere el proceso lineal
ser tau convergente.

-D, --punto muerto
detectar interbloqueos (es decir, por cada interbloqueo se imprime un mensaje)

-F, --divergencia
detectar divergencias (es decir, para cada estado con una divergencia (= bucle tau) se envía un mensaje
impreso). El algoritmo para detectar las divergencias es lineal para cada estado, por lo que
La exploración espacial de estado se vuelve cuadrática con esta opción activada, lo que provoca un estado
la exploración espacial se vuelve lenta cuando esta opción está habilitada.

-yBOOL, --ficticio=BOOL
reemplace las variables libres en el LPS con valores ficticios basados ​​en el valor de BOOL:
'sí' (predeterminado) o 'no'

- rastreo de errores
Si ocurre un error durante la exploración, guarde un rastro al estado que no pudo ser
explorado

--init-tamaño=NUM
establecer el tamaño inicial de las tablas hash utilizadas internamente (el valor predeterminado es 10000)

-lNUM, --máx=NUM
explorar como máximo NUM estados

-mNOMBRES, --multiacción=NOMBRES
detectar y reportar multiacciones en el sistema de transiciones de NAMES, una coma
lista separada. Funciona como -a, excepto que las acciones múltiples coinciden exactamente,
incluidos los parámetros de datos.

--sin información
No agregue información de estado a OUTFILE Sin esta opción lps2lts agrega estado
vector al LTS. Esta opción hace que esta información se descarte y declare
sólo se indican mediante un número de secuencia. La información explícita del estado es útil para
fines de visualización, por ejemplo, pero puede hacer que el OUTFILE crezca
importantemente. Tenga en cuenta que esta opción está implícita al escribir en formato AUT.

-oFORMATO, --fuera=FORMATO
guardar la salida en el FORMATO especificado

--ciruela pasa
utilice la poda de suma para acelerar la generación de espacio de estado.

-QNUM, --qlímite=NUM
limitar la enumeración de cuantificadores a NUM variables. (Predeterminado NUM = 1000, NUM = 0 para
ilimitado).

-rNOMBRE, --recritor=NOMBRE
usar la estrategia de reescritura NOMBRE: 'jitty' jitty reescritura (predeterminado) 'jittyc' compilado
jitty reescribiendo 'jittyp' jitty reescribiendo con prover

-sNOMBRE, --estrategia=NOMBRE
explorar el espacio de estados usando la estrategia NAME: 'b', 'amplitud' búsqueda primero en amplitud
(predeterminado) 'd', 'profundidad' búsqueda en profundidad primero 'p', 'priorizado' priorizar individual
acciones en su primer argumento son de tipo Nat donde solo aquellas acciones con el
se selecciona el valor más bajo para este parámetro. Ej. Si hay acciones a(3) y
b(4) a(3) permanece y b(4) se omite. Acciones sin un primer parámetro de ordenación
Siempre se eligen nat y multacciones con más de una acción (la opción es
experimental) 'q', 'rprioritized' priorizan acciones en su primer argumento siendo de
ordenar Nat (ver opción --prioritized), y seleccionar aleatoriamente uno de estos para obtener un
simulación aleatoria priorizada (la opción es experimental) 'r', 'aleatoria' aleatoria
simulación. De todos los estados siguientes, uno se elige al azar independientemente de si
este estado ya se ha observado. En consecuencia, la simulación aleatoria solo
termina cuando se encuentra un estado de interbloqueo.

--reprimir
en modo detallado, no imprima mensajes de progreso que indiquen el número de visitas
estados y transiciones. Para espacios de estado grandes, el número de mensajes de progreso puede
ser bastante horrendo. Esta característica ayuda a suprimirlos. Otros mensajes detallados,
como el número total de estados explorados, simplemente permanecen visibles.

--tiempo[=ARCHIVO]
anexar medidas de tiempo a ARCHIVO. Las medidas se escriben con error estándar si
no se proporciona ningún ARCHIVO

--todo-max=NUM
mantener como máximo NUM estados en las listas de tareas pendientes; esta opción solo es relevante para la amplitud
primera búsqueda, donde NUM es el número máximo de estados por nivel, y para la profundidad
primera búsqueda, donde NUM es la profundidad máxima

-t[NUM], --rastro[=NUM]
Escribe un rastro más corto para cada estado que se alcanza con una acción de NAMES de
opción --acción, es un interbloqueo detectado con --deadlock, o es una divergencia
detectado con --divergence a un archivo. No se escribirán más de NUM seguimientos. Si
No se proporciona NUM, el número de trazas es ilimitado. Para cada traza que se va a
escrito, se creará un archivo único con extensión .trc (seguimiento) que contiene un
traza más corta desde el estado inicial hasta el estado de interbloqueo. Las huellas pueden ser
bastante impreso y convertido a otros formatos usando tracepp.

-u, --datos-no utilizados
no elimine las partes no utilizadas de la especificación de datos

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 lps2lts en línea usando los servicios de onworks.net