pbes2bool - En ligne dans le Cloud

PROGRAMME:

Nom

pbes2bool - Générez un BES à partir d'un PBES et résolvez-le.

SYNOPSIS

pbes2bool [OPTION]...[DANS LE FICHIER]

DESCRIPTION

Résout (P)BES de INFILE. Si INFILE n'est pas présent, stdin est utilisé.

OPTIONS

OPTION peut être l'un des éléments suivants :

-c, --contrer
imprimer à la fin un arbre étiqueté avec des instanciations du côté gauche de
équations; cet arbre est une indication de la façon dont pbes2bool est arrivé à la validité ou
invalidité du PBES

-eNIVEAU, --effacer=NIVEAU
utiliser supprimer le niveau LEVEL pour supprimer les variables bes 'aucun' ne pas supprimer les bes générés
variables. Cela peut entraîner une utilisation excessive de la mémoire. (par défaut) 'certains' supprimer
généré bes ​​variables qui ne sont pas utilisées, sauf si le côté droit de son
l'équation est vraie ou fausse. Le rhss des variables doit être recalculé, si
rencontré à nouveau, ce qui est tout à fait normal. 'all' supprime toutes les variables bes qui sont
n'est plus utilisé dans aucune équation. C'est assez économe en mémoire, mais cela peut être
beaucoup de temps car le rhss des variables bes supprimées peut devoir être
recalculé assez souvent.

-H, --tables de hachage
utiliser des tables de hachage lors de la substitution dans les équations bes et traduire interne
expressions aux diagrammes de décision binaires (déconseillé, en raison des performances)

-iFormat, --dans=Format
utiliser le format d'entrée FORMAT : 'pbes' PBES au format interne 'pbes_text' PBES dans
format textuel interne 'texte' PBES en format textuel (mCRL2) 'bes' BES en interne
format 'bes_text' BES au format textuel interne 'cwi' BES au format CWI 'pgsolver'
BES au format PGsolver

-oFormat, --output=Format
utiliser le format de sortie FORMAT (cette option est dépréciée. Utilisez l'outil pbes2bes
à la place).

-QNUM, --qlimite=NUM
limiter l'énumération des quantificateurs à NUM variables. (Par défaut NUM=1000, NUM=0 pour
illimité).

-rNom, --réscripteur=Nom
utiliser la stratégie de réécriture NOM : 'jitty' réécriture jitty (par défaut) 'jittyc' compilé
réécriture jitty 'jittyp' réécriture jitty avec prouveur

-zRechercher, --chercher=Rechercher
utiliser la stratégie de recherche RECHERCHE : "en largeur d'abord" Calculer le côté droit du
variables booléennes selon le principe du premier arrivé, premier servi. Ceci est comparable à un
recherche en largeur d'abord. C'est bon pour générer des contre-exemples. (défaut)
'profondeur d'abord' Calculer le côté droit d'une variable booléenne où la dernière
la variable générée est étudiée en premier. Cela correspond à une profondeur d'abord
chercher. Cela peut considérablement surpasser la recherche en largeur d'abord lorsque la validité de
une formule est déterminée après une plus grande profondeur. 'b' Abréviation pour la largeur d'abord.
'd' Main courte pour la profondeur d'abord.

-sSTRAT, --stratégie=STRAT
utiliser la stratégie de substitution STRAT : '0' Calculer toutes les équations booléennes qui peuvent être
atteint depuis l'état initial, sans optimisation. C'est le plus de données
option efficace par équation générée. (par défaut) '1' Optimiser immédiatement
substituer les membres de droite aux variables déjà étudiées qui sont vraies
ou false lors de la génération d'une expression. C'est aussi efficace en mémoire que 0. '2' dans
en plus de 1, remplacez également les variables qui sont vraies ou fausses dans un déjà
généré côté droit. Cela peut signifier que certaines variables deviennent inaccessibles
(par exemple X0 dans X0 et X1, lorsque X1 devient faux, en supposant que X0 ne se produit pas ailleurs.
Il sera maintenu quelles variables sont devenues inaccessibles car elles n'ont pas
à enquêter. Selon le PBES, cela peut réduire la taille du
généré BES substantiellement mais nécessite une plus grande empreinte mémoire. '3' dans
en plus de 2, rechercher les variables générées si elles se produisent sur une boucle,
de telle sorte qu'ils puissent être mis à vrai ou faux, selon le symbole de virgule fixe.
Cela peut augmenter considérablement le temps nécessaire pour générer une équation.

--horaires[=DOSSIER]
ajouter des mesures de synchronisation à FILE. Les mesures sont écrites avec l'erreur standard si
aucun FICHIER n'est fourni

-u, --unused_data
ne supprimez pas les parties inutilisées de la spécification des données

Options standards :

-q, --silencieux
ne pas afficher les messages d'avertissement

-v, --verbeux
afficher de courts messages intermédiaires

-d, --déboguer
afficher des messages intermédiaires détaillés

--niveau de journal=NIVEAU
afficher des messages intermédiaires jusqu'au niveau inclus

-h, --Aidez-moi
afficher les informations d'aide

--version
afficher les informations de version

Utilisez pbes2bool en ligne en utilisant les services onworks.net