+++ /dev/null
-/*
- * Model of cell-phone handoff strategy in a mobile network.
- * A translation from the pi-calculus description of this
- * model presented in:
- * Fredrik Orava and Joachim Parrow, 'An algebraic verification
- * of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
- * For more information on this model, email: joachim@it.kth.se
- *
- * See also the simplified version of this model in mobile2
- *
- * The ltl property definition for this version is in mobile1.ltl
- *
- * to perform the verification with xspin, simply use the ltl property
- * manager, which will load the above .ltl file by default.
- * to perform the verificaion from a Unix command line, type:
- * $ spin -a -N mobile1.ltl mobile1
- * $ cc -o pan pan.c
- * $ pan -a
- */
-
-mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
-
-chan in = [1] of { mtype };
-chan out = [1] of { mtype };
-
-byte a_id, p_id; /* ids of processes refered to in the property */
-
-proctype CC(chan fa, fp, l) /* communication controller */
-{ chan m_old, m_new, x;
- mtype v;
-
- do
- :: in?v ->
- printf("MSC: DATA\n");
- fa!data; fa!v
- :: l?m_new ->
- fa!ho_cmd; fa!m_new;
- printf("MSC: HAND-OFF\n");
- if
- :: fp?ho_com ->
- printf("MSC: CH_REL\n");
- fa!ch_rel; fa?m_old;
- l!m_old;
- x = fa; fa = fp; fp = x
- :: fa?ho_fail ->
- printf("MSC: FAIL\n");
- l!m_new
- fi
- od
-}
-
-proctype HC(chan l, m) /* handover controller */
-{
- do
- :: l!m; l?m
- od
-}
-
-proctype MSC(chan fa, fp, m) /* mobile switching center */
-{ chan l = [0] of { chan };
-
- atomic {
- run HC(l, m);
- run CC(fa, fp, l)
- }
-}
-
-proctype BS(chan f, m; bit how) /* base station */
-{ chan v;
-
- if
- :: how -> goto Active
- :: else -> goto Passive
- fi;
-
-Active:
- printf("MSC: ACTIVE\n");
- do
- :: f?data -> f?v; m!data; m!v
- :: f?ho_cmd -> /* handover command */
-progress: f?v; m!ho_cmd; m!v;
- if
- :: f?ch_rel ->
- f!m;
- goto Passive
- :: m?ho_fail ->
- printf("MSC: FAILURE\n");
- f!ho_fail
- fi
- od;
-
-Passive:
- printf("MSC: PASSIVE\n");
- m?ho_acc -> f!ho_com;
- goto Active
-}
-
-proctype MS(chan m) /* mobile station */
-{ chan m_new;
- mtype v;
-
- do
- :: m?data -> m?v; out!v
- :: m?ho_cmd; m?m_new;
- if
- :: m_new!ho_acc; m = m_new
- :: m!ho_fail
- fi
- od
-}
-
-proctype P(chan fa, fp)
-{ chan m = [0] of { mtype };
-
- atomic {
- run MSC(fa, fp, m);
- p_id = run BS(fp, m, 0) /* passive base station */
- }
-}
-
-proctype Q(chan fa)
-{ chan m = [0] of { mtype }; /* mixed use as mtype/chan */
-
- atomic {
- a_id = run BS(fa, m, 1); /* active base station */
- run MS(m)
- }
-}
-
-active proctype System()
-{ chan fa = [0] of { mtype }; /* mixed use as mtype/chan */
- chan fp = [0] of { mtype }; /* mixed use as mtype/chan */
-
- atomic {
- run P(fa, fp);
- run Q(fa)
- }
-}
-
-active proctype top()
-{
- do
- :: in!red; in!white; in!blue
- od
-}
-active proctype bot()
-{
- do /* deadlock on loss or duplication */
- :: out?red; out?white; out?blue
- od
-}