MACHINE devoir3

/* Voici un commentaire */

SETS

  Personne={p0, p1, p2, p3, p4, p5, p6, p7}
; Cours = {c0,c1,c2,c3,c4,c5}

CONSTANTS

/* Constantes initiales */

    Homme         /* Ensemble des personnes qui sont des hommes */
  , Femme         /* Ensemble des personnes qui sont des femmes */
  , Parent        /* (x,y) ∈ Parent ssi x est un parent de y */
  , Prealable     /* (x,y) ∈ Prealable ssi x est un prealable y */

/* Constantes à définir dans le devoir */

//  , Mere              /* Ensemble des personnes qui sont des meres */
//  , Mere_alt          /* Définition alternative de Mere */
//  , SansEnfant        /* Ensemble des personnes qui n'ont pas d'enfants */
//  , SansEnfant_alt    /* Définition alternative de SansEnfant */
//  , Fraterie          /* (x,y) ∈ Fraterie ssi x et y ont les mêmes parents */
//  , FratLarge         /* (x,y) ∈ FratLarge ssi x et y ont un parent en commun */
//  , FratLarge_alt     /* Définition alternative de FratLarge */
//  , Frere             /* (x,y) ∈ Frere ssi (x,y) ∈ FratLarge et x est un homme */
//  , Frere_alt         /* Définition alternative de Frere */
//  , Cousin            /* (x,y) ∈ Cousin ssi x est un cousin ou une cousine de y */
//  , Cousin_alt        /* Définition alternative de Cousin */
//  , Parent_2          /* comme Parent, mais avec permutation des enfants de p1 et p2 */
//  , Ancetre           /* (x,y) ∈ Ancetre ssi x est un ancêtre de y */
//  , PasDeCycle        /* PasDeCycle = TRUE ssi la relation Parent
//                                               ne contient pas de cycle */
//  , Prealables_c5     /* x ∈ Prea_de_c5 ssi x est un préalable de c5 */
//  , Prealables_c5_alt /* Définition alternative de Prea_de_c5 */
//  , PrealableTrans   /* (x,y) ∈ Prealables_trans ssi
//                            x est un préalable immédiat ou indirect
//                            (ie, par transitivité) de y */
//  , MemePrealable     /* (x,y) ∈ MemePrealable ssi x et y ont les mêmes préalables */
//  , AuMoinsUnPrealable  /* (x,y) ∈ AuMoinsUnPrealable ssi
//                            x et y sont préalables d’un même cours */
//  , AuMoinsUnPrealable_alt  /* Définition alternative de AuMoinsUnPrealable */
//  , PlusRestreint     /* x ∈ PlusRestreint ssi x a le plus grand nombre de 
//                          préalables, directement ou indirectement */

PROPERTIES

/* Définition des constantes initiales */

  Homme={p0, p1}
& Femme=Personne-Homme
& Parent={
           (p0,p1)
          ,(p0,p2)
          ,(p1,p3)
          ,(p1,p4)
          ,(p2,p5)
          ,(p2,p6)
          ,(p7,p3)
          ,(p7,p4)
         }
& Prealable = { (c0,c2), (c0,c3), (c1,c2), (c1,c3), (c2,c4), (c4,c5)}

/* Définitions des constantes à compléter */

// & Mere = ...

// & Mere_alt = ...

// & SansEnfant = ...

// & SansEnfant_alt = ...

// & Fraterie =  ...

// & FratLarge = ...

// & FratLarge_alt = ..

// & Frere = ...

// & Frere_alt = ...

// & Cousin =  ...

// & Cousin_alt = ...

// & Parent_2 = ...

// & Ancetre = ...

// & PasDeCycle = ...

// & Prealables_c5 = ...

// & Prealables_c5_alt = ...

// & PrealableTrans = ...

// & MemePrealable = ...

// & AuMoinsUnPrealable =  ...

// & AuMoinsUnPrealable_alt =  ...

// & PlusRestreint = ...

END