(FR)
Ce dossier contient les fichiers relatifs a mon stage au MIT :

* les modeles Alloy (ALS)

- a.als : Monde abstrait, definitions, operations et coherence du modele.
- b.als : Monde intermediaire, definition.
- c.als : Monde concret, definitions et operations individuelles.
- cop.als : Operations au niveau des mondes concrets et coherence du
  modele.
- op.als : Operations au niveau des mondes intermediaires et coherence du
  modele.
- rab.als : Relation d'abstraction abstrait/intermediaire, toutes
  operations.
- rab_alpha.als : Relation d'abstraction abstrait/intermediaire, controle
  optimise pour les operations qui commencent par abandonner la transaction
  en cours (de la forme Abort ; OpEafrom)
- rab_abort.als : Relation d'abstraction abstrait/intermediaire, controle
  optimise pour l'operation d'abandon (Abort)
- rbc.als : Relation d'abstraction intermediaire/concret.


(EN)
This folder contains the files related to my internship at MIT :

* the Alloy models (ALS)

- a.als : Abstract world, definitions, operations and model consistency.
- b.als : Between world, definition.
- c.als : Concrete world, definitions and individual purse operations.
- cop.als : Concrete world operations and model consistency.
- op.als : Between world operations and model consistency.
- rab.als : Abstract/Between refinement, all operations.
- rab_alpha.als : Abstract/Between refinement, optimized assertion checking
  for operations that first abort (Abort ; OpEafrom)
- rab_abort.als : Abstract/Between refinement, optimized assertion checking
  for Abort.
- rbc.als : Between/Concrete refinement.