(************************************************************ * IMITATOR MODEL * * Modeling of an "AND" and an "OR" logical gate * * Description : Modeling of an "AND" and an "OR" logical gate * Correctness : Alternating sequence: b- x- a- b+ a+ x+ * Source : From "Verification of Concurrent Systems with Parametric Delays Using Octahedra" (2005) by Clariso and Cortadella; Fig 3a * Author : Roberto Clariso and Jordi Cortadella * Modeling : Étienne André and Laurent Fribourg * Input by : Étienne André * * Created : 2008/01 * Last modified : 2020/04/30 * * IMITATOR version: 3 ************************************************************) var ckOr, ckAnd, cka, ckb : clock; dA_High_l, dA_High_u, dA_Low_l, dA_Low_u, dB_High_l, dB_High_u, dB_Low_l, dB_Low_u, dOr_l, dOr_u, dAnd_l, dAnd_u : parameter; (************************************************************) automaton input (************************************************************) synclabs: aUp, aDown, bUp, bDown; loc InputInit: invariant ckb <= dB_High_u when ckb >= dB_High_l sync bDown do {ckb := 0} goto Input2; loc Input2: invariant cka <= dA_High_u when cka >= dA_High_l sync aDown do {cka := 0} goto Input3; loc Input3: invariant ckb <= dB_Low_u when ckb >= dB_Low_l sync bUp do {ckb := 0} goto Input4; loc Input4: invariant cka <= dA_Low_u when cka >= dA_Low_l sync aUp do {cka := 0, ckb := 0} goto InputInit; end (*input*) (************************************************************) automaton andGate (************************************************************) (* Input 1 : t (output of OR) Input 2 : b Output : x *) synclabs: tUp, tDown, bUp, bDown, xUp, xDown; loc And000: invariant ckAnd >= 0 when True sync tUp do {} goto And100; when True sync bUp do {} goto And010; loc And001: invariant ckAnd <= dAnd_u & ckAnd>=0 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 {} goto And000; loc And010: invariant ckAnd >= 0 when True sync tUp do {ckAnd := 0} goto And110; when True sync bDown do {} goto And000; loc And011: invariant ckAnd <= dAnd_u & ckAnd>=0 when True sync tUp do {} goto And111; when True sync bDown do {ckAnd := 0} goto And001; when ckAnd >= dAnd_l sync xDown do {} goto And010; loc And100: invariant ckAnd >= 0 when True sync tDown do {} goto And000; when True sync bUp do {ckAnd := 0} goto And110; loc And101: invariant ckAnd <= dAnd_u & ckAnd>=0 when True sync tDown do {ckAnd := 0} goto And001; when True sync bUp do {} goto And111; when ckAnd >= dAnd_l sync xDown do {} goto And100; loc And110: invariant ckAnd <= dAnd_u& ckAnd>=0 when True sync tDown do {} goto And010; when True sync bDown do {} goto And100; when ckAnd >= dAnd_l sync xUp do {} goto And111; loc And111: invariant ckAnd >= 0 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; loc Or000: invariant ckOr >= 0 when True sync xUp do {ckOr := 0} goto Or100; when True sync aUp do {ckOr := 0} goto Or010; loc Or001: invariant ckOr <= dOr_u & ckOr >= 0 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: invariant ckOr <= dOr_u & ckOr >= 0 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: invariant ckOr >= 0 when True sync xUp do {} goto Or111; when True sync aDown do {ckOr := 0} goto Or001; loc Or100: invariant ckOr <= dOr_u & ckOr >= 0 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: invariant ckOr >= 0 when True sync xDown do {ckOr := 0} goto Or001; when True sync aUp do {} goto Or111; loc Or110: invariant ckOr <= dOr_u & ckOr >= 0 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: invariant ckOr >= 0 when True sync xDown do {} goto Or011; when True sync aDown do {} goto Or101; end (*orGate*) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* INITIAL LOCATION *) (*------------------------------------------------------------*) loc[input] = InputInit & loc[andGate] = And111 & loc[orGate] = Or111 (*------------------------------------------------------------*) (* INITIAL CLOCKS *) (*------------------------------------------------------------*) & ckOr >= 0 & ckAnd >= 0 & cka = 0 & ckb = 0 & ckb <= dB_High_u (*------------------------------------------------------------*) (* PARAMETER CONSTRAINTS *) (*------------------------------------------------------------*) & dA_High_l <= dA_High_u & dA_Low_l <= dA_Low_u & dB_High_l <= dB_High_u & dB_Low_l <= dB_Low_u & dOr_l <= dOr_u & dAnd_l <= dAnd_u & 0 <= dA_High_l & 0 <= dA_Low_l & 0 <= dB_High_l & 0 <= dB_Low_l & 0 <= dOr_l & 0 <= dAnd_l (* -- JEU DE VALEURS DONNANT 9 ETATS (DONC MAUVAIS) -- & dA_High_u = 20 -- & dA_High_l = 19 -- & dAnd_u = 10 -- & dAnd_l = 9 -- & bpre_u = 8 -- & bpre_l = 7 -- & dOr_u = 5 -- & dOr_l = 4 -- & dB_Low_u = 19 -- & dB_Low_l = 18 -- & dA_Low_u = 18 -- & dA_Low_l = 16 -- JEU DE VALEURS DONNANT 8 ETATS (tous sauf le 1) mais qui apparemment ne reboucle pas DONC MAUVAIS -- & dA_High_u = 20 -- & dA_High_l = 19 -- & dAnd_u = 10 -- & dAnd_l = 9 -- & bpre_u = 8 -- & bpre_l = 7 -- & dOr_u = 5 -- & dOr_l = 4 -- & dB_Low_u = 21 -- & dB_Low_l = 20 -- & dA_Low_u = 18 -- & dA_Low_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--- -- & dA_High_l = 13 -- & dA_High_u = 14 -- & dA_Low_l = 16 -- & dA_Low_u = 18 -- -- & dB_High_l = 10 -- -- & dB_High_u = 12 -- & dB_High_l = 7 -- & dB_High_u = 8 -- & dB_Low_l = 19 -- & dB_Low_u = 20 -- & dAnd_l = 3 -- & dAnd_u = 4 -- & dOr_l = 1 -- & dOr_u = 2 ---END PI0--- ---------------------- -- Contraintes donnees par IMITATOR 1 ---------------------- -- & dOr_l <= dOr_u -- & dOr_u + dA_High_u < bpre_l + dB_Low_l -- & dA_Low_l <= dA_Low_u -- & dA_High_l <= dA_High_u -- & bpre_l <= bpre_u -- & 0 < dAnd_l -- & 0 < dOr_l -- & bpre_l + dB_Low_l <= dA_Low_u + dA_High_u -- & dAnd_u + dOr_u < bpre_l -- & 0 < dA_Low_l -- & dB_Low_l <= dB_Low_u -- & dAnd_l <= dAnd_u -- & bpre_u + dAnd_u < dA_High_l -- print (reach forward from init endreach); (* & dA_High_l = 13 & dA_High_u = 14 & dA_Low_l = 16 & dA_Low_u = 18 -- & dB_High_l = 10 -- & dB_High_u = 12 & dB_High_l = 7 & dB_High_u = 8 & dB_Low_l = 19 & dB_Low_u = 20 & dAnd_l = 3 -- & dAnd_u = 4 & dOr_l = 1 & dOr_u = 2 *) (* CARTO 5 PARAM (INFINITY'10 ?) & dA_High_l = 13 -- & dA_High_u = 13 .. 30 -- 14 & dA_Low_l = 16 -- & dA_Low_u = 16 .. 30 -- 16 .. 25 -- 18 & dB_High_l = 7 -- & dB_High_u = 7 .. 20 --7 .. 15 -- 8 & dB_Low_l = 19 -- & dB_Low_u = 20 -- 19 .. 25 -- 20 & dAnd_l = 3 -- & dAnd_u = 3 .. 10 -- 3 .. 5 -- 4 & dOr_l = 1 -- & dOr_u = 1 .. 5 -- 1 .. 5 -- 2 *) (* CARTO 4 PARAM (as of 2013/01/23) *) (* & dA_High_l = 13 & dA_High_u = 14 & dA_Low_l = 16 (* & dA_Low_u = 16 .. 30 -- 16 .. 25 -- 18 *) & dB_High_l = 7 (* & dB_High_u = 7 .. 20 --7 .. 15 -- 8 *) & dB_Low_l = 19 (* & dB_Low_u = 20 -- 19 .. 25 -- 20 *) & dAnd_l = 3 (* & dAnd_u = 3 .. 10 -- 3 .. 5 -- 4 *) & dOr_l = 1 (* & dOr_u = 1 .. 5 (* 1 .. 5 -- 2*) *) *) *) ; (************************************************************) (* The end *) (************************************************************) end