Este es el comando maria 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
maria - Analizador de accesibilidad modular para redes de Petri de alto nivel
SINOPSIS
maria [opciones] archivos...
DESCRIPCIÓN
Esta página de manual documenta brevemente la maria mando. La documentación más completa es
disponible en formato GNU Info; vea abajo.
maria es un programa que analiza modelos de sistemas concurrentes, descritos en su entrada
lenguaje que se basa en redes del sistema algebraico. El formalismo fue presentado por Ekkart
Kindler y Hagen Völzer en ICATPN'98, Flexibilidad in Algebraico Nets.
Redes del sistema algebraico es un marco que no define ningún tipo de datos ni
operaciones. El sistema de tipos de datos y las operaciones en María están diseñados con alto nivel
lenguajes de programación y especificación en mente. A pesar de eso, cada modelo de María tiene un
despliegue finito.
Para garantizar la interoperabilidad con herramientas de red de Petri de bajo nivel, Maria traduce identificadores en
redes desplegadas a cadenas de caracteres alfanuméricos y guiones bajos. El filtro
nombrepliegue.pl se puede utilizar o adaptar para mejorar la legibilidad de los identificadores.
CAMPUS
María sigue la sintaxis habitual de la línea de comandos de GNU, con opciones largas que comienzan con dos
guiones (`-'). Un resumen de las opciones se incluye a continuación. Para obtener una descripción completa, consulte
los archivos de información.
-a límitar, --array-limit =límitar
Limite el tamaño de los tipos de índice de matriz a límitar valores posibles. Un límite de 0
desactiva los cheques.
-b modelo, --breadth-first-search =modelo
Genere el gráfico de accesibilidad de modelo utilizando la búsqueda en amplitud.
-C directorio, --compile =directorio
Generar código C en directorio para evaluar expresiones y para el nivel bajo
rutinas del algoritmo de análisis de la instancia de transición. Cuando se utiliza esta opción,
los errores de evaluación se informan de una manera ligeramente diferente. El interprete
muestra la valoración y expresión que causó el primer error en un estado; los
el código compilado muestra el número de errores. Por razones de rendimiento, el
El código generado no comprueba si hay errores de desbordamiento al agregar elementos a conjuntos múltiples.
-C, --no-compilar
Lo contrario a -C. Evalúe todas las expresiones en el intérprete integrado. Este es
el comportamiento predeterminado.
-D símbolo, --define =símbolo
Definir el símbolo del preprocesador símbolo.
-d modelo, --depth-first-search =modelo
Genere el gráfico de accesibilidad de modelo utilizando la búsqueda en profundidad.
-E intervalo, --edges =intervalo
Al generar el gráfico de accesibilidad, informe el tamaño del gráfico después de cada
intervalo bordes generados.
-e cadena, --execute =cadena
Implementación cadena.
-g archivo gráfico, --graph =archivo gráfico
Cargue un gráfico de accesibilidad generado previamente desde archivo gráfico.rgh.
-H h[,f[,t]], --hashes =h[,f[,t]]
Configure los parámetros para la verificación probabilística (-P). Asignar t universal
funciones hash de f elementos y tablas hash correspondientes de h bits cada uno. Ambos h
y f se redondeará a los siguientes valores adecuados.
- ?, -h, --ayuda
Imprima un resumen de las opciones de la línea de comandos para María y salga.
-I directorio, --include =directorio
Adjuntar directorio a la lista de directorios buscados para incluir archivos.
-i columnas, --width =columnas
Establezca el margen derecho de la salida en columnas. El valor predeterminado es 80.
-j en costes, --jobs = en costes
Al comprobar las propiedades de seguridad (opciones -L, -M y -P), use esta cantidad de trabajadores
procesos para acelerar el análisis en una computadora multiprocesador. Ver también -k y
-Z.
-k Puerto[/fortaleza], --connect =Puerto[/fortaleza]
Distribuir la verificación del modelo de seguridad (opciones -L, -M y -P) en una red TCP / IP. Para
el servidor, solo Puerto se especifica como un entero sin signo de 16 bits, normalmente entre
1024 y 65535. Para los procesos de trabajador, Puerto/fortaleza especifica el puerto y el
dirección del servidor. Ver también -j.
-L modelo, --lossless =modelo
Carga modelo y prepararse para analizarlo mediante la construcción de un conjunto de estados alcanzables
en archivos de disco. Ver también -M, -P, -j y -k.
-m modelo, --modelo =modelo
Carga modelo y borrar su gráfico de accesibilidad.
-M modelo, --md5-compactado =modelo
Carga modelo y prepararse para analizarlo construyendo una sobreaproximación de
conjunto de estados alcanzables en la memoria principal. Ver también -P, -L, -j y -k.
-N cregexp, --name =cregexp
Especifique los nombres permitidos en contexto c como la expresión regular extendida regexp.
El contexto se identifica por el primer carácter de la cadena de parámetros; los
los caracteres sucesivos constituyen la expresión regular que los nombres permitidos deben
partido.
-n cregexp, --no-name =cregexp
Especifique los nombres no permitidos en contexto c como la expresión regular extendida
regexp.
Si ambos -N y y -n se especifican para un contexto c, entonces la coincidencia de permiso toma
precedencia. Por ejemplo, para requerir que todos los nombres de tipo definidos por el usuario sean
terminado con _t, especificar -Nuevo Testamento -Nt'_t $ '. Las comillas en el último parámetro son
necesario para eliminar el significado especial de $ en el shell de la línea de comandos estás
probablemente usando para invocar a María.
-P modelo, --probabilístico =modelo
Carga modelo y prepararse para analizarlo mediante la construcción de un conjunto de estados alcanzables
en la memoria principal mediante el uso de una técnica llamada estado de bits Hashing.
-p comando, --property-translate =comando
Especifique el comando que se utilizará para traducir autómatas de propiedades. El comando debe
leer una fórmula de la entrada estándar y escribir un autómata correspondiente
descripción a la salida estándar. El traductor LBT es compatible con esto
.
-q límitar, --quantification-limit =límitar
Evitar la cuantificación (suma de conjuntos múltiples) de tipos que tienen más de límitar posible
valores. Un límite de 0 desactiva las comprobaciones.
-U símbolo, --undefine =símbolo
Eliminar la definición del símbolo del preprocesador símbolo.
-u [a][f[archivar]], --unfold =[a][f[archivar]]
Despliegue la red usando un algoritmo a y escríbelo en formato f a archivar. Si archivar
no se especifica, volcar la red desplegada a la salida estándar. Posibles formatos
en m (Maria (legible por humanos), predeterminado), l (LoLA), p (PEP) y r (PINCHAR). Allí
Hay dos algoritmos: tradicional (predeterminado) y reducido mediante la construcción de un envidiable
marcado (M).
-V, --versión
Imprime el número de versión de Maria y sal.
-v, --verboso
Muestra información detallada sobre las diferentes etapas del análisis.
-W, - advertencias
Habilite las advertencias sobre construcciones de red sospechosas. Este es el comportamiento predeterminado.
-w, --no-advertencias
Lo contrario a -W. Desactive todas las advertencias.
-x base de números, --radix =base de números
Especifique la base numérica para la salida de diagnóstico. Valores permitidos para base de números en
oct, octal, 8, hexagonal, hexadecimal, 16, dic, decimal y 10. El valor predeterminado es usar
numeros decimales.
-Y, --comprimir-oculto
Reducir el conjunto de estados alcanzables al no almacenar los estados sucesores de
instancias de transición para las cuales un ocultar la condición se mantiene. Los sucesores ocultos son
almacenado en un conjunto de estados separado. Esta opción puede ahorrar memoria (-L or -m) o reducir
la probabilidad de que se omitan estados (-M or -P), y puede mejorar la
eficiencia del análisis paralelo (-j or -k), pero también puede aumentar considerablemente
el requisito de tiempo del procesador. La opción también funciona con el modelo de vivacidad.
comprobación, pero no hay garantía de que los valores de verdad de las propiedades de vivacidad
permanece inalterable. Esta opción se puede combinar con -Z.
-y, --no-comprimir-oculto
Lo contrario a -Y. Este es el comportamiento predeterminado.
-Z, --comprimir-rutas
Reducir el conjunto de estados alcanzables al no almacenar estados intermedios que tienen en
la mayoría de un sucesor. Esta opción puede ahorrar memoria (-L or -m) o reducir el
probabilidad de que se omitan estados (-M or -P), y puede mejorar la eficiencia
de análisis paralelo (-j or -k), pero también puede aumentar considerablemente la
requisito de tiempo de procesador. La opción también funciona con la verificación del modelo de vida,
pero no hay garantía de que los valores de verdad de las propiedades de la vitalidad permanezcan
sin alterar. Esta opción se puede combinar con -Y.
-z, --no-comprimir-rutas
Lo contrario a -Z. Este es el comportamiento predeterminado.
Usa maria en línea usando los servicios de onworks.net
