From a60ebe895980075761c397b60177bad48cd49419 Mon Sep 17 00:00:00 2001
From: Pascal Raymond <Pascal.Raymond@imag.fr>
Date: Wed, 4 Jul 2012 08:52:51 +0200
Subject: [PATCH] ...
---
tests/should_work/lionel/pilote-1.0.lus | 819 ++++++++++++++++++++++++
1 file changed, 819 insertions(+)
create mode 100644 tests/should_work/lionel/pilote-1.0.lus
diff --git a/tests/should_work/lionel/pilote-1.0.lus b/tests/should_work/lionel/pilote-1.0.lus
new file mode 100644
index 00000000..1a81d5ca
--- /dev/null
+++ b/tests/should_work/lionel/pilote-1.0.lus
@@ -0,0 +1,819 @@
+-- 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
\ No newline at end of file
--
GitLab