maria - En ligne dans le Cloud

PROGRAMME:

Nom

maria - Analyseur d'accessibilité modulaire pour réseaux de Petri de haut niveau

SYNOPSIS

maria [Options] fichiers

DESCRIPTION

Cette page de manuel documente brièvement les maria commander. Une documentation plus complète est
disponible au format GNU Info ; voir ci-dessous.

maria est un programme qui analyse les modèles de systèmes concurrents, décrit dans son entrée
langage basé sur les réseaux de systèmes algébriques. Le formalisme a été présenté par Ekkart
Kindler et Hagen Völzer à ICATPN'98, Flexibilité in Algébrique Nets.
Algebraic System Nets est un framework qui ne définit aucun type de données ou algébrique
opérations. Le système de type de données et les opérations dans Maria sont conçus avec des
langages de programmation et de spécification à l'esprit. Malgré cela, chaque modèle Maria a un
déroulement fini.
Pour assurer l'interopérabilité avec les outils de réseau de Petri de bas niveau, Maria traduit les identifiants en
des filets dépliés en chaînes de caractères alphanumériques et de traits de soulignement. Le filtre
nom de dossier.pl peuvent être utilisés ou adaptés pour améliorer la lisibilité des identifiants.

OPTIONS

Maria suit la syntaxe habituelle de la ligne de commande GNU, avec de longues options commençant par deux
tirets (`-'). Un résumé des options est inclus ci-dessous. Pour une description complète, voir
les fichiers d'informations.

-a limite, --array-limit=limite
Limiter la taille des types d'index de tableau à limite valeurs possibles. Une limite de 0
désactive les contrôles.

-b modèle, --breadth-first-search=modèle
Générer le graphique d'accessibilité de modèle en utilisant la recherche en largeur d'abord.

-C annuaire, --compiler=annuaire
Générer du code C dans annuaire pour évaluer les expressions et pour le bas niveau
routines de l'algorithme d'analyse d'instance de transition. Lorsque cette option est utilisée,
les erreurs d'évaluation sont signalées d'une manière légèrement différente. L'interprète
affiche l'évaluation et l'expression qui ont causé la première erreur dans un état ; les
le code compilé affiche le nombre d'erreurs. Pour des raisons de performances, le
le code généré ne vérifie pas les erreurs de débordement lors de l'ajout d'éléments à des ensembles multiples.

-c, --pas de compilation
L'opposé de -C. Évaluez toutes les expressions dans l'interpréteur intégré. C'est
le comportement par défaut.

-D symbole, --définir=symbole
Définir le symbole du préprocesseur symbole.

-d modèle, --profondeur-premier-recherche=modèle
Générer le graphique d'accessibilité de modèle en utilisant la recherche en profondeur d'abord.

-E intervalle, --bords=intervalle
Lors de la génération du graphique d'accessibilité, indiquez la taille du graphique après chaque
intervalle arêtes générées.

-e un magnifique, --exécuter=un magnifique
Exécution un magnifique.

-g fichier graphique, --graphe=fichier graphique
Chargez un graphique d'accessibilité généré précédemment à partir de fichier graphique.rgh.

-H h[,f[,t]], --hachages=h[,f[,t]]
Configurer les paramètres de vérification probabiliste (-P). Allouer t universel
fonctions de hachage de f éléments et tables de hachage correspondantes de h bits chacun. Les deux h
ainsi que f sera arrondi aux valeurs appropriées suivantes.

- ?, -h, --Aidez-moi
Imprimez un résumé des options de la ligne de commande à Maria et quittez.

-I annuaire, --include=annuaire
Ajouter annuaire à la liste des répertoires recherchés pour inclure les fichiers.

-i colonnes, --largeur=colonnes
Réglez la marge droite de la sortie sur colonnes. La valeur par défaut est 80.

-j les process, --emplois=les process
Lors de la vérification des propriétés de sécurité (options -L, -M ainsi que -P), utilisez ce nombre de travailleurs
processus pour accélérer l'analyse sur un ordinateur multiprocesseur. Voir également -k ainsi que
-Z.

-k port[/hôte], --connect=port[/hôte]
Distribuer la vérification du modèle de sécurité (options -L, -M ainsi que -P) dans un réseau TCP/IP. Pour
le serveur, seulement port est spécifié comme un entier non signé de 16 bits, généralement compris entre
1024 et 65535. Pour les processus de travail, port/hôte spécifie le port et le
adresse du serveur. Voir également -j.

-L modèle, --sans perte=modèle
Charge modèle et se préparer à l'analyser en construisant un ensemble d'états atteignables
dans les fichiers disque. Voir également -M, -P, -j ainsi que -k.

-m modèle, --modèle=modèle
Charge modèle et effacez son graphique d'accessibilité.

-M modèle, --md5-compacté=modèle
Charge modèle et se préparer à l'analyser en construisant une sur-approximation de
ensemble d'états accessibles dans la mémoire principale. Voir également -P, -L, -j ainsi que -k.

-N crégexp, --nom=crégexp
Spécifiez les noms autorisés dans le contexte c comme expression régulière étendue regexp.
Le contexte est identifié par le premier caractère de la chaîne de paramètres ; les
les caractères suivants constituent l'expression régulière que les noms autorisés doivent
correspondre.

-n crégexp, --sans-nom=crégexp
Spécifiez les noms non autorisés dans le contexte c comme expression régulière étendue
regexp.
Si les deux -N et et -n sont spécifiés pour un contexte c, alors la correspondance d'autorisation prend
priorité. Par exemple, pour exiger que tous les noms de type définis par l'utilisateur soient
terminé avec _t, Spécifiez -NT -Nt'_t$'. Les guillemets de ce dernier paramètre sont
nécessaire pour supprimer le sens spécial de $ dans le shell de ligne de commande, vous êtes
probablement utiliser pour invoquer Maria.

-P modèle, --probabiliste=modèle
Charge modèle et se préparer à l'analyser en construisant un ensemble d'états atteignables
dans la mémoire principale en utilisant une technique appelée état binaire Hachage.

-p commander, --propriété-traducteur=commander
Spécifiez la commande à utiliser pour traduire les automates de propriété. La commande doit
lire une formule à partir de l'entrée standard et écrire un automate correspondant
description à la sortie standard. Le traducteur lbt est compatible avec ça
option.

-q limite, --quantification-limite=limite
Empêcher la quantification (somme multi-ensembles) de types ayant plus de limite possible
valeurs. Une limite de 0 désactive les contrôles.

-U symbole, --undefine=symbole
Dédéfinir le symbole du préprocesseur symbole.

-u [a][f[fichier de sortie]], --déplier=[a][f[fichier de sortie]]
Dépliez le filet à l'aide d'un algorithme a et l'écrire au format f à fichier de sortie. Si fichier de sortie
n'est pas spécifié, videz le filet déplié vers la sortie standard. Formats possibles
m (Maria (lisible par l'homme), par défaut), l (LoLA), p (PEP), et r (PROD). Là
sont deux algorithmes : traditionnel (par défaut) et réduit en construisant un recouvrable
des (M).

-V, --version
Imprimez le numéro de version de Maria et quittez.

-dans, --verbeux
Affichez des informations détaillées sur les différentes étapes de l'analyse.

-W, --mises en garde
Activez les avertissements concernant les constructions de réseau suspectes. Ceci est le comportement par défaut.

-w, --pas d'avertissements
L'opposé de -W. Désactivez tous les avertissements.

-x base de nombres, --base=base de nombres
Spécifiez la base de nombres pour la sortie de diagnostic. Valeurs autorisées pour base de nombres
oct, octal, 8, hex, hexadécimal, 16, déc, décimal ainsi que 10. La valeur par défaut est d'utiliser
Nombres décimaux.

-O, --compress-caché
Réduire l'ensemble des états accessibles en ne stockant pas les états successeurs de
transitions instances pour lesquelles un cacher la condition tient. Les successeurs cachés sont
stocké dans un ensemble d'états distinct. Cette option peut économiser de la mémoire (-L or -m) ou réduire
la probabilité que des états soient omis (-M or -P), et cela peut améliorer la
efficacité de l'analyse parallèle (-j or -k), mais il peut aussi augmenter considérablement
le temps processeur requis. L'option fonctionne également avec le modèle de vivacité
vérification, mais il n'y a aucune garantie que les valeurs de vérité des propriétés de vivacité
restent inchangés. Cette option peut être combinée avec -Z.

-oui, --no-compress-caché
L'opposé de -Y. Ceci est le comportement par défaut.

-Z, --compress-chemins
Réduisez l'ensemble des états accessibles en ne stockant pas les états intermédiaires qui ont au
plus un successeur. Cette option peut économiser de la mémoire (-L or -m) ou réduire le
probabilité que des états soient omis (-M or -P), et cela peut améliorer l'efficacité
d'analyse parallèle (-j or -k), mais cela peut aussi augmenter considérablement la
temps processeur requis. L'option fonctionne également avec la vérification du modèle de vivacité,
mais il n'y a aucune garantie que les valeurs de vérité des propriétés de vivacité restent
inchangé. Cette option peut être combinée avec -Y.

-z, --pas de chemins de compression
L'opposé de -Z. Ceci est le comportement par défaut.

Utiliser maria en ligne en utilisant les services onworks.net