Il s'agit de la commande mcrl2i qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks à l'aide de 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
mcrl2i - Interprète pour le langage de données mCRL2
SYNOPSIS
mrcl2i [OPTION]... [DANS LE FICHIER]
DESCRIPTION
Évaluez les expressions de données mCRL2 via une interface textuelle. Si INFILE est présent et s'il
contient un LPS ou PBES, les types de données de cette spécification peuvent être utilisés. Si aucune entrée
est donné, seuls les types de données numériques standard sont disponibles. Stdin est ignoré.
les commandes suivantes sont disponibles pour manipuler les expressions de données mcrl2. Essentiellement, il
sont des commandes pour réécrire et taper des expressions, ainsi que pour générer les solutions pour un
Expression booléenne. Les expressions peuvent contenir des variables affectées ou non affectées. Noter
qu'il n'y a pas de limites sur le nombre d'étapes pour évaluer ou résoudre une expression, ni
le nombre de solutions borné. Par conséquent, les commandes assign, eval solve peuvent donner lieu à
boucles infinies.
h[elp] imprime ce message d'aide.
q[uit] quitter.
t[ype] EXPRESSION type d'impression d'EXPRESSION.
a[ssign] VAR=EXPRESSION évalue l'expression et l'affecte au
variable.
e[val] EXPRESSION réécrit EXPRESSION et imprime le résultat.
v[ar] VARLIST déclare des variables dans VARLIST.
r[ewriter] STRATEGY utilise STRATEGY pour la réécriture.
s[résoudre] VARLIST. EXPRESSION donne toutes les évaluations des variables dans
VARLIST qui satisfont à l'EXPRESSION. VARLIST est du
forme x,y,... : S ; ... v, w,... : T.
OPTIONS
OPTION peut être l'un des éléments suivants :
-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
Utiliser mcrl2i en ligne à l'aide des services onworks.net
