mardi 20 mars 2007

De nouveaux transparents sur ...

mes pages web Spec2.

Une information : Le New York Times nous informe du décès de J. Backus, l'inventeur du langage FORTRAN.
Rappel BNF, Backus Naur Form

Si il n'y avait pas eu cette invention, peut-être que l'informatique ne serait pas celle que vous connaissez...

Rappel : demain à Nantes, la venue d'un prix Turing, Robin Milner, dont nous vous enseignons CCS en Spec2.

lundi 19 mars 2007

Dernier cours (le 19 mars)

Nous avons traité :
  • de l'étude système (à partir d'un texte de J.R. Abrial)
  • de B événementiel (idem)
Les transparents ont été fournis par courriel et mis sur site web.

lundi 12 mars 2007

Choix indéterministe

/* "Tout dans la vie est une affaire de choix, ça commence par la tétine ou le téton, ça se termine par le chêne ou le sapin. ", Pierre Desproges */

VIE = COMMENCEMENT,
COMMENCEMENT = (tetine -> SUITE | teton -> SUITE),
SUITE = (areu -> areu -> youpi -> youpi -> aille -> aille -> TERMINAISON),
TERMINAISON = (chêne -> STOP | sapin -> STOP).

Cours du 12 mars 07

Aujourd'hui j'ai traité :
- de l'équivalence entre processus
- de la vérification de modèles (avec rappel sur le concept de modèle - cours dans le poly Spec1 -)

Les transparents ont été indiqués dans mes messages spec2 de la semaine dernière. Qui les a consultés ? un ? deux ?

Je vous ai parlé de conférences ce we sur des sujets pas forcément éloignés de notre enseignement.
Voir : http://lefenetrou.blogspot.com

et sur les algèbres de processus
http://lefenetrou.blogspot.com/2007/03/nietzche-et-les-algbres-de-processus.html

La semaine prochaine, B événementiel (les transparents ont aussi été indiqués la semaine dernière).

vendredi 9 mars 2007

Se méfier de l'inférieur...

qui ne passe pas quand on fait un copier coller d'un texte corps de courriel...

Finalement ce n'est pas mal les erreurs ...

on apprend en faisant et en découvrant des erreurs.
Le copier-coller a foiré quelque part... alors voici une spec du massage faite à l'instant par un de vous à partir des versions abimées :

DEBUT(N=2) = DEBUT[0],
DEBUT[i:0..N] = (when(i < N) insuf -> DEBUT[i+1] | when(i==N) obs -> OBS1),
OBS1 = ( mvt -> STOP | pas_mvt -> COMP[0]),
COMP[j:0..4] = (when(j < 4) comp -> COMP[j+1] | when(j==4) obs -> OBS2),
OBS2 = ( mvt -> STOP | pas_mvt -> DEBUT).

/* FC */

jeudi 8 mars 2007

Erreurs dans l'affichage

Un étudiant consciencieux m'écrit :

"Bonjour,
Je pense qu'il y a une erreur de retranscription sur votre blog Spec2.
En effet, les lignes 7 et 11 doivent être respectivement :

