Este es el comando lpsinvelm 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
lpsinvelm: verifique los invariantes y utilícelos para simplificar o eliminar los sumandos de un LPS
SINOPSIS
lpsinvelm [OPCIÓN] ... --invfile = INVFILE [EN ARCHIVO [PERFIL]]
DESCRIPCIÓN
Comprueba si la fórmula booleana (una expresión de datos mCRL2 de tipo Bool) proporcionada como
invariante es un invariante de la especificación de proceso lineal (LPS) en INFILE. Si esto es
caso, la herramienta elimina todos los sumandos del SPCR cuya condición viole la
invariante y escribe el resultado en OUTFILE. Si INFILE está presente, se usa stdin. Si
OUTFILE no está presente, se utiliza stdout.
La herramienta también se puede utilizar para simplificar las condiciones de los sumandos del LPS dado.
CAMPUS
OPCIÓN puede ser cualquiera de los siguientes:
-y, --todas las violaciones
no terminan tan pronto como se encuentra una sola violación del invariante, pero
informe todas las infracciones en su lugar
-c, --contraejemplo
mostrar una valoración que indique por qué la invariante podría posiblemente ser violada si
es incierto si un sumando viola la invariante
-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 eliminar los sumandos inalcanzables
-e, --no eliminación
no elimine ni simplifique los sumandos, pero agregue el invariante a cada condición
-pPREFIJO, --imprimir-punto=PREFIJO
guardar un archivo .dot del BDD resultante si es imposible determinar si un
summand viola el invariante; 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
-l, --simplificar-todo
simplificar las condiciones de todos los sumandos, en lugar de simplemente eliminar los sumandos
cuyas condiciones en conjunción con el invariante son contradicciones
-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
-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 lpsinvelm en línea utilizando los servicios de onworks.net
