Projet complet : demandes NKILItech

1. Le cahier des charges pédagogique

Le portail NKILItech reçoit initialement deux demandes et dispose d’un agent. Après traitement, chaque demande entre en contrôle ; l’agent est immédiatement libéré pour la suivante. Le contrôle décide soit de valider, soit de renvoyer la demande en attente. Aucune nouvelle demande, panne ou annulation n’est ajoutée pendant ce lot.

Le PDG, M. Joel Stephane Yankam Ngueguim, est présenté comme commanditaire de cette étude pédagogique. Les règles et chiffres du cas sont fictifs. On cherche à prouver que l’agent n’est pas dupliqué, qu’aucune demande n’est perdue et qu’une fin avec deux validations reste atteignable.

2. Définir les quatre événements

L’ordre des places est (Attente, Libre, En cours, Contrôle, Terminé), avec M₀ = (2,1,0,0,0). Après Commencer puis Soumettre : (1,1,0,1,0). À cet état, un nouveau Commencer est possible en même temps qu’un choix de contrôle ; Valider et Reprendre se disputent le même jeton Contrôle.

3. Manipuler le modèle

Le simulateur applique la règle Pre/Post du chapitre 2. Les boutons grisés correspondent aux transitions non franchissables. Le journal affiche chaque événement et le marquage obtenu ; Réinitialiser revient au lot initial. Les choix ne sont pas enregistrés et aucun service externe n’est appelé.

Sans JavaScript, les figures, les vecteurs et les corrections restent lisibles. Essayez d’abord Commencer, Soumettre, Valider deux fois de suite, puis une séquence contenant Reprendre. Observez que Reprendre renvoie une demande dans Attente sans créer un troisième dossier.

4. Vérifier le graphe et les invariants

L’exploration exhaustive produit 9 états et 14 arcs. Le seul marquage sans transition possible est (0,1,0,0,2) : deux demandes terminées et l’agent libre. Tous les autres états peuvent atteindre cette fin, comme le vérifie une recherche inverse depuis le sommet terminal.

Les invariants sont Libre + En cours = 1 et Attente + En cours + Contrôle + Terminé = 2. Ils bornent toutes les places, avec au plus un traitement engagé et au plus deux demandes dans une même étape de leur cycle. Le graphe ne comporte donc pas de blocage accidentel dans les hypothèses retenues.

5. Ce qui est possible n’est pas garanti

La séquence Commencer, Soumettre, Reprendre ramène de M₀ à M₀. Elle peut être répétée indéfiniment. Le fait qu’une fin soit accessible depuis chaque état ne prouve donc pas que toute exécution se termine. Pour garantir une terminaison, il faudrait notamment limiter les reprises ou définir et justifier une politique qui impose finalement la validation.

Pour remettre le projet, fournir l’énoncé des hypothèses, la liste ordonnée des places, les matrices Pre/Post, deux scénarios calculés, les invariants et le résultat d’exploration. Préciser les propriétés non étudiées : délais, identité des demandes, disponibilité réelle des personnes, priorité et arrivée de nouveaux dossiers.

Télécharger les neuf modèles, l’analyseur et les résultats vérifiés. Modifier ensuite une règle à la fois et comparer les états. Un résultat informatique ne porte que sur le modèle effectivement fourni.

Trois exercices corrigés