Il s'agit de la commande lps2pbes 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
lps2pbes - générer un PBES à partir d'un LPS et d'une formule d'état
SYNOPSIS
lps2pbes [OPTION]... --formula=FICHIER [DANS LE FICHIER [FICHIERS]]
DESCRIPTION
Convertir la formule d'état dans FILE et le LPS dans INFILE en un booléen paramétré
système d'équations (PBES) et enregistrez-le dans OUTFILE. Si OUTFILE n'est pas présent, stdout est utilisé.
Si INFILE n'est pas présent, stdin est utilisé.
OPTIONS
OPTION peut être l'un des éléments suivants :
-fDOSSIER, --formule=DOSSIER
utiliser la formule d'état de FILE
-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)
-s, --structuré
générer des équations telles qu'aucune conjonction mixte et disjonction ne se produise
-t, --chronométré
utiliser la version temporisée de l'algorithme, même pour les LPS non temporisés
--horaires[=DOSSIER]
ajouter des mesures de synchronisation à FILE. Les mesures sont écrites avec l'erreur standard si
aucun FICHIER n'est fourni
-u, --non optimisé
ne pas simplifier les expressions booléennes
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 lps2pbes en ligne en utilisant les services onworks.net
