From a85bb57d9a4c19d7c6a69f2947e327879f498bd8 Mon Sep 17 00:00:00 2001
From: JOLIMAITRE Matthieu <matthieu@imagevo.fr>
Date: Sun, 10 Mar 2024 21:33:20 +0100
Subject: [PATCH] surete tp1

---
 surete/tp1/Exercice2.pdf                 | Bin 0 -> 18091 bytes
 surete/tp1/sequential/Makefile           |  22 ++++++++++++++++
 surete/tp1/sequential/always.ec          |  13 +++++++++
 surete/tp1/sequential/bounds.ec          |  17 ++++++++++++
 surete/tp1/sequential/count_succ_true.ec |  15 +++++++++++
 surete/tp1/sequential/count_true.ec      |  13 +++++++++
 surete/tp1/sequential/sequential.lus     |  32 +++++++++++++++++++++++
 surete/tp1/temp_prop/after.ec            |  13 +++++++++
 surete/tp1/temp_prop/always_since.ec     |  14 ++++++++++
 surete/tp1/temp_prop/build.sh            |  15 +++++++++++
 surete/tp1/temp_prop/nodes.lus           |  30 +++++++++++++++++++++
 surete/tp1/temp_prop/once_since.ec       |  15 +++++++++++
 12 files changed, 199 insertions(+)
 create mode 100644 surete/tp1/Exercice2.pdf
 create mode 100644 surete/tp1/sequential/Makefile
 create mode 100644 surete/tp1/sequential/always.ec
 create mode 100644 surete/tp1/sequential/bounds.ec
 create mode 100644 surete/tp1/sequential/count_succ_true.ec
 create mode 100644 surete/tp1/sequential/count_true.ec
 create mode 100644 surete/tp1/sequential/sequential.lus
 create mode 100644 surete/tp1/temp_prop/after.ec
 create mode 100644 surete/tp1/temp_prop/always_since.ec
 create mode 100755 surete/tp1/temp_prop/build.sh
 create mode 100644 surete/tp1/temp_prop/nodes.lus
 create mode 100644 surete/tp1/temp_prop/once_since.ec

diff --git a/surete/tp1/Exercice2.pdf b/surete/tp1/Exercice2.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..2877de8c07ccad294b096f5dcdd83befa5c5c185
GIT binary patch
literal 18091
zcmch91zc6l*0)HfAdSQ!MH&t*A>Ex)g5;q)1(og&NhxWOmPWc$LRz|8>G;k8G4As`
z_rCZ2zTe08?3g_>duFXYYpwr(W=knAEK1MJz=lLwzEyaJ#0p>nSUopI;^6@>N*h`l
z+nWH`z)6Zo004kd6l891XbV1?>)9I$8|qsb7$WiUA=%m68tPdfIVY)v6r;XkLV<CU
z+d~d-Aw?S~eL`dE4ZsGZ>b)S$8IXvjpKidH%~cnBz>^h&_8hAZ<uUhSP#~%H3m>~S
zK}7iS=LAq=A$p7me0Z;0Ouoq*f65Xmq^7)JxbpTmUDw<3_sGuVdE`M<hGb}I@Z+iA
zGe~<Ojf5P*&17ccfZT^%0e|-9y8R-~_F_u*;I;#JcpwSjKSn(!@CATTNC3bLVAR(G
z@4-C+-?-T`s>?k$HPpAi&g0AuV28*8au59P$1@;FkZ1iSF)m21>nHx5#2`;qcCj`D
z+*W>_Q_11E{dJ<Km952filCsCGe8qu6%&AsogKiz#s<*7zM*JnXXRk4Z)gYLynYb4
zEk9LI_h#B^k`v|A?1kE~0vv%#I$s@Q>Vs2j_$jCd`=i8g91ayzl(NQ;R}W`ND7gZL
zDnXbZg(BJ_3?kDzNI+NO&g+-!R%<SeLsl|Pim^2Bl`@ny;?}-#L1PW=4pteGISuiJ
z+Ds$Zn!fL>3S@jrLkZi4=QoTXRn?0fx8@v?BqwIxGLW>#T16Je-_891ktLpODbbul
zAYy#pQiowm_i1_Q`U4%PhZa?p-J-gkEYLFR&qJH1B5P1~a^jqx&M$XWC&$Pf_8-ex
z;mJe8nG-)N8D^pJzCW6-=g9&p@a$u%XAibc2)UABXrIBLo7jwEiO(c_6S<t$L%aXZ
zT+Lz0ar7%clz~Q1;*d5{NmE^Qyvwo6Ts^1dsD&BJ(~)g7+hr>$@v}Pn=iU_MxZ~a=
z7Io{HG8;=|T6058;{}$r%lm%Mg!9;?k}^btS)630?dXRvvH>nB8Lb~p_6kfjK33*T
z=<bzNI}tOou;$l)PjQrW<>AC@MUUj;WRF`#M?vf^_<Ay-2X}!-2&d_%VtK_?Mb8mP
zoYWRIRIaGJByC#HSofyF&|T*I(zA4C(^8x`TMA!@-lRU@KzvLFx90Ndd~u69Aoh_(
zuxpN|mhpx^ku@F?R#%+pk+~j`Y4!v|%)2+ZRYhkdACk?Oyx>w^wb;PvauRaCe$j!5
zfUJxpKl&}{lcp04CzU8qa7bl3OFwg+mXV&$l0QOEffL`t?g8l(`Z#`xgTna==h(Xg
z107$w7n2-kW341F8;%YbQm5a@b{uz$!1=zYela`h^U%B#bXMvv+I2{drYB3ELYgBq
z<-JgekL=FQdE#qNnBU48j5T6`r>=VNY+KSQ%g6#jgR%7Sn|vpdDbtr|B<xX>>PKJf
z=JRV}K5x84+OIS5+(ego*UpsphK?6tbJ7LN@|4X)c%HIAW+XFS1@qZxiCEPJV6}2m
z;X${+9K8+TEqzxwxh20x&ZCDqiL=~IT<kb6XN(a=pA3!=SheTY!o?`jeT4gFw#yyq
z5k7X{hCAegeDSPTZAJDi&e-BIo%6DNuo#s%-7?O@uK?lDcIN^?B%0l?M=B_voaspD
zy5f?KocAb##Y%ic!<hr1E=usiRPOAz-q}DdCdCU=ekH=BnX-dhtrMJqWyz%W@?M*E
zk{Rv_RRFa1>Jx`LAqPBR2lMy2@&qu1>D8Q}>%{~56LS_<>x1;dVh*!Tu6Y@so3MCf
z9Z1oXraS!wIv?j{R6ih5eZBtp5Q|80g_1$0!iizJlV@DSs&U6^!mDQDlXk%z1MgIw
z9a-f^S&lwfG*O+5hf&&iFO0mVo?ajsgk_SD)z~elksvS(f9NzgC<1z~McBq`B2|UE
zyKkYVx6rVL0$CmU-JstPcgG<CQPQZ1^<6tMm9}u(6boFwT<~`}@a|&4@YRVYd#ybp
zVzfu{gmSO~ECMI(=n%e)0Cyh+A)Y5_9VyIsvttxTm<QBPW(Nrf$3-gTm*c?CT6HY=
z6C?9J`4+T3W?4E>*MY9tVmWIvyks%fUuZLF!%XUg&{kShpHx1}`*@>hRsVQGpyDa{
znE-i8!Q(wK1fs~!qsfke((>2a7m9%I*+hl|KE_NQUPkqWXcE--?&UQvm-j{)KH27M
z*PO-nD9g)t#eL|dGnWw?t|fIskP7bqV3VBL)p^PB1jC2U-ZqstlE%|Ez8^4)F!3n_
z7C6TS^asLy`4mabWvfJ-w{!9CT&dSLVwR%ltd~pEC4d4CbzRmLF8kv+?+jEuP;<v%
z_C6~{f{Hey{H_C9+gXXQa5hrlxAJ(#KU<eXiT8c3KDm$&AZTfN$MP+743bFT@%@is
zVL%NjAA#&|4693{)~!G~yM&|~MiIIK_j9fj621oQ>c9Fah-<j@Q>-kkw@w6N$Zwp;
zwT1s*I4V&qONf_(6o)t%BYGx!Ca^2Kb`U?)m?3G*f2OfO(pdgX1JW}Cm?6&d+Kb)P
z#|%k>ga^N+u|mrJj1T^BiyYvbw{G#q+sQpQRkFWvZ9gIl=4*F)-D6n*^Yu{_WNT*+
zVEu9a@52q=-a4cvCM?*mb#gX1D_P}%f~x~atpeezRA`hsl5rG^Vw;nR!t2iUZk5?^
zw47ot&rs58LoxNd^6n@WW%AH4`J>>v_UdQzI}1PmLUhE*%9e8S#cWA`I_=~LKHm#!
z<x%GOWJmQ7eI8K^5G2Jw`*zMEmF;`6L;4Y&1d4W3Meh|X7f}I)pT$h@IjnCM%h_M`
zeci>M3g^7lH}fxr|BSPk|8v;zGf03)lv(JH;43B?B(1E5)js=5EYu<}$K4~Ry!`zH
zWx_<J>V{%Sw19<n8Vwn>q)N05j6h>Zyq@kQbaM}2mFZOkHNt|YdO(@Uh)GCWY$dB{
z{t#<LmZ@3Z8j&sY8WEMuX`_dU&J0)8PO@A7PD*d;_q7as6yM#B%;*9XeNorLRpyL#
z6JNfBEd1feUHlX+{1jNWprgudVS+q9!|(Sx3^AbAh|$9n?z``xylCS}z`=+)av2Sb
z{*F1sqV%~`&5!~#Ax<v~G-aM>pOB_keURQex(q5U<C-v@u(v2=mwAAmuH|RCQ1;oE
z+1H?%%?sfvks={C=kWb?#Ea5?tiY_(dUA~I2ImI1ywGf=4idyBu1H?V0A7m1NA8gZ
zPY@pm@JI8B@RB^achqlx8sb{j39?D3vO#4l1WALmn&Bfm^&AqnaC}=0Dm0#oc5r}{
zw%ckwwYKRf_hR1&J&#V3N@nkxO;-C@9Qqk8lSKOQC)x%;e)FPd)SP_{A=)8PntLy5
zy?d{g_Qw0YVVkm$MR~4>#h~X{*v{1LvWQU80hf(o-&)GMOP@EAkgd}Y7jve`zoiI*
zvPD<-UBKi*|G*rWqfB7gg}!(9nD)h*g@vwhRW}qzvmR|}O!51!iqER8`#E?YYWh-Y
zPl>)jRl~itX{U>IT#}hWZ*CDHIx<PI9Rzyy!F!gzu`ZpPoa8IC8HpM3v`H}1-4E<>
z2?oq{hkZNWg4N`}w$-?lR6;topu524XYw#V+af*2OXzL4{bJ~VT@^U4v$fyU%t_&=
zl7Mw3^@aidi7!)uK^*Bv-++}ydXx9NE-o)otGbfw)N(3RC-dBh0;eWv9<K(hzdH~c
zv@g~XqtI5!r^Uj5!a`V`kBhBtR}>R*0r;5bogZXo&i0kIa{AT7;EgtNpyOUiV6Lo|
zZW+<6JIqut)yAdZp++8ZolzmDNI*^8wmM3RuMIw4Yj~9R0h$2}xurxOnKj+K*}@TA
zMD0CjanW^Ulw^a=!OL>_tD2zJjZ1l=IFKw;A?{rp8FH<Oy)nkG7rXIhrC(~&%!yd=
zHO)2eejPe&=&8WS+tP8ykK=IYWZI=`$u0<433<k7l?1EfAHT*W<%vH@<9i0bo_B1V
zA0pT6c_x+PVqw;XU$p9HM|L+1|0vF1KoPpXz3ICI?bGNElW7)*#>(QaOK)DHZ=o<p
z%7Z3fONyRx&~JTxYi*0dr$}@+sCQqkz8X^np6c6j{$l}`EkkEfVOvC8-Ug@Fi30|O
zXZ`ua075#h=-HkJp;V(3aL3E<du36$-FCmc)KGhxUfjhJx=sDa={`<e=oRr)D5i?o
z;eITdWViN57i?$zp7uGVu^h6!JeDm0zC4-dGCTmdbMkG`GuW9<t?wz`f##<%($f>i
z%N}dmniT`}E$bqT=)hWc6W!<tcQu!Hb`Qs_@@8k`d$3a{IcL`@JFPL$tPU(p<_}q_
zk!g5jq#{ftX>_HE$4%kla;(Jj<(!H-3yG~sO>Fg~S*e&5r=Ql0+T@nkB8bpb#-`7c
z&BU5@in5cxXR%Vlc`Gxf?Z}~}dyj|xUL~<TniIYMbK$PbNySEH=WMt*Jo+<tKccBQ
zlJpvZxB+x8pJ0)38$0B2n32gmBv}^O%{5Ln47xYc5nEv+hF_LJAB22aW-95LTXj`v
zFe*u#0Llk}MG~GPfafQHbi)?1oY2kNZF_|^OPhBc=6Zx{+uua<D7J36Q%tc;Bc&u;
zEAb3Y9#)JxzRG`sTWk#X94{XPv-pKh99q9IZ5;QLu}yKwd!J%5&KPz~9!ELd$f>8p
zY<H6ij5>Uu6fZvB-#VdV?{;z!#(ch@$PfEaZ_cueSyCnR!*F?ZRp+?56~mUu@dM-~
z=>5NO0)KdYX0BT=zyfj4w@&hhPh|P&p8q4<){f}6YzCmT?eO@7O{O79)ELFcXXe%{
z7V&FTz>7E9iz5qo6Yn23SFUFgeInt18T!12`>?;x2{G@8a{~%feMP3luwFRCx~cRa
z-SQJ>a^VNt4G>CtS8H=MMUtzPaT=B~30GBSWz%$2yqq)RomAH#xQqki$}?`XU|%T&
ze$F&GfXLWufkgfz7T+-&!5qoGEDo-nq3TY<m!bV^0M;e#1ID%SulGemY`z&|Np_({
zmnT25x?Ec4jY}%HB+ihp@iUKMflr%gPq#xi?SJvixw)3K-msq1UDq9O?;!Trk&fGM
zlX;VQF=8{Kh0RWe;3>I_<K{SqRs6?HdNZkNBkef256SZRWl@tT-znR8>PsqFI1=6*
zI8R!<fmVq*K-S=l>iercu4VkgDYJ0>WD8gzQP8bAZekWlR3&U^r*8|gwzsmqiAump
zvU(O^`2JK`R8dxeR!9$IYX!*&3At{vnClta-3Bq>8$XdeJqr^Mz|O%2-~dNbH(*}E
zUe6q)FJNhGZV0$3Enuf_2#)2zS*|OCJRWilDSMqDq-QN|2r@SLl|{+k&_Wf!c~cy6
zA%1%SX%?7+Fa!dwBM!yic#G@U@UOkSe#D<~#&wdQo}J-!jQMZ64T;@^O!RC4K$hz=
z(t1CxnOS}a2Hc!q;sjg^{5qUu6tM)eNgzvO0HYenQozy<benKpks8Rr-o)+)83GwJ
z|INn24vAX-y0NiCV$}c5#>xgM$;twWkbmqsAfYS^%T0}tBL^EhfR&3GzzV(tIWmET
z!Uh1cgMX~I?O_FS-n<21LdZ(R5(FXC0M|z0cST)4=2lU+R^n$M{<l^F60!fO!#`ui
zcd8(HWi=cRR4v{Fn6W--85&@Kbg)e)UK~<@8wDO4wLdNO8QFS~zvnB!v?Is#1=~Of
zT?zYFI5NvO)YM4ZnuOhN-Z0~1$Jr?A-#314n^=`)y1l`!a>C4SWO}MHtF}{ru+6pd
z7`&Nak&uXF3?BCd%W5Rve-l}2*`ul7Mnga%qQJV(Kk+>>ZiCXwKWC<B#{95ks*5DG
zPyu?R+%CMD#@6Ms=j)YqX!`l#dk)-|51I|^T)d>NGDE@9Uj}Kf@S<YzIT&ai&b^O}
zXu5O_U$N*QD&sr~ijg<0FOiRbSDOv<$Szt>vgm$lZEBC|@*`jjY?tDayP^O6EN^Nd
z?DzB8=Q=0JajZj{fsD!wrdc5K1T!7?TC%$OZyuj(M$R&i+~1<|y)Au$(~Wi*Ka>4#
zr>OpA2150Wl|)0~W&Y_iXNGT8rMnLJ#MPBJ2jduJT%p7FQ(}S4=+fJ}{N0mW{ZUd(
zMCuGE+{r0Tm@6BCPhO42aa>$f;9PFTMpw0-FUfv5RM^p?_ef~A?Bex^*;CNfqz{Jo
zZ!Vzma)+ggJz!L~(Cdv|zh6CUzs$o&9$oT+PyE>79<(9pWCAR~qe9b0TD+Zmj;OQP
zWx*NqG9rmZ0Y%hQG(17iIYh|`C{88c7Xrqt3kO9D0>q<YeRTKgzX78grfZvPqmE%g
z9fs589kLpw9O*_r=LQHyT@AW0n6y~#t}qK;PugwLPY2K@=BXbE<EQm4mT^mz9e^gf
zO2zu0-Nnw0-Aqv<l5W~MZ>V>Yc+iT@K8X4T$<xF@U6tzsDF-=OWowdpg-|o9ijM=T
z>@MuI38gjWLc_t6{F!5PoK#o&eIHt3V#g@G82Vhk_@rF=Hk<($t@n>#_@lR3=GY(@
zMXAvDqU?CL%D}biJHS>ir8zAkgNB}+h{vUigz-ept&tsx@kGu^Hiw+`Dr?Tu<wZr*
z&^%+5)*zk_P0RNVvqc@8M@pPKX(Otn^9@=G+j;G%_i?Z)#S|E*7$MnFS}g=1Brfhn
zVXM&SXsJrMc)|mp;J5V11|!7_zJhm9qokK>*}MctJ(vk&)T1G7N|0??!;F3vZhNy4
zv+3RL0%>_!fon9P8X~;r13tK|#u?98o;-HdwY(5z8y_Ez0&2~>34w?bcp`7ch{uy9
zh`9JCn3IbP*4hx{ndTqh?(9=6=k8D>?Nlw;YCD+az&E4?oAG=(%UM2SihkNHFT2WZ
zy$h2A8*-ZL+Vs@-l&b?4wfTI|+3V}WX^9KutL#Gqsr&=XaH7rVG(M~#1lo9#mS}qf
zE5Y5@<6}><ZE|bfNk|8wU(z;@rSX1v)r4Lcq#*`(kac$vlVuCPLVBK?StCf^_g>Se
zJA$OJ32G<?cSFIrRW_BIlEP<T-qQ4@Ohk*MBgsT!PnHY&NP!E%xt-(j!3+Af;<NoV
zz6aU+HpdK!6%Ps!T1TJDqXs(049jl~PJ||8D64C%=D_T2>8gxYe+s0a(VRqIEs{@b
zEtJG<wxqqA3=QP^-q$OO^mR_@M6oIoly7skEExHy6l$6EvuFZUY#-Jf6j?C4@j6gu
zs2Ef$*zJD&R^1TZ4AX0zD577uH~|kXWhHPh5XvRWhpx~aQ9mr?MM-3mudAIGYc@YI
zZ$xeQ(=A}kJ?syXZS`aY8u`%sWK-+a-|u|8^KhosxoP+dMzg@Bx~t07K$N3Ep~93@
z&2t%p>J~ecCd&new3XH5_Eaj?c*kX>_x0QjqGGKhJ|iL{2DByPdJi|Th4MxvwHce9
zImZk0d&(+?OrzIFei#lY><V*=Y}V0O%tb>j;XW^clSCg26xbv$V&@B=V|Qy8+Avl)
zd!|0pXU)4(?@U|<V>dKJ*3s4A&|c%Ta@9C;rC8uKSBmNco9ke2DY<{Y%ZydkSVbYh
zE=HftgfI4CyBJ?SA;-(PDZSBHd+LSE;AbRS%R+n5bCxJCWxhWr^#o?zpHd0L<#|6w
zkWH7!LX71H>o!33apCFQXkOsZebbytl?vo<Y<wP4@5-SP-}}A|8jg~EN{l>}=lU$x
zgsDf5_DF<-KAiMGBz&MLY_|<@FP{Y21o?}EJqPiWTvJE8ncl~0@)rkFbv3CMCSBHT
zQQ9jVr4j^4FMZ#HtAIpV)ZcLrzz84W6;_QLo~lWDU@uJ^1Rmtb99IOshWBB_UU{zl
zUNY=?46*U2gsL%t!tplz@#I!n&Q2<PTumG`9JxM;Nh*uC(ud|7a3`IQVgf8JRnm(J
zbCM1Z1pJO)xxYXkr`?JXiD7MSvd^UxZz*wRj!mQdFft&x#+&Ojb{L+P^0Y#o=p@xp
z_kmtFZAW(SlUNoSQIlZ(4jSfMTI+;$6QUi=);gt1-z?`(3#O?pYIKDT5lX5GX^mRr
zP=5KS=pRTh8|J(O9$LR>zpV2%Bo2;>uVm1N^&9D}W(=EtnTgZ!8J{x104S*AEz_@P
z%qp~)6jMy&ILLv@!9xn1vJo-OFRYk~HLnY?+i89#>3Y_S@J3_<IND9po6?H{Ck18i
z-P-d#aM(2@fU%&UrnGcpQQ`D_$cwfFt^;NbxR<tS_K^3>Bto$4i)1>gQh`Iv#IzQ5
z^YoJ1p`^eUVWZY;&zBJUyw`<Ik<5|I(K6BIT9IT#s1nVe;K0@KY0k%DCSp^!`zdF}
zWW|IpK#!VC7+J!&doBaNYum?%)qHxWwTNjFR64w7J!D=az1Y*MDS~JvirP;io5h{~
zc`<W%M~x@+G!{ixYE4u=6@Ht)(ib#1Cp+{O&dubVF??jGK?iZOVe^8}C+wyzXFkED
zcCwyc|Imjz0Kqcf+@OatFqFCi$Y_#d3vcR9r0pK$z&~u$r;+$7qq+d}CaLZ!Lv`yS
za2gv7P2gR!)!_^{6s7~bz#}H84Hyc^t*}QX^-qR16NV<Rw}0-wAXsh%D+*hifB5;S
zA6Z|1u6`ej(R1juSL1fc<C+I+)`DuwYj-D*%8fnT?y=PDNo=kS;B?V<malNH+8#v6
zjf7s97<_D4Kh2B@5HMg)?4<^%Qx1f5VvqOJO}A#7xrA`nNb9fbc4ik_EpFX)6SC0S
zDUw)s1~JEfD`QUX#lfOJ?Tdugu;d1=_fU;9SjCz#UM!G}*>`wT=T6R3jel;GrjrM8
z&nFrSJ>>A>g(InI@N5t*0`ho#pKn3RW6b^dxI3qAPx-MdhR5!iGKxd^o72w#F8yuY
zbIOj!=!T-a7cc_-OpKhS3TUksfnL&}!LZpVMVv!~P0mnF?$OVe1r==JLb99dnIrLK
zEaa*r`c!k-8uJ^cNwgDm(`~hMM6CrutaNb?gIgzG@KhGaosYfUThnSgA}3@a?8sd2
zRXG`P&8u$48SVd&#Arwk(7_^k(lI9uv%4Zf9T(LrVjuH%Mn>gbkAjwZ&QNiqvXzCk
z{+ZRKaJAjvz$Hkqc?*}=xR`#z*V{?g-=;oUeo?xAH~0DbRHb(0EqsM--<J3B#ZpBS
zNvM`WJIgS1dxa&93nKN;^sB#MD&z+Fwea^G;XlmccI?;2Q`4!-9zQIy<%f&Yjc4q<
z%irjNVy<S#G4Z{E#_BO@gv$8TvpDQ5hU0kr=KQeQs)DsH4mnG{M(BkkHLFemg64Ru
z`cU3?r&7WEOakgvx)$9;$6DKl{vVoQYH5}&R`xF|bv}+CW*^szesy@dlSBFVvHH9&
zDe4?b55l1Bf_pch@}-+%_|oFmQTUsP8aiw;cq3ElBxvASwKZB#j{6+pn?ad5LKY>R
zIG#0!K_wy|hqBDtmfG}M!7MxMlzh5k5k7Ph7LH6%V4Knmxsr?zo7w(o>zVk8n1R@4
zcrJ%e9VjoiIBT?pfbE+$QiD{a4i4}4jA9ace^}ET_yAt<eaUa^ixvZu;Z*R1En8s=
z;=9{Z#uki^mYCy^RhNUJh@hu-bd$)dyAF`8bjvLNMx(cr)?lCjWC#9K=wC_ue+z)+
zHKc@9Wq$*};Q57Xyarw%@Q(nP6^v||0356={}BMQ-k`|e0PqbW{tW>C$nrk{z}GP9
zcU*Nn5ps*Ge!>0g4*Ut8u9JQN;D7G+zX8BMrZ@ft07C@+{{#TD+yKz)Js6a7K|trP
z-#>v|b~a7`J3AAA9e4{#|2`)>D+Iv)^9BLAY+$Xjg7e)TfncfwymA4Y%JQRj$dQBd
zM^13-Aon0YAQ%P%Il)J8YarL)_FVUa^>)R>AMp5Qy6M;Y3zol`N@4jgrc#6?gds0E
z<ON{*6D8{#=<4a|8W=3v$@b87Id%8b4zdli8R#15>FVmjJkKCu;WwypS@aMGUW6NM
zZ(m}3FAXe@6O+K9K8hEE6;|2H@yt>5Kp&^*_=LhLqfXGu(;j`EsoWnuTpQUFDG3Kh
z6+YObd+^$vN>p??$+DiLd-e(e%VFJU>(IFFF2$99kq*2fzp#3P-JP|Cf`+Qs!%iZj
z+aaIPb~cvPhk3I>ve5AI>27+`P8J+~Pn{xF6Up0;mKuD7Yp!6P*uxiTyqu+*uxNC>
z*HP1MI!NE;w@Y}hqZQ?eXM_^Moo`8!?SEq!eq$=ZEXJ*2078^<J5+v95WxR}s0?p3
zZDvC8-SI#osu8joYL+Es0vr0RwjsV(`rYw*5h3%0`-e(X1C223;#XJkvqLM}bs6CT
zFKx?sjdouXE)e2YAV7z{R(8LOYd%wBJK0I`4t9HtYhgGdED!YLWdNtK&fM<u{3}MJ
zJKx|RFFqkB++Mk4UXP3Ruomo+&#i#<(@Cj$W6y@^$*@~&m+n_f40~obHR^3m<9^|9
zkkQPAA7pMKJff^f&#IHBBEJ2$Udij@tZz^a4u|T9na$2Y$RythiXpC1rxLq@r#Z&m
zIlHHivO;K9a7Bu&6aFg3YuVg-Ocu7EV*D=&Mkz@tSw*Ek?CTFR@=x{^JOtUmgY3UI
zt~Yl3e`#5NE<?IqcJ*uB)$LLz$PoL}vi?5q{>8xlW52;=lw9n<1gC_hkrkv6B=S%+
zGzNj!Ke+&?1;C5G3?D(#!GDZ$wg!f_5K56+!T?O5g6v&>-coX~wl+7kfY7Sf9S2(z
zNQpn49hk5Kzx6lPSq-4cbWK09fmN%m{X30%8yrEJ^6$LJjf8)Bk$>#uE%OOrylpqV
z_;vGc9HD_8n9>DH6GDdqujlA*h~!@k;`M0#-P2v$-+vvxKd0^gR}5l^DzbXCA<ktL
zA+NK{^ti@WiD7(2?mHLU;bCQ_)*4SO73G#!P>b^&C@6NkKrN$66fY(dny;|ZciFIe
zdsyii-(>|fl51F2StK5!x(}Dm@-Og}pKbE>^YOp9I_ST8x$=02YsaO3FXH@yl7!?f
z-)H?%TFhDT7qkw?IddPx`7R?VPW-RproCQFd!74hK2A>7aF#qbSf~9k7}mLgd$Fi;
zU+V4g<yC7aMcuLL{5l)6O>S2jraq?cyLZwPm3kwIpO<@(wQ8+Td(^}XGL1#wzjPU1
z9isr%W6|_R&xGs58A(WGiYUHf6;EKOd-Od#Rx;?_!*?!2S|DFmL04H<34%ww^dS+V
zQvFgwnU{*sKt5$!NKsjmjfz&FSKr_zNKwCIU!EZf$?)}`VjZJ>n_fJ7&3J&kH~H0R
zWJmJ~@bWInG4kd%&VYs8$G0^r_KaH|_|VL7jIh%8#P4z9Sf{lY5r^=4xoNnuf8&`o
zll?&A3a>!&(F@gyKP$DHDfv}(Y?FhHKK>Ju7`{yakKCE+AYrC?X~M90?WZ$7_?#g{
zkr;6`mdDQbn$QEK)iDEv1NkhWm1^{{Yu}pQkMoE3*Y@CWu{uOa^Lq82zTq$=<b<5d
zJNXrJ0V9cU$5oGn9z!}=3F$QV-Uv|>8aLl-QF7SUx?`R>P7NEbqtLN>uf4u<q<J;c
z3Xfc~fG<Q(kdL1b1b*9ue{p9+%Gon?%QYJc6yHAG$NBZGQ%pDfmmGw(?xXFghvu1|
zJIe?q=u<)7QH)SNy}@DRghIv7Og^~vBRSl=kidvV&({*?jL*`}+=+0flhzr~LN;sk
zo*u*=^bP`v>`#o~5v4H4Et9P^HbHOO@{hhP@(JZibWD3cVEOKTCQV(pmd`mtVgWV(
z=NH>7bCjk?<^2Md5pq%%hWD^!Ycg6u?d~x<U(nD~(uhh87)yJ{$)JS%`^704NP8_j
z4(`uAIxQ=xA_mcG#e6P-Use4!Hr4J+;E9bDj~Nl@B3drc7N_$@PeLqf=>rWlo=M|*
z*^)PNSwR9?#`o3lffqjNn(A@Sq=>(6HaFDZQfDD%q*;ql`8L^kYC`p>P02yS+nhn=
z3~PzL6W`h5w2!gQ1|>R*5f42Aj6LtB669?(NWe|tLj5jzA9qMt?<~%5JBaKhv~F3u
zN22<PYHF*Y02!ct&E#b6qs;;6%bUU;oHc*4Y32#P7P?O<-&5#kzua*aa{Na8psyOs
z9@ohEWCO89GS%!czs0Oy47*yr)RXEvjjZhKhQ%EDaz&1oDmlqCeiH$VMVEW#WW{4G
z82TIP1JH+JbavcChO%0+;j;Jvn#vuNGiKOtC0_*Vc9l`p2cs^!4-}S~Cfi2(kT}c+
zyc*;@mQ1?B4qni1aN8}aP@&plv>_HH_J!V<mEo1?s2+sPO7#<WY8tom?5Ol#&K7M)
zd}etEh%~fL^#OrE22U!8AV=Z+yo6)fP~1;;hhOrTccejB31&mwc+|}<&h21OL9K4_
z?Rw*j5~X}<C9cwL<>PREoo?uWFl=3&pcTw#UoRBiD;nmj+(oX;$;+AwkbYiAFs}Uk
zE=wX#bL`&hf_tVx!H4t|WaL8CkA#+czv`{vWFDV8j7Zu)Ix;yzPkC25B8CR=af`=9
zdTpEH1P$9J91@WmR~ZwE_<3vIhlxFPj|54`RR_tCjFPv5j!n-ecSu>n*@xRS;Djt0
z+3aZ%wi>4&{@Pu|&yNe85RVk<^sLxbSG(+J?A1>Zy{&?%pNew&h(7G_M0aLhjxy)T
ztcw*R6{l_fEK<dgn$soXR-2Z0Rw&c=S=N(c=3WBgjA0m5d86|o$;n26G5M4`_BZ_6
z%N=f)ip}=P64}xA!Gc-)lHDt}mv?d+hf^nl645^7phRhFzNz#;r21G}?p9quYsXHb
z=K3hV`a5+t?vndO<GS~Q_n&m;ItNTW3ld~%SRD1{U$?YnifT>X^%b-z4(FDNcwdxy
z=V;r9=&|GGL@{)7pJcW^Z72(L*j&D_Mv3>fo4w_+TwqU<w1W|vrTqKB_vAg4coxs5
zWyiub66<k1$A#e!2%=3mzSujGYvcuLFWz_gO1_1Y)+jgRJd^0mn8{PLZ%H(zhBJSZ
z+iFt@7vz!slHp!z-?N4t6pUA%OHb6fFG%^zIeTM$cMbwpPSp4OMDoZ~(vbLZdC8l!
zp(h!jFXr!Y7)Zi5>w21(EaI2t%pf$r*f%Gxd?hF99?RaH6hL*??ww=42d!^ODwnw;
zQ)2KsH`5pT3iGDM{XKG1IwZYQWE|9j1l>eL%iS1Vjz;>s+75+M8%@+WcOnX$U^eJg
zgY`U8r!5P*$gq+Xt=QK@s(kh%&^z5k_g;y==JADIG+fNu@a~f}MDwW|RZvn48p+n0
zZz^#WtFz#b4TP@Qqy6-r_;T6}%Lk3IP@%-C`|4EFMBLk#&A}b+v6^5mBA#<Yl$nIE
zmz6D}p8_2MtLoE;)|oENZI8fSs`3POazjqGNyO<UM@p6PTmq1$ssxSR7}Q-<5FLRa
zJ*Za$xbEUDXxO2o#6Fa@pF~icACsCu69h^WPs~%E`HuQJ0>yyU4aixQW|uW3r5?W-
z{1(@<;b@Q0{(}1DLADi%04NURhWG^;1`SG|fFA)HWS#iRuXJNTb;Ki}UbIArILi4b
zOoy(GK9-)s+xOmbx*C%o0zu=-xA%Hi)O7Niyeef(+(r^`ZH6DRM&_F>_gyZgIf$th
zRdN$!2!gu<nG5eTiVnfB2Ydkvn!!!$zLw5elQ2~!Qc9Px`ix8y_fc^5(8bWM^&_o6
zf8Waew+~J2v);(y6eBc+tqFIo@vhSOrr*t1Nde@2A6YiF(wnIn<I)5q!ET#C?XlQ9
z#6`s3#S~5lezI~|p*$?*pb6r^93nbmZY9+$O_PB6*o|2GHXEZv)yggE?NoyxTBDJq
zTyIw+8)%M8u+ko;%78_&5Pf8}Y{Q9{DoY%pgk0ZDRRm{-2&J#5?!hDYM-M%`XfQG7
z?~hWo=&8CI`O*++if|A$Eki$OTj@?(p?%6-gdTebv!xlpM|}L*oRC8E$zi3PWK~g5
z$~saEmy1f-yoLgyPq{o6Dt75tnvX&fC0e}m^lp+Sb?BXlFK`WdUL`Rxso}Nw<SC_Y
zidQGwKlmPcuBafU$MPg<D5tTdxKn>fG{e!$h_^N4>286-=NztAp!bhBqO8)3TjWh?
zFwz<Hqj?``YL-_#Ct^pnAa=CIi=}DI>mSn;J_ADGOS?v4*hLp{IewOoxT26Op~TH_
zNM;^<*G?1FtuFFK)S>6Y@_iixrPO-&my<J&boO5eVV9mq`k-{7bcVL0MzPCE;)nT4
z3uT!|w%w0(7uTD{K@g}6o1ht(>^({MHga3v=6m+OgL%zPf>yNazC~3|>IICC0dR7$
zaqOwEY$j5gNlA%mZ&iAV>7pykWqykAWb9-v!d`|4*J}_KYnPHL5wYI!>~xn<9=lU?
zlS^*l)`KQZdn25HZ9ap|;PC?{iCkr>hx+p9i%a;ZEab7CZbg3Y&!vD#JQKF_iwd=_
zm)j3p?yQ*)RqaAoRxsr8kdcg}BM+Q+s0a;aa;%F#^!pNN{26<-m}0X2o%Dgpa>E9L
z3KlkQG#1W6N;AD1fAqVn4pR+(to!vQ9_(4Gk#vu!GF^5t8XYG@N2;88zHhZsh?cBH
z03Tw&DO!K-0?y-=_7w<u-R}|9lUN)^D7TBZ+T`jl`!=op+(R5UL$-g?D?v~uVj_@)
zgOFF`8QC<6;|oGPbf1DC1c4|8<v^%Tl;|4XT-J?<w`}Hlo+@2Y9awUV7$;YW+46o}
z0&giw`Nv>Dd!I_HQ|=s4RqDLw9P&6{Zk${-opSl&icbF=XIaX-_~qSrZQFvsft$BP
zEEvSFaIrG~#GAJ?-){sh@E7Iup9$JV%Sk45;hj??;wT|Nd}a#)Ito^2t6!$bw8tyq
zLM<p}%7OjHmn3Kp#a|Os@X;H`Wh{;Mx5w!xaj0BL2l01iWpVjZj4j31<|y>p6*y}6
zj9a~ZwzS3AtTDoMV&7nC%hd+TJ=Ga$*k5*#a{9i@OP9f;Dw%sKh7`H%ta|TdiX2L^
z<;E!kZa|`GUb6sfylvH(p8Era^!3PddlZ+KGuv`pTW{x&+_B$vABD!A-(Rdo(-}hV
zSNtwxCx5|8L=!OAz*}nE#d*>oly@pyQU=<ObRm<|m8$p}JLT!LNK{Gg6i@UW%{9A|
zyYy0(lTpRWx5=fmYS@0jK4mj)R;fXZC}qRC5NP1VO}-J_f!c$r+g5WwyWVR?Q9rHt
zo7LRxK3z~L-I?wnyinci`lXlU#~)%-G@UC7tfbse%XUHPv#Iq)G9d|}?$)bbb_VcS
z@bLHO&t_vUfit9q<0K)Mc&<#lx~q-RDFenj)@yG+25qz_dGy9Kyo(mgL$QmelpZ8p
zGMgDQ6j62IyHmT{z4bThzol)#>Sty8xyBgGs{JBuej(Fe>u-Ky-kar2q5>Ln;xfOn
z4d9jGH(CCPZJ=ji<pOYUfC&dSFe<*z`_Idn*lwtcUu-Tb*L8{CIENou{wHkiHKhF=
z<6bXezs0z}dVBqdf6M0nbGQFnHuqZK|5t1-kQ2g$Li7e^O*tTHz1c$;U9LZVzqnXP
zj+<N@*Cnp`Q}Fj<5LOpb6B`$#o?kUW&Nv}DW4d_`I3Fv-ez1cX*uUFuYGnoAWdko}
zX9X`_x;+A!Amt$ZE~F+_aJwOA99%zgfLjc?3j}k*Ku#cdo&mxQU$+Z<#R|TH{I1`c
z-}zl2B**WH1>RDUzZo%BNX0jj{yQTE;c|ZJ{CA$|Kl8hz|Aya<KXm6cV+@O=li$V*
zL-Nm?SAbP`cMd3#2!D-ll2F7N=o0$qL?SokQLYPRJY@_DiZmc2zHu3PTsk<o=WzN3
z|H{l+y=qxjX<=GTU`EYz)#fJ4P!hSCrz?*AiBom2GTih=h9fOQ`4g+3KB#`+N>I&}
zP?K1bP{UbWBXWYiy#&SO2_-y*arcfF;bY{#+JS4S{9qlKxma$!z%_S&J2HNdw_t+s
z-wE)KX}WM3(-tNapCdk>*w3wB1I9?@vl8h}g+3F1Dqb390&}-?wr4acOg>2F;WKAF
zrQgb5u06sTAW52f1uIC=Uzr(0)a0*3F@m={7?Y9zG0{R*<Ex$~QXj8R<^;~SY=5aa
zRM~#MkmJldPZ~<aLRlNv&bX(<niCFCjWh4!jyQZ}?y&p7-Y||YpmsdvHmE<|=Xt?Z
zUlFWpIy*&PwP@2hN~)P4UyhrLHUSuUL~$j@pTk^9(mgWmKl!Fj`G|S8>LMyk-qJ9Z
z#{rYAgP8O_Uu=xhOs=a36x&y8qrZ{jElCS;roX<>Vf}kf^B=9LfU2~JxX^Fb6#Pxi
zzqh8~Nipz(NEYzm_z$KOoaMTvTT}Y4-0kiC|B)TNnJM`-opQZ6@%C-`Cp-H4n7VGt
zFIw{-`~ClyyS-M|zi_t@OZF#s`}aEitIzmX?)D!$`Co9i*Me63SMK(Du>NlTu5I(J
zK5j?vjg5qux&LVXAS(QqFNG}RHN}+`uy}zB5h0!*Dg*p6^bq0=^r#ic5?;ro&Ap;n
zCZ_`qFwu7-I_UKED7MEBvOIiHzRDaw;unJ+e5!EY2q(5q3h8t=8=*=qltdf$>QvpV
z_{g_>Y=!^_tA&+7MqPEhb0Wc=ZNx$1kwm97W((fuoG*DTrZMV7!Zo&5oh=K)qXE0v
z3?b@s6CKz_G@u6Ii*`Tedb_iVGNR!3#tL+vtwj!W>iOIo>b!300V6%2AoQ#kXT@a-
zO}4C8Fxw(yAt}Vwe4JB{VNL@twL2bCEJqu@W{Kd?VwY`4uIe>qZ4zX<r?tvHDBPJ}
zjUP^Um&-#IRse0X3?L}5#5t;^l0V9&h4xB6g|S^ok%NKyB}L}Jox6S6I!(6NxQOdK
z$+WclDM7t?)cjT0vFx-RuVS;PfJ6lyOh%qXrfJHI`0q3lPlDG75$_8LJ|qrAw~3QB
zeju0eT7Gtn3BeS;0Xl4UA)}#W<>RJK^z`t;&fc@b&+jyAn@8qM?J&8y;QF5B!;kAZ
zeHm5l5ZO<Mf$wKtF?tXhIilNu04?C%9Z_TW-Ye;A3EI9dsKdtF$&U(cibBb+6J(wt
zF+16QoT^iZ8KJb7D(sKPD-4tNRbkD9NSpbHpw2N5ef)k>s4OSq2Wb7b0!q%RYvV#D
z%N-0u*`9|ByYk&)BOpaV-1eU6E6P>awg<IOVKg;q&AsdJ*-lcmR^3CaMoZvnTO+Mp
z7f*OhaO}jwCB?=2`WZ6MZQT_Fn9K1{jacs&tb4up<|$Op<A3(Gn;U*-=fO8Lt#`!{
zpDy;`S%KV-L!X&?nqZu2i>K0y)6z<i*7RBm(Khz!t+7|r*`HxKJ>~AT>^Aj%Ie^0I
z_%{X^@^=4lW9)1{C(l@Kquk%)07&5R&vC#XZcM%#{ILXj?E$u%G#bVil}y6$cQkd!
z17&%W_dXR>in9TN?_Hi1l1jcK)-@&pKGyKqdgi*rvU`N}?G=8(0oC07(M$}{q$Fb*
z<hHdJ{aqi7vGE`77t!Od%uIgDgt-*xrOZY}>!%8KHn{U?HnMT?9LDd%hP+fW!NR@1
zRUpEsgYH1&RDK`_8~Lsv-*?|r2CIkZ7cws_G1BN=l<3!Vtpg<W6+Hy0d{&=mOfr94
zezv29pD{8^!+c_&B|%D!Zb@T_@UcP{Nx5P8)Ue&6)nc$de^c|&j%Ra&jnY=fQk8DU
zD7n4;slNZ?{Mu)_LC$|CT8O-Uh?a%*muP<vv3}Y7fAnon)f5z^fA?+R??C^(Z@Wec
zY+&s9{~sw_8_?e^>h%Y!w-)tRZ~tobZ~XNy*Y?ld{zs(1#(pE0KbL)gQPb^f`^#bc
zUwrq##t9i4kp0cs%{e4ShFt$8#J(O$e@Nu_p>-n>xxaj@%l0c|lm*-bAU7ZDGIQMY
z@jv|MATnXy;IDPjMUE~4Yf42-j1-@V+hkN?2(%<uBCw4<S&L@%JpFDeYz+*0Z0Bo-
zA03RiaAdF>9981Y&BKjc4lLioykol1#~V5T*t7{8RJ63X^Dsz+!cnL1W0z}YjE&AG
zF1Z7YAu|MRel?n`a*pW{6?caEzLK2>Rx;rn6*1Xn1YYF_hh#?$@1q<IJw>V$%!XjG
zS@pEBT)8QT(GB^1K71R3`7BPfr+(+W_>!>hP8<ba?_bT+wH$toA!g2>UvRViHI`6U
zG&H&v%@4N?$^CDAHptZwz;=@dJmJg?07rv2@qwb1l|2|d{d{X6)87EL8xZunk;Cq9
zM1rzGhua;uFbmkcv=dX;qD+71XxI%cZ^;na)!R7^?R<BN$CtY6fq#&ecFXJG)B5fY
zAXB4yj0mP-k$~0bfhM+;I9zvn;Ul1!Rt)YA!yDA6I>PjlP`iRDzCqGeyn?Jx1QGZ}
z&yqr3FA`+hw!p4&9JLBKBJU&4-^rG1OC4AUd7QJ^39Ib1h_X&Qz!~wt8v7A*0;-18
zSNaaP<9k$W#~<#8tZK-MGOh-mL%nJzOZ=;h?d<hz?VWAG;$!CE0J0-dQi{llBK;qW
CzGkHW

literal 0
HcmV?d00001

diff --git a/surete/tp1/sequential/Makefile b/surete/tp1/sequential/Makefile
new file mode 100644
index 0000000..a656f4d
--- /dev/null
+++ b/surete/tp1/sequential/Makefile
@@ -0,0 +1,22 @@
+LUCIOLE=luciole
+LUSTRE=lv6
+LESAR=lesar
+
+run:
+	 $(LUCIOLE) sequential.lus $(node)
+#	 $(LUCIOLE) $(LUSTRE) sequential.lus -node $(node) -exec
+
+always:
+	 make node=always run
+	 
+count_true:
+	 make node=count_true run
+	 
+count_succ_true:
+	 make node=count_succ_true run
+	 
+bounds:
+	 make node=bounds run
+	 
+clean:
+	 rm luciole.rif
diff --git a/surete/tp1/sequential/always.ec b/surete/tp1/sequential/always.ec
new file mode 100644
index 0000000..1951e70
--- /dev/null
+++ b/surete/tp1/sequential/always.ec
@@ -0,0 +1,13 @@
+node always
+  (i: bool)
+returns
+  (o: bool);
+
+var
+  V4_prev: bool;
+
+let
+  o = (if i then V4_prev else false);
+  V4_prev = (true -> (pre o));
+tel
+
diff --git a/surete/tp1/sequential/bounds.ec b/surete/tp1/sequential/bounds.ec
new file mode 100644
index 0000000..e68edf0
--- /dev/null
+++ b/surete/tp1/sequential/bounds.ec
@@ -0,0 +1,17 @@
+node bounds
+  (i: int)
+returns
+  (min: int;
+  max: int);
+
+var
+  V18_prev_min: int;
+  V19_prev_max: int;
+
+let
+  min = (if (i < V18_prev_min) then i else V18_prev_min);
+  max = (if (i > V19_prev_max) then i else V19_prev_max);
+  V18_prev_min = (i -> (pre min));
+  V19_prev_max = (i -> (pre max));
+tel
+
diff --git a/surete/tp1/sequential/count_succ_true.ec b/surete/tp1/sequential/count_succ_true.ec
new file mode 100644
index 0000000..6508862
--- /dev/null
+++ b/surete/tp1/sequential/count_succ_true.ec
@@ -0,0 +1,15 @@
+node count_succ_true
+  (i: bool)
+returns
+  (o: int);
+
+var
+  V12_prev_i: bool;
+  V13_prev_o: int;
+
+let
+  o = (if (i and V12_prev_i) then (V13_prev_o + 1) else V13_prev_o);
+  V12_prev_i = (false -> (pre i));
+  V13_prev_o = (0 -> (pre o));
+tel
+
diff --git a/surete/tp1/sequential/count_true.ec b/surete/tp1/sequential/count_true.ec
new file mode 100644
index 0000000..7b7f437
--- /dev/null
+++ b/surete/tp1/sequential/count_true.ec
@@ -0,0 +1,13 @@
+node count_true
+  (i: bool)
+returns
+  (o: int);
+
+var
+  V8_prev: int;
+
+let
+  o = (if i then (V8_prev + 1) else V8_prev);
+  V8_prev = (0 -> (pre o));
+tel
+
diff --git a/surete/tp1/sequential/sequential.lus b/surete/tp1/sequential/sequential.lus
new file mode 100644
index 0000000..d59a996
--- /dev/null
+++ b/surete/tp1/sequential/sequential.lus
@@ -0,0 +1,32 @@
+node always(i : bool) returns (o : bool);
+var prev : bool;
+let
+  prev = true -> pre o;
+  o = if i then prev else false; 
+tel
+
+node count_true(i : bool) returns (o : int);
+var prev : int;
+let
+  prev = 0 -> pre o;
+  o = if i then prev + 1 else prev;
+tel
+
+node count_succ_true(i : bool) returns (o : int);
+var
+  prev_i : bool;
+  prev_o : int;
+let
+  prev_i = false -> pre i;
+  prev_o = 0 -> pre o;
+  o = if i and prev_i then prev_o + 1 else prev_o;
+tel
+
+node bounds(i : int) returns (min, max : int);
+var prev_min, prev_max : int;
+let
+  prev_min = i -> pre min;
+  prev_max = i -> pre max;
+  min = if (i < prev_min) then i else prev_min;
+  max = if (i > prev_max) then i else prev_max;
+tel
diff --git a/surete/tp1/temp_prop/after.ec b/surete/tp1/temp_prop/after.ec
new file mode 100644
index 0000000..bfb2cc1
--- /dev/null
+++ b/surete/tp1/temp_prop/after.ec
@@ -0,0 +1,13 @@
+node after
+  (a: bool)
+returns
+  (o: bool);
+
+var
+  V4_prev_o: bool;
+
+let
+  o = (V4_prev_o or a);
+  V4_prev_o = (false -> (pre o));
+tel
+
diff --git a/surete/tp1/temp_prop/always_since.ec b/surete/tp1/temp_prop/always_since.ec
new file mode 100644
index 0000000..ca4f6de
--- /dev/null
+++ b/surete/tp1/temp_prop/always_since.ec
@@ -0,0 +1,14 @@
+node always_since
+  (a: bool;
+  b: bool)
+returns
+  (o: bool);
+
+var
+  V9_prev_o: bool;
+
+let
+  o = (if b then a else (V9_prev_o and a));
+  V9_prev_o = (false -> (pre o));
+tel
+
diff --git a/surete/tp1/temp_prop/build.sh b/surete/tp1/temp_prop/build.sh
new file mode 100755
index 0000000..e089fea
--- /dev/null
+++ b/surete/tp1/temp_prop/build.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+set -e
+cd "$(dirname "$(realpath "$0")")"
+
+
+if [ $# -lt 1 ]
+then echo "Usage: ./build.sh <node>" && exit 1
+fi
+
+
+node="$1"
+src=./nodes.lus
+
+
+luciole $src "$node"
diff --git a/surete/tp1/temp_prop/nodes.lus b/surete/tp1/temp_prop/nodes.lus
new file mode 100644
index 0000000..01247a3
--- /dev/null
+++ b/surete/tp1/temp_prop/nodes.lus
@@ -0,0 +1,30 @@
+
+node after (a: bool) returns (o: bool);
+var prev_o: bool;
+let
+  prev_o = false -> pre o;
+  o = prev_o or a;
+tel;
+
+node always_since (a: bool; b: bool) returns (o: bool);
+var prev_o: bool;
+let
+  prev_o = false -> pre o;
+  o = if b then a else prev_o and a;
+tel;
+
+node once_since(a: bool; reset: bool) returns (o: bool);
+var a_happened: bool;
+let
+  a_happened = a -> if reset then false else (pre a_happened or a);
+  o = (a and not reset) -> a_happened;
+tel;
+
+node always_from_to(b: bool; reset: bool; c: bool) returns (x: bool);
+var
+  c_happened: bool;
+  prev_b: bool;
+let
+  c_happened = c -> if reset then false else (c or pre c_happened);*
+  prev_b = b -> if reset then true else (b and prev_b);
+tel;
diff --git a/surete/tp1/temp_prop/once_since.ec b/surete/tp1/temp_prop/once_since.ec
new file mode 100644
index 0000000..a66656e
--- /dev/null
+++ b/surete/tp1/temp_prop/once_since.ec
@@ -0,0 +1,15 @@
+node once_since
+  (a: bool;
+  reset: bool)
+returns
+  (o: bool);
+
+var
+  V14_a_happened: bool;
+
+let
+  o = ((a and (not reset)) -> V14_a_happened);
+  V14_a_happened = (a -> (if reset then false else ((pre V14_a_happened) or a))
+  );
+tel
+