Este es el comando spadesimp 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
spadesimp: simplifica las condiciones de verificación de SPARK
SINOPSIS
diablillo [OPCIONES] [UNIDAD]
DESCRIPCIÓN
El simplificador de SPARK, diablillo, analiza las condiciones de verificación generadas por el
Examina SPARK e intenta descargarlos automáticamente. Para cada archivo vcg leído,
el Simplificador producirá un archivo siv (vcs simplificado) y un slg (simplificador
archivo de registro.
Esta página de manual solo resume el diablillo banderas de la línea de comandos, consulte la
el manual completo del Simplificador para obtener más información.
OPCIONES
Estas opciones no siguen la sintaxis habitual de la línea de comandos de GNU, ya que las opciones comienzan con
un solo guión en lugar de los dos habituales.
-ayuda Muestra la ayuda de la línea de comandos.
-versión
Muestra información sobre la versión.
-nolog No genere un archivo de registro de simplificación.
-log =especificación_archivo
Especifique el nombre de archivo para el archivo de registro de simplificación.
-nieve
No ajuste de línea los archivos de salida.
-verboso
Muestre las estrategias de simplificación intentadas.
-nouserreglas
No use reglas de usuario.
-llanura Adopte un estilo de salida simple (por ejemplo, sin fechas ni números de versión).
-comprobación de tipo
Solo compruebe los archivos de entrada.
-noreno
No vuelva a numerar hipótesis y conclusiones en archivos siv.
-nosimplification =RANGOS, -nostandardización =RANGOS, -norule_substitution =RANGOS,
-nocontradiction_hunt =RANGOS, -nosubstitution_elimination =RANGOS,
-noexpression_reduction =RANGOS
Ajuste la estrategia para diferentes VC. RANGOS puede ser una lista de rangos separados por comas.
Cada rango puede ser un solo número de VC o un rango simple de la forma VC-VC.
-complexity_limit =LIMITE LAS
(Límite en rango 10 .. 200)
-depth_limit =LIMITE LAS
(Límite en rango 1 .. 10)
-inference_limit =LIMITE LAS
(Límite en rango 10 .. 400)
Use spadesimp en línea usando los servicios de onworks.net
