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 TransmissionPoison
SETS
PERSONNES = {Dorville, Warseberg, Laforest, Saimson, Ricourt, LaFerte, Rozetti, Narrator}
VARIABLES
current_holder
INVARIANT
current_holder ∈ PERSONNES
INITIALISATION
current_holder := Dorville
OPERATIONS
donner_a_Warseberg =
PRE
current_holder = Dorville
THEN
current_holder := Warseberg
END;
donner_a_Laforest =
PRE
current_holder = Warseberg
THEN
current_holder := Laforest
END;
donner_a_Saimson =
PRE
current_holder = Laforest
THEN
current_holder := Saimson
END;
donner_a_Ricourt =
PRE
current_holder = Saimson
THEN
current_holder := Ricourt
END;
donner_a_LaFerte =
PRE
current_holder = Ricourt
THEN
current_holder := LaFerte
END;
donner_a_Rozetti =
PRE
current_holder = LaFerte
THEN
current_holder := Rozetti
END;
donner_a_Narrator =
PRE
current_holder = Rozetti
THEN
current_holder := Narrator
END
END
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 TransmissionPoison
VARIABLES
current_holder
INVARIANT
current_holder ∈ PERSONNES
EVENTS
donner_a_Warseberg
WHEN
current_holder = Dorville
THEN
current_holder := Warseberg
END
donner_a_Laforest
WHEN
current_holder = Warseberg
THEN
current_holder := Laforest
END
donner_a_Saimson
WHEN
current_holder = Laforest
THEN
current_holder := Saimson
END
donner_a_Ricourt
WHEN
current_holder = Saimson
THEN
current_holder := Ricourt
END
donner_a_LaFerte
WHEN
current_holder = Ricourt
THEN
current_holder := LaFerte
END
donner_a_Rozetti
WHEN
current_holder = LaFerte
THEN
current_holder := Rozetti
END
donner_a_Narrator
WHEN
current_holder = Rozetti
THEN
current_holder := Narrator
END
END
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 Greluchonage
SETS
PERSONNES = {
Dorville,
Warseberg,
Laforest,
Saimson,
Ricourt,
LaFerte,
Rozetti,
Narrator
}
VARIABLES
liaisons_greluchon /* ensemble des paires en greluchonage */
INVARIANT
liaisons_greluchon ⊆ PERSONNES ↔ PERSONNES
liaisons_greluchon = liaisons_greluchon~ /* symétrie (mutuel) */
/* Pas d'auto-liaison */
∀p·p ∈ PERSONNES ⇒ {p ↔ p} ∩ liaisons_greluchon = ∅
INITIALISATION
liaisons_greluchon := {Laforest ↔ Saimson} /* couple explicitement cité */
OPERATIONS
/* Établir une nouvelle liaison (ex. : Warseberg et Laforest, etc.) */
etablir_greluchonage(p1, p2) =
PRE
p1 ∈ PERSONNES ∧
p2 ∈ PERSONNES ∧
p1 ≠ p2 ∧
{p1 ↔ p2} ∩ liaisons_greluchon = ∅
THEN
liaisons_greluchon := liaisons_greluchon ∪ {p1 ↔ p2, p2 ↔ p1}
END;
/* Rompre une liaison */
rompre_greluchonage(p1, p2) =
PRE
p1 ∈ PERSONNES ∧
p2 ∈ PERSONNES ∧
{p1 ↔ p2} ⊆ liaisons_greluchon
THEN
liaisons_greluchon := liaisons_greluchon \ {p1 ↔ p2, p2 ↔ p1}
END;
/* Vérifier si deux personnes sont en greluchonage (utile pour transmission) */
est_en_greluchonage(p1, p2) =
PRE
p1 ∈ PERSONNES ∧ p2 ∈ PERSONNES
THEN
IF {p1 ↔ p2} ⊆ liaisons_greluchon
THEN
skip /* ou RETURN TRUE dans un contexte plus complet */
ELSE
skip /* ou RETURN FALSE */
END
END
END
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
PRE
current_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
