Topic outline

  • Systèmes de transitions

    • Lien vers les supports de cours, sujets de TP et examens passés.
    • Installation de la TLA+ Toolbox (pour les TP en local) : https://lamport.azurewebsites.net/tla/toolbox.html
      Sur les machines école, /mnt/n7fs/tla/toolbox/toolbox (cf README du premier sujet de TP).
      Autre fonctionnement : plugin TLA+ pour Visual Studio Code. Éditeur plus agréable mais moins de finesse dans les paramètres de vérification.
    • Fonctionnement année 2020-2021 : tout se passe sur discord (serveur 2A SN N7 - S8, onglet Systèmes de transitions) :
      • Les cours sont en distanciel semi-synchrone : Philippe Quéinnec fait une courte introduction puis répond aux questions. Les supports à étudier sont les transparents avec annotations audios.
      • Les TD (ou CTD) sont prévus en présentiel (jusqu'à contre-ordre).
        Les TD sont en distanciel, imposé par la direction de l'école. (TD L34 -> discord)
      • Les TP sont en distanciel sur discord. Une demande de TP en présentiel a été faite mais elle va sans doute échouer.
    • Planning:
      C1 26/01 système de transitions
      TD1 27/01 TLA+ actions partie 1
      TD2 28/01 TLA+ actions partie 2
      C2 04/02 L'équité
      C3 09/02 logique temporelle LTL
      TP1 16/02 missionnaires et cannibales
      TD3 16/02 TLA+ logique
      TD4 19/02 exclusion mutuelle, Peterson
      TD5 23/02 exclusion mutuelle avec jeton
      C4 23/02 logique temporelle CTL
      TP2 24/02 exclusion mutuelle avec jeton
      C5 24/02 (démo preuve + exos ???)
      TP3 02/03 philosophes
      TP4 03/03 vchan
      TP5 05/03 vchan (suite)
      
    TLA+, c'est encore Leslie Lamport qui en parle le mieux...