lpsinvelm - En ligne dans le Cloud

PROGRAMME:

Nom

lpsinvelm - vérifie les invariants et utilise-les pour simplifier ou éliminer les sommations d'un LPS

SYNOPSIS

lpsinvelm [OPTION]... --invfile=INVFILE [DANS LE FICHIER [FICHIERS]]

DESCRIPTION

Vérifie si la formule booléenne (une expression de données mCRL2 de tri Bool) fournie comme
invariant est un invariant de la spécification de processus linéaire (LPS) dans INFILE. Si c'est
le cas, l'outil élimine toutes les sommations du LPS dont la condition viole la
invariant et écrit le résultat dans OUTFILE. Si INFILE est présent, stdin est utilisé. Si
OUTFILE n'est pas présent, stdout est utilisé.

L'outil peut également être utilisé pour simplifier les conditions des sommations du LPS donné.

OPTIONS

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

-y, --toutes-violations
ne se termine pas dès qu'une seule violation de l'invariant est trouvée, mais
signaler toutes les violations à la place

-c, --contre-exemple
afficher une évaluation indiquant pourquoi l'invariant pourrait éventuellement être violé s'il
est incertain si une sommation viole l'invariant

-o, --induction
appliquer l'induction sur les listes

-iFICHIER INV, --invariant=FICHIER INV
utilisez la formule booléenne (une expression de données mCRL2 de tri Bool) dans INVFILE comme
invariant

-n, --pas de vérification
ne pas vérifier si l'invariant tient avant d'éliminer les summands inaccessibles

-e, --pas d'élimination
n'éliminez pas ou ne simplifiez pas les sommations, mais ajoutez l'invariant à chaque condition

-pPRÉFIXE, --impression-point=PRÉFIXE
enregistrer un fichier .dot du BDD résultant s'il est impossible de déterminer si un
summand viole l'invariant ; PREFIX sera utilisé comme préfixe des fichiers de sortie

-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

-l, --simplifier-tout
simplifier les conditions de tous les summands, au lieu de simplement éliminer les summands
dont les conditions en conjonction avec l'invariant sont des contradictions

-zSOLVEUR, --smt-solveur=SOLVEUR
utilisez SOLVER pour supprimer les chemins incohérents des BDD utilisés en interne (par défaut,
aucune élimination de chemin n'est appliquée): 'cvc' le solveur SMT CVC3

-tLIMIT, --limite de temps=LIMIT
passer au plus LIMIT secondes à prouver une seule formule

--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 lpsinvelm en ligne en utilisant les services onworks.net