Este es el comando pbes2bool 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
pbes2bool: genera un BES a partir de un PBES y resuélvelo.
SINOPSIS
pbes2bool [OPCIÓN] ... [EN ARCHIVO]
DESCRIPCIÓN
Resuelve (P) BES de INFILE. Si INFILE no está presente, se usa stdin.
OPCIONES
OPCIÓN puede ser cualquiera de los siguientes:
-c, --encimera
imprimir al final un árbol etiquetado con instanciaciones del lado izquierdo de
ecuaciones este árbol es una indicación de cómo pbes2bool llegó a la validez o
invalidez del PBES
-eNIVEL, --borrar=NIVEL
use remove level LEVEL para eliminar las variables bes 'none' no elimine las bes generadas
variables. Esto puede provocar un uso excesivo de la memoria. (predeterminado) 'algunos' eliminar
generado bes variables que no se utilizan, excepto si el lado derecho de su
la ecuación es verdadera o falsa. El rhss de las variables debe volver a calcularse, si
encontrado de nuevo, lo cual es bastante normal. 'all' elimina todas las variables bes que son
ya no se usa en ninguna ecuación. Esto es bastante eficiente en memoria, pero puede ser
requiere mucho tiempo, ya que el rhss de las variables bes eliminadas puede tener que ser
recalculado con bastante frecuencia.
-H, --tablas hash
use tablas hash al sustituir en ecuaciones bes, y traduzca internas
expresiones a diagramas de decisión binarios (desaconsejado, debido al rendimiento)
-iFORMATO, --en=FORMATO
use el formato de entrada FORMAT: 'pbes' PBES en formato interno 'pbes_text' PBES en
formato textual interno 'texto' PBES en formato textual (mCRL2) formato 'bes' BES en interno
formato 'bes_text' BES en formato textual interno 'cwi' BES en formato CWI 'pgsolver'
BES en formato PGSolver
-oFORMATO, --producción=FORMATO
utilizar formato de salida FORMAT (esta opción está obsoleta. Utilice la herramienta pbes2bes
en lugar).
-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
-zBUSCAR, --buscar=BUSCAR
utilizar la estrategia de búsqueda SEARCH: 'amplitud primero' Calcule el lado derecho de la
variables booleanas por orden de llegada. Esto es comparable con un
búsqueda en amplitud. Esto es bueno para generar contraejemplos. (defecto)
'profundidad primero' Calcula el lado derecho de una variable booleana donde la última
La variable generada se investiga primero. Esto corresponde a una profundidad primero
buscar. Esto puede superar sustancialmente la búsqueda en amplitud cuando la validez de
una fórmula se determina después de mayores profundidades. 'b' Mano corta para el ancho primero.
'd' Mano corta para la profundidad primero.
-sSTRAT, --estrategia=STRAT
usar la estrategia de sustitución STRAT: '0' Calcular todas las ecuaciones booleanas que se pueden
alcanzado desde el estado inicial, sin optimización. Esta es la mayor cantidad de datos
opción eficiente por ecuación generada. (predeterminado) '1' Optimizar inmediatamente
sustituyendo los lados derechos por variables ya investigadas que son verdaderas
o falso al generar una expresión. Esto es tan eficiente en memoria como 0. '2' En
Además de 1, también sustituya las variables que sean verdaderas o falsas en una
lado derecho generado. Esto puede significar que ciertas variables se vuelven inalcanzables
(por ejemplo, X0 en X0 y X1, cuando X1 se vuelve falso, asumiendo que X0 no ocurre en otro lugar.
Se mantendrán las variables que se han vuelto inalcanzables ya que estas no tienen
Para ser investigado. Dependiendo del PBES, esto puede reducir el tamaño del
generó BES sustancialmente pero requiere una mayor huella de memoria. '3 en
Además de 2, investigue las variables generadas si ocurren en un bucle,
de modo que se puedan establecer en verdadero o falso, según el símbolo de punto fijo.
Esto puede aumentar sustancialmente el tiempo necesario para generar una ecuación.
--tiempo[=ARCHIVO]
anexar medidas de tiempo a ARCHIVO. Las medidas se escriben con error estándar si
no se proporciona ningún ARCHIVO
-u, --datos_no_usados
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
Utilice pbes2bool en línea utilizando los servicios de onworks.net
