First commit
This commit is contained in:
commit
b7a1213f91
29 changed files with 1312 additions and 0 deletions
16
Alt/Ctrl.alt
Normal file
16
Alt/Ctrl.alt
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
node Ctrl
|
||||
/* Controller observations
|
||||
*/
|
||||
flow rate : [0,2][3];
|
||||
level : [0,nbSensors];
|
||||
/* The 27 commands of the controller
|
||||
* d for dec, i for inc and n for nop
|
||||
*/
|
||||
event ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn;
|
||||
trans true |- ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn
|
||||
-> ;
|
||||
edon
|
||||
49
Alt/CtrlVV.alt
Normal file
49
Alt/CtrlVV.alt
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
node CtrlVV
|
||||
/* Virtual valves to simulate real valves in order to discover failures
|
||||
*/
|
||||
sub V : ValveVirtual[3];
|
||||
/* Controller observations
|
||||
*/
|
||||
flow rate : [0,2][3];
|
||||
level : [0,nbSensors];
|
||||
assert V[0].rateReal = rate[0];
|
||||
V[1].rateReal = rate[1];
|
||||
V[2].rateReal = rate[2];
|
||||
/* The 27 commands of the controller
|
||||
* d for dec, i for inc and n for nop
|
||||
*/
|
||||
event ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn;
|
||||
trans true |- ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn
|
||||
-> ;
|
||||
sync <ddd, V[0].dec, V[1].dec, V[2].dec>;
|
||||
<ddi, V[0].dec, V[1].dec, V[2].inc>;
|
||||
<ddn, V[0].dec, V[1].dec>;
|
||||
<did, V[0].dec, V[1].inc, V[2].dec>;
|
||||
<dii, V[0].dec, V[1].inc, V[2].inc>;
|
||||
<din, V[0].dec, V[1].inc>;
|
||||
<dnd, V[0].dec, V[2].dec>;
|
||||
<dni, V[0].dec, V[2].inc>;
|
||||
<dnn, V[0].dec>;
|
||||
<idd, V[0].inc, V[1].dec, V[2].dec>;
|
||||
<idi, V[0].inc, V[1].dec, V[2].inc>;
|
||||
<idn, V[0].inc, V[1].dec>;
|
||||
<iid, V[0].inc, V[1].inc, V[2].dec>;
|
||||
<iii, V[0].inc, V[1].inc, V[2].inc>;
|
||||
<iin, V[0].inc, V[1].inc>;
|
||||
<ind, V[0].inc, V[2].dec>;
|
||||
<ini, V[0].inc, V[2].inc>;
|
||||
<inn, V[0].inc>;
|
||||
<ndd, V[1].dec, V[2].dec>;
|
||||
<ndi, V[1].dec, V[2].inc>;
|
||||
<ndn, V[1].dec>;
|
||||
<nid, V[1].inc, V[2].dec>;
|
||||
<nii, V[1].inc, V[2].inc>;
|
||||
<nin, V[1].inc>;
|
||||
<nnd, V[2].dec>;
|
||||
<nni, V[2].inc>;
|
||||
<nnn>;
|
||||
edon
|
||||
25
Alt/GNUmakefile
Normal file
25
Alt/GNUmakefile
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
TARGET = tank.alt
|
||||
|
||||
SOURCE_ALT = Parameters.alt\
|
||||
Valve.alt\
|
||||
ValveVirtual.alt\
|
||||
Tank.alt\
|
||||
System.alt\
|
||||
|
||||
DIFF_ALT =
|
||||
|
||||
all: $(TARGET) $(DIFF_ALT)
|
||||
|
||||
clean:
|
||||
rm -f *~
|
||||
|
||||
cleandir : clean
|
||||
rm -f $(TARGET) $(DIFF_ALT) test.alt
|
||||
|
||||
$(TARGET) : $(SOURCE_ALT)
|
||||
rm -f $(TARGET)
|
||||
for d in $(SOURCE_ALT); do \
|
||||
cat $$d >> $(TARGET);\
|
||||
done
|
||||
|
||||
$(DIFF_ALT) : $(SOURCE_ALT)
|
||||
9
Alt/Parameters.alt
Normal file
9
Alt/Parameters.alt
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
/* nbSensors : the number of sensors
|
||||
* nbSensors must be greater or equal to 4
|
||||
*/
|
||||
const nbSensors = 4;
|
||||
|
||||
/* nbFailures : the maximum number if failures (0, 1, 2 or 3)
|
||||
* nbFailures is use to limit the reachables configurations
|
||||
*/
|
||||
const nbFailures = NbPannes;
|
||||
47
Alt/System.alt
Normal file
47
Alt/System.alt
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
node SystemNbPannesFNomDuControleur
|
||||
sub V : Valve[3];
|
||||
T : Tank;
|
||||
C : NomDuControleur;
|
||||
assert T.input = (V[0].rate + V[1].rate);
|
||||
T.output = V[2].rate;
|
||||
/* les observations du controleurs */
|
||||
C.rate[0] = V[0].rate;
|
||||
C.rate[1] = V[1].rate;
|
||||
C.rate[2] = V[2].rate;
|
||||
C.level = T.level;
|
||||
/* to limit the number of failures */
|
||||
nbFailures >= (V[0].stucked + V[1].stucked + V[2].stucked);
|
||||
state ctrl : bool;
|
||||
init ctrl := true;
|
||||
event env, cmd;
|
||||
trans ctrl |- cmd -> ctrl := false;
|
||||
~ctrl |- env -> ctrl := true;
|
||||
sync <env, T.time>;
|
||||
<C.ddd, cmd, V[0].dec, V[1].dec, V[2].dec>;
|
||||
<C.ddi, cmd, V[0].dec, V[1].dec, V[2].inc>;
|
||||
<C.ddn, cmd, V[0].dec, V[1].dec>;
|
||||
<C.did, cmd, V[0].dec, V[1].inc, V[2].dec>;
|
||||
<C.dii, cmd, V[0].dec, V[1].inc, V[2].inc>;
|
||||
<C.din, cmd, V[0].dec, V[1].inc>;
|
||||
<C.dnd, cmd, V[0].dec, V[2].dec>;
|
||||
<C.dni, cmd, V[0].dec, V[2].inc>;
|
||||
<C.dnn, cmd, V[0].dec>;
|
||||
<C.idd, cmd, V[0].inc, V[1].dec, V[2].dec>;
|
||||
<C.idi, cmd, V[0].inc, V[1].dec, V[2].inc>;
|
||||
<C.idn, cmd, V[0].inc, V[1].dec>;
|
||||
<C.iid, cmd, V[0].inc, V[1].inc, V[2].dec>;
|
||||
<C.iii, cmd, V[0].inc, V[1].inc, V[2].inc>;
|
||||
<C.iin, cmd, V[0].inc, V[1].inc>;
|
||||
<C.ind, cmd, V[0].inc, V[2].dec>;
|
||||
<C.ini, cmd, V[0].inc, V[2].inc>;
|
||||
<C.inn, cmd, V[0].inc>;
|
||||
<C.ndd, cmd, V[1].dec, V[2].dec>;
|
||||
<C.ndi, cmd, V[1].dec, V[2].inc>;
|
||||
<C.ndn, cmd, V[1].dec>;
|
||||
<C.nid, cmd, V[1].inc, V[2].dec>;
|
||||
<C.nii, cmd, V[1].inc, V[2].inc>;
|
||||
<C.nin, cmd, V[1].inc>;
|
||||
<C.nnd, cmd, V[2].dec>;
|
||||
<C.nni, cmd, V[2].inc>;
|
||||
<C.nnn, cmd>;
|
||||
edon
|
||||
16
Alt/Tank.alt
Normal file
16
Alt/Tank.alt
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
node Tank
|
||||
state level : [0,nbSensors] : public;
|
||||
init level := nbSensors/2;
|
||||
flow input : [0,4];
|
||||
output : [0,2];
|
||||
event time;
|
||||
trans input>output |- time -> level := level + 1;
|
||||
input<output |- time -> level := level - 1;
|
||||
input=output & input=0 |- time -> ;
|
||||
input=output & input>0 |- time -> level := level - 1;
|
||||
input=output & input>0 |- time -> ;
|
||||
input=output & input>0 |- time -> level := level + 1;
|
||||
/* To avoid deadlocks */
|
||||
input>output & level=nbSensors |- time -> ;
|
||||
input<output & level=0 |- time -> ;
|
||||
edon
|
||||
15
Alt/Valve.alt
Normal file
15
Alt/Valve.alt
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
node Valve
|
||||
state rate : [0,2] : public;
|
||||
stucked : [0,1] : public;
|
||||
init rate := 0;
|
||||
stucked := 0;
|
||||
event dec, inc;
|
||||
trans stucked=0 |- dec -> rate := rate - 1;
|
||||
stucked=0 |- inc -> rate := rate + 1;
|
||||
stucked=0 & rate=0 |- dec -> ;
|
||||
stucked=0 & rate=2 |- inc -> ;
|
||||
/* a problem may appear */
|
||||
stucked=0 |- dec, inc -> stucked := 1;
|
||||
/* After the failure, the valve is stuck */
|
||||
stucked=1 |- dec, inc -> ;
|
||||
edon
|
||||
16
Alt/ValveVirtual.alt
Normal file
16
Alt/ValveVirtual.alt
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
/* A virtual valse is use by the controller :
|
||||
* - to simulate a perfect valve
|
||||
* - to stop the use of a valve when it is stuck
|
||||
*/
|
||||
node ValveVirtual
|
||||
state rate : [0,2] : public;
|
||||
/* information given via the controller
|
||||
* rate different from rateReal means that this valve is stuck.
|
||||
* so there is no need to use it any more
|
||||
*/
|
||||
flow rateReal : [0,2];
|
||||
init rate := 0;
|
||||
event dec, inc;
|
||||
trans rate=rateReal |- dec -> rate := rate - 1;
|
||||
rate=rateReal |- inc -> rate := rate + 1;
|
||||
edon
|
||||
9
Controleurs/GNUmakefile
Normal file
9
Controleurs/GNUmakefile
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
TARGET =
|
||||
|
||||
all: $(TARGET)
|
||||
|
||||
clean:
|
||||
rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
rm -f $(TARGET) Ctrl*alt
|
||||
9
ControleursOpt/GNUmakefile
Normal file
9
ControleursOpt/GNUmakefile
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
TARGET =
|
||||
|
||||
all: $(TARGET)
|
||||
|
||||
clean:
|
||||
rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
rm -f $(TARGET) Ctrl*alt
|
||||
10
ControleursOpt/Optimisation-2.alt
Normal file
10
ControleursOpt/Optimisation-2.alt
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
event
|
||||
/*
|
||||
* les priorites dependent des actions sur la vanne aval
|
||||
* inc > nop > dec
|
||||
*/
|
||||
{ddi, dii, dni, idi, iii, ini, ndi, nii, nni} >
|
||||
{ddn, din, dnn, idn, iin, inn, ndn, nin, nnn};
|
||||
{ddn, din, dnn, idn, iin, inn, ndn, nin, nnn} >
|
||||
{ddd, did, dnd, idd, iid, ind, ndd, nid, nnd};
|
||||
edon
|
||||
10
ControleursOpt/Optimisation.alt
Normal file
10
ControleursOpt/Optimisation.alt
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
event
|
||||
/*
|
||||
* les priorites dependent des actions sur la vanne aval
|
||||
* inc > nop > dec
|
||||
*/
|
||||
{ddi, dii, dni, idi, iii, ini, ndi, nii, nni} >
|
||||
{ddn, din, dnn, idn, iin, inn, ndn, nin, nnn};
|
||||
{ddn, din, dnn, idn, iin, inn, ndn, nin, nnn} >
|
||||
{ddd, did, dnd, idd, iid, ind, ndd, nid, nnd};
|
||||
edon
|
||||
68
Ctrl_System.alt
Normal file
68
Ctrl_System.alt
Normal file
|
|
@ -0,0 +1,68 @@
|
|||
/*
|
||||
* This node is the result of the projection of the node 'System'
|
||||
* on its subnode 'Ctrl'.
|
||||
*/
|
||||
node Ctrl_System
|
||||
flow
|
||||
r : [0, 2][3];
|
||||
l : [0, 4];
|
||||
event
|
||||
nnn;
|
||||
nni;
|
||||
nnd;
|
||||
nin;
|
||||
nii;
|
||||
nid;
|
||||
ndn;
|
||||
ndi;
|
||||
ndd;
|
||||
inn;
|
||||
ini;
|
||||
ind;
|
||||
iin;
|
||||
iii;
|
||||
iid;
|
||||
idn;
|
||||
idi;
|
||||
idd;
|
||||
dnn;
|
||||
dni;
|
||||
dnd;
|
||||
din;
|
||||
dii;
|
||||
did;
|
||||
ddn;
|
||||
ddi;
|
||||
ddd;
|
||||
/* Existential transitions */
|
||||
trans
|
||||
(0<=r[2] and r[2]<=1 and r[0]=0 or (0<=r[2] and r[2]<=1 and 0<=r[1] and r[1]<=1 or r[1]=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and 0<=r[0] and r[0]<=1 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=2) and l=3 |- 'ddd' -> ;
|
||||
(r[2]=0 and 0<=r[0] and r[0]<=1 or (r[2]=0 and 0<=r[1] and r[1]<=1 or r[2]=1 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and 0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and 0<=r[1] and r[1]<=1 and r[0]=2) and l=3 |- 'ddi' -> ;
|
||||
(r[2]=0 and r[0]=0 or (r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=1 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[2]=1 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and 0<=r[0] and r[0]<=1 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=2) and l=3 |- 'ddn' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[1]=0 or r[2]=2 and 1<=r[1] and r[1]<=2) and l=2 or (r[1]=0 or r[2]=2 and r[1]=1) and 0<=r[0] and r[0]<=1 and l=3 |- 'did' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=0 or (r[2]=0 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and 0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=2) and l=3 |- 'dii' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[1]=0 or 1<=r[2] and r[2]<=2 and 1<=r[1] and r[1]<=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and 0<=r[0] and r[0]<=1 or r[2]=2 and r[1]=0 and r[0]=2) and l=3 |- 'din' -> ;
|
||||
((0<=r[2] and r[2]<=1 and 0<=r[1] and r[1]<=1 or r[1]=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and 0<=r[0] and r[0]<=1 or r[2]=2 and r[1]=0 and r[0]=2) and l=3 |- 'dnd' -> ;
|
||||
((r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=0 or (r[2]=0 and 0<=r[1] and r[1]<=1 or r[1]=2) and r[0]=1 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and 0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=2) and l=3 |- 'dni' -> ;
|
||||
((r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=0 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[1]=2) and r[0]=1 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and 0<=r[0] and r[0]<=1 or r[2]=2 and r[1]=0 and r[0]=2) and l=3 |- 'dnn' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[0]=0 or r[2]=2 and 1<=r[0] and r[0]<=2) and l=2 or (0<=r[1] and r[1]<=1 and r[0]=0 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'idd' -> ;
|
||||
((r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=0 or 1<=r[2] and r[2]<=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'idi' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[0]=0 or 1<=r[2] and r[2]<=2 and 1<=r[0] and r[0]<=2) and l=2 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and r[0]=0 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'idn' -> ;
|
||||
(0<=r[0] and r[0]<=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((r[1]=0 or r[2]=2 and 1<=r[1] and r[1]<=2) and r[0]=0 or r[2]=2 and r[1]=0 and 1<=r[0] and r[0]<=2) and l=2 or r[1]=0 and r[0]=0 and l=3 |- 'iid' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[0]=0 or r[1]=0 and 1<=r[0] and r[0]<=2) and l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and r[0]=0 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=1) and l=3 |- 'iii' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and 1<=r[1] and r[1]<=2) and r[0]=0 or 1<=r[2] and r[2]<=2 and r[1]=0 and 1<=r[0] and r[0]<=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'iin' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and r[0]=0 or r[2]=2 and 0<=r[1] and r[1]<=1 and 1<=r[0] and r[0]<=2) and l=2 or (r[1]=0 and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'ind' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[1]=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (r[0]=0 or 0<=r[1] and r[1]<=1 and 1<=r[0] and r[0]<=2) and l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and r[0]=0 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=1) and l=3 |- 'ini' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[1]=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=0 or 1<=r[2] and r[2]<=2 and 0<=r[1] and r[1]<=1 and 1<=r[0] and r[0]<=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'inn' -> ;
|
||||
(0<=r[2] and r[2]<=1 and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[0] and r[0]<=1 or r[2]=2 and r[0]=2) and l=2 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and r[0]=0 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'ndd' -> ;
|
||||
(r[2]=0 and r[0]=0 or (r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or l=2 or ((0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=0 or 1<=r[2] and r[2]<=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'ndi' -> ;
|
||||
(r[2]=0 and r[0]=0 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and r[0]=2) and l=2 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and r[0]=0 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=1) and l=3 |- 'ndn' -> ;
|
||||
((0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=0 or r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((r[1]=0 or r[2]=2 and 1<=r[1] and r[1]<=2) and 0<=r[0] and r[0]<=1 or r[2]=2 and r[1]=0 and r[0]=2) and l=2 or (r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 and l=3 |- 'nid' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[0] and r[0]<=1 or r[1]=0 and r[0]=2) and l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and r[0]=0 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=1) and l=3 |- 'nii' -> ;
|
||||
((r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and 1<=r[1] and r[1]<=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and 1<=r[1] and r[1]<=2) and 0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'nin' -> ;
|
||||
((0<=r[2] and r[2]<=1 and 0<=r[1] and r[1]<=1 or r[1]=2) and r[0]=0 or (0<=r[2] and r[2]<=1 and r[1]=0 or 1<=r[1] and r[1]<=2) and r[0]=1 or (0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((0<=r[1] and r[1]<=1 or r[2]=2 and r[1]=2) and 0<=r[0] and r[0]<=1 or r[2]=2 and 0<=r[1] and r[1]<=1 and r[0]=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'nnd' -> ;
|
||||
((r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=0 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[1]=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or (0<=r[0] and r[0]<=1 or 0<=r[1] and r[1]<=1 and r[0]=2) and l=2 or ((r[1]=0 or 1<=r[2] and r[2]<=2 and r[1]=1) and r[0]=0 or 1<=r[2] and r[2]<=2 and r[1]=0 and r[0]=1) and l=3 |- 'nni' -> ;
|
||||
((r[2]=0 and 0<=r[1] and r[1]<=1 or 0<=r[2] and r[2]<=1 and r[1]=2) and r[0]=0 or (r[2]=0 and r[1]=0 or 0<=r[2] and r[2]<=1 and r[1]=1 or r[1]=2) and r[0]=1 or (0<=r[2] and r[2]<=1 and r[1]=0 or r[1]=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2) and l=1 or ((0<=r[1] and r[1]<=1 or 1<=r[2] and r[2]<=2 and r[1]=2) and 0<=r[0] and r[0]<=1 or 1<=r[2] and r[2]<=2 and 0<=r[1] and r[1]<=1 and r[0]=2) and l=2 or ((r[1]=0 or r[2]=2 and r[1]=1) and r[0]=0 or r[2]=2 and r[1]=0 and r[0]=1) and l=3 |- 'nnn' -> ;
|
||||
/* Universal transitions */
|
||||
/* no transition */
|
||||
edon
|
||||
68
Ctrl_SystemPerfect.alt
Normal file
68
Ctrl_SystemPerfect.alt
Normal file
|
|
@ -0,0 +1,68 @@
|
|||
/*
|
||||
* This node is the result of the projection of the node 'SystemPerfect'
|
||||
* on its subnode 'Ctrl'.
|
||||
*/
|
||||
node Ctrl_SystemPerfect
|
||||
flow
|
||||
r : [0, 2][3];
|
||||
l : [0, 4];
|
||||
event
|
||||
nnn;
|
||||
nni;
|
||||
nnd;
|
||||
nin;
|
||||
nii;
|
||||
nid;
|
||||
ndn;
|
||||
ndi;
|
||||
ndd;
|
||||
inn;
|
||||
ini;
|
||||
ind;
|
||||
iin;
|
||||
iii;
|
||||
iid;
|
||||
idn;
|
||||
idi;
|
||||
idd;
|
||||
dnn;
|
||||
dni;
|
||||
dnd;
|
||||
din;
|
||||
dii;
|
||||
did;
|
||||
ddn;
|
||||
ddi;
|
||||
ddd;
|
||||
/* Existential transitions */
|
||||
trans
|
||||
((1<=l and l<=3 and 0<=r[2] and r[2]<=1 or 2<=l and l<=3 and r[2]=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=2 |- 'ddd' -> ;
|
||||
(2<=l and l<=3 and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or l=2 and r[1]=2) and r[0]=2 |- 'ddi' -> ;
|
||||
((1<=l and l<=3 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=2) and r[0]=2 |- 'ddn' -> ;
|
||||
((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and 0<=r[0] and r[0]<=1 or (1<=l and l<=2 and r[1]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=1 or (l=1 and r[2]=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=2 |- 'did' -> ;
|
||||
((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and 1<=r[1] and r[1]<=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=2 |- 'dii' -> ;
|
||||
((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'din' -> ;
|
||||
((1<=l and l<=3 and 0<=r[2] and r[2]<=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=1 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or (l=1 and r[2]=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=2 |- 'dnd' -> ;
|
||||
(2<=l and l<=3 and r[1]=0 or (l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=1 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=2 |- 'dni' -> ;
|
||||
((1<=l and l<=3 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=1 or (l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=2) and 0<=r[0] and r[0]<=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=1 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'dnn' -> ;
|
||||
((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or 1<=l and l<=2 and r[1]=2) and r[0]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or (l=1 and r[2]=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=2 |- 'idd' -> ;
|
||||
((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or 1<=l and l<=2 and r[1]=2) and r[0]=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=2 |- 'idi' -> ;
|
||||
((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=2) and r[0]=0 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'idn' -> ;
|
||||
(1<=l and l<=2 and r[1]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and r[0]=0 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=0 or l=1 and 1<=r[1] and r[1]<=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'iid' -> ;
|
||||
((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and 1<=r[1] and r[1]<=2) and r[0]=0 or (1<=l and l<=2 and r[1]=0 or l=1 and 1<=r[1] and r[1]<=2) and r[0]=1 or (1<=l and l<=2 and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'iii' -> ;
|
||||
((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and 1<=r[1] and r[1]<=2) and r[0]=0 or ((l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or l=1 and 1<=r[1] and r[1]<=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'iin' -> ;
|
||||
((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=0 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or l=1 and r[1]=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'ind' -> ;
|
||||
((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or 1<=l and l<=2 and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or l=1 and r[1]=2) and r[0]=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'ini' -> ;
|
||||
((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=1 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=0 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or l=1 and r[1]=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'inn' -> ;
|
||||
((1<=l and l<=3 and 0<=r[2] and r[2]<=1 or 2<=l and l<=3 and r[2]=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or 1<=l and l<=2 and r[1]=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or (l=1 and r[2]=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=2 |- 'ndd' -> ;
|
||||
(2<=l and l<=3 and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=0 or ((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (l=2 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=2 |- 'ndi' -> ;
|
||||
((1<=l and l<=3 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and 0<=r[1] and r[1]<=1 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'ndn' -> ;
|
||||
((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and r[0]=0 or (1<=l and l<=2 and r[1]=0 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nid' -> ;
|
||||
((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and 1<=r[1] and r[1]<=2) and r[0]=0 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and 1<=r[1] and r[1]<=2) and r[0]=1 or (1<=l and l<=2 and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nii' -> ;
|
||||
((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and 1<=r[1] and r[1]<=2) and r[0]=0 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and 1<=r[1] and r[1]<=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or l=1 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nin' -> ;
|
||||
((1<=l and l<=3 and 0<=r[2] and r[2]<=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=1 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or (l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and r[1]=2) and r[0]=1 or ((l=1 and 0<=r[2] and r[2]<=1 or 1<=l and l<=2 and r[2]=2) and 0<=r[1] and r[1]<=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nnd' -> ;
|
||||
(2<=l and l<=3 and r[1]=0 or (l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=1 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=0 or ((l=2 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or 1<=l and l<=2 and r[1]=2) and r[0]=1 or ((1<=l and l<=2 and r[2]=0 or l=2 and 1<=r[2] and r[2]<=2) and r[1]=0 or 1<=l and l<=2 and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nni' -> ;
|
||||
((1<=l and l<=3 and r[2]=0 or 2<=l and l<=3 and 1<=r[2] and r[2]<=2) and r[1]=0 or (1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=1 or (l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=2) and r[0]=0 or ((1<=l and l<=2 and r[2]=0 or l=2 and r[2]=1 or 2<=l and l<=3 and r[2]=2) and r[1]=0 or (1<=l and l<=2 and 0<=r[2] and r[2]<=1 or l=2 and r[2]=2) and r[1]=1 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=2) and r[0]=1 or ((l=1 and r[2]=0 or 1<=l and l<=2 and r[2]=1 or l=2 and r[2]=2) and r[1]=0 or (l=1 and r[2]=0 or 1<=l and l<=2 and 1<=r[2] and r[2]<=2) and r[1]=1 or l=1 and 1<=r[2] and r[2]<=2 and r[1]=2) and r[0]=2 |- 'nnn' -> ;
|
||||
/* Universal transitions */
|
||||
/* no transition */
|
||||
edon
|
||||
198
GNUmakefile
Normal file
198
GNUmakefile
Normal file
|
|
@ -0,0 +1,198 @@
|
|||
USER = $(shell whoami)
|
||||
|
||||
TEX = pdflatex
|
||||
|
||||
MODEL = tank
|
||||
|
||||
SOURCE_ALT = Alt/*.alt
|
||||
|
||||
SOURCE_SPEC = Spec/*.spe
|
||||
|
||||
ARCHIVE_SUJET = FD-2022-2023-M1-CC-sujet.tgz
|
||||
|
||||
ARCHIVE_RAPPORT = FD-2022-2023-M1-CC-rapport-$(USER).tgz
|
||||
|
||||
ARCHIVE_CORRIGE = FD-2022-2023-M1-CC-corrige.tgz
|
||||
|
||||
TARGET_SUJET = sujet.pdf\
|
||||
$(ARCHIVE_SUJET)\
|
||||
|
||||
TARGET_RAPPORT = rapport-$(USER).pdf\
|
||||
$(ARCHIVE_RAPPORT)\
|
||||
|
||||
TARGET_CORRIGE = corrige.pdf\
|
||||
$(ARCHIVE_CORRIGE)\
|
||||
|
||||
TARGET = $(TARGET_SUJET)\
|
||||
$(TARGET_RAPPORT)\
|
||||
$(TARGET_CORRIGE)\
|
||||
|
||||
SOURCE_TEX = $(MODEL).tex\
|
||||
sujet.tex\
|
||||
rapport.tex\
|
||||
corrige.tex\
|
||||
|
||||
SUBDIRS = Alt Spec
|
||||
|
||||
SUBDIRS2 = Res Controleurs Graphs LaTeX
|
||||
|
||||
SUBDIRS3 = ControleursOpt
|
||||
|
||||
SUBDIRS4 = Optimisations
|
||||
|
||||
SOURCE_SUJET = $(SUBDIRS)\
|
||||
Controleurs/GNUmakefile\
|
||||
ControleursOpt/GNUmakefile\
|
||||
ControleursOpt/Optimisation.alt\
|
||||
ControleursOpt/Optimisation-2.alt\
|
||||
Graphs/GNUmakefile\
|
||||
LaTeX/GNUmakefile\
|
||||
Res/GNUmakefile\
|
||||
$(MODEL).tex\
|
||||
sujet.tex\
|
||||
sujet.pdf\
|
||||
TODO\
|
||||
rapport.tex\
|
||||
GNUmakefile\
|
||||
|
||||
SOURCE_RAPPORT = $(SUBDIRS)\
|
||||
$(SUBDIRS2)\
|
||||
$(SUBDIRS3)\
|
||||
$(MODEL).tex\
|
||||
rapport.tex\
|
||||
rapport-$(USER).pdf\
|
||||
GNUmakefile\
|
||||
|
||||
SOURCE_CORRIGE = $(SUBDIRS)\
|
||||
$(SUBDIRS4)\
|
||||
Controleurs/GNUmakefile\
|
||||
Graphs/GNUmakefile\
|
||||
LaTeX/GNUmakefile\
|
||||
Res/GNUmakefile\
|
||||
$(MODEL).tex\
|
||||
TODO\
|
||||
ControleursOpt/GNUmakefile\
|
||||
ControleursOpt/Optimisation.alt\
|
||||
corrige.tex\
|
||||
corrige.pdf\
|
||||
GNUmakefile\
|
||||
|
||||
# pour iterer sur le nombre de pannes
|
||||
PANNES = 0 1 2 3
|
||||
|
||||
# pour iterer sur les controleurs generes
|
||||
ITERATIONS = 1 2 3 4 5
|
||||
|
||||
# contient le controleur original
|
||||
CONTROLEURS_INIT = Ctrl CtrlVV
|
||||
|
||||
# La liste des controleurs que l'on souhaite optimiser est genere automatiquement par la detection de la stabilite
|
||||
|
||||
all: sources $(MODEL).time $(TARGET)
|
||||
|
||||
clean:
|
||||
for d in $(SUBDIRS); do \
|
||||
$(MAKE) -C $$d $@ || exit 1;\
|
||||
done
|
||||
for d in $(SUBDIRS2); do \
|
||||
$(MAKE) -C $$d $@ || exit 1;\
|
||||
done
|
||||
rm -f *.dvi *.eps *.log *.aux *.toc *.bbl *.blg *.out *.snm *.nav *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
for d in $(SUBDIRS); do \
|
||||
$(MAKE) -C $$d $@ || exit 1;\
|
||||
done
|
||||
for d in $(SUBDIRS2); do \
|
||||
$(MAKE) -C $$d $@ || exit 1;\
|
||||
done
|
||||
for d in $(SUBDIRS3); do \
|
||||
$(MAKE) -C $$d $@ || exit 1;\
|
||||
done
|
||||
rm -f *.dot *.prop *.res *.results *.validate
|
||||
rm -f $(TARGET) $(MODEL).time
|
||||
|
||||
sources :
|
||||
for d in $(SUBDIRS); do \
|
||||
$(MAKE) -C $$d all || exit 1;\
|
||||
done
|
||||
|
||||
$(MODEL).time: $(SOURCE_ALT) $(SOURCE_SPEC)
|
||||
for c in $(CONTROLEURS_INIT); do \
|
||||
for p in $(PANNES); do \
|
||||
cat Alt/Parameters.alt > Alt/tank.alt;\
|
||||
cat Alt/Valve.alt >> Alt/tank.alt;\
|
||||
cat Alt/ValveVirtual.alt >> Alt/tank.alt;\
|
||||
cat Alt/Tank.alt >> Alt/tank.alt;\
|
||||
cat 'Alt/'$$c'.alt' >> Alt/tank.alt;\
|
||||
cat Alt/System.alt >> Alt/tank.alt;\
|
||||
sed -e 's:NbPannes:'$$p':' -e 's:NomDuControleur:'$$c':' Alt/tank.alt > Alt/test.alt;\
|
||||
sed -e 's:CtrlInitial:'$$c':' -e 's:NbPannes:'$$p':' -e 's:NumIter:1I:' -e 's:NomDuControleur:'$$c':' Spec/System.spe > Spec/test.spe;\
|
||||
arc -b Alt/test.alt Spec/test.spe 2>> $(MODEL).time;\
|
||||
echo '\small{\lstinputlisting{Res/System'$$p'F'$$c'.res}}' > 'LaTeX/System'$$p'F'$$c'.tex';\
|
||||
for d in $(ITERATIONS); do \
|
||||
cat Alt/Parameters.alt > Alt/tank.alt;\
|
||||
cat Alt/Valve.alt >> Alt/tank.alt;\
|
||||
cat Alt/ValveVirtual.alt >> Alt/tank.alt;\
|
||||
cat Alt/Tank.alt >> Alt/tank.alt;\
|
||||
cat 'Controleurs/'$$c$$p'F'$$d'I.alt' >> Alt/tank.alt;\
|
||||
cat Alt/System.alt >> Alt/tank.alt;\
|
||||
nd=$$(expr $$d + 1);\
|
||||
pd=$$(expr $$d - 1);\
|
||||
sed -e 's:NbPannes:'$$p':' -e 's:NomDuControleur:'$$c$$p'F'$$d'I:' Alt/tank.alt > Alt/test.alt;\
|
||||
sed -e 's:CtrlInitial:'$$c':' -e 's:NbPannes:'$$p':' -e 's:NumIter:'$$nd'I:' -e 's:NomDuControleur:'$$c$$p'F'$$d'I:' Spec/System.spe > Spec/test.spe;\
|
||||
arc -b Alt/test.alt Spec/test.spe 2>> $(MODEL).time;\
|
||||
echo '\lstinputlisting{Res/System'$$p'F'$$c$$p'F'$$d'I.res}' >> 'LaTeX/System'$$p'F'$$c'.tex';\
|
||||
if [ $$d -eq 1 ] ; \
|
||||
then diff -I "Properties for node" 'Res/System'$$p'F'$$c$$p'F'$$d'I.res' 'Res/System'$$p'F'$$c'.res';\
|
||||
else diff -I "Properties for node" 'Res/System'$$p'F'$$c$$p'F'$$d'I.res' 'Res/System'$$p'F'$$c$$p'F'$$pd'I.res';\
|
||||
fi;\
|
||||
if [ $$? -eq 0 ] ;\
|
||||
then \
|
||||
sed -e 's:'$$c$$p'F'$$d'I:'$$c$$p'F'$$d'I_Opt:' -e 's:edon::' 'Controleurs/'$$c$$p'F'$$d'I.alt' > 'ControleursOpt/'$$c$$p'F'$$d'I_Opt.alt';\
|
||||
cat ControleursOpt/Optimisation.alt >> 'ControleursOpt/'$$c$$p'F'$$d'I_Opt.alt';\
|
||||
cat Alt/Parameters.alt > Alt/tank.alt;\
|
||||
cat Alt/Valve.alt >> Alt/tank.alt;\
|
||||
cat Alt/ValveVirtual.alt >> Alt/tank.alt;\
|
||||
cat Alt/Tank.alt >> Alt/tank.alt;\
|
||||
cat 'ControleursOpt/'$$c$$p'F'$$d'I_Opt.alt' >> Alt/tank.alt;\
|
||||
cat Alt/System.alt >> Alt/tank.alt;\
|
||||
nd=$$(expr $$d + 1);\
|
||||
pd=$$(expr $$d - 1);\
|
||||
sed -e 's:NbPannes:'$$p':' -e 's:NomDuControleur:'$$c$$p'F'$$d'I_Opt:' Alt/tank.alt > Alt/test.alt;\
|
||||
sed -e 's:CtrlInitial:'$$c':' -e 's:NbPannes:'$$p':' -e 's:NumIter:'$$nd'I_Opt:' -e 's:NomDuControleur:'$$c$$p'F'$$d'I_Opt:' Spec/System.spe > Spec/test.spe;\
|
||||
sed -e 's:CtrlInitial:'$$c':' -e 's:NbPannes:'$$p':' -e 's:NumIter:'$$nd'I_Opt:' -e 's:NomDuControleur:'$$c$$p'F'$$d'I_Opt:' Spec/Graphs.spe >> Spec/test.spe;\
|
||||
arc -b Alt/test.alt Spec/test.spe 2>> $(MODEL).time;\
|
||||
echo '\fbox{\small{\lstinputlisting{Res/System'$$p'F'$$c$$p'F'$$d'I_opt.res}}}' > 'LaTeX/System'$$p'F'$$c'_opt.tex';\
|
||||
break ;\
|
||||
fi;\
|
||||
done;\
|
||||
done;\
|
||||
done;
|
||||
for d in $(SUBDIRS2); do \
|
||||
$(MAKE) -C $$d || exit 1;\
|
||||
done
|
||||
uname -mps > $(MODEL).time
|
||||
|
||||
sujet.pdf: sujet.tex tank.tex
|
||||
|
||||
rapport.pdf: rapport.tex $(MODEL).time
|
||||
|
||||
rapport-$(USER).pdf: rapport.pdf
|
||||
ln -f rapport.pdf rapport-$(USER).pdf
|
||||
|
||||
corrige.pdf: corrige.tex $(MODEL).time
|
||||
|
||||
$(ARCHIVE_SUJET): $(SOURCE_SUJET)
|
||||
tar -czf $(ARCHIVE_SUJET) $(SOURCE_SUJET)
|
||||
|
||||
$(ARCHIVE_RAPPORT): $(SOURCE_RAPPORT)
|
||||
tar -czf $(ARCHIVE_RAPPORT) $(SOURCE_RAPPORT)
|
||||
|
||||
$(ARCHIVE_CORRIGE): $(SOURCE_CORRIGE)
|
||||
tar -czf $(ARCHIVE_CORRIGE) $(SOURCE_CORRIGE)
|
||||
|
||||
.SUFFIXES: .pdf .tex
|
||||
|
||||
.tex.pdf:
|
||||
$(TEX) $*.tex && $(TEX) $*.tex
|
||||
16
Graphs/GNUmakefile
Normal file
16
Graphs/GNUmakefile
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
SRC = $(wildcard *.dot)
|
||||
|
||||
TARGET = $(SRC:.dot=.pdf)
|
||||
|
||||
all: $(TARGET)
|
||||
|
||||
clean:
|
||||
rm -f *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
rm -f $(TARGET) $(SRC)
|
||||
|
||||
.SUFFIXES: .dot .pdf
|
||||
|
||||
.dot.pdf: $*.dot
|
||||
dot -Tpdf $*.dot -o $*.pdf
|
||||
9
LaTeX/GNUmakefile
Normal file
9
LaTeX/GNUmakefile
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
TARGET =
|
||||
|
||||
all: $(TARGET)
|
||||
|
||||
clean:
|
||||
rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
rm -f $(TARGET) *.tex
|
||||
13
Res/GNUmakefile
Normal file
13
Res/GNUmakefile
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
TARGET =
|
||||
|
||||
ITER1 = 1 2 3
|
||||
|
||||
ITER2 = 4 5 6
|
||||
|
||||
all: $(TARGET)
|
||||
|
||||
clean:
|
||||
rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core
|
||||
|
||||
cleandir: clean
|
||||
rm -f $(TARGET) *.res
|
||||
23
Spec/GNUmakefile
Normal file
23
Spec/GNUmakefile
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
TARGET = tank.spe
|
||||
|
||||
SOURCE_SPE = System.spe
|
||||
|
||||
DIFF_SPE =
|
||||
|
||||
all: $(TARGET) $(DIFF_SPE)
|
||||
|
||||
clean:
|
||||
rm -f *~
|
||||
|
||||
cleandir : clean
|
||||
rm -f $(TARGET) $(DIFF_SPE) test.spe
|
||||
|
||||
|
||||
$(TARGET) : $(SOURCE_SPE)
|
||||
rm -f $(TARGET)
|
||||
for d in $(SOURCE_SPE); do \
|
||||
cat $$d >> $(TARGET);\
|
||||
done
|
||||
|
||||
|
||||
$(DIFF_SPE) : $(SOURCE_SPE)
|
||||
8
Spec/Graphs.spe
Normal file
8
Spec/Graphs.spe
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
with Valve, ValveVirtual do
|
||||
dot(any_s, any_t - self_epsilon) > 'Graphs/$NODENAME.dot';
|
||||
modes() > 'Graphs/$NODENAME-modes.dot';
|
||||
quot() > 'Graphs/$NODENAME-quot.dot';
|
||||
done
|
||||
with SystemNbPannesFNomDuControleur do
|
||||
dot(any_s, any_t - self_epsilon) > 'Graphs/$NODENAME.dot';
|
||||
done
|
||||
40
Spec/System-2.spe
Normal file
40
Spec/System-2.spe
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
with SystemNbPannesFNomDuControleur do
|
||||
deadlock := any_s - src(any_t - self_epsilon);
|
||||
notResettable := any_s -coreach(initial,any_t);
|
||||
/* output */
|
||||
out0 := any_s & [V[2].rate=0];
|
||||
out1 := any_s & [V[2].rate=1];
|
||||
out2 := any_s & [V[2].rate=2];
|
||||
dec21 := any_t & label V[2].dec & rsrc(out2);
|
||||
dec10 := any_t & label V[2].dec & rsrc(out1);
|
||||
/* Niveaux critiques et Situations redoutees */
|
||||
NC := any_s & [T.level=0 | T.level=nbSensors];
|
||||
SR := deadlock | NC;
|
||||
EPerdu := any_s - SR;
|
||||
CGagne := any_s - SR;
|
||||
/* systeme d'equation au point fixe
|
||||
* CGagnant = CGagne & src(CCoupGagnant)
|
||||
* CCoupGagnant = CCoup & rtgt(EPerdant)
|
||||
* EPerdant = EPerdu & (src(ECoupPerdant) - src(ECoupNonPerdant))
|
||||
* ECoupPerdant = ECoup & rtgt(CGgagnant)
|
||||
* ECoupNonPerdant = ECoup & rtgt(any_s - CGagnant)
|
||||
*/
|
||||
CCoup := any_t & label cmd;
|
||||
ECoup := any_t & label env;
|
||||
CCoupGagnant -= CCoup & rtgt(EPerdu & (src(ECoup & rtgt(CGagne & src(CCoupGagnant))) - src(ECoup & rtgt(any_s - (CGagne & src(CCoupGagnant))))));
|
||||
/* Controller projection */
|
||||
/* Syntax and semantic of the "project" command
|
||||
* param 1 : les configurations projetees
|
||||
* param 2 : les transitions projetees
|
||||
* - arg1 : projection existentielle
|
||||
* - arg2 : projection universelle
|
||||
* param 3 : nom du noeud AltaRica genere
|
||||
* param 4 : simplification ou non des expressions booleennes
|
||||
* param 5 (optionel) : noeud de la hierarchie servant a la projection
|
||||
*/
|
||||
/* Universal projection is use */
|
||||
project(any_s, (empty_t,CCoupGagnant), 'CtrlInitialNbPannesFNumIter', true,C)
|
||||
> 'Controleurs/CtrlInitialNbPannesFNumIter.alt';
|
||||
/* record results */
|
||||
show(any_s, any_t, deadlock, NC, SR , out0, out1, out2, dec21, dec10, CCoupGagnant) > 'Res/$NODENAME.res';
|
||||
done
|
||||
40
Spec/System.spe
Normal file
40
Spec/System.spe
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
with SystemNbPannesFNomDuControleur do
|
||||
deadlock := any_s - src(any_t - self_epsilon);
|
||||
notResettable := any_s -coreach(initial,any_t);
|
||||
/* output */
|
||||
out0 := any_s & [V[2].rate=0];
|
||||
out1 := any_s & [V[2].rate=1];
|
||||
out2 := any_s & [V[2].rate=2];
|
||||
dec21 := any_t & label V[2].dec & rsrc(out2);
|
||||
dec10 := any_t & label V[2].dec & rsrc(out1);
|
||||
/* Niveaux critiques et Situations redoutees */
|
||||
NC := any_s & [T.level=0 | T.level=nbSensors];
|
||||
SR := deadlock | NC;
|
||||
EPerdu := any_s - SR;
|
||||
CGagne := any_s - SR;
|
||||
/* systeme d'equation au point fixe
|
||||
* CGagnant = CGagne & src(CCoupGagnant)
|
||||
* CCoupGagnant = CCoup & rtgt(EPerdant)
|
||||
* EPerdant = EPerdu & (src(ECoupPerdant) - src(ECoupNonPerdant))
|
||||
* ECoupPerdant = ECoup & rtgt(CGgagnant)
|
||||
* ECoupNonPerdant = ECoup & rtgt(any_s - CGagnant)
|
||||
*/
|
||||
CCoup := any_t & label cmd;
|
||||
ECoup := any_t & label env;
|
||||
CCoupGagnant -= CCoup & rtgt(EPerdu & (src(ECoup & rtgt(CGagne & src(CCoupGagnant))) - src(ECoup & rtgt(any_s - (CGagne & src(CCoupGagnant))))));
|
||||
/* Controller projection */
|
||||
/* Syntax and semantic of the "project" command
|
||||
* param 1 : les configurations projetees
|
||||
* param 2 : les transitions projetees
|
||||
* - arg1 : projection existentielle
|
||||
* - arg2 : projection universelle
|
||||
* param 3 : nom du noeud AltaRica genere
|
||||
* param 4 : simplification ou non des expressions booleennes
|
||||
* param 5 (optionel) : noeud de la hierarchie servant a la projection
|
||||
*/
|
||||
/* Universal projection is use */
|
||||
project(any_s, (empty_t,CCoupGagnant), 'CtrlInitialNbPannesFNumIter', true,C)
|
||||
> 'Controleurs/CtrlInitialNbPannesFNumIter.alt';
|
||||
/* record results */
|
||||
show(any_s, any_t, deadlock, NC, SR , out0, out1, out2, dec21, dec10, CCoupGagnant) > 'Res/$NODENAME.res';
|
||||
done
|
||||
29
TODO
Normal file
29
TODO
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
L'archive du sujet contient :
|
||||
|
||||
0/ Les sources latex du cahier des charges, du sujet et d'un squelette de rapport.
|
||||
1/ Le pdf du sujet du projet.
|
||||
2/ Ce ficher TODO
|
||||
3/ Des sources AltaRica dans le répertoire Alt
|
||||
4/ Un fichier System.spe de spécification pour le calcul des controleurs dans le répertoire Spec
|
||||
|
||||
|
||||
Pour votre étude, vous pouvez utiliser au choix les commandes :
|
||||
$> make
|
||||
$> altarica-studio <liste de fichiers>
|
||||
$> arc -b <liste de fichiers>
|
||||
|
||||
L'option "-b" signifie "-batch" et vous redonne "la main" aussitôt les calculs terminés.
|
||||
|
||||
Si vous utiliser "make" (ce qui est conseillé) les controleurs générés et les résultats seront mis dans les répertoires :
|
||||
- Controleurs : pour les fichiers AltaRica générés.
|
||||
- ControleursOpt : pour les fichiers AltaRica générés et optimisés.
|
||||
- Res : pour les propriétés.
|
||||
et des fichiers suivants seront générés.
|
||||
- rapport.pdf
|
||||
- rapport"login".pdf
|
||||
- FD-2022-2023-M1-CC-rapport.tgz
|
||||
|
||||
|
||||
Pour le rapport, vous devez compléter le fichier "rapport.tex", les questions sont indiquées en commentaires.
|
||||
|
||||
Le fichier à transmettre par mail est le suivant : FD-2022-2023-M1-CC-rapport.tgz
|
||||
92
projet.alt
Normal file
92
projet.alt
Normal file
|
|
@ -0,0 +1,92 @@
|
|||
// node vanne
|
||||
// state debit : [0,2];
|
||||
// init debit := 0;
|
||||
// event inc, dec;
|
||||
// trans
|
||||
// debit < 2 |- inc -> debit := debit + 1;
|
||||
// debit > 0 |- dec -> debit := debit - 1;
|
||||
// edon
|
||||
|
||||
|
||||
node Vanne
|
||||
state debit : [0,2];
|
||||
state panne : bool;
|
||||
init debit := 0;
|
||||
init panne := false;
|
||||
event inc, dec, estEnPanne, estRepare;
|
||||
trans
|
||||
~panne |- inc -> debit := debit + 1;
|
||||
~panne |- dec -> debit := debit - 1;
|
||||
// La panne est une transition comme les autres
|
||||
// elle intervien de maniere non deterministe
|
||||
// comme le Zabbix
|
||||
~panne |- inc -> panne := true;
|
||||
~panne |- dec -> panne := true;
|
||||
panne |- inc -> ;
|
||||
panne |- dec -> ;
|
||||
debit = 0 |- dec ->;
|
||||
debit = 2 |- inc ->;
|
||||
edon
|
||||
|
||||
node Cuve
|
||||
state niveau : [0,4];
|
||||
flow
|
||||
amont: [0,4];
|
||||
aval: [0,2];
|
||||
init niveau := 2;
|
||||
event time;
|
||||
trans
|
||||
// On modelise exactement ce qui est dit dans l'énoncé
|
||||
amont > aval |- time -> niveau := niveau + 1;
|
||||
amont < aval |- time -> niveau := niveau - 1;
|
||||
amont = aval & amont = 0 |- time ->;
|
||||
amont = aval & amont = 0 |- time -> niveau := niveau + 1;
|
||||
amont = aval & amont = 0 |- time -> niveau := niveau - 1;
|
||||
amont = aval & amont = 0 |- time ->;
|
||||
edon
|
||||
|
||||
node Controlleur
|
||||
|
||||
edon
|
||||
|
||||
node Systeme
|
||||
sub
|
||||
// Valves amont
|
||||
Am: Vanne[2];
|
||||
//Valve Aval
|
||||
Av: Vanne;
|
||||
C: Cuve;
|
||||
Ctrl: Controlleur;
|
||||
assert
|
||||
C.amont = (Am[0].debit + Am[1].debit);
|
||||
C.aval = Av.debit;
|
||||
sync
|
||||
// d decremente, i incrémente, n nop
|
||||
<ddd, V[0].dec, V[1].dec, V[2].dec>;
|
||||
|
||||
<ddi, V[0].dec, V[1].dec, V[2].inc>;
|
||||
<did, V[0].dec, V[1].inc, V[2].dec>;
|
||||
<idd, V[0].inc, V[1].dec, V[2].dec>;
|
||||
|
||||
<iid, V[0].inc, V[1].inc, V[2].dec>;
|
||||
<dii, V[0].dec, V[1].inc, V[2].inc>;
|
||||
<idi, V[0].inc, V[1].dec, V[2].inc>;
|
||||
|
||||
<iii, V[0].inc, V[1].inc, V[2].inc>;
|
||||
|
||||
<nii, V[1].inc, V[2].inc>;
|
||||
<ini, V[0].inc, V[2].inc>;
|
||||
<iin, V[0].inc, V[1].inc>;
|
||||
|
||||
<nni, V[2].inc>;
|
||||
<nin, V[1].inc>;
|
||||
<inn, V[0].inc>;
|
||||
|
||||
<ddn, V[0].dec, V[1].dec>;
|
||||
<dnd, V[0].dec, V[2].dec>;
|
||||
<ndd, V[1].dec, V[2].dec>;
|
||||
<nnd, V[2].dec>;
|
||||
<nnn,>
|
||||
|
||||
edon
|
||||
|
||||
162
rapport.tex
Normal file
162
rapport.tex
Normal file
|
|
@ -0,0 +1,162 @@
|
|||
\documentclass[a4paper]{book}
|
||||
\usepackage{fullpage}
|
||||
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[francais]{babel}
|
||||
|
||||
\usepackage{latexsym}
|
||||
\usepackage{fancyhdr}
|
||||
\usepackage{makeidx}
|
||||
\usepackage{graphics}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{longtable}
|
||||
\usepackage{moreverb}
|
||||
\usepackage{listings}
|
||||
|
||||
\newcommand{\altarica}{{\sc AltaRica}}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Master 1, Conceptions Formelles\\
|
||||
Projet du module \altarica\\
|
||||
Synthèse (assistée) d'un contrôleur du niveau d'une cuve}
|
||||
|
||||
\date{}
|
||||
|
||||
\author{Nom1 \and Nom2 \and Nom3}
|
||||
|
||||
\maketitle
|
||||
|
||||
\chapter{Le sujet}
|
||||
\input{tank}
|
||||
|
||||
\chapter{Le rapport}
|
||||
Le rapport est sur 20 points.
|
||||
|
||||
\section{Processus}
|
||||
\subsection{Rôle du fichier {\tt GNUmakefile} (1.5 points)}
|
||||
% A COMPLETER en expliquant les enchainements des calculs effectués.
|
||||
|
||||
\subsection{Rôle de la constante {\tt nbFailures} et de l'assertion associée (0.5 point)}
|
||||
% A COMPLETER en expliquant le rôle de la constante.
|
||||
|
||||
\section{Résultats avec le contrôleur initial {\tt Ctrl}}
|
||||
\subsection{Calcul d'un contrôleur}
|
||||
\subsubsection{Avec 0 défaillance (0.5 point)}
|
||||
\input{LaTeX/System0FCtrl.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 1 défaillance (0.5 point)}
|
||||
\input{LaTeX/System1FCtrl.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 2 défaillances (0.5 point)}
|
||||
\input{LaTeX/System2FCtrl.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 3 défaillances (0.5 point)}
|
||||
\input{LaTeX/System3FCtrl.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsection{Bilan avec le contrôleur initial (1 point)}
|
||||
% A COMPLETER
|
||||
|
||||
\section{Construction d'un contrôleur initial plus performant}
|
||||
\subsection{Rôle du composant {\tt ValveVirtual}(2 points)}
|
||||
\includegraphics[height=.2\textheight,width=.5\textwidth]{Graphs/Valve-modes.pdf}
|
||||
\includegraphics[height=.2\textheight,width=.5\textwidth]{Graphs/ValveVirtual-modes.pdf}
|
||||
% A COMPLETER en expliquant sa sémantique et son rôle.
|
||||
|
||||
\subsection{Rôle du composant {\tt CtrlVV} (4 points)}
|
||||
% A COMPLETER en expliquant les mécanismes mis en oeuvre, leurs rôles et les avantages de ce contrôleur par rapport au précédent CtrlVV.
|
||||
|
||||
\section{Résultats avec le contrôleur {\tt CtrlVV}}
|
||||
\subsection{Calcul d'un contrôleur}
|
||||
\subsubsection{Avec 0 défaillance (0.5 point)}
|
||||
\input{LaTeX/System0FCtrlVV.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 1 défaillance (0.5 point)}
|
||||
\input{LaTeX/System1FCtrlVV.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 2 défaillances (0.5 point)}
|
||||
\input{LaTeX/System2FCtrlVV.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsubsection{Avec 3 défaillances (0.5 point)}
|
||||
\input{LaTeX/System3FCtrlVV.tex}
|
||||
\paragraph{Interprétation des résultats}
|
||||
% A COMPLETER
|
||||
|
||||
\subsection{Bilan avec le contrôleur CtrlVV (1 point)}
|
||||
% A COMPLETER
|
||||
|
||||
\section{Une première optimisation des contrôleurs pour améliorer le débit aval}
|
||||
\subsection{Une optimisation basée sur les priorités (1 point)}
|
||||
\small{\lstinputlisting{ControleursOpt/Optimisation.alt}}
|
||||
% A COMPLETER en expliquant en quoi consiste l'optimisation mise en place.
|
||||
|
||||
\subsection{Calcul des contrôleurs optimisés avec {\tt CtrlVV}}
|
||||
\paragraph{Avec 0 défaillance}\ \\
|
||||
\input{LaTeX/System0FCtrlVV_opt.tex}
|
||||
|
||||
\paragraph{Avec 1 défaillance}\ \\
|
||||
\input{LaTeX/System1FCtrlVV_opt.tex}
|
||||
|
||||
\paragraph{Avec 2 défaillances}\ \\
|
||||
\input{LaTeX/System2FCtrlVV_opt.tex}
|
||||
|
||||
\paragraph{Avec 3 défaillances}\ \\
|
||||
\input{LaTeX/System3FCtrlVV_opt.tex}
|
||||
|
||||
\subsection{Bilan avec la première optimisation du contrôleur CtrlVV (1 point)}
|
||||
% A COMPLETER
|
||||
|
||||
\section{Une deuxième optimisation (3 points)}
|
||||
Il est possible d'obtenir de meilleurs résultats que les précédents par au moins deux façons.
|
||||
\begin{enumerate}
|
||||
\item En utilisant un meilleur ordre pour les priorités entre événements.
|
||||
\item En introduisant cet objectif dans le système de calcul de point fixe des actions du contrôleur.
|
||||
\end{enumerate}
|
||||
|
||||
Vous devez proposer une des deux optimisations conduisant à une solution dans laquelle le débit de la vanne aval est le moins souvent possible décrémenter, voire jamais. Pour cela, vous pouvez~:
|
||||
\begin{itemize}
|
||||
\item Meilleur ordre sur les événements.
|
||||
\begin{enumerate}
|
||||
\item Modifier le fichier \texttt{ControleursOpt/Optimisation.alt}.
|
||||
\item Faites \texttt{make}.
|
||||
\item Quand vos résultats sont satisfaisants, notez les, puis copiez votre fichier dans \texttt{ControleursOpt/Optimisation-2.alt}.
|
||||
\item Remettez le fichier \texttt{ControleursOpt/Optimisation.alt} d'origine.
|
||||
\item Faites \texttt{make}.
|
||||
\end{enumerate}
|
||||
\item Meilleur système d'équations au point fixe.
|
||||
\begin{enumerate}
|
||||
\item Modifier le fichier \texttt{Spec/System.spe}.
|
||||
\item Faites \texttt{make}.
|
||||
\item Quand vos résultats sont satisfaisants, notez les, puis copiez votre fichier dans \texttt{Spec/System-2.spe}.
|
||||
\item Remettez le fichier \texttt{Spec/System.spe} d'origine.
|
||||
\item Faites \texttt{make}.
|
||||
\end{enumerate}
|
||||
\end{itemize}
|
||||
|
||||
\paragraph{Le nouvel ordre}\ \\
|
||||
\small{\lstinputlisting{ControleursOpt/Optimisation-2.alt}
|
||||
% A COMPLETER en décrivant les résultats obtenus
|
||||
|
||||
\paragraph{Le nouveau système d'équations}\ \\
|
||||
\small{\lstinputlisting[texcl]{Spec/System-2.spe}}
|
||||
% A COMPLETER en décrivant les résultats obtenus
|
||||
|
||||
\section{Conclusion sur la synthèse de contrôleur (1 point)}
|
||||
% A COMPLETER
|
||||
|
||||
\end{document}
|
||||
39
sujet.tex
Normal file
39
sujet.tex
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
\documentclass[a4paper]{article}
|
||||
\usepackage{fullpage}
|
||||
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[francais]{babel}
|
||||
|
||||
\usepackage{latexsym}
|
||||
\usepackage[?]{amsmath}
|
||||
\usepackage{fancyhdr}
|
||||
\usepackage{makeidx}
|
||||
\usepackage{moreverb}
|
||||
|
||||
\newcommand{\altarica}{{\sc AltaRica}}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Master 1, Conceptions Formelles\\
|
||||
Projet du module \altarica\\
|
||||
Synthèse (assistée) d'un contrôleur du niveau d'une cuve}
|
||||
|
||||
\date{Lundi 30 janvier 2023}
|
||||
|
||||
\author{Alain Griffault}
|
||||
|
||||
\maketitle
|
||||
|
||||
\input{tank}
|
||||
|
||||
\section{Conditions générales}
|
||||
|
||||
\begin{itemize}
|
||||
\item Vous pouvez utiliser les fichiers sources de l'archive {\tt FD-2022-2023-M1-CC-sujet.tgz}.
|
||||
\item {\bf Groupes de deux étudiants conseillés, de trois étudiants maximum acceptés.}
|
||||
\item Le rapport est constitué de l'archive {\tt FD-2022-2023-M1-CC-rapport.tgz} généré par la commande {\tt make}. Il sera envoyé par mail à Alain.Griffault@u-bordeaux.fr
|
||||
\item Date limite de remise du travail : {\bf vendredi 3 mars 20223}.
|
||||
\end{itemize}
|
||||
|
||||
\end{document}
|
||||
158
tank.alt
Normal file
158
tank.alt
Normal file
|
|
@ -0,0 +1,158 @@
|
|||
node ValvePerfect
|
||||
state rate : [0,2] : public;
|
||||
init rate := 0;
|
||||
event dec, inc;
|
||||
trans true |- dec -> rate := rate - 1;
|
||||
true |- inc -> rate := rate + 1;
|
||||
rate = 0 |- dec -> ;
|
||||
rate = 2 |- inc -> ;
|
||||
edon
|
||||
|
||||
node Valve
|
||||
state rate : [0,2] : public;
|
||||
stucked : bool;
|
||||
init rate := 0;
|
||||
stucked := false;
|
||||
event dec, inc;
|
||||
trans ~stucked |- dec -> rate := rate - 1;
|
||||
~stucked |- inc -> rate := rate + 1;
|
||||
~stucked |- dec -> stucked := true;
|
||||
~stucked |- inc -> stucked := true;
|
||||
stucked |- dec -> ;
|
||||
stucked |- inc -> ;
|
||||
rate = 0 |- dec -> ;
|
||||
rate = 2 |- inc -> ;
|
||||
edon
|
||||
|
||||
node Tank
|
||||
state level : [0,4] : public;
|
||||
init level := 2;
|
||||
flow amont : [0,4];
|
||||
aval : [0,2];
|
||||
event time;
|
||||
trans amont > aval |- time -> level := level + 1;
|
||||
amont < aval |- time -> level := level - 1;
|
||||
amont = aval & amont = 0 |- time -> ;
|
||||
amont = aval & amont > 0 |- time -> level := level + 1;
|
||||
amont = aval & amont > 0 |- time -> level := level - 1;
|
||||
amont = aval & amont > 0 |- time -> ;
|
||||
level = 4 & (amont > aval) |- time -> ;
|
||||
level = 0 & (amont < aval) |- time -> ;
|
||||
edon
|
||||
|
||||
node Ctrl
|
||||
// les observations du controleur
|
||||
flow r : [0,2][3];
|
||||
l : [0,4];
|
||||
event ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn;
|
||||
trans
|
||||
true |-
|
||||
ddd, ddi, ddn, did, dii, din, dnd, dni, dnn,
|
||||
idd, idi, idn, iid, iii, iin, ind, ini, inn,
|
||||
ndd, ndi, ndn, nid, nii, nin, nnd, nni, nnn
|
||||
-> ;
|
||||
edon
|
||||
|
||||
node SystemPerfect
|
||||
sub V : ValvePerfect[3];
|
||||
T : Tank;
|
||||
//C : Ctrl;
|
||||
C : Ctrl_SystemPerfect;
|
||||
state ctrl : bool;
|
||||
init ctrl := true;
|
||||
// d pour dec, i pour inc, n pour nop
|
||||
event action;
|
||||
time;
|
||||
trans
|
||||
ctrl |- action -> ctrl := false;
|
||||
~ctrl |- time -> ctrl := true;
|
||||
assert
|
||||
T.amont = (V[0].rate + V[1].rate);
|
||||
T.aval = V[2].rate;
|
||||
// liens avec le controleur
|
||||
C.r[0] = V[0].rate;
|
||||
C.r[1] = V[1].rate;
|
||||
C.r[2] = V[2].rate;
|
||||
C.l = T.level;
|
||||
sync <action, C.ddd, V[0].dec, V[1].dec, V[2].dec>;
|
||||
<action, C.ddi, V[0].dec, V[1].dec, V[2].inc>;
|
||||
<action, C.ddn, V[0].dec, V[1].dec>;
|
||||
<action, C.did, V[0].dec, V[1].inc, V[2].dec>;
|
||||
<action, C.dii, V[0].dec, V[1].inc, V[2].inc>;
|
||||
<action, C.din, V[0].dec, V[1].inc>;
|
||||
<action, C.dnd, V[0].dec, V[2].dec>;
|
||||
<action, C.dni, V[0].dec, V[2].inc>;
|
||||
<action, C.dnn, V[0].dec>;
|
||||
<action, C.idd, V[0].inc, V[1].dec, V[2].dec>;
|
||||
<action, C.idi, V[0].inc, V[1].dec, V[2].inc>;
|
||||
<action, C.idn, V[0].inc, V[1].dec>;
|
||||
<action, C.iid, V[0].inc, V[1].inc, V[2].dec>;
|
||||
<action, C.iii, V[0].inc, V[1].inc, V[2].inc>;
|
||||
<action, C.iin, V[0].inc, V[1].inc>;
|
||||
<action, C.ind, V[0].inc, V[2].dec>;
|
||||
<action, C.ini, V[0].inc, V[2].inc>;
|
||||
<action, C.inn, V[0].inc>;
|
||||
<action, C.ndd, V[1].dec, V[2].dec>;
|
||||
<action, C.ndi, V[1].dec, V[2].inc>;
|
||||
<action, C.ndn, V[1].dec>;
|
||||
<action, C.nid, V[1].inc, V[2].dec>;
|
||||
<action, C.nii, V[1].inc, V[2].inc>;
|
||||
<action, C.nin, V[1].inc>;
|
||||
<action, C.nnd, V[2].dec>;
|
||||
<action, C.nni, V[2].inc>;
|
||||
<action, C.nnn>;
|
||||
<time, T.time>;
|
||||
edon
|
||||
|
||||
node System
|
||||
sub V : Valve[3];
|
||||
T : Tank;
|
||||
//C : Ctrl;
|
||||
C : Ctrl_System;
|
||||
state ctrl : bool;
|
||||
init ctrl := true;
|
||||
// d pour dec, i pour inc, n pour nop
|
||||
event action;
|
||||
time;
|
||||
trans
|
||||
ctrl |- action -> ctrl := false;
|
||||
~ctrl |- time -> ctrl := true;
|
||||
assert
|
||||
T.amont = (V[0].rate + V[1].rate);
|
||||
T.aval = V[2].rate;
|
||||
// liens avec le controleur
|
||||
C.r[0] = V[0].rate;
|
||||
C.r[1] = V[1].rate;
|
||||
C.r[2] = V[2].rate;
|
||||
C.l = T.level;
|
||||
sync <action, C.ddd, V[0].dec, V[1].dec, V[2].dec>;
|
||||
<action, C.ddi, V[0].dec, V[1].dec, V[2].inc>;
|
||||
<action, C.ddn, V[0].dec, V[1].dec>;
|
||||
<action, C.did, V[0].dec, V[1].inc, V[2].dec>;
|
||||
<action, C.dii, V[0].dec, V[1].inc, V[2].inc>;
|
||||
<action, C.din, V[0].dec, V[1].inc>;
|
||||
<action, C.dnd, V[0].dec, V[2].dec>;
|
||||
<action, C.dni, V[0].dec, V[2].inc>;
|
||||
<action, C.dnn, V[0].dec>;
|
||||
<action, C.idd, V[0].inc, V[1].dec, V[2].dec>;
|
||||
<action, C.idi, V[0].inc, V[1].dec, V[2].inc>;
|
||||
<action, C.idn, V[0].inc, V[1].dec>;
|
||||
<action, C.iid, V[0].inc, V[1].inc, V[2].dec>;
|
||||
<action, C.iii, V[0].inc, V[1].inc, V[2].inc>;
|
||||
<action, C.iin, V[0].inc, V[1].inc>;
|
||||
<action, C.ind, V[0].inc, V[2].dec>;
|
||||
<action, C.ini, V[0].inc, V[2].inc>;
|
||||
<action, C.inn, V[0].inc>;
|
||||
<action, C.ndd, V[1].dec, V[2].dec>;
|
||||
<action, C.ndi, V[1].dec, V[2].inc>;
|
||||
<action, C.ndn, V[1].dec>;
|
||||
<action, C.nid, V[1].inc, V[2].dec>;
|
||||
<action, C.nii, V[1].inc, V[2].inc>;
|
||||
<action, C.nin, V[1].inc>;
|
||||
<action, C.nnd, V[2].dec>;
|
||||
<action, C.nni, V[2].inc>;
|
||||
<action, C.nnn>;
|
||||
<time, T.time>;
|
||||
edon
|
||||
28
tank.spe
Normal file
28
tank.spe
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
with SystemPerfect, System do
|
||||
// propriétés universelles
|
||||
deadlock := any_s - src(any_t - self_epsilon);
|
||||
notResettable := any_s - coreach(initial, any_t);
|
||||
// Systèmes réactifs
|
||||
control := any_t & label action;
|
||||
uncontrol := any_t & label time;
|
||||
SR := any_s & ([T.level=0] | [T.level=4] | deadlock);
|
||||
LossCtrl := src(control) & SR;
|
||||
WinCtrl := src(control) - SR;
|
||||
LossEnv := src(uncontrol) - SR;
|
||||
WinEnv := src(uncontrol) & SR;
|
||||
/* Classical equations for
|
||||
* - winning strategy (| for lfp and to reach winning states)
|
||||
* - controller synthesis (& for gfp and to avoid loosing states)
|
||||
Winning = Win |& src(WinningStep);
|
||||
WinningStep = Step & rtgt(Loosing);
|
||||
Loosing = Loss |& (src(LoosingStep) - src(NotLoosingStep));
|
||||
LoosingStep = Step & rtgt(Winning);
|
||||
NonLoosingStep = Step - rtgt(Winning);
|
||||
*/
|
||||
WinningCtrl -=
|
||||
control &
|
||||
rtgt(LossEnv &
|
||||
(src(uncontrol & rtgt(WinCtrl & src(WinningCtrl))) -
|
||||
src(uncontrol - rtgt(WinCtrl & src(WinningCtrl)))));
|
||||
project(any_s, (WinningCtrl|uncontrol,empty_t), 'Ctrl_$NODENAME', true,C) > 'Ctrl_$NODENAME.alt';
|
||||
done
|
||||
90
tank.tex
Normal file
90
tank.tex
Normal file
|
|
@ -0,0 +1,90 @@
|
|||
\section{Cahier des charges}
|
||||
|
||||
Le système que l'on souhaite concevoir est composé~:
|
||||
\begin{itemize}
|
||||
\item d'un réservoir contenant {\bf toujours} suffisamment d'eau pour alimenter l'exploitation,
|
||||
\item d'une cuve,
|
||||
\item de deux canalisations parfaites amont reliant le réservoir à la cuve, et permettant d'amener l'eau à la cuve,
|
||||
\item d'une canalisation parfaite aval permettant de vider l'eau de la cuve,
|
||||
\item chaque canalisation est équipée d'une vanne commandable, afin de réguler l'alimentation et la vidange de la cuve,
|
||||
\item d'un contrôleur.
|
||||
\end{itemize}
|
||||
|
||||
\subsection{Détails techniques}
|
||||
|
||||
\subsubsection{La vanne}
|
||||
Les vannes sont toutes de même type, elles possèdent trois niveaux de débits correspondant à trois diamètres d'ouverture~: 0 correspond à la vanne fermée, 1 au diamètre intermédiaire et 2 à la vanne complètement ouverte. Les vannes sont commandables par les deux instructions {\tt inc} et {\tt dec} qui respectivement augmente et diminue l'ouverture. Malheureusement, la vanne est sujet à défaillance sur sollicitation, auquel cas le système de commande devient inopérant, la vanne est désormais pour toujours avec la même ouverture.
|
||||
|
||||
\subsubsection{La Cuve}
|
||||
Elle est munie de $nbSensors$ capteurs (au moins quatre) situés à $nbSensors$ hauteurs qui permettent de délimiter $nbSensors+1$ zones. La zone 0 est comprise entre le niveau 0 et le niveau du capteur le plus bas; la zone 1 est comprise entre ce premier capteur et le second, et ainsi de suite.
|
||||
|
||||
Elle possède en amont un orifice pour la remplir limité à un débit de 4, et en aval un orifice pour la vider limité à un débit de 2.
|
||||
|
||||
\subsubsection{Le contrôleur}
|
||||
Il commande les vannes avec les objectifs suivants ordonnés par importance~:
|
||||
\begin{enumerate}
|
||||
\item Le système ne doit pas se bloquer, et le niveau de la cuve ne doit jamais atteindre les zones 0 ou $nbSensors$.
|
||||
\item Le débit de la vanne aval doit être le plus important possible.
|
||||
\end{enumerate}
|
||||
|
||||
On fera également l'hypothèse que les commandes ne prennent pas de temps, et qu'entre deux pannes et/ou cycle {\em temporel}, le contrôleur à toujours le temps de donner au moins un ordre. Réciproquement, on fera l'hypothèse que le système à toujours le temps de réagir entre deux commandes.
|
||||
|
||||
\subsubsection{Les débits}
|
||||
Les règles suivantes résument l'évolution du niveau de l'eau dans la cuve~:
|
||||
\begin{itemize}
|
||||
\item Si $(amont > aval)$ alors au temps suivant, le niveau aura augmenté d'une unité.
|
||||
\item Si $(amont < aval)$ alors au temps suivant, le niveau aura baissé d'une unité.
|
||||
\item Si $(amont = aval = 0)$ alors au temps suivant, le niveau n'aura pas changé.
|
||||
\item Si $(amont = aval > 0)$ alors au temps suivant, le niveau pourra~:
|
||||
\begin{itemize}
|
||||
\item avoir augmenté d'une unité,
|
||||
\item avoir baissé d'une unité,
|
||||
\item être resté le même.
|
||||
\end{itemize}
|
||||
\end{itemize}
|
||||
|
||||
\section{L'étude}
|
||||
|
||||
\subsection{Rappel méthodologique}
|
||||
Comme indiqué en cours, le calcul par point fixe du contrôleur est exact, mais l'opération de projection effectuée ensuite peut perdre de l'information et générer un contrôleur qui n'est pas satisfaisant. Plus précisemment, le contrôleur \altarica\ généré~:
|
||||
\begin{itemize}
|
||||
\item ne garanti pas la non accessibilité des \emph{Situations Redoutées}.
|
||||
\item ne garanti pas l'absence de \emph{nouvelles situations de blocages}.
|
||||
\end{itemize}
|
||||
|
||||
Dans le cas ou il existe toujours \emph{des situations de blocages ou redoutées}, vous pouvez au choix~:
|
||||
\begin{enumerate}
|
||||
\item Corriger manuellement le contrôleur calculé (sans doute très difficile).
|
||||
\item Itérer le processus du calcul du contrôleur jusqu'à stabilisation du résultat obtenu.
|
||||
\begin{itemize}
|
||||
\item Si le contrôleur obtenu est sans blocage et sans situation redoutée, il est alors correct.
|
||||
\item Si le contrôleur obtenu contient toujours des blocages ou des situations redoutées, c'est que le contrôleur initial n'est pas assez performant, mais rien ne garanti que l'on soit capable de fournir ce premier contrôleur suffisemment performant.
|
||||
\end{itemize}
|
||||
\end{enumerate}
|
||||
|
||||
{\bf Remarque} : Pour vos calculs, vous pouvez utiliser au choix les commandes~:
|
||||
\begin{itemize}
|
||||
\item {\tt altarica-studio xxx.alt xxx.spe}
|
||||
\item {\tt arc -b xxx.alt xxx.spe}
|
||||
\item {\tt make} pour utiliser le fichier GNUmakefile fourni.
|
||||
\end{itemize}
|
||||
|
||||
\subsection{Le travail a réaliser}
|
||||
L'étude consiste à étudier le système suivant trois paramètres~:
|
||||
\begin{enumerate}
|
||||
\item $nbFailures$~: une constante qui est une borne pour le nombre de vannes pouvant tomber en panne.
|
||||
\item Le contrôleur initial qui peut être soit {\tt Ctrl}, soit {\tt CtrlVV}.
|
||||
\item Une éventuelle optimisation pour améliorer le débit aval.
|
||||
\end{enumerate}
|
||||
|
||||
Les questions auxquelles vous devez répondre sont dans le fichier {\tt fichier rapport.tex}. Elles correspondent aux interrogations suivantes~:
|
||||
\begin{enumerate}
|
||||
\item Est-il possible de contrôler en évitant les blocages et les situations critiques ?
|
||||
\item Si oui, donnez quelques caractéristiques de ce contrôleur, si non, expliquez pourquoi.
|
||||
\item Est-il possible de contrôler en optimisant le débit aval et en évitant les blocages et les situations critiques ?
|
||||
\item Si oui, donnez quelques caractéristiques de ce contrôleur, si non, expliquez pourquoi.
|
||||
\end{enumerate}
|
||||
|
||||
Vous écrirez vos réponses dans ce même fichier.
|
||||
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue