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 */

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) !

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

Cours du 5 mars (suite)

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.