********** Question 1 ********** Le modele 11 semble a peu pres valide; la presence de deadlock n'est pas etonante : elle correspond au crash du systeme (lorsque l'echangeur thermique passe dans l'etat KO par la transition BOOM). L'etat KO (le seul blocage) est un etat a part entiere : la transition e doit etre rajoutee a cet etat (KO |- e -> KO). Un detail important : l'operateur peut agir n'importe quand et n'importe comment. Par exemple, il peut tres bien fermer la vanne V5 avant meme d'inhiber AP. Le resultat obtenu est : Syst. Trans. | hno3_v11 |Syst. Synchro. |------------Etats--------------:----------Transitions----------| Vanne1 |* 320:* 3728|hno3_v11 EchangeurThermique |initial 1:boucle 3664|hno3_v12 CapteurTemperature |dead 0:boucleinitial 3040| ControleurTemperature |deadlock 0: | AirComprime |pbModifTemp 0: | Vanne5 |pbBOOM 0: | EauPrincipale |pbPlusAir 0: | EauSecondaire |pbMoinsAir 0: | Pompe |pbFermerV1 0: | IndicateurTemperature |pbFermerV5 0: | ControleurPannePompe |pbOuvrirV1 0: | OperateurV1 |pbOuvrirV5 0: | OperateurV2 |pbActiverAP 0: | hno3_v11 |pbInhiberAP 0: | Dans le systeme de synchronisation, les transitions plusEau ne sont pas defini dans les composantes EauPrincipal (MP) et EauSecondaire (ES) du systeme de transition 11. Pour etre syntaxiquement correct, on peut les remplacer par des transitions e; cela implique que l'on ne fait plus de differences entre l'arrivee d'eau primaire et secondaire. ********** Question 2 ********** Le modele 12 est un peu plus evolue que le 11. Les 3 principales differences entre le 11 et le 12 sont : - Les composantes EauPrimaire et EauSecondaire sont bien gerees dans le modele 12 : les transitions plusEau existent bien. - L'indicateur thermique se met maintenant a bipper lorsque une temperature tres elevee est affichee. - L'operateur n'est maintenant charge d'intervenir que si l'indicateur de temperature (TI) se met a bipper. Et il respecte une certaine chronologie dans son comportement : maintenant il doit forcement inhiber le controleur pneumatique avant toute action sur la vanne V5. Syst. Trans. | hno3_v12 |Syst. Synchro. |------------Etats--------------:----------Transitions----------| Vanne1 |* 65:* 275|hno3_v11 EchangeurThermique |initial 1:boucle 252|hno3_v12 CapteurTemperature |dead 0:boucleinitial 230| ControleurTemperature |deadlock 0: | AirComprime |pbModifTemp 0: | Vanne5 |pbBOOM 0: | EauPrincipale |pbPlusAir 0: | EauSecondaire |pbMoinsAir 0: | Pompe |pbFermerV1 6: | IndicateurTemperature |pbFermerV5 2: | ControleurPannePompe |pbOuvrirV1 5: | OperateurV1 |pbOuvrirV5 15: | OperateurV2 |pbActiverAP 4: | hno3_v12 |pbInhiberAP 23: | NB: Quelques problemes apparaissent : cela vient de la composante OperateurV2 dans laquelle chaque operation est definie comme incontrolable. Ceci n'est plus tout a fait exact, car les actions de l'operateur sont consecutives a la detection d'une panne ou a l'elevation de la temperature. NB: Certaines lignes du systeme de transitions sont inutiles : si AP est en mode automatique, l'operateur ne pourra jamais actionner (ouvrir et fermer) V5. /* ... AP ... OP */ (..... isAuto ..... fermerV5); (..... isAuto ..... ouvrirV5); ********** Question 3 ********** 3.1 Validite du modele Le modele 21 n'est pas valide : - les actions de l'operateur doivent etre incontrolables car celui-ci doit avoir tous les pouvoirs. Or pbActiverAP est different de 0, c'est pourquoi la transition associee a cette action (activerAP) doit etre dissociee du fait que l'indicateur de temperature TI soit en train de bipper ou pas. /* ........ AP .......... TI .......... OP */ ( activer NotBIP activerAP); devient : ( activer BIP activerAP); ( e NotBIP activerAP); On obtient alors pbActiverAP egal a 0. On fait de meme pour les autres actions incontrolables de la composante OperateurV2 (inhiberAP, ouvrirV5, fermerV5, ouvrirV1, fermerV1) et on obtient : Syst. Trans. | hno3_v21 |Syst. Synchro. |-----------Etats--------------:---------Transitions----------| Vanne1 |* 650:* 3715|hno3_v21 EchangeurThermique |initial 1:boucle 3210| CapteurTemperature |dead 0:boucleinitial 1448| ControleurTemperature |deadlock 0: | AirComprime |pbModifTemp 0: | Vanne5 |pbBOOM 0: | EauPrincipale |pbPlusAir 0: | EauSecondaire |pbMoinsAir 0: | Pompe |pbPanneMP 0: | IndicateurTemperature |pbFermerV1 0: | ControleurPannePompe |pbFermerV5 0: | OperateurV2 |pbOuvrirV1 0: | hno3_v21 |pbOuvrirV5 0: | |pbActiverAP 0: | |pbInhiberAP 0: | Voici les 6 lignes ainsi ajoutees au systeme de synchronisation : \* V1 ... . P . TI . FD . OP *\ ( e ... . e . NotBIP . e . fermerV1 ); ( e ... . e . BIP . e . ouvrirV1 ); ( e ... . e . BIP . e . fermerV5 ); ( e ... . e . NotBIP . e . ouvrirV5 ); ( e ... . e . BIP . e . activerAP ); ( e ... . e . NotBIP . e . inhiberAP ); 3.2 Injection de la panne de la vanne V1 La composante VanneV1 est modifiee, la transition toPanne est ajoutee a chaque etat. Deux autres etats sont ajoutes : bloqueeOuverte et bloqueeFermee. Dans ces etats, quelque soit l'action effectuee (e, OK/KO, toPanne, isPanne) on reste dans cet etat, ce qui traduit bien la notion de vanne bloquee. transition_system Vanne1 < width = 0 >; ouverte |- e -> ouverte, OK -> ouverte, fermer -> fermee, ouvrir -> ouverte, toPanne -> bloqueeOuverte ; fermee |- e -> fermee, KO -> fermee, fermer -> fermee, ouvrir -> ouverte, toPanne -> bloqueeFermee ; bloqueeOuverte |- e -> bloqueeOuverte, OK -> bloqueeOuverte, toPanne -> bloqueeOuverte , isPanne -> bloqueeOuverte; bloqueeFermee |- e -> bloqueeFermee, KO -> bloqueeFermee, toPanne -> bloqueeFermee , isPanne -> bloqueeFermee; < initial = { ouverte } >. Les actions ouvrir et fermer ne doivent plus etre possibles dans les etats bloqueeOuverte et bloqueeFermee. C'est pourquoi on doit ajouter les 2 lignes suivantes dans le systeme de synchronisation : /* V1 .......... . TI ... . OP */ ( isPanne . BIP . fermerV1 ); ( isPanne . NotBIP . ouvrirV1 ); La ligne traduisant la panne doit aussi etre ajoutee : /* V1 ... */ ( toPanne . e ........ . e); 3.3 Injection de la panne sur le controleur pneumatique AP Quelque soit l'etat (automatique ou manuel) du controleur pneumatique, ce dernier peut tomber en panne (toPanne) C'est pourquoi, deux etats sont crees (panneAuto et panneManu). La panne est une fuite d'air comprime qui rend le controleur pneumatique inoperant. Neanmoins, si l'operateur desactive le controleur (inhiber), l'operateur peut quand meme ouvrir ou fermer la vanne V5. Lorsqu'il repasse en mode automatique, le controleur reste inoperant (isPanne) ; il ne peut n'y ouvrir V5, n'y fermer V5. Dans la plupart des cas l'augmentation de la temperature sera stoppee par tot ou tard par l'operateur sur la vanne V5 (le cas echeant sur la vanne V1). transition_system AirComprime < width = 0 >; automatique |- e -> automatique, isAuto -> automatique, activer -> automatique, inhiber -> manuel, ouvrirV5 -> automatique, fermerV5 -> automatique, toPanne -> panneAuto ; manuel |- e -> manuel, isManuel -> manuel, activer -> automatique, inhiber -> manuel, toPanne -> panneManu ; panneAuto |- e -> panneAuto, activer -> panneAuto, inhiber -> panneManu, isPanne -> panneAuto; panneManu |- e -> panneManu, activer -> panneAuto, inhiber -> panneManu, ouvrirV5 -> panneManu, fermerV5 -> panneManu, isManuel -> panneManu; < initial = { automatique } >. Les lignes inserees dans le systeme de synchronisation sont : \* V1 . HE . TS . TC . AP . V5 . MP . ES . P . TI . FD . OP *\ ( e . e . e . e . toPanne . e . e . e . e . e . e . e ); ( e . e . e . PlusAir . isPanne . e . e . e . e . e . e . e ); ( e . e . e . MoinsAir . isPanne . e . e . e . e . e . e . e ); ( e . e . e . e . isPanne . e . e . e . e . NotBIP . e . fermerV5 ); ( e . e . e . e . isPanne . e . e . e . e . BIP . e . ouvrirV5 ); 3.4 autres pannes ********** Question 4 ********** 4.1 Modele hno3_v11 * L'evenement tant redoute (ER) est inevitable : il y a 32 deadlock qui correspondent a cet evenement. En voila un : e(ouverte.danger.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( ma_trace ) >, (ER est l'ensemble des etats buts des transitions incontrolable2 de la composante HE) * Il est possible que ER arrive meme si l'operateur ne faillit pas a ses obligations car il y a des etats ou HE est KO et ou la temperature afficher par TI est correct (TEgalTC). * Soit manu := !state[5]="manuel" l'ensemble des etats ou l'utilisateur a decide d'intervenir Soit HEKO := !state[2]="KO" l'ensemble des etats ou HE est KO. On calcule la trace menant de l'etat initial a un etat commun de manu et HEKO : ma_trace := trace(initial, *, manu /\ HEKO); wts(src(ma_trace),ma_trace); transition_system hno3_v11 < width = 12; list = (Vanne1, EchangeurThermique, CapteurTemperature, ControleurTemperature, AirComprime, Vanne5, EauPrincipale, EauSecondaire, Pompe, IndicateurTemperature, ControleurPannePompe, OperateurV1 )>; e(ouverte.normal.0.TEgalTc.automatique.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.e.e.e.inhiber.e.e.e.e.e.e.inhiberAP) -> e(ouverte.normal.0.TEgalTc.manuel.ouverteAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, ma_trace, boucleinitial ) >, ; e(ouverte.normal.0.TEgalTc.manuel.ouverteAlimentee.0.0.0.TEgalTc.0.0) |- (e.e.e.e.isManuel.fermer.e.e.e.e.e.fermerV5) -> e(ouverte.normal.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, ma_trace, boucleinitial ) >, ; e(ouverte.normal.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.chaud.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, ma_trace, boucleinitial ) >, ; e(ouverte.chaud.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (OK.tMonte.e.e.e.KO.e.e.e.e.e.e) -> e(ouverte.danger.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( boucle, ma_trace, boucleinitial ) >, ; e(ouverte.danger.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TEgalTc.manuel.fermeeAlimentee.0.0.0.TEgalTc.0.0) < property = ( ma_trace )<>, ; * On calcule l'ensemble des etats inevitables HE a l'etat KO (inevitable(*, ER)). C'est le meme ensemble que ER. Donc il n'ya pas d'etats qui menent inevitablement a ER. 4.2 Modele hno3_v12 * La encore, l'evenement tant redoute n'est pas impossible : e(ouverte.danger.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) |- (e.BOOM.e.e.e.e.e.e.e.e.e.e) -> e(ouverte.KO.0.TInfTc.automatique.fermeeAlimentee.0.0.0.TInfTc.0.0) < property = ( ma_trace ) >, * idem modele 11 * meme demarche que le systeme 11 * idem modele 11 4.3 Modele hno3_v21 Meme demarche que precedement : * pas impossible * pas impossible * posssible * idem modele 11 NB: nous n'avons pas insere dans la question 3 l'ensemble des pannes mais seulement 2, cela par manque de temps. De plus, inserer une panne conduit quasiment toujours aux memes demarches plus ou moins lourdes selon la complexite de la panne.