--****************************************************-- --****************************************************-- -- Laboratoire Specification et Verification -- -- Modeling of an "AND" and an "OR" logical gate -- From "Verification of Concurrent Systems with Parametric Delays Using Octahedra" by Clariso and Cortadella -- -- Modelisation: Etienne ANDRE and Laurent FRIBOURG -- -- Created : 01/2008 -- Last modified : 22/01/2009 --****************************************************-- --****************************************************-- var ckOr, ckAnd, cka, ckb : clock; dAUp_l, dAUp_u, dADown_l, dADown_u, dBDown_l, dBDown_u, dOr_l, dOr_u, dAnd_l, dAnd_u, bpre_l, bpre_u, -- corresponds to the end of the high part of B -- following the rise of A qa, qx : parameter; --****************************************************-- --****************************************************-- -- AUTOMATA --****************************************************-- --****************************************************-- --****************************************************-- automaton input --****************************************************-- synclabs: aUp, aDown, bUp, bDown; initially InputInit; loc InputInit: while ckb <= bpre_u & ckb>=0 & cka>=0 wait {} when ckb >= bpre_l sync bDown do {ckb'=0} goto Input2; loc Input2: while cka <= dAUp_u & cka>=0 & ckb>=0 wait {} when cka >= dAUp_l sync aDown do {cka'=0, qa'=0} goto Input3; loc Input3: while ckb <= dBDown_u & ckb >=0 & cka>=0 wait {} when ckb >= dBDown_l sync bUp do {} goto Input4; loc Input4: while cka <= dADown_u & cka>=0 & ckb >=0 wait {} when cka >= dADown_l sync aUp do {cka'=0,ckb'=0,qa'=1} goto InputInit; end -- input --****************************************************-- automaton andGate --****************************************************-- -- Input 1 : t (output of OR) -- Input 2 : b -- Output : x synclabs: tUp, tDown, bUp, bDown, xUp, xDown; initially And111; loc And000: while ckAnd >= 0 wait {} when True sync tUp do {} goto And100; when True sync bUp do {} goto And010; loc And001: while ckAnd <= dAnd_u & ckAnd>=0 wait {} when True sync tUp do {ckAnd' = 0} goto And101; when True sync bUp do {ckAnd' = 0} goto And011; when ckAnd >= dAnd_l sync xDown do {qx'=0} goto And000; loc And010: while ckAnd >= 0 wait {} when True sync tUp do {ckAnd' = 0} goto And110; when True sync bDown do {} goto And000; loc And011: while ckAnd <= dAnd_u & ckAnd>=0 wait {} when True sync tUp do {} goto And111; when True sync bDown do {ckAnd' = 0} goto And001; when ckAnd >= dAnd_l sync xDown do {qx'=0} goto And010; loc And100: while ckAnd >= 0 wait {} when True sync tDown do {} goto And000; when True sync bUp do {ckAnd' = 0} goto And110; loc And101: while ckAnd <= dAnd_u & ckAnd>=0 wait {} when True sync tDown do {ckAnd' = 0} goto And001; when True sync bUp do {} goto And111; when ckAnd >= dAnd_l sync xDown do {qx'=0} goto And100; loc And110: while ckAnd <= dAnd_u& ckAnd>=0 wait {} when True sync tDown do {} goto And010; when True sync bDown do {} goto And100; when ckAnd >= dAnd_l sync xUp do {qx'=1} goto And111; loc And111: while ckAnd >= 0 wait {} when True sync tDown do {ckAnd' = 0} goto And011; when True sync bDown do {ckAnd' = 0} goto And101; end -- andGate --****************************************************-- automaton orGate --****************************************************-- -- Input 1 : x (output of AND) -- Input 2 : a -- Output : t synclabs: xUp, xDown, aUp, aDown, tUp, tDown; initially Or111; loc Or000: while ckOr >= 0 wait {} when True sync xUp do {ckOr' = 0} goto Or100; when True sync aUp do {ckOr' = 0} goto Or010; loc Or001: while ckOr <= dOr_u & ckOr >= 0 wait {} when True sync xUp do {} goto Or101; when True sync aUp do {} goto Or011; when ckOr >= dOr_l sync tDown do {} goto Or000; loc Or010: while ckOr <= dOr_u & ckOr >= 0 wait {} when True sync xUp do {ckOr' = 0} goto Or110; when True sync aDown do {} goto Or000; when ckOr >= dOr_l sync tUp do {} goto Or011; loc Or011: while ckOr >= 0 wait {} when True sync xUp do {} goto Or111; when True sync aDown do {ckOr' = 0} goto Or001; loc Or100: while ckOr <= dOr_u & ckOr >= 0 wait {} when True sync xDown do {} goto Or000; when True sync aUp do {ckOr' = 0} goto Or110; when ckOr >= dOr_l sync tUp do {} goto Or101; loc Or101: while ckOr >= 0 wait {} when True sync xDown do {ckOr' = 0} goto Or001; when True sync aUp do {} goto Or111; loc Or110: while ckOr <= dOr_u & ckOr >= 0 wait {} when True sync xDown do {ckOr' = 0} goto Or010; when True sync aDown do {ckOr' = 0} goto Or100; when ckOr >= dOr_l sync tUp do {} goto Or111; loc Or111: while ckOr >= 0 wait {} when True sync xDown do {} goto Or011; when True sync aDown do {} goto Or101; end -- orGate --****************************************************-- --****************************************************-- -- ANALYSIS --****************************************************-- --****************************************************-- var init_reg, final_reg, post_reg : region; init_reg := ---------------------- -- Initial locations ---------------------- loc[input] = InputInit & loc[andGate] = And111 & loc[orGate] = Or111 & qa=1 & qx=1 ---------------------- -- Clocks ---------------------- -- & s = 0 -- & ckOr = 0 -- & ckAnd = 0 & cka =0 & ckb = 0 ---------------------- -- Constraints ---------------------- & dAUp_l <= dAUp_u & dADown_l <= dADown_u & dOr_l <= dOr_u & dAnd_l <= dAnd_u & bpre_l <= bpre_u & dBDown_l <= dBDown_u & 0 < dAUp_l & 0 < dADown_l & 0 < dBDown_l & 0 < dOr_l & 0 < dAnd_l & 0 < bpre_l -- JEU DE VALEURS DONNANT 9 ETATS (DONC MAUVAIS) -- & dAUp_u = 20 -- & dAUp_l = 19 -- & dAnd_u = 10 -- & dAnd_l = 9 -- & bpre_u = 8 -- & bpre_l = 7 -- & dOr_u = 5 -- & dOr_l = 4 -- & dBDown_u = 19 -- & dBDown_l = 18 -- & dADown_u = 18 -- & dADown_l = 16 -- JEU DE VALEURS DONNANT 8 ETATS (tous sauf le 1) mais qui apparemment ne reboucle pas DONC MAUVAIS -- & dAUp_u = 20 -- & dAUp_l = 19 -- & dAnd_u = 10 -- & dAnd_l = 9 -- & bpre_u = 8 -- & bpre_l = 7 -- & dOr_u = 5 -- & dOr_l = 4 -- & dBDown_u = 21 -- & dBDown_l = 20 -- & dADown_u = 18 -- & dADown_l = 16 -- JEU DE VALEURS VERIFIANT LES CONTRAINTES DE LAURENT avec 8 etats (tous sauf le 1) et qui boucle (donc tout va bien) ---START PI0--- -- & dAUp_l = 13 -- & dAUp_u = 14 -- & dADown_l = 16 -- & dADown_u = 18 -- & bpre_l = 7 -- & bpre_u = 8 -- & dBDown_l = 19 -- & dBDown_u = 20 -- & dAnd_l = 3 -- & dAnd_u = 4 -- & dOr_l = 1 -- & dOr_u = 2 ---END PI0--- ; final_reg := ---------------------- -- final locations ---------------------- loc[input] = Input4 & qa=0 & qx=1 ---------------------- -- Clocks ---------------------- -- & s = 0 & ckOr >= 0 & ckAnd >= 0 & cka >=0 & ckb >= 0 & dAUp_l <= dAUp_u & dADown_l <= dADown_u & dOr_l <= dOr_u & dAnd_l <= dAnd_u & bpre_l <= bpre_u & dBDown_l <= dBDown_u & 0 < dAUp_l & 0 < dADown_l & 0 < dBDown_l & 0 < dOr_l & 0 < dAnd_l & 0 < bpre_l ; post_reg := reach forward from init_reg endreach; prints "---START LOG---"; print(hide ckOr, ckAnd,cka,ckb, qa, qx in post_reg endhide ); prints "---END LOG---"; -- prints "--****************************************************--"; -- prints " INTERSECTION"; -- prints "--****************************************************--"; -- inter_reg := post_reg & final_reg; -- print(hide -- ckOr, ckAnd, ckb, cka -- -- dOr_l, dOr_u, dAnd_l, dAnd_u -- in inter_reg -- endhide); -- prints "--****************************************************--"; -- prints " TRACE"; -- prints "--****************************************************--"; -- print trace to ( -- loc[input] = InputInit -- & loc[andGate] = And111 -- & loc[orGate] = Or111 -- ) -- using post_reg;