Extension spécification : nouvelles variables pour les ports

[gzoumix]

Dans notre modèle, nous sommes confrontés à deux problèmes : l'arité provide des ports peut être infinie, et donc non exprimable par une variable dans les contraintes ; il est impossible de parler d'un composant en particulier. Cela a deux conséquences sur l'expressivité de nos spécifications :

• manipuler des variables qui mentionne l'arité provide d'un port est difficile dans les spécification
  • il est impossible de savoir combien de bindings aura un composant sur un port.

Pour ces raisons, Ralf propose les deux variables de ports suivantes :

• #@p = \sum_{t_p\in UP(p)}N(t_p) <- le nombre de composant providant p
  Cette variable est utilisable librement car elle ne mentionne pas l'arité de p
• NC(@p, t_p) = N(t_p) * U(t_p).P(p) - \sum_{t_r\in UR(p)} B(p,t_r,t_p) <- le nombre de connexion encore possibles sur p pour les composants de type t_p. Cette variable mentionne l'arité d'un port, et donc ne peut être présente que dans des contrainte de la forme
  NC(@p, t_p) op e où e ne mentionne pas de NC (comme cela, nous sommes sûr que e est fini).

Après un peu de réflexion de mon côté, on peut relaxer la contrainte en disant que NC ne peut apparaitre qu'une seule fois dans une contrainte de base (e op e'). L'encodage est seulement un peu pénible (mais pas plus que l'encodage proposé par ralf).