CPT1[i:0..INSUF] = (when (iinsufflation -> CPT1[i+1]

CPT2[x:0..COMPR] = (when (xcompression -> CPT2[x+1]

Elles ont peut-être été coupées lors de l'édition du billet car elles
étaient trop longues? (Le même bug apparait sur le billet de R.L.)

Bonne journée"

Exact. Il était tard (et j'ai loupé l'heure du film que je devais aller voir) et je n'ai pas vérifié l'affichage. Pan sur le bec dirait le Canard Enchaîné.

Je corrige

Voici la spec de votre camarade :
DEBUT(N=2) = DEBUT[0],
DEBUT[i:0..N] = (when(i DEBUT[i+1]
| when(i==N) obs -> OBS1),
OBS1 = ( mvt -> STOP
| pas_mvt -> COMP[0]),
COMP[j:0..4] = (when(j<4) comp
-> COMP[j+1] | when(j==4) obs -> OBS2),
OBS2 = ( mvt -> STOP | pas_mvt -> DEBUT).

Merci beacoup pour les autres étudiants et nos fidèles lecteurs.

errare humanum est
et
homo sum et nihil humani a me alienum puto (Terence) !

mercredi 7 mars 2007

Une application des algèbres de processus

Dear FACS members

I am emailing to let you know about a funded studentship opportunity in the
interface between life sciences and computing science and mathematics at the
University of Stirling. Please distribute this information to your students.

The project "System Dynamics from Individual Interactions: A process algebra
approach
to epidemiology" starts in April and runs for three years. The aim
is to gain a better understanding of disease through modelling, and to
develop modelling techniques which will be applicable in a range of
application areas including systems biology and distributed computing.
See http://www.cs.stir.ac.uk/jobs/sdistudentship.html for further details.

For informal discussion and more information please contact Dr Carron
Shankland: 01786 467444 or email: carron@cs.stir.ac.uk.

Best wishes,
Carron

Le massage cardiaque de R.L. Groupe 2

DEBUT(N=2) = DEBUT[0],
DEBUT[i:0..N] = (when(i DEBUT[i+1] | when(i==N) obs -> OBS1),
OBS1 = ( mvt -> STOP | pas_mvt -> COMP[0]),
COMP[j:0..4] = (when(j<4) comp -> COMP[j+1] | when(j==4) obs -> OBS2),
OBS2 = ( mvt -> STOP | pas_mvt -> DEBUT).


obs : observation
comp : compression
mvt : il ... encore
pas mvt : il ne ...pas

Massage cardiaque

Spec2, le module qui peut vous sauver la vie !

Voici a spec en FSP :

/*
* Rédigé par S. Raynaud et G. Quéméner
*/

const COMPR=3

CPT1(INSUF=2) = CPT1[0],
CPT1[i:0..INSUF] = (when (i CPT1[i+1]
|when (i==INSUF) compression -> CPT2[0]
|respiration -> STOP
),
CPT2[x:0..COMPR] = (when (x CPT2[x+1]
|when (x==COMPR) compression -> CPT1[0]
|respiration -> STOP
).

Exercice : faites le diagramme de transition d'états.

Nota : on a indiqué seulement 3 pour compression (il aurait fallu indiquer 15 pour un adulte, mais on a voulu pouvoir représenter facilement le diagramme de transitions d'état.

Exlusion mutuelle

La présence aux cours et aux TD est obligatoire en IUT.
Dans les faits, je constate que, dans les cours et TD de 8 heures ou de 16 heures, il y a de 10 à 12 étudiants (TD) sur 22, et en cours (40 sur 100).
Sans doute les absents sont très très forts. Ils ont l'informatique dans le sang depuis la naissance (c'est un peu ce qu'écrivent certains dans leur dossiers de candidature à l'iut).

Alors si certains des absents se sont révéillés... voici pour eux :


On a deux utilisateurs et une imprimante.
L'accès à l'imprimante est exclusif.

Modélisez en utilisant le typage de processus.

Voici ce qu'a fait Dudule :

CONS = (prend -> utilise -> rend -> CONS).
IMP = (prend -> rend -> IMP).

||SYS = (u1 : CONS || u2 : CONS || IMP).


u1 : CONS va donner :
u1.CONS = (u1.prend -> u1.utilise -> u1.rend -> u1.CONS).
c'est un préfixage comme on en a vu en B lors de l'inclusion de machines.

Est-ce qu'il a bien modélisé l'exclusion mutuelle ?

NON ... faites le diagramme de transitions d'état pour voir...

Alors modifiez la spec de Dudule.

Animations de specs FSP

http://www.doc.ic.ac.uk/~jnm/book/book_applets/concurrency.html

lundi 5 mars 2007

Cours du 5 mars 2007

A 8h15 ce matin.

J'ai présenté le cas du chariot et de la trémie. Architecture avec "Partie commande", "Partie opérative" et entrées et sorties. Ainsi que le Grafcet de la partie commande.
J'ai donné les différences essentielles entre RDP et GRAFCET

Puis transparents sur les sémantiques du parallélisme avec illustration en FSP (ce qui est possible en FSP)

Puis j'ai donné exemple de passage d'un arbre de Jackson à un automate de Mealy

Les transparents des deux derniers cours à venir sont

ici

Les photos du tableau seront mises sur le blog sous peu.