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.
mardi 20 mars 2007
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)
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).
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).
- 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 */
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 (i
CPT2[x:0..COMPR] = (when (x
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) !
"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 (i
CPT2[x:0..COMPR] = (when (x
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
| 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
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
DEBUT[i:0..N] = (when(i
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.
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
|when (i==INSUF) compression -> CPT2[0]
|respiration -> STOP
),
CPT2[x:0..COMPR] = (when (x
|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.
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.
mardi 6 mars 2007
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.
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.
Inscription à :
Articles (Atom)
