Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
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: