commit b7a1213f919951e2f1d548b5ae6abb457470fde4 Author: Yorick Barbanneau Date: Wed Mar 1 21:40:15 2023 +0100 First commit diff --git a/Alt/Ctrl.alt b/Alt/Ctrl.alt new file mode 100644 index 0000000..c2ff5ef --- /dev/null +++ b/Alt/Ctrl.alt @@ -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 diff --git a/Alt/CtrlVV.alt b/Alt/CtrlVV.alt new file mode 100644 index 0000000..33f8cf4 --- /dev/null +++ b/Alt/CtrlVV.alt @@ -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 ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; +edon diff --git a/Alt/GNUmakefile b/Alt/GNUmakefile new file mode 100644 index 0000000..f31601f --- /dev/null +++ b/Alt/GNUmakefile @@ -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) diff --git a/Alt/Parameters.alt b/Alt/Parameters.alt new file mode 100644 index 0000000..9765223 --- /dev/null +++ b/Alt/Parameters.alt @@ -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; diff --git a/Alt/System.alt b/Alt/System.alt new file mode 100644 index 0000000..054059c --- /dev/null +++ b/Alt/System.alt @@ -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 ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; +edon diff --git a/Alt/Tank.alt b/Alt/Tank.alt new file mode 100644 index 0000000..a31d857 --- /dev/null +++ b/Alt/Tank.alt @@ -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 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 ; +edon diff --git a/Alt/Valve.alt b/Alt/Valve.alt new file mode 100644 index 0000000..ab41b77 --- /dev/null +++ b/Alt/Valve.alt @@ -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 diff --git a/Alt/ValveVirtual.alt b/Alt/ValveVirtual.alt new file mode 100644 index 0000000..cfcee31 --- /dev/null +++ b/Alt/ValveVirtual.alt @@ -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 diff --git a/Controleurs/GNUmakefile b/Controleurs/GNUmakefile new file mode 100644 index 0000000..f327c4c --- /dev/null +++ b/Controleurs/GNUmakefile @@ -0,0 +1,9 @@ +TARGET = + +all: $(TARGET) + +clean: + rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core + +cleandir: clean + rm -f $(TARGET) Ctrl*alt diff --git a/ControleursOpt/GNUmakefile b/ControleursOpt/GNUmakefile new file mode 100644 index 0000000..f327c4c --- /dev/null +++ b/ControleursOpt/GNUmakefile @@ -0,0 +1,9 @@ +TARGET = + +all: $(TARGET) + +clean: + rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core + +cleandir: clean + rm -f $(TARGET) Ctrl*alt diff --git a/ControleursOpt/Optimisation-2.alt b/ControleursOpt/Optimisation-2.alt new file mode 100644 index 0000000..e65d314 --- /dev/null +++ b/ControleursOpt/Optimisation-2.alt @@ -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 diff --git a/ControleursOpt/Optimisation.alt b/ControleursOpt/Optimisation.alt new file mode 100644 index 0000000..e65d314 --- /dev/null +++ b/ControleursOpt/Optimisation.alt @@ -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 diff --git a/Ctrl_System.alt b/Ctrl_System.alt new file mode 100644 index 0000000..d703d6c --- /dev/null +++ b/Ctrl_System.alt @@ -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 diff --git a/Ctrl_SystemPerfect.alt b/Ctrl_SystemPerfect.alt new file mode 100644 index 0000000..1db1740 --- /dev/null +++ b/Ctrl_SystemPerfect.alt @@ -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 diff --git a/GNUmakefile b/GNUmakefile new file mode 100644 index 0000000..71e1f95 --- /dev/null +++ b/GNUmakefile @@ -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 diff --git a/Graphs/GNUmakefile b/Graphs/GNUmakefile new file mode 100644 index 0000000..4e53130 --- /dev/null +++ b/Graphs/GNUmakefile @@ -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 diff --git a/LaTeX/GNUmakefile b/LaTeX/GNUmakefile new file mode 100644 index 0000000..e20c694 --- /dev/null +++ b/LaTeX/GNUmakefile @@ -0,0 +1,9 @@ +TARGET = + +all: $(TARGET) + +clean: + rm -f *.dvi *.log *.aux *.toc *.bbl *.blg *~ *.core + +cleandir: clean + rm -f $(TARGET) *.tex diff --git a/Res/GNUmakefile b/Res/GNUmakefile new file mode 100644 index 0000000..5ca2533 --- /dev/null +++ b/Res/GNUmakefile @@ -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 diff --git a/Spec/GNUmakefile b/Spec/GNUmakefile new file mode 100644 index 0000000..696b7a9 --- /dev/null +++ b/Spec/GNUmakefile @@ -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) diff --git a/Spec/Graphs.spe b/Spec/Graphs.spe new file mode 100644 index 0000000..981d1cf --- /dev/null +++ b/Spec/Graphs.spe @@ -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 diff --git a/Spec/System-2.spe b/Spec/System-2.spe new file mode 100644 index 0000000..1580a88 --- /dev/null +++ b/Spec/System-2.spe @@ -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 diff --git a/Spec/System.spe b/Spec/System.spe new file mode 100644 index 0000000..1580a88 --- /dev/null +++ b/Spec/System.spe @@ -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 diff --git a/TODO b/TODO new file mode 100644 index 0000000..b08ed2e --- /dev/null +++ b/TODO @@ -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 + $> arc -b + +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 diff --git a/projet.alt b/projet.alt new file mode 100644 index 0000000..e6f995f --- /dev/null +++ b/projet.alt @@ -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 + ; + + ; + ; + ; + + ; + ; + ; + + ; + + ; + ; + ; + + ; + ; + ; + + ; + ; + ; + ; + + +edon + diff --git a/rapport.tex b/rapport.tex new file mode 100644 index 0000000..46fd282 --- /dev/null +++ b/rapport.tex @@ -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} diff --git a/sujet.tex b/sujet.tex new file mode 100644 index 0000000..6d147ee --- /dev/null +++ b/sujet.tex @@ -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} diff --git a/tank.alt b/tank.alt new file mode 100644 index 0000000..fe9206b --- /dev/null +++ b/tank.alt @@ -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 ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; +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 ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; + ; +edon diff --git a/tank.spe b/tank.spe new file mode 100644 index 0000000..bb05d4f --- /dev/null +++ b/tank.spe @@ -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 \ No newline at end of file diff --git a/tank.tex b/tank.tex new file mode 100644 index 0000000..c451966 --- /dev/null +++ b/tank.tex @@ -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. + +