(******************************************************************************* * IMITATOR MODEL * * Title : fischer_2 * Description : Fischer's mutual exclusion protocol with 2 processes * Correctness : The mutual exclusion is ensured * Scalable : * Generated : * Categories : Academic ; Protocol ; RTS * Source : ? * bibkey : * Author : ? * Modeling : Romain Soulat * Input by : Romain Soulat, Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : < 2012/02/14 * Last modified : 2021/07/09 * Model version : * * IMITATOR version : 3.1 ******************************************************************************) var (* Clocks *) x1, (* P1's clock *) x2 (* P2's clock *) :clock; (* Discrete *) k : int; (* Parameters *) a, b : parameter; (************************************************************) automaton proc1 (************************************************************) synclabs : tau,start1,set1,enter1,abort1,release1; loc idle: invariant True when k=0 sync start1 do {x1 := 0} goto start; when True sync tau goto idle; loc start: invariant x1<=a when True sync set1 do {k := 1, x1 := 0} goto check; when True sync tau goto start; loc check: invariant True when k=1 & x1>=b sync enter1 goto CS; when k<>1 & x1>=b sync abort1 goto idle; when True sync tau goto check; loc CS: invariant True when True sync release1 do {k := 0} goto idle; when True sync tau goto CS; end (************************************************************) automaton proc2 (************************************************************) synclabs : tau,start2,set2,enter2,abort2,release2; loc idle: invariant True when k=0 sync start2 do {x2 := 0} goto start; when True sync tau goto idle; loc start: invariant x2<=a when True sync set2 do {k := 2, x2 := 0} goto check; when True sync tau goto start; loc check: invariant True when k=2 & x2>=b sync enter2 goto CS; when k<>2 & x2>=b sync abort2 goto idle; when True sync tau goto check; loc CS: invariant True when True sync release2 do {k := 0} goto idle; when True sync tau goto CS; end (************************************************************) automaton arbitrer (************************************************************) synclabs : set1,release1, set2,release2, tau; loc loc_arbitrer: invariant True when True sync set1 goto loc_arbitrer; when True sync release1 goto loc_arbitrer; when True sync set2 goto loc_arbitrer; when True sync release2 goto loc_arbitrer; when True sync tau goto loc_arbitrer; end (************************************************************) (* Initial state *) (************************************************************) init := { discrete = (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) loc[proc1] := idle, loc[proc2] := idle, loc[arbitrer] := loc_arbitrer, (*------------------------------------------------------------*) (* Initial discrete variables assignments *) (*------------------------------------------------------------*) k := 0, ; continuous = (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x1 = 0 & x2 = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & a >= 0 & b >= 0 ; } (************************************************************) (* The end *) (************************************************************) end