-- 22 jan 2009
package util
provides
node observer(dataBoiteCP_IN,
localDataFromRead,
localErasedDataFromBoiteCP,
localCopyedDataFromBoiteCP,
localErasedDataFromPilote,
localCopyedDataFromPilote,
localErasedDataFromMem,
localCopyedDataFromMem : int;
productionEvent,
consumptionEvent,
eraseMemEvent,
eraseBoiteCPEvent,
erasePiloteEvent,
copyBoiteCPEvent,
copyPiloteEvent,
copyMemEvent : bool)
returns (retard, indiceCount : int; HindiceCount : bool);
body
type accChangeTab = {numEvent : int; cpt : int; indice : int};
node change_tab2(tabIn : int^10;
indiceIn : int;
num_event : int)
returns (tabOut : int^10);
var accOut : accChangeTab;
let
accOut, tabOut =
fillred<<change_elt2, 10>>(accChangeTab{numEvent = num_event; cpt = 0; indice = indiceIn}, tabIn);
tel
node change_elt2(accIn : accChangeTab;
--num_event : int;
--cptOut : int;
--indiceIn : int;
eltIn : int)
returns (accOut : accChangeTab;
--num_event : int;
--cptOut : int;
--indiceIn : int;
eltOut : int);
let
eltOut = if(accIn.indice = accIn.cpt)
then if accIn.numEvent=0
then 1
else if accIn.numEvent=1 or accIn.numEvent=3 or accIn.numEvent=7
then eltIn-1
else if accIn.numEvent=2 or accIn.numEvent=4 or accIn.numEvent=6
then eltIn+1
else eltIn
else eltIn;
accOut = accChangeTab{numEvent = accIn.numEvent;
indice = accIn.indice;
cpt = accIn.cpt+1};
tel
type accObserver = {nbCopy : int^10;
indice : int};
node observer(dataBoiteCP_IN,
localDataFromRead,
localErasedDataFromBoiteCP,
localCopyedDataFromBoiteCP,
localErasedDataFromPilote,
localCopyedDataFromPilote,
localErasedDataFromMem,
localCopyedDataFromMem : int;
productionEvent,
consumptionEvent,
eraseMemEvent,
eraseBoiteCPEvent,
erasePiloteEvent,
copyBoiteCPEvent,
copyPiloteEvent,
copyMemEvent : bool)
returns (retard, indiceCount : int; HindiceCount : bool);
var
-- accIterOut : accObserver;--
-- nbrCopy : int^10; -- pour stocker le nombre de copies, nbrCopy[i] : nb de copies dans le syst?me d'un donn?e identifi?e par "i"
CptRetard : int^10; -- les horloges qui mesurent le retard correspondant ? chaque don?e (?)
numEvent_tab : bool^8;--
value_tab : int^8;--
nbrCopy : int^10;
-- indiceBidon : int;
let
numEvent_tab = [productionEvent,
consumptionEvent,
eraseMemEvent,
copyMemEvent,
eraseBoiteCPEvent,
copyBoiteCPEvent,
erasePiloteEvent,
copyPiloteEvent
];
value_tab = [dataBoiteCP_IN,
localDataFromRead,
localErasedDataFromMem,
localCopyedDataFromMem,
localErasedDataFromBoiteCP,
localCopyedDataFromBoiteCP,
localErasedDataFromPilote,
localCopyedDataFromPilote
];
nbrCopy = updateNbrCopy(numEvent_tab, value_tab);
CptRetard = updateCptRetard(nbrCopy);
retard = calculRetard(consumptionEvent, CptRetard, localDataFromRead);
indiceCount, HindiceCount = updateIndice(nbrCopy);
-- nbrCopy = for(i=0;i<8;i++){
-- if num_event_tab[i]=true
-- then nbrCopy = change_tab2(pre(nbrCopy), value_tab[i], i)
-- else nbrCopy = pre(nbrCopy)
-- }
tel
type tIterRetard = {conEvent : bool;
dataFromRead : int;
retardCalcule : int;
cpt : int};
node calculRetard(consumptionEvent : bool;
CptRetard : int^10;
localDataFromRead : int)
returns (retard : int);
var accOut : tIterRetard;
let
accOut = red<<updateRetard;10>>(tIterRetard{conEvent = consumptionEvent;
dataFromRead = localDataFromRead;
retardCalcule = -1;
cpt = 0},
CptRetard);
retard = accOut.retardCalcule;
tel
node updateRetard(accIn : tIterRetard; elt : int) returns (accOut : tIterRetard);
let
accOut = tIterRetard{conEvent = accIn.conEvent;
dataFromRead = accIn.dataFromRead;
retardCalcule = -1 -> if accIn.conEvent and accIn.cpt=accIn.dataFromRead
then elt
else -1;
cpt = accIn.cpt+1};
tel
node updateNbrCopy(numEvent_tab : bool^8;
value_tab : int^8)
returns (nbrCopy : int^10);
var accIterOut : accObserver;
let
accIterOut = accObserver{nbCopy = (-1)^10;
indice = 0}
-> red<<Niter;8>>(accObserver{
nbCopy = pre(accIterOut.nbCopy);
indice = 0
},
numEvent_tab, value_tab);
nbrCopy = accIterOut.nbCopy;
tel
node Niter(accIn : accObserver;
--{tabIn : int^10;
-- indice : int;
--};
numEvent : bool;
value_tab : int)
returns (accOut : accObserver);
--{tabOut : int^10;
-- indiceOut : int;
--})
let
accOut = accObserver{nbCopy = if numEvent
then change_tab2(accIn.nbCopy, value_tab, accIn.indice)
else accIn.nbCopy;
indice = accIn.indice+1};
tel
-- indCount = -1 -> if consumptionEvent and (nbrCopy[localDataFromRead]=0)
-- then localDataFromRead
-- else -1;
-- HrinsCount = false -> consumptionEvent and (nbrCopy[localDataFromRead]=0)
type tCounterIter = {indice : int; Hindice : bool; cpt : int};
node updateIndice(nbrCopy : int^10)
returns (indiceCount : int;
HindiceCount : bool);
var iterOut : tCounterIter;
let
iterOut = red<<countIter;10>>(tCounterIter{indice = -1 ; Hindice = false; cpt = 0}, nbrCopy);
indiceCount = iterOut.indice;
HindiceCount = iterOut.Hindice;
tel
node countIter(accIn : tCounterIter; eltCopy : int)
returns (accOut : tCounterIter);
let
accOut = if pre(eltCopy<>-1) and pre(eltCopy<>0) and eltCopy=0
then tCounterIter{indice = accIn.cpt;
Hindice = true;
cpt = accIn.cpt+1}
else tCounterIter{indice = accIn.indice;
Hindice = accIn.Hindice;
cpt = accIn.cpt+1};
tel
-----------
node updateCptRetard(nbrCopy : int^10)
returns (CptRetard : int^10);
let
CptRetard = (-1)^10 -> map<<checkCopy;10>>(nbrCopy, pre(CptRetard));
tel
node checkCopy(eltCopy : int; oldCptRetard : int) returns (newCptRetard : int);
let
newCptRetard = if(pre(eltCopy=-1) and eltCopy=1)
then 0
else if pre(eltCopy<>-1) and pre(eltCopy<>0) and eltCopy=0
then -1
else oldCptRetard+1;
tel
end
package pilote
uses util;
provides
node system(in : bool) returns (v : bool;
dataBoiteCP_IN, dataBoiteCP_OUT : int;
piloteData, readData : int;
getMem : bool;
localDataFromRead : int;
Hcapt, Hpilote, Happli : bool;
dataBoiteCP_PUT, dataBoiteCP_GET : bool; -- commandes de la boite aux lettres
semMemTakeP, semMemTakeR, semMemGive : bool; -- commandes du s?maphore
semMemAutP,semMemAutR : bool;
putMem : bool;
res : bool;
retard : int);
body
node system (in : bool)
returns (v : bool;
dataBoiteCP_IN, dataBoiteCP_OUT : int;
piloteData, readData : int;
getMem : bool;
localDataFromRead : int;
Hcapt, Hpilote, Happli : bool;
dataBoiteCP_PUT, dataBoiteCP_GET : bool; -- commandes de la boite aux lettres
semMemTakeP, semMemTakeR, semMemGive : bool; -- commandes du s?maphore
semMemAutP,semMemAutR : bool;
putMem : bool;
res : bool;
retard : int);
--var --Hcapt, Hpilote, Happli : bool; -- les horloges
--dataBoiteCP_IN,
-- dataBoiteCP_OUT : int; -- donn?es en entr?es/sorties de la boite aux lettres
-- dataBoiteCP_PUT, dataBoiteCP_GET : bool; -- commandes de la boite aux lettres
-- semMemTakeP, semMemTakeR, semMemGive : bool; -- commandes du s?maphore
-- semMemAutP,semMemAutR : bool; -- autorisations en sortie du s?maphore
--piloteData, readData : int;
-- getMem,
-- putMem : bool;
var free, demandeR : bool;
HrinstCount : bool; indCount : int;
localErasedDataFromBoiteCP,
localCopiedDataFromBoiteCP,
localErasedDataFromPilote,
localCopiedDataFromPilote,
localErasedDataFromMem,
localCopiedDataFromMem : int;
productionEvent,
consumptionEvent,
eraseMemEvent,
eraseBoiteCPEvent,
erasePiloteEvent,
copyBoiteCPEvent,
copyPiloteEvent,
copyMemEvent : bool;
let
(Hcapt, Hpilote, Happli) = ctrl(in);
(dataBoiteCP_PUT, dataBoiteCP_IN, productionEvent) = capt(Hcapt, HrinstCount, indCount);
(dataBoiteCP_OUT, localErasedDataFromBoiteCP, localCopiedDataFromBoiteCP,
copyBoiteCPEvent, eraseBoiteCPEvent) = boiteCP(dataBoiteCP_IN, dataBoiteCP_GET, dataBoiteCP_PUT);
(semMemTakeP, putMem, dataBoiteCP_GET, piloteData, localErasedDataFromPilote,
erasePiloteEvent, copyPiloteEvent, localCopiedDataFromPilote)
= pilote(Hpilote, semMemAutP, dataBoiteCP_OUT);
(semMemGive, readData, localErasedDataFromMem, localCopiedDataFromMem,
eraseMemEvent, copyMemEvent) = mem(getMem, putMem, piloteData);
(semMemAutP, semMemAutR, free, demandeR) = semMem(semMemTakeP, semMemTakeR, semMemGive);
(getMem, semMemTakeR, localDataFromRead, consumptionEvent) = read(Happli, semMemAutR, readData);
retard, indCount, HrinstCount = observer(dataBoiteCP_IN,
localDataFromRead,
localErasedDataFromBoiteCP,
localCopiedDataFromBoiteCP,
localErasedDataFromPilote,
localCopiedDataFromPilote,
localErasedDataFromMem,
localCopiedDataFromMem,
productionEvent,
consumptionEvent,
eraseMemEvent,
eraseBoiteCPEvent,
erasePiloteEvent,
copyBoiteCPEvent,
copyPiloteEvent,
copyMemEvent);
-- une valeur bidon;
v = not(dataBoiteCP_IN=-1) and not(localDataFromRead=-1);
res = false -> v or pre(res);
tel
-- node observer(dataBoiteCP_IN,
-- localDataFromRead,
-- localErasedDataFromBoiteCP,
-- localCopyedDataFromBoiteCP,
-- localErasedDataFromPilote,
-- localCopyedDataFromPilote,
-- localErasedDataFromMem,
-- localCopyedDataFromMem : int;
-- productionEvent,
-- consumptionEvent,
-- eraseMemEvent,
-- eraseBoiteCPEvent,
-- erasePiloteEvent,
-- copyBoiteCPEvent,
-- copyPiloteEvent,
-- copyMemEvent : bool)
-- returns (retard, indCount : int, HrinsCount : bool);
-- var
-- nbrCopy : int^10; -- pour stocker le nombre de copies, nbrCopy[i] : nb de copies dans le syst?me d'un donn?e identifi?e par "i"
-- CptRetard : int^10; -- les horloges qui mesurent le retard correspondant ? chaque don?e (?)
-- let
-- nbre de copie d'occurence dans le syst?me
--nbrCopy[dataBoiteCP_IN] = 0 -> if productionEvent
-- then 1
-- else pre(nbrCopy[dataBoiteCP_IN]);
-- nbrCopy[localErasedDataFromBoiteCP] = if eraseBoiteCPEvent
-- then (pre(nbrCopy[localErasedDataFromBoiteCP])-1)
-- else pre(nbrCopy[localErasedDataFromBoiteCP]);
-- nbrCopy[localCopyedDataFromBoiteCP] = if copyBoiteCPEvent
-- then (pre(nbrCopy[localCopyedDataFromBoiteCP])+1)
-- else pre(nbrCopy[localCopyedDataFromBoiteCP]);
-- nbrCopy[localErasedDataFromMem] = if eraseMemEvent
-- then (pre(nbrCopy[localErasedDataFromMem])-1)
-- else pre(nbrCopy[localErasedDataFromMem]);
-- nbrCopy[localCopyedDataFromMem] = if copyMemEvent
-- then (pre(nbrCopy[localCopyedDataFromMem])+1)
-- else pre(nbrCopy[localCopyedDataFromMem]);
-- nbrCopy[localErasedDataFromPilote] = if erasePilotemEvent
-- then (pre(nbrCopy[localErasedDataFromPilote])-1)
-- else pre(nbrCopy[localErasedDataFromPilote]);
-- nbrCopy[localCopyedDataFromPilote] = if copyPiloteEvent
-- then (pre(nbrCopy[localCopyedDataFromPilote])+1)
-- else pre(nbrCopy[localCopyedDataFromPilote]);
-- nbrCopy[localDataFromRead] = 0 -> if consumptionEvent
-- then (pre(nbrCopy[localDataFromRead])-1)
-- else pre(nbrCopy[localDataFromRead]);
-- -- Horloges de cacul de retard
-- CptRetard[dataBoiteCP_IN] = -1 -> if productionEvent and (pre(CptRetard[dataBoiteCP_IN])=-1) and (nbrCopy[dataBoiteCP_IN]=1)
-- then 0
-- else if (nbrCopy[dataBoiteCP_IN]=0)
-- then -1
-- else (pre(CptRetard[dataBoiteCP_IN])+1);
-- -- cacul de retard a la reception d'une donn?e
-- retard = -1 -> if consumptionEvent
-- then CptRetard[localDataFromRead]
-- else -1;
-- gerer la reutilisation des ompteur d'occurence
-- indCount = -1 -> if consumptionEvent and (nbrCopy[localDataFromRead]=0)
-- then localDataFromRead
-- else -1;
-- HrinsCount = false -> consumptionEvent and (nbrCopy[localDataFromRead]=0)
--tel
node capt(Hcapt,
HrinstCount : bool;
indCount : int)
returns (dataPUT : bool;
stampedData : int;
productionEvent : bool);--stampedData : int when Hcapt);
var localCnt : int;
indCountTab : bool^10;
let
--recherche d'un indice libre
--for (localCnt=0;indCountTab[localCnt]=true,localCnt);
-- localCnt = 0 -> if Hcapt
-- then pre(localCnt) + 1
-- else pre(localCnt);
dataPUT = Hcapt;
stampedData = if Hcapt
then localCnt
else -1;
-- production observed
-- il faut utiliser productionEvent = Hcapt
-- il faut utiliser dataCP_IN
productionEvent = Hcapt;
-- gestion de num d'occurence
-- indCountTab[indCount] = false -> if HrinstCount
-- then false
-- else pre(indCountTab[indCount]);
-- indCountTab[localCnt] = false -> if Hcapt
-- then true
-- else pre(indCountTab[localCnt]);
localCnt, indCountTab = updateCnt(indCount, HrinstCount, Hcapt);
tel
type tUpdateCntElt = {indCnt : int;
HrinstCnt : bool;
Hcap : bool;
locCnt : int;
i : int;
locCntFound : bool};
node udpateCntElt(accIn : tUpdateCntElt; eltIn : bool)
returns (accOut : tUpdateCntElt;
eltOut : bool);
let
eltOut = if (accIn.i = accIn.indCnt) and accIn.HrinstCnt
then true else eltIn;
accOut = tUpdateCntElt{indCnt = accIn.indCnt;
HrinstCnt = accIn.HrinstCnt;
Hcap = accIn.Hcap;
locCnt = if eltIn and accIn.Hcap and not(accIn.locCntFound)
then accIn.i
else accIn.locCnt;
i = accIn.i + 1;
locCntFound = (eltIn and accIn.Hcap) or accIn.locCntFound;
-- ? initialiser ? false !!!!
};
tel
node updateCnt(indCount : int; HrinstCount, Hcapt : bool)
returns (localCnt : int;
tab : bool^10);
var accOut : tUpdateCntElt;
let
accOut, tab = fillred<<udpateCntElt, 10>>(tUpdateCntElt{
indCnt = indCount;
HrinstCnt = HrinstCount;
Hcap = Hcapt;
locCnt = -1;
i = 0;
locCntFound = false;
},
false^10);
localCnt = accOut.locCnt;
tel
-- boite aux lettres
node boiteCP(dataIN : int; dataGET, dataPUT : bool)
returns (dataOUT : int;
localDataErasedFromBoiteCP : int;
localDataCopydFromBoiteCP : int;
copyBoiteCPEvent, erasedBoiteCPEvent : bool);
var localData : int;
pLocalData : int;
let
localData = -1 -> if dataPUT
then dataIN
else if dataGET
then -1
else pre localData;
-- observation dans Boite CP
-- ecrasement
localDataErasedFromBoiteCP = -1 -> if dataPUT
then pLocalData
else -1;
erasedBoiteCPEvent = dataPUT;
localDataCopydFromBoiteCP = -1 -> if dataPUT
then localData
else -1;
copyBoiteCPEvent = dataPUT;
-- localData = dataIN when dataPUT;
pLocalData = localData -> pre(localData);
dataOUT = if dataGET
then pLocalData
else -1;
tel
node pilote(Hpilote, semAutP : bool;
dataBoiteCP : int)
returns (semMemTakeP, putMemP, dataGET : bool;
piloteData : int;
localDataErasedFromPilote : int;
erasedPiloteEvent, copyPiloteEvent : bool;
localDataCopiedFromPilote : int;
);
var localData : int;
let
dataGET = Hpilote;
localData = if Hpilote
then dataBoiteCP
else -1;
semMemTakeP = Hpilote;
piloteData = if (semAutP and Hpilote)
then localData --current(localData)
else -1;
putMemP = if (semAutP and Hpilote)
then true
else false;
-- observation dans pilote
-- ecrasement
localDataErasedFromPilote = -1 -> if Hpilote
then pre localData
else -1;
erasedPiloteEvent = Hpilote;
localDataCopiedFromPilote = -1 -> if Hpilote
then localData
else -1;
copyPiloteEvent = Hpilote;
tel
-- semaphore Memoire partage
--node sem(semMemP, semMemR, semMemGive : bool) returns (semAutP,semAutR : bool);
--let
--semAutP = semMemGive when semMemP;
--semAutR = semMemGive when semMemR;
--tel
node semMem(semMemTakeP,
semMemTakeR,
semMemGive : bool)
returns (semMemAutP : bool;
semMemAutR : bool;
free : bool;
demandeR : bool);
--var free : bool;
-- demandeR : bool; -- R a demand? le sem, mais il n'est pas encore libre
let
free = true -> ((pre(free) and (not semMemTakeP) and (not semMemTakeR))
or
((not semMemTakeP) and (not semMemTakeR) and semMemGive));
-- semMemAutR = false -> (pre free) and (not semMemTakeP) and semMemTakeR;
semMemAutP = false -> (pre free) and semMemTakeP;
demandeR = false -> if semMemTakeR and semMemTakeP
then true
else if pre(semMemAutR)
then false
else pre demandeR;
-- (semMemTakeR or pre(demandeR));
semMemAutR = false -> (pre free) and (not semMemTakeP) and demandeR;
tel
-- node semMem2
-- (semMemTakeP: bool;
-- semMemTakeR: bool;
-- semMemGive: bool)
-- returns
-- (semMemAutP: bool;
-- semMemAutR: bool;
-- free: bool;
-- demandeR: bool);
-- let
-- semMemAutP = (false -> ((pre free) and semMemTakeP));
-- semMemAutR = (false -> (((pre free) and (not semMemTakeP)) and
-- demandeR));
-- free = (true -> ((((pre free) and (not semMemTakeP)) and (not
-- semMemTakeR)) or (((not semMemTakeP) and (not semMemTakeR)) and semMemGive)))
-- ;
-- demandeR = (semMemTakeR -> (semMemTakeR or (pre demandeR)));
-- tel.
-- memoire partage
node mem(getMem, putMem : bool;
piloteData : int)
returns (semMemGive : bool;
readData : int;
localDataErasedFromMem, localDataCopiedFromMem : int;
erasedMemEvent : bool;
copyMemEvent : bool); --when getMem);
var localData : int;
demandeGetMem : bool;
let
semMemGive = not (getMem or putMem);
localData = -1 -> if (putMem)
then piloteData
else pre(localData); -- when putMem;
readData = if demandeGetMem
then localData -- current(locaData)
else -1;
demandeGetMem = getMem -> if getMem
then true
else if pre(not(readData=-1))
then false
else pre demandeGetMem;
-- observation dans Mem
-- ecrasement
localDataErasedFromMem = -1 -> if putMem
then pre localData
else -1;
erasedMemEvent = putMem;
localDataCopiedFromMem = -1 -> if putMem
then localData
else -1;
copyMemEvent = putMem;
tel
-- application
node read(Happli, semAutR : bool;
readData : int)
returns (getMemR, semMemR : bool;
localData : int;
consumptionEvent : bool);
--var localData : int;
let
semMemR = Happli;
getMemR = semAutR; -- and Happli;
-- if (semAutR and Happli)
--then true
--else false;
localData = readData;-- if Happli
-- then readData
-- else -1;
consumptionEvent= not (readData=-1);
tel
const periodePilote : int = 5;
const periodeCapt : int = 10;
const periodeAppli : int = 20;
const periodeDureeAppli : int = 7;
const periodeDureePilote : int = 2;
-- Horloges
node ctrl(in : bool)
returns (Hcapt,
Hpilote,
Happli : bool);
var cptC,
cptP,
cptA,
cptDureeP,
cptDureeA : int;
countDP,
countDA : bool;
Hduree_pilote, Hduree_appli : bool;
let
Hpilote = (cptP=periodePilote);
Hcapt = (cptC=periodeCapt);
Happli = (cptA=periodeAppli);
Hduree_pilote = (cptDureeP=periodeDureePilote);
Hduree_appli = (cptDureeA=periodeDureeAppli);
countDP = false -> if Hpilote
then true
else if (pre(cptDureeP)=periodeDureePilote)
then false
else pre(countDP);
countDA = false -> if Happli
then true
else if (pre(cptDureeA)=periodeDureeAppli)
then false
else pre(countDA);
cptDureeP = 1 -> if countDP
then pre(cptDureeP)+1
else 1;
cptDureeA = 1 -> if countDA
then pre(cptDureeA)+1
else 1;
cptC = 1 -> if (pre(cptC)=periodeCapt)
then 1
else pre(cptC)+1;
cptP = 1 -> if (pre(cptP)=periodePilote)
then 1
else pre(cptP)+1;
cptA = 1 -> if (pre(cptA)=periodeAppli)
then 1
else pre(cptA)+1;
tel
end