MGL7160: Exercice #8

27 mars 2001

1. Ensemble de traces (10 pts) (10 pts)

Soit les deux définitions suivantes de processus:

  PROCESS P1[x, y, z]: EXIT :=
    x; EXIT  []  x; y; EXIT  []  x; y; z; EXIT
  ENDPROC

  PROCESS P2[a, b, c]: EXIT :=
    a; (EXIT [] b; (EXIT [] c; EXIT))
  ENDPROC

1.

Donnez l'ensemble des traces complètes de chacun des processus indiqués plus bas.

  P1[u, v, w]
  P2[u, v, u]
  P1[v, w, x] |[w,x]| P2[u, w, x]

2.

Les processus P1[u, v, w] et P2[u, v, w] ont le même ensemble de traces complètes. Peut-on dire pourtant que ces deux processus sont équivalents dans n'importe quel contexte? Justifiez votre réponse.

2. Propriétés du processus ChangerExposants (10 pts) ( pts)

Soit la définition de processus présentée au bas de la page. Formalisez les propriétés indiquées plus bas pour le processus suivant en utilisant la logique modale et temporelle:

  ChangerExposants[entree, sortie]

1.

En tout temps, l'action entree peut être effectuée.

2.

Les seules actions possibles pour ce processus sont entree et sortie.

3.

Dès que deux caractères '*' sont reçus en entrée, le caractère '^' est produit en sortie, et ce à tout instant.

4.

Si un caractère '*' est reçu en entrée et qu'il est suivi immédiatement d'un '^', alors les deux caractères seront émis, inchangés, en sortie.

5.

Si un caractères '^' est reçu en entrée, alors il sera éventuellement émis en sortie.

  PROCESS ChangerExposants[entree, sortie]: NOEXIT :=
    entree ?x: char;
    ([x ~= '*'] ->
       sortie !x; ChangerExposants[entree, sortie];
     []
     [x  = '*'] ->
       (entree ?y: char;
        [y ~= '*'] ->
          sortie !'*'; sortie !y; ChangerExposants[entree, sortie];
        []
        [y  = '*'] ->
          sortie !'^'; ChangerExposants[entree, sortie]
       )
    )
  ENDPROC

About this document ...

MGL7160: Exercice #8

This document was generated using the LaTeX2HTML translator Version 97.1 (release) (July 13th, 1997)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split +0 -auto_navigation exposant-logique-temp.tex.

The translation was initiated by Tremblay Guy on 3/27/2001