maria - Online na nuvem

PROGRAMA:

NOME

maria - Analisador de acessibilidade modular para redes de Petri de alto nível

SINOPSE

maria [opções] arquivos...

DESCRIÇÃO

Esta página de manual documenta resumidamente o maria comando. A documentação mais completa é
disponível no formato GNU Info; Veja abaixo.

maria é um programa que analisa modelos de sistemas concorrentes, descritos em sua entrada
linguagem baseada em Redes de Sistemas Algébricos. O formalismo foi apresentado por Ekkart
Kindler e Hagen Völzer na ICATPN'98, Flexibilidade in Algébrico Nets.
Algebraic System Nets é uma estrutura que não define quaisquer tipos de dados ou
operações. O sistema de tipo de dados e as operações em Maria são projetados com alto nível
linguagens de programação e especificação em mente. Apesar disso, cada modelo Maria tem um
desdobramento finito.
Para garantir a interoperabilidade com ferramentas de rede de Petri de baixo nível, Maria traduz identificadores em
redes desdobradas em cadeias de caracteres alfanuméricos e sublinhados. O filtro
nome.pl pode ser usado ou adaptado para melhorar a legibilidade dos identificadores.

OPÇÕES

Maria segue a sintaxe de linha de comando GNU usual, com longas opções começando com dois
travessões (`-'). Um resumo das opções está incluído abaixo. Para uma descrição completa, veja
os arquivos de informação.

-a limitar, --array-limit =limitar
Limitar o tamanho dos tipos de índice de matriz a limitar valores possíveis. Um limite de 0
desabilita as verificações.

-b modelo, --breadth-first-search =modelo
Gere o gráfico de alcançabilidade de modelo usando a pesquisa em amplitude.

-C anuário, --compile =anuário
Gerar código C em anuário para avaliar expressões e para o baixo nível
rotinas do algoritmo de análise de instância de transição. Quando esta opção é usada,
os erros de avaliação são relatados de uma maneira ligeiramente diferente. O intérprete
exibe a valoração e a expressão que causou o primeiro erro em um estado; a
o código compilado exibe o número de erros. Por motivos de desempenho, o
o código gerado não verifica se há erros de estouro ao adicionar itens a conjuntos múltiplos.

-c, --sem compilar
O oposto de -C. Avalie todas as expressões no interpretador integrado. Isto é
o comportamento padrão.

-D símbolo, --define =símbolo
Defina o símbolo do pré-processador símbolo.

-d modelo, --depth-first-search =modelo
Gere o gráfico de alcançabilidade de modelo usando pesquisa em profundidade.

-E intervalo, --edges =intervalo
Ao gerar o gráfico de alcançabilidade, relate o tamanho do gráfico após cada
intervalo bordas geradas.

-e corda, --execute =corda
Execute corda.

-g arquivo gráfico, --graph =arquivo gráfico
Carregue um gráfico de acessibilidade gerado anteriormente a partir de arquivo gráfico.rgh.

-H h[,f[,t]], --hashes =h[,f[,t]]
Configure os parâmetros para verificação probabilística (-P) distribuir t universal
funções hash de f elementos e tabelas de hash correspondentes de h bits cada. Ambos h
e f será arredondado para os próximos valores adequados.

- ?, -h, --Socorro
Imprima um resumo das opções de linha de comando para Maria e saia.

-I anuário, --include =anuário
Acrescentar anuário à lista de diretórios pesquisados ​​para incluir arquivos.

-i colunas, --width =colunas
Defina a margem direita da saída para colunas. O padrão é 80.

-j processos, --jobs =processos
Ao verificar as propriedades de segurança (opções -L, -M e -P), use tantos trabalhadores
processos para acelerar a análise em um computador multiprocessador. Veja também -k e
-Z.

-k porta[/hospedeiro], --connect =porta[/hospedeiro]
Distribuir a verificação do modelo de segurança (opções -L, -M e -P) em uma rede TCP / IP. Para
o servidor, apenas porta é especificado como um inteiro não assinado de 16 bits, geralmente entre
1024 e 65535. Para os processos de trabalho, porta/hospedeiro especifica a porta e o
endereço do servidor. Veja também -j.

-L modelo, --lossless =modelo
Ver modelo e se preparar para analisá-lo, construindo um conjunto de estados alcançáveis
em arquivos de disco. Veja também -M, -P, -j e -k.

-m modelo, --model =modelo
Ver modelo e limpar seu gráfico de acessibilidade.

-M modelo, --md5-compacted =modelo
Ver modelo e se preparar para analisá-lo, construindo uma superproximação de
conjunto de estados alcançáveis ​​na memória principal. Veja também -P, -L, -j e -k.

-N cregexp, --name =cregexp
Especifique os nomes permitidos no contexto c como a expressão regular estendida regexp.
O contexto é identificado pelo primeiro caractere da string de parâmetro; a
os caracteres seguintes constituem a expressão regular que os nomes permitidos devem
partida.

-n cregexp, --no-name =cregexp
Especifique os nomes não permitidos no contexto c como a expressão regular estendida
regexp.
Se ambos -N e e -n são especificados para um contexto c, então a partida de permissão leva
precedência. Por exemplo, para exigir que todos os nomes de tipo definidos pelo usuário sejam
terminado com _t, especificamos -nt -Nt'_t $ '. As aspas no último parâmetro são
necessário para remover o significado especial de $ no shell da linha de comando você está
provavelmente usando para invocar Maria.

-P modelo, --probabilistic =modelo
Ver modelo e se preparar para analisá-lo, construindo um conjunto de estados alcançáveis
na memória principal usando uma técnica chamada estado de bits Hashing.

-p comando, --property-Translator =comando
Especifique o comando a ser usado para traduzir autômatos de propriedade. O comando deve
leia uma fórmula da entrada padrão e escreva um autômato correspondente
descrição para a saída padrão. O tradutor lb é compatível com isso
opção.

-q limitar, --quantification-limit =limitar
Impedir a quantificação (soma de vários conjuntos) de tipos com mais de limitar possível
valores. Um limite de 0 desativa as verificações.

-U símbolo, --undefine =símbolo
Indefina o símbolo do pré-processador símbolo.

-u [a][f[arquivo de saída]], --unfold =[a][f[arquivo de saída]]
Desdobre a rede usando um algoritmo a e escrever no formato f para arquivo de saída. Se arquivo de saída
não for especificado, despeje a rede desdobrada na saída padrão. Formatos possíveis
e guarante que os mesmos estão m (Maria (legível), padrão), l (LoLA), p (PEP), e r (PROD). Lá
são dois algoritmos: tradicional (padrão) e reduzido pela construção de um coberto
marca��o (M).

-V, --versão
Imprima o número da versão de Maria e saia.

-dentro, --verbose
Exibe informações detalhadas sobre os diferentes estágios da análise.

-C, - advertências
Habilite avisos sobre construções de rede suspeitas. Este é o comportamento padrão.

-C, --sem avisos
O oposto de -W. Desative todos os avisos.

-x base numérica, --radix =base numérica
Especifique a base numérica para saída de diagnóstico. Valores permitidos para base numérica e guarante que os mesmos estão
outubro, octal, 8, feitiço, hexadecimal, 16, dezembro, decimal e 10. O padrão é usar
números decimais.

-Sim, --comprimir-oculto
Reduza o conjunto de estados alcançáveis, não armazenando os estados sucessores de
instâncias de transição para as quais um esconder condição é mantida. Os sucessores ocultos são
armazenados em um conjunto de estados separado. Esta opção pode economizar memória (-L or -m) ou reduzir
a probabilidade de que os estados sejam omitidos (-M or -P), e pode melhorar o
eficiência da análise paralela (-j or -k), mas também pode aumentar consideravelmente
o requisito de tempo do processador. A opção também funciona com modelo de vivacidade
verificação, mas não há garantia de que os valores verdadeiros das propriedades de vivacidade
permanece inalterado. Esta opção pode ser combinada com -Z.

- sim, --sem compressão oculta
O oposto de -Y. Este é o comportamento padrão.

-Z, --compress-path
Reduza o conjunto de estados alcançáveis, não armazenando estados intermediários que têm
mais um sucessor. Esta opção pode economizar memória (-L or -m) ou reduzir o
probabilidade de que os estados sejam omitidos (-M or -P), e pode melhorar a eficiência
de análise paralela (-j or -k), mas também pode aumentar consideravelmente o
requisito de tempo do processador. A opção também funciona com verificação de modelo de atividade,
mas não há garantia de que os valores verdadeiros das propriedades de vivacidade permaneçam
inalterado. Esta opção pode ser combinada com -Y.

-z, --no-compress-path
O oposto de -Z. Este é o comportamento padrão.

Use maria online usando serviços onworks.net