414956c51e
Add an algorithm to split an automaton in several automata. * bench/scc-stats: New directory. Contains input files and test program for computing statistics. * bench/split-product: New directory. Contains test program for synchronised product on splitted automata. * bench/split-product/models: New directory. Contains Promela files and LTL formulae that should be verified by the models. * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: New files. Small class to avoid long initializations with numerous constants when translating to TGBA many LTL formulae from a given file. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: New file. From a single automaton, create, at most, X sub automata. * src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Adjust to compute self-loops count.
155 lines
2.9 KiB
Promela
155 lines
2.9 KiB
Promela
/*
|
|
* 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
|
|
*/
|
|
|
|
#define p in?[red]
|
|
#define q out?[red]
|
|
#define r (BS[a_id]@progress || BS[p_id]@progress)
|
|
|
|
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
|
|
}
|