Il s'agit de la commande mona qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos nombreux postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
mona - une procédure de décision pour les logiques WS1S et WS2S
SYNOPSIS
mona [ Options ] fichier mona
DESCRIPTION
MONA est un outil qui traduit les formules des logiques WS1S ou WS2S en états finis
automates représentés par des BDD. Les formules peuvent exprimer des modèles de recherche, des fonctions temporelles
propriétés des systèmes réactifs, contraintes d'arbre d'analyse, etc. MONA analyse également les
automate résultant de la compilation, et détermine si la formule est valide et,
si la formule n'est pas valide, génère un contre-exemple.
Le projet MONA est un projet de recherche au Département d'informatique d'Aarhus
Université.
La documentation complète, le code source GPL et les documents de recherche associés sont disponibles sur le site
Page d'accueil du projet MONA à http://www.brics.dk/mona
OPTIONS
-w Affiche l'automate entier. Par défaut, seule sa taille est affichée.
-n Ne pas analyser l'automate. Par défaut, l'analyse porte sur la validité et l'insatisfaction.
et de générer un exemple et un contre-exemple satisfaisants.
-t Affiche le temps écoulé pour chaque phase. Si -s est également utilisé, le temps pour chaque automate est affiché.
l'opération est également imprimée.
-s Affiche les statistiques. Imprime des informations pour chaque opération de l'automate et un résumé.
-i Imprime les automates intermédiaires (implique -s).
-d Vidage de l'AST, de la table des symboles et du code DAG. Utile pour le débogage.
-q Silencieux, n'imprime pas la progression.
-e Activer la compilation séparée. (Voir la variable d'environnement MONALIB ci-dessous.)
-oN Niveau d'optimisation du code N (0=aucun, 1=sûr, 2=heuristique) (par défaut 1).
-r Désactiver la réorganisation de l'index BDD, utiliser l'ordre de déclaration comme ordre d'index. Par défaut
consiste à réorganiser les indices BDD de manière heuristique.
-f Force le style de sortie en mode arborescence normal. Applicable uniquement au mode WSRT.
-m Émulation alternative M2L-Str (style v1.3).
-h Activer l'analyse d'acceptation héritée.
-u Automates de sortie non restreints. Créer des automates conventionnels en convertissant les automates « sans importance ».
les États à « rejeter » les États et à minimiser.
-gw Affiche l'automate entier au format Graphviz (implique -n -q). (Graphviz est disponible
at http://www.graphviz.org/)
-gs Sortie d'un arbre d'exemple satisfaisant au format Graphviz (implique -q).
-gc Affiche l'arbre de contre-exemples au format Graphviz (implique -q).
-gd Vider le code DAG au format Graphviz (implique -n -q).
-xw Affiche l'automate entier au format externe (implique -n -q). « Format externe » est le
format utilisé par dfalib et gtalib, voir le paquet source.
ENVIRONNEMENT
MONALIB
Définit le répertoire utilisé pour les automates de compilation séparée (la valeur par défaut est current
annuaire).
Utiliser Mona en ligne avec les services onworks.net
