Chemins d'acces : source /mnt/n7fs/etr2013/etr.sh
I Token-ring paramétré
Modélisation d'un système de token-ring à K sites. K sera un paramètre de la modélisation. On utilise ici l'anneau à jeton pour résoudre le problème de l'exclusion mutuelle. Chaque site est composé d'une station et d'un client. La station s'occupe de la circulation du jeton et d'offrir un service d'exclusion mutuelle à son client.
Le client i est régi par trois états:
- idle_i : Client i oisif
- wait_i : Client i en attente de la CS
- work_i : Client i en CS
Le jeton est régi par deux ensembles indexés d'états:
- token_i : Le jeton est disponible sur la station i
- after_i : Le jeton est en transit entre la station i et la station i+1
Pour permettre une modélisation paramétrée du problème, nous utilisons un programme auxilliaire pour générer le réseau de Petri correspondant. Le fichier ctk est un script tcl permettant de générer le réseau associé à une configuration à k sites. Pour générer un réseau à 4 sites faire
./exemples/ctk 4 > ctk4.net (ne pas oublier de rendre exécutable le script par la commande chmod +x).
- Générez un anneau à 4 sites. Chargez le sous nd et dessinez le avec neato
- Simulez le avec le stepper.
- Son comportement vous semble-t-il a priori correct ?
La solution proposée ne garantit pas l'absence de famine :
un client peut rester indéfiniment en attente (le service fourni par la station devrait assurer
qu'il travaillera au bout d'un temps fini). La solution proposée comporte deux erreurs
(une lecture attentive des invariants de transition doit vous mettre sur la piste pour
trouver les problèmes et les corriger).
- Analyse structurelle du réseau (onglet tools Structural analysis
- Donnez une interprétation aux invariants de place (P-Semiflows)
Quelles propriétés permettent-ils de déduire ?
- Donnez une interprétation aux invariants de transitions (T-Semiflows)
Quels types de comportement laissent-ils augurer ?
- Model-Checking
- Exprimez et vérifiez les propriétés d'exclusion mutuelle et d'absence de famine en LTL
- Exprimez et vérifiez les propriétés d'exclusion mutuelle et d'absence de famine en CTL
Proposez les modifications du réseau (du comportement de la station)
de facon à éliminer les comportements "pathologiques" révélés par l'analyse du réseau.
Pour mettre au point vos corrections, vous travaillerez directement sur la
forme graphique (ndr). Vous vous aiderez de la simulation et de l'analyse structurelle
pour valider vos corrections.
- Quelques extensions utiles pour obtenir une solution plus directe:
- Un arc inhibiteur permet d'interdire la sensibilisation d'une transition
si sa place d'entree est marquée (tracer un arc entre une place et une transition
et choisir l'option inhibitor)
- Il est possible de spécifier des priorités entre des transitions
(il suffit de tracer un arc entre deux transitions)
- Expérimentez ces extensions et utilisez les pour obtenir une variante
de la solution que vous aviez initialement proposée.
- Evaluez de nouveau sur le modèle corrigé les formules LTL et CTL
exprimamnt l'absence de famine et l'exclusion mutuelle.
- Regardez et simulez la solution proposée dans tk4.ndr
- Donnez une interprétation aux transitions t3 et t4 ainsi qu'aux places nbMax et frozen
- Proposez une version "équivalente" sans arc inhibiteur.
II Modélisation d'un système paramétré: le diner des philosophes
N philosophes sont assis autour d'une table ronde. Ils sont dans trois états
(pense, attente, dine). Chaque philosophe a besoin de
deux fourchettes pour manger, mais il n'y a qu'une
fourchette par assiette. Ainsi pour manger un philosophe doit prendre la fourchette se trouvant à sa gauche et la fourchette se trouvant à sa droite en deux étapes distinctes. Ainsi à tout moment deux philosophes qui sont l'un à coté de l'autre ne peuvent pas manger simultanément.
En vous inspirant du script fourni, modélisez le diner des
philosophes ; il faut bien sur faire disparaitre l'anneau mais on gardera
un esprit compositionnel en distinguant le comportement du philosophe
(qui ne changera pas durant tout l'exercice) et de son disciple en charge
d'aller chercher et rendre les fourchettes.
Vous simplifierez le problème en supposant que les N
disciples disposent d'un ensemble de N fourchettes banalisées dans
lequel peuvent piocher les deux fourchettes simultanément (V0),
ils piochent les fourchettes l'une après l'autre (V1), les fourchettes
sont individualisées et sont prises séquentiellement (V2).
Note: Pour les versions V0 et V1, on autorisera 2 philisophes
voisins à manger en même temps.
Pour chacune des versions:
- Ecrire le script associé.
- Analysez structurellement le réseau
- (Vous ne chercherez pas à garantir l'absence de famine)