Este es el comando pbesrewr 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
pbesrewr - reescribe y simplifica un PBES
SINOPSIS
pbesrewr [OPCIÓN] ... [EN ARCHIVO [PERFIL]]
DESCRIPCIÓN
Reescriba el PBES en INFILE, elimine las variables cuantificadas y escriba el PBES resultante en
OUTFILE. Si INFILE no está presente, se usa stdin. Si OUTFILE no está presente, stdout es
usado.
OPCIONES
OPCIÓN puede ser cualquiera de los siguientes:
-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, --fuera=FORMATO
utilizar formato de salida FORMATO: 'pbes' PBES en formato interno 'pbes_text' PBES en
formato textual interno 'texto' PBES en formato textual (mCRL2)
-pNOMBRE, --pbes-reescritor=NOMBRE
use la estrategia de reescritura de pbes NOMBRE: 'simplificar' para simplificar (predeterminado)
'cuantificador-todo' para eliminar todos los cuantificadores 'cuantificador-finito' para
eliminar las variables cuantificadoras finitas 'cuantificador-un-punto' para la regla de un punto
eliminación del cuantificador 'pfnf' para reescribir en forma normal PFNF 'ppg' para
reescritura en el formulario de juego de paridad parametrizado 'bqnf-quantifier' para reescribir
cuantificadores sobre conjunciones a conjunciones de cuantificadores (experimental)
-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
--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 pbesrewr en línea utilizando los servicios de onworks.net
