Attention, il y a par ex.. des fautes de syntaxe en B.
Spécifier en B puis en Event-B ce texte : «Le baron Warseberg, malgré qu’il entretenait la demoiselle Laforest voyait encore les filles de la Varenne. Il puisa dans le flanc de Mlle Dorville ce poison destructeur, qu’il procura à Mlle Laforest, qui de son côté en fit présent à M. Saimson, mousquetaire, avec qui elle greluchonait, lequelle par la même voie en fit cadeau à Mlle Ricourt, de la Comédie Italienne, qui, sans façon la voitura à M. de la Ferté, intendant des Menus Plaisirs, qui en gratifia Mlle Rozetti, qui, de même, me la souffla… »
Réflexion d'une durée de 54 s
Voici la spécification formelle du texte que tu as fourni, modélisée comme un système de transmission d’un jeton « poison destructeur » le long d’une chaîne linéaire exacte de personnes (fidèle à la narration : le poison est « puisé », « procuré », « fait présent », « cadeau », « voiture », « gratifié » et « soufflé »).Les relations secondaires (« entretenait la demoiselle Laforest », « voyait encore les filles de la Varenne », « greluchonait ») sont mentionnées en commentaire mais non modélisées car elles n’interviennent pas dans la transmission du poison.1. Spécification en B classique (syntaxe Atelier B)
b
MACHINE TransmissionPoisonSETSPERSONNES = {Dorville, Warseberg, Laforest, Saimson, Ricourt, LaFerte, Rozetti, Narrator}VARIABLEScurrent_holderINVARIANTcurrent_holder ∈ PERSONNESINITIALISATIONcurrent_holder := DorvilleOPERATIONSdonner_a_Warseberg =PREcurrent_holder = DorvilleTHENcurrent_holder := WarsebergEND;donner_a_Laforest =PREcurrent_holder = WarsebergTHENcurrent_holder := LaforestEND;donner_a_Saimson =PREcurrent_holder = LaforestTHENcurrent_holder := SaimsonEND;donner_a_Ricourt =PREcurrent_holder = SaimsonTHENcurrent_holder := RicourtEND;donner_a_LaFerte =PREcurrent_holder = RicourtTHENcurrent_holder := LaFerteEND;donner_a_Rozetti =PREcurrent_holder = LaFerteTHENcurrent_holder := RozettiEND;donner_a_Narrator =PREcurrent_holder = RozettiTHENcurrent_holder := NarratorENDEND
Comportement : Pour raconter l’histoire, on appelle les opérations dans l’ordre exact. Si on appelle une opération hors séquence, la précondition échoue → erreur.2. Spécification en Event-B (syntaxe Rodin)
eventb
MACHINE TransmissionPoisonVARIABLEScurrent_holderINVARIANTcurrent_holder ∈ PERSONNESEVENTSdonner_a_WarsebergWHENcurrent_holder = DorvilleTHENcurrent_holder := WarsebergENDdonner_a_LaforestWHENcurrent_holder = WarsebergTHENcurrent_holder := LaforestENDdonner_a_SaimsonWHENcurrent_holder = LaforestTHENcurrent_holder := SaimsonENDdonner_a_RicourtWHENcurrent_holder = SaimsonTHENcurrent_holder := RicourtENDdonner_a_LaFerteWHENcurrent_holder = RicourtTHENcurrent_holder := LaFerteENDdonner_a_RozettiWHENcurrent_holder = LaFerteTHENcurrent_holder := RozettiENDdonner_a_NarratorWHENcurrent_holder = RozettiTHENcurrent_holder := NarratorENDEND
Comportement : Il n’y a plus d’appel. Chaque événement est réactif : dès que sa garde est vraie, il peut se déclencher. Les gardes forcent ici l’ordre chronologique du texte, mais le modèle reste ouvert au nondéterminisme ou au raffinement (ex. : plusieurs partenaires possibles en parallèle).Différence essentielle (comme pour la porte)
B classique : séquentiel, commandes explicites (on « exécute » l’histoire).
Event-B : réactif, événements activés par conditions (le système « vit » l’histoire).
Tu veux que je te fournisse :
les fichiers prêts à importer (.mch pour Atelier B / .eventb pour Rodin) ?
un raffinement (ajout des relations amoureuses, version cumulative où tous restent porteurs, etc.) ?
ou une version avec phases + invariants plus riches (comme pour la piscine) ?
Dis-le-moi
et je te le génère tout de suite !
Raffiner avec relations amoureuses
Modéliser greluchonage en B
Modéliser greluchonage en B
Réflexion d'une durée de 44 s
Voici une modélisation formelle en B classique (syntaxe Atelier B / ClearSy) du concept de « greluchonage ».Dans le texte historique, « greluchonait » désigne une liaison intime / amoureuse (relation sexuelle ou sentimentale occasionnelle) entre deux personnes, qui sert de canal de transmission du « poison destructeur ». Le greluchonage est donc modélisé comme une relation binaire symétrique (mutuelle) entre personnes, avec :
initialisation du seul couple explicitement mentionné dans le texte,
opérations pour établir/rompre une liaison,
vérification d’existence (utile pour conditionner une transmission du poison).
b
MACHINE GreluchonageSETSPERSONNES = {Dorville,Warseberg,Laforest,Saimson,Ricourt,LaFerte,Rozetti,Narrator}VARIABLESliaisons_greluchon /* ensemble des paires en greluchonage */INVARIANTliaisons_greluchon ⊆ PERSONNES ↔ PERSONNESliaisons_greluchon = liaisons_greluchon~ /* symétrie (mutuel) *//* Pas d'auto-liaison */∀p·p ∈ PERSONNES ⇒ {p ↔ p} ∩ liaisons_greluchon = ∅INITIALISATIONliaisons_greluchon := {Laforest ↔ Saimson} /* couple explicitement cité */OPERATIONS/* Établir une nouvelle liaison (ex. : Warseberg et Laforest, etc.) */etablir_greluchonage(p1, p2) =PREp1 ∈ PERSONNES ∧p2 ∈ PERSONNES ∧p1 ≠ p2 ∧{p1 ↔ p2} ∩ liaisons_greluchon = ∅THENliaisons_greluchon := liaisons_greluchon ∪ {p1 ↔ p2, p2 ↔ p1}END;/* Rompre une liaison */rompre_greluchonage(p1, p2) =PREp1 ∈ PERSONNES ∧p2 ∈ PERSONNES ∧{p1 ↔ p2} ⊆ liaisons_greluchonTHENliaisons_greluchon := liaisons_greluchon \ {p1 ↔ p2, p2 ↔ p1}END;/* Vérifier si deux personnes sont en greluchonage (utile pour transmission) */est_en_greluchonage(p1, p2) =PREp1 ∈ PERSONNES ∧ p2 ∈ PERSONNESTHENIF {p1 ↔ p2} ⊆ liaisons_greluchonTHENskip /* ou RETURN TRUE dans un contexte plus complet */ELSEskip /* ou RETURN FALSE */ENDENDEND
Intégration possible avec la transmission du poison (extension recommandée)On peut très facilement ajouter cette machine en SEES à la machine TransmissionPoison précédente et modifier chaque opération donner_à_XXX pour ajouter la garde :
b
PREcurrent_holder = Laforest ∧{Laforest ↔ Saimson} ⊆ liaisons_greluchon /* greluchonage obligatoire */
Cela force formellement que le « cadeau » du poison ne puisse se faire que via une liaison greluchonage – exactement ce que décrit le texte.Tu veux :
la version Event-B de cette modélisation (avec événements réactifs) ?
l’extension complète de TransmissionPoison avec le greluchonage intégré (gardes sur chaque donner) ?
ou un raffinement (ex. : greluchonage avec durée, secret, etc.) ?
Dis-moi
et je te fournis le fichier prêt à importer immédiatement !
Intégrer greluchonage à TransmissionPoison
Modéliser autres relations amoureuses
Articles
