Problème outil Acme Studio

[AbirGuédria]

Bonjour,

Je suis étudiant et je fais mon PFE autour de la vérification formelle des contrats de qualité de service pour une composition de Services Web. Pour cela, j'utilise l'outil Acme Studio (qui est basé sur Eclipse).

Bref, j'ai un problème avec l'outil Acme Studio (ADL: Acme/Armani). En effet, je ne peux pas accéder à la valeur d'un attribut dans une propriété de type "record". De plus, je ne sais pas comment appliquer une contrainte sur la valeur de l'attribut par exemple:

Code :

1
2
3
4
5
6
Family Famil=
{
property type exp =record[nom:string; valeur:integer;];
//la règle à appliquer sur l'attribut valeur
invariant forall x: property in self.properties|declaresType(x,exp)-> (x.valeur<9);
}

Donc lorsque je fais une instance avec cette "Family" afin de vérifier si la contrainte fonctionne ou nn (car syntaxiquement ça ne provoque pas de problème), exemple:

Code :

1
2
3
4
5
import families/Famil.acme;
 
System Syst : Famil = new Famil extended with{
property y: exp= [nom=""; valeur=10;];
}

Donc normalement, dans ce cas il doit vérifier si ce système respecte la règle ou nn et si ce n'est pas cas, il faut qu'il indique que la règle n'est pas respectée.

Mon problème est qu'il ne voit pas la valeur de l'attribut et je ne sais pas comme vérifier ça.

Quelqu'un saurait-il m'expliquer comment résoudre ce problème ?

Merci d'avance pour votre aide.