Este é o comando mona que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas múltiplas estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online de Windows ou emulador online de MAC OS.
PROGRAMA:
NOME
mona - um procedimento de decisão para as lógicas WS1S e WS2S
SINOPSE
mona [ opções ] arquivo mona
DESCRIÇÃO
MONA é uma ferramenta que traduz fórmulas nas lógicas WS1S ou WS2S em estado finito
autômatos representados por BDDs. As fórmulas podem expressar padrões de pesquisa, temporais
propriedades de sistemas reativos, restrições de árvore de análise, etc. MONA também analisa o
autômato resultante da compilação, e determina se a fórmula é válida e,
se a fórmula não for válida, gera um contraexemplo.
O projeto MONA é um projeto de pesquisa no Departamento de Ciência da Computação, Aarhus
Universidade.
A documentação completa, o código-fonte da GPL e os documentos de pesquisa relacionados estão disponíveis em
Página inicial do projeto MONA em http://www.brics.dk/mona
OPÇÕES
-w Produz o autômato inteiro. O padrão é gerar apenas seu tamanho.
-n Não analise o autômato. O padrão é analisar a validade e a insatisfatibilidade
e para gerar um exemplo e contra-exemplo satisfatórios.
-t Imprime o tempo decorrido para cada fase. Se -s também for usado, o tempo para cada autômato
operação também é impressa.
-s Imprimir estatísticas. Imprime informações para cada operação do autômato e um resumo.
-i Imprime autômatos intermediários (implica -s).
-d Despeja AST, tabela de símbolos e código DAG. Útil para depuração.
-q Silêncio, não imprima o progresso.
-e Habilita compilação separada. (Veja a variável de ambiente MONALIB abaixo.)
-oN Nível de otimização de código N (0=nenhum, 1=seguro, 2=heurística) (padrão 1).
-r Desativa a reordenação do índice BDD, usa a ordem da declaração como ordenação do índice. Padrão
é reordenar os índices BDD heuristicamente.
-f Força o estilo de saída normal do modo árvore. Aplicável apenas ao modo WSRT.
-m Emulação alternativa M2L-Str (estilo v1.3).
-h Habilita a análise de aceitação herdada.
-u Autômatos de saída irrestritos. Crie autômatos convencionais convertendo "não me importo"
estados para "rejeitar" estados e minimiza.
-gw Produz o autômato inteiro no formato Graphviz (implica -n -q). (Graphviz está disponível
at http://www.graphviz.org/)
-gs Produz uma árvore de exemplo satisfatória no formato Graphviz (implica -q).
-gc Árvore de contra-exemplo de saída no formato Graphviz (implica -q).
-gd Código de despejo DAG no formato Graphviz (implica -n -q).
-xw Produz o autômato inteiro em formato externo (implica -n -q). "Formato externo" é o
formato usado por dfalib e gtalib, consulte o pacote fonte.
MEIO AMBIENTE
MONÁLIB
Define a pasta usada para os autômatos de compilação separada (o padrão é o atual
diretório).
Use mona online usando serviços onworks.net
