lpsconfcheck: en línea en la nube

PROGRAMA:

NOMBRE

lpsconfcheck - marca tau-sumandos confluentes de un LPS

SINOPSIS

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

DESCRIPCIÓN

Comprueba qué tau-sumandos del mCRL2 LPS en INFILE son confluentes, los marca cambiando el nombre
ellos en ctau, y escriba el resultado en OUTFILE. Si INFILE no está presente, se usa stdin. Si
OUTFILE no está presente, se utiliza stdout.

OPCIONES

OPCIÓN puede ser cualquiera de los siguientes:

-a, --Comprobar todo
comprobar la confluencia de los sumandos tau con respecto a todos los demás sumandos, en lugar de
continuar con el siguiente sumando tau tan pronto como se encuentre un sumando que sea
no confluente con el tau-summand actual

-c, --contraejemplo
mostrar una valoración para la que no se cumple la condición de confluencia, en caso de que
La condición encontrada no es una contradicción ni una tautología.

-g, --invariantes generados
tratar de demostrar que la condición de confluencia reducida es una invariante del LPS, en
caso de que la condición de confluencia no sea una tautología

-o, --inducción
aplicar inducción en listas

-iINVARCHIVO, --invariante=INVARCHIVO
use la fórmula booleana (una expresión de datos mCRL2 de tipo Bool) en INVFILE como
invariante

-n, --sin verificación
no verifique si el invariante se mantiene antes de verificar la confluencia

-m, --no marcar
no marque los sumandos tau confluentes; dado que no se han realizado cambios en el LPS,
no se escribe nada en OUTFILE

-pPREFIJO, --imprimir-punto=PREFIJO
guardar un archivo .dot del BDD resultante en caso de que no se puedan probar dos sumandos
confluente; PREFIX se utilizará como prefijo de los archivos de salida

-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

-zSOLUCIONADOR, --smt-solucionador=SOLUCIONADOR
use SOLVER para eliminar rutas inconsistentes de los BDD usados ​​internamente (por defecto,
no se aplica eliminación de ruta): 'cvc' el solucionador SMT CVC3

-sNUM, --resumir=NUM
eliminar o simplificar el sumando solo con el número NUM

-tLIMITE LAS, --límite de tiempo=LIMITE LAS
dedica como máximo LIMIT segundos a probar una sola fórmula

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