Il s'agit de la commande pbesrewr qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples 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
pbesrewr - réécrire et simplifier un PBES
SYNOPSIS
pbesrewr [OPTION]... [DANS LE FICHIER [FICHIERS]]
DESCRIPTION
Réécrivez le PBES dans INFILE, supprimez les variables quantifiées et écrivez le PBES résultant dans
SORTIE. Si INFILE n'est pas présent, stdin est utilisé. Si OUTFILE n'est pas présent, stdout est
utilisé.
OPTIONS
OPTION peut être l'un des éléments suivants :
-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, --dehors=Format
utiliser le format de sortie FORMAT : 'pbes' PBES au format interne 'pbes_text' PBES dans
format textuel interne 'texte' PBES au format textuel (mCRL2)
-pNom, --pbes-réécrivain=Nom
utiliser la stratégie de réécriture pbes NAME : 'simplify' pour la simplification (par défaut)
'quantifier-all' pour éliminer tous les quantificateurs 'quantifier-finite' pour
élimination des variables de quantification finies 'quantifier-un-point' pour une règle à un point
élimination du quantificateur 'pfnf' pour la réécriture en PFNF forme normale 'ppg' pour
réécriture dans le formulaire de jeu de parité paramétré 'bqnf-quantifier' pour la réécriture
quantificateurs sur conjonctions à conjonctions de quantificateurs (expérimental)
-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
--horaires[=DOSSIER]
ajouter des mesures de synchronisation à FILE. Les mesures sont écrites avec l'erreur standard si
aucun FICHIER n'est fourni
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 pbesrewr en ligne en utilisant les services onworks.net
