help outils fourmel

salut.
en revisant le cours de OFD , je trouver du mal à comprendr  la diference entre les diferente type de machine B , je pense qu'il y'a une machine B evennemenetiel et autre normale , le probleme et que dans une probleme  elle nous a demandé de resoudre  avec ABMN malgres que le base de fonct(ionnement de systeme est du à des evennement.
ch pas si j'ai bien expliqué mais je trouve vraiment de probleme à comprendre :
-ce quoi BAMN
-quel diference avec B evennementiel
et surtout quand choisir B AMN ou B evennementiel pour resoudre le probleme
et merci d'avance

+1
quelqu un nous aide SVP
bon fel diapo il n ya que le B evennementiel, qui est il ce B AMN ?

une autre question : c'est quoi la "PLTL" pour la verification des preuve de vivacité et de sureté, et le rafinnement est inclus dans le chapitre à reviser pour cette matiere

apparamen juste nous les deux qui s interessent a l OFD ya guevara
bon pour PLTL tu le trouve dans ce diapo
http://www.partage-facile.com/125703-Cours_modelchecking.ppt.html

merci , ce que je compris des examen , lorsquelle nous donne une automate , alors on doit resoudre avec la B evennementiel , exatement le petit exercice dans la derniere seance( a_to_a ....events...) , mais si elle nous donne une explication de probleme alors on resoudre suivant ce qu'on a fait avec l'exemple de bariere de train( fonction=pre .... then......) et je pense que celle la est la B AMN (machine B normale).bon c'est une conclusion personnelle et peut etre elle fausse.
merci pour le doc.

En 1996, Jean-Raymond Abrial a proposé une extension de B, appelée B évenementiel, qui permet la spécification
de systèmes réactifs. Dans cette extension, les concepts de machine abstraite et d’opérations
sont respectivement remplacés par ceux de système abstrait et d’événements.

cad fel corps de B on trouve les oprations, mai le B evenementiel les opérations se sautent et on trouve les evenements.
http://www3.partage-facile.com/1027037-255.pdf.html

j'ai eu la chance d'avoir un tout petit RDV avec madame jemni:
-le cours est autorisé(malgres qu'il y'a des question de cours alors imaginez vous ces question)
-y'a pas de rafinement dans l'examen
-y'a pas de logique PLTL dans l'examen
-y'a pas des obligation  pour le B evennementiel , parcontre il existe pour BAMN
-on aura une indication sur le type de B  à choisir pour resoudre le probleme.

Un automate peut atre resoulu à traves le B evennemetiel ou le BAMN, si on choisi le B AMN alors on  peut faire le operation suivant le nombre d'etat , ( changer_etat_1,changer_etat_2,changer_etat_3)  , ou on peut resoudre avec B evennementiel , alors là tous le cas possible de changement inter-etat doit figurer(etat1_tot_eta2,etat1_tot_eta3,etat2_tot_eta3).

une petite resumé pour demain et inchaallah rabi m3ana.
bonne chance à tous

guevara a écrit:-le cours est autorisé(malgres qu'il y'a des question de cours alors imaginez vous ces question)
-y'a pas des obligation pour le B evennementiel , parcontre il existe pour BAMN
-on aura une indication sur le type de B à choisir pour resoudre le probleme.

oui guevara jé pa compri ces indication
et merci pr nous parager l information.

-y'a pas des obligation pour le B evennementiel , parcontre il existe pour BAMN --> les obligation des preuves existe dans tous les exam que j'ai fait , il y'a deux type des obligation , la premiere concerne la machine BAMN( [intialisation]invariant ,I et precondition => I apres action) , la deusieme pour la B evennementiel on n'a pas etudier


--on aura une indication sur le type de B à chois ==> c'est à dire elle va nous donner si on doit travailler avec BAMN ou B evennementiel.
bonne chance pour tous .

BAREKA ALLAHOU FIK
BONNE CHANCE PR DEMAIN

mdr on dirait que ya que nina et guivara qui ont eu cette option ^^

non , aujourdhui l'amphi B est plein , mais ils ont raison d'ignorer cette matiere , inchaallah rabi m3ana

rabi m3ana bisara7a
elli yasma3 doc autorisé y9oul malla jaww 3and hajme3a
allah elmosta3an, el7amdoulelleh