A forum for Spin users
You are not logged in.
Pages: 1
> spinroot wrote:
> Okay -- then I think you only forgot to negate the claim
you can generate the never claim with:
spin -f '!([]<> (connected1 == 1) && [] <> (connected2 == 1))'
which would be the same as saying:
spin -f '(<>[] !connected1 || <>[] !connected2)'
since the two parts of this property are independent, you can of course also verify them in two separate steps
(first for connected1 and then for connected2)
Why should I negate the claim? I think if we aim to verify whether all executions of program exhibit property 'p', we should generate a never claim for 'p'. never claim will produce Buchi automaton for '!q' and SPIN computes the xxx of automatons of all program executions and '!q'. If there is an accepted sequence which satisfies '!p' and must not exhibit property 'p'.
> spinroot wrote:
> if the requirement is that connected1 and connected2 cannot both simultaneously become and remain true then the claim would be that this is impossible:
<>[] (connected1 != 0 || connected2 != 0)
to verify that claim you have to negate this formula -- to find executions that match a counter-example:
!<>[] (connected1 != 0 || connected2 != 0) which is the same as
[]<> (connected1 == 0 && connected2 == 0)
I think you misunderstand my requirement. my requirement is connected1 and connected2 always eventually (infinitely often) becomes true. both connected1 and connected2 do not need remain true but, if they become false, should eventually become true again.
How to specify a temporal logic for above requirement?
[quote=Chengxiu]obviously doesn't satisfy what I aim to verify [/quote]
sorry I mean a cyclic execution with 'connected2' changing between 0 and 1 is what I don't expect. I expect a cyclic execution with 'connected1' or 'connected2' remain being 0 or both, that's the counter-example of the temporal logic I aim to verify.
> spinroot wrote:
> don't you mean <>[] (connected1 ==1 && connected2 == 1) ?
Thanks. I aim to verify for both connected1 and connected2, infinitely often (always eventually) connectedi (i=1,2) are true in a single verification.
I think [] stands for temporal operator 'always in the further', <> stands for temporal operator 'sometime in the further'.
I represent as [] <> (connected1 == 1) && [] <> (connected2 == 1), but it seems SPIN return a counter-example with 'connected2' is always changing between 0 and 1, obviously doesn't satisfy what I aim to verify.
I expect a counter-example with both connected1 and connected2 always remain being 0.
Sorry I attach my code as below, many thanks.
bool connected1 = 0; /*connectivity mode, robot1*/
bool connected2 = 0; /*connectivity mode, robot2*/
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};
proctype Robot1()
{
int robot1Loc = 0; /*inital robot location*/
int range =1; /*communication range*/
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0; /*ford == for, for is keyword, so we cannot use it, two motion modes: forward, coherence*/
bool fcon, fnocon, cohcon, cohnocon; /*four alternatives combining the two motion modes and connectivity modes*/
bool insn1, inss1, inse1, insw1;
if /*initially, random direction*/
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
:: robot1x = robot1Loc / 10; printf("%d", robot1x); /*xcoordinate*/
robot1y = robot1Loc % 10; printf ("%d", robot1y); /*ycoordinate*/
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected1 = ((abs12x <= range) || ((lenmax - abs12x) <= range)) && ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected1);
insn1 = (robot1x == robot2x && (robot1y + 1) % lenmax == robot2y); /*if insn1 == 1, robot2 is at one step north of robot1*/
inss1 = (robot1x == robot2x && (robot1y - 1) % lenmax == robot2y);
inse1 = ((robot1x + 1) % lenmax == robot2x && robot1y == robot2y);
insw1 = ((robot1x - 1) % lenmax == robot2x && robot1y == robot2y);
fcon = (ford ==1 && coh == 0 && connected1 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == n && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == n && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == s && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == s && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == s && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == e && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == e && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == e && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == w && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == w && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == w && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fnocon && direction == n && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc); /*moving south*/
::(fnocon && direction == n && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fnocon && direction == n && inss1) -> (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fnocon && direction == s && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc); /*moving north*/
::(fnocon && direction == s && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fnocon && direction == s && insn1) -> (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fnocon && direction == e && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*moving west*/
::(fnocon && direction == e && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fnocon && direction == e && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fnocon && direction == w && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc); /*moving east*/
::(fnocon && direction == w && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fnocon && direction == w && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(cohnocon && direction == n && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == n && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(cohnocon && direction == n && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(cohnocon && direction == s && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == s && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(cohnocon && direction == s && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(cohnocon && direction == e && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == e && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(cohnocon && direction == e && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(cohnocon && direction == w && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == w && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(cohnocon && direction == w && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == n && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); nextDirection = e; printf ("%d", robot1Loc); /*moving east*/
:: (cohcon && direction == n && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == n && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == n && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc);
:: (cohcon && direction == n && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == n && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == s && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc);
:: (cohcon && direction == s && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == s && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == s && !insw1) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc);
:: (cohcon && direction == s && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == s && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == e && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc);
:: (cohcon && direction == e && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); nextDirection = e; /*next robot location, moving east*/
:: (cohcon && direction == e && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
:: (cohcon && direction == e && !inss1) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); nextDirection = s;printf ("%d", robot1Loc);
:: (cohcon && direction == e && inss1) ->robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); nextDirection = e; /*next robot location, moving east*/
:: (cohcon && direction == e && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); nextDirection = w; /*next robot location, moving west*/
:: (cohcon && direction == w && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc);
:: (cohcon && direction == w && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc); /*next robot location, moving east*/
:: (cohcon && direction == w && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
:: (cohcon && direction == w && !inss1) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot1Loc);
:: (cohcon && direction == w && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc); /*next robot location, moving east*/
:: (cohcon && direction == w && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == w) -> direction = w; printf ("%e", direction);
fi;
od
}
proctype Robot2()
{
int robot2Loc = 1;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0; /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon;
bool insn2, inss2, inse2, insw2;
if
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
:: robot2x = robot2Loc / 10; printf("%d", robot2x);
robot2y = robot2Loc % 10; printf("%d", robot2y);
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x; printf ("%d", abs12x);
::(robot2x < robot1x) -> abs12x = robot1x - robot2x; printf("%d", abs12x);
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y; printf("%d", abs12y);
::(robot2y < robot1y) -> abs12y = robot1y - robot2y; printf("%d", abs12y);
fi;
connected2 = ((abs12x <= range) || ((lenmax - abs12x) <= range)) && ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected2);
insn2 = (robot2x == robot1x && (robot2y + 1) % lenmax == robot1y);
inss2 = (robot2x == robot1x && (robot2y - 1) % lenmax == robot1y);
inse2 = ((robot2x + 1) % lenmax == robot1x && robot2y == robot1y);
insw2 = ((robot2x - 1) % lenmax == robot1x && robot2y == robot1y);
fcon = (ford ==1 && coh ==0 && connected2 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected2 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected2== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected2 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fcon && direction == n && insn2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
::(fcon && direction == n && insn2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fcon && direction == s && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(fcon && direction == s && inss2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
::(fcon && direction == s && inss2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fcon && direction == e && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fcon && direction == e && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == e && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == w && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fcon && direction == w && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == w && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc);
::(fnocon && direction == n && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc); /*moving south*/
::(fnocon && direction == n && inss2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fnocon && direction == n && inss2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fnocon && direction == s && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(fnocon && direction == s && insn2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fnocon && direction == s && insn2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fnocon && direction == e && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == e && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fnocon && direction == e && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(fnocon && direction == w && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == w && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fnocon && direction == w && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(cohnocon && direction == n && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == n && insn2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(cohnocon && direction == n && insn2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(cohnocon && direction == s && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == s && inss2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(cohnocon && direction == s && inss2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(cohnocon && direction == e && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == e && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(cohnocon && direction == e && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(cohnocon && direction == w && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == w && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(cohnocon && direction == w && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == n && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); nextDirection = e; printf ("%d", robot2Loc);
:: (cohcon && direction == n && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == n && inse2) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == n &&!insw2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc);
:: (cohcon && direction == n &&insw2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == n &&insw2 ) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == s &&!inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc);
:: (cohcon && direction == s &&inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == s &&inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == s &&!insw2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc);
:: (cohcon && direction == s &&insw2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == s &&insw2 ) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == e &&!insn2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc);
:: (cohcon && direction == e &&insn2 ) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == e &&insn2 ) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == e && !inss2 ) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot2Loc);
:: (cohcon && direction == e && inss2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == e && inss2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == w && !insn2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc);
:: (cohcon && direction == w && insn2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == w && insn2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == w && !inss2 ) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot2Loc);
:: (cohcon && direction == w && inss2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == w && inss2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == w) -> direction = w; printf ("%e", direction);
fi;
od
}
init { atomic {run Robot1(); run Robot2()} }
/*
* Formula As Typed: ([] <> (connected1 == 1) && [] <> (connected2 == 1))
* The Never Claim Below Corresponds
* To The Negated Formula !(([] <> (connected1 == 1) && [] <> (connected2 == 1)))
* (formalizing violations of the original)
*/
never { /* !(([] <> (connected1 == 1) && [] <> (connected2 == 1))) */
T0_init:
if
:: (! ((connected2 == 1))) -> goto accept_S5
:: (! ((connected1 == 1))) -> goto accept_S10
:: (1) -> goto T0_init
fi;
accept_S5:
if
:: (! ((connected2 == 1))) -> goto accept_S5
fi;
accept_S10:
if
:: (! ((connected1 == 1))) -> goto accept_S10
fi;
}Dear all,
I just finished writing the following code, two processes Robot1 and Robot2, and they repeatedly execute and have several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. I want to verify "connected1 and connected2 are always eventually simultaneously true". So at the last part, I added a 'Never Claim' which was automatically generated by system corresponding to my temporal logic formula representation "[] <> (connected1 == 1) && [] <> (connected2 == 1)", and the system returned a counter-example, but it is as following:
preparing trail, please wait...done
MSC: ~G line 422
1: proc - (never_0) pan_in:422 (state 1) [(!((connected1==1)))]
Never claim moves to line 422 [(!((connected1==1)))]
Starting Robot1 with pid 2
2: proc 0 (:init:) pan_in:410 (state 1) [(run Robot1())]
Starting Robot2 with pid 3
3: proc 0 (:init:) pan_in:410 (state 2) [(run Robot2())]
MSC: ~G line 427
4: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
Never claim moves to line 427 [(!((connected1==1)))]
n 5: proc 2 (Robot2) pan_in:230 (state 2) [printf('%e',direction)] <
6: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
n 7: proc 1 (Robot1) pan_in:27 (state 2) [printf('%e',direction)] <
8: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
10: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 11: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
12: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
14: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 15: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
16: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
17: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
18: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
20: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 21: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
22: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
23: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
24: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
26: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 27: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
28: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
30: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 31: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
32: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
34: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
36: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
38: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
40: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
42: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 43: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
44: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
46: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 47: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
48: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
50: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 51: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
52: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
54: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 55: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
56: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
57: proc 2 (Robot2) pan_in:271 (state 45) [(((fcon&&(direction==n))&&!(insn2)))] <
2 57: proc 2 (Robot2) pan_in:271 (state 47) [printf('%d',robot2Loc)] <
58: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
59: proc 2 (Robot2) pan_in:360 (state 251) [(fcon)] <
60: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
61: proc 2 (Robot2) pan_in:370 (state 265) [((fcon&&(direction==n)))] <
n 61: proc 2 (Robot2) pan_in:370 (state 267) [printf('%e',direction)] <
62: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
64: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 65: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
66: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
68: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2 69: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
70: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
71: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
72: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
74: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 75: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
76: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
77: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
78: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
80: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2 81: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
82: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
84: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 85: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
86: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
88: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
90: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
92: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
94: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
96: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 97: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
98: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
100: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1101: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
102: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
104: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0105: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
106: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
108: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0109: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
110: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
111: proc 2 (Robot2) pan_in:288 (state 81) [(((fnocon&&(direction==n))&&!(inss2)))] <
1111: proc 2 (Robot2) pan_in:288 (state 83) [printf('%d',robot2Loc)] <
112: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
113: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
114: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
115: proc 2 (Robot2) pan_in:375 (state 277) [((fnocon&&(direction==n)))] <
s115: proc 2 (Robot2) pan_in:375 (state 279) [printf('%e',direction)] <
116: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
118: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0119: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
120: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
122: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1123: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
124: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
125: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
126: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
128: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0129: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
130: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
131: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
132: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
134: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1135: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
136: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
138: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1139: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
140: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
142: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
144: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
146: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
148: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
150: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0151: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
152: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
154: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0155: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
156: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
158: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1159: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
160: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
162: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0163: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
164: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
165: proc 2 (Robot2) pan_in:330 (state 177) [(((cohcon&&(direction==s))&&!(inse2)))] <
11165: proc 2 (Robot2) pan_in:330 (state 180) [printf('%d',robot2Loc)] <
166: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
167: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
168: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
169: proc 2 (Robot2) pan_in:390 (state 313) [(((cohcon&&(direction==s))&&(nextDirection==e)))] <
e169: proc 2 (Robot2) pan_in:390 (state 315) [printf('%e',direction)] <
170: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
172: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1173: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
174: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
176: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1177: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
178: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
179: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
180: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
182: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1183: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
184: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
185: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
186: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
188: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1189: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
190: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
192: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1193: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
194: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
196: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
198: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
200: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
202: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
204: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1205: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
206: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
208: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0209: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
210: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
212: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0213: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
214: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
216: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0217: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
218: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
219: proc 2 (Robot2) pan_in:279 (state 63) [(((fcon&&(direction==e))&&!(inse2)))] <
21219: proc 2 (Robot2) pan_in:279 (state 65) [printf('%d',robot2Loc)] <
220: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
221: proc 2 (Robot2) pan_in:360 (state 251) [(fcon)] <
222: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
223: proc 2 (Robot2) pan_in:372 (state 271) [((fcon&&(direction==e)))] <
e223: proc 2 (Robot2) pan_in:372 (state 273) [printf('%e',direction)] <
<<<<<START OF CYCLE>>>>>
224: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
226: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2227: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
228: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
230: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1231: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
232: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
233: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
234: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
236: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2237: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
238: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
239: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
240: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
242: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1243: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
244: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
246: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0247: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
248: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
250: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
252: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
254: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
256: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
258: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0259: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
260: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
262: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1263: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
264: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
266: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0267: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
268: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
270: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0271: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
272: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
273: proc 2 (Robot2) pan_in:296 (state 99) [(((fnocon&&(direction==e))&&!(insw2)))] <
11273: proc 2 (Robot2) pan_in:296 (state 101) [printf('%d',robot2Loc)] <
274: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
275: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
276: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
277: proc 2 (Robot2) pan_in:376 (state 280) [((fnocon&&(direction==e)))] <
w277: proc 2 (Robot2) pan_in:376 (state 282) [printf('%e',direction)] <
278: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
280: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1281: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
282: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
284: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1285: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
286: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
287: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
288: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
290: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1291: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
292: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
293: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
294: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
296: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1297: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
298: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
300: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1301: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
302: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
304: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
306: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
308: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
310: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
312: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0313: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
314: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
316: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0317: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
318: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
320: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1321: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
322: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
324: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0325: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
326: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
327: proc 2 (Robot2) pan_in:346 (state 225) [(((cohcon&&(direction==w))&&!(insn2)))] <
12327: proc 2 (Robot2) pan_in:346 (state 228) [printf('%d',robot2Loc)] <
328: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
329: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
330: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
331: proc 2 (Robot2) pan_in:400 (state 337) [(((cohcon&&(direction==w))&&(nextDirection==n)))] <
n331: proc 2 (Robot2) pan_in:400 (state 339) [printf('%e',direction)] <
332: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
334: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1335: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
336: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
338: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2339: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
340: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
341: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
342: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
344: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1345: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
346: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
347: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
348: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
350: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2351: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
352: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
354: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0355: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
356: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
358: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
360: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
362: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
364: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
366: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0367: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
368: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
370: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1371: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
372: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
374: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0375: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
376: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
378: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0379: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
380: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
381: proc 2 (Robot2) pan_in:288 (state 81) [(((fnocon&&(direction==n))&&!(inss2)))] <
11381: proc 2 (Robot2) pan_in:288 (state 83) [printf('%d',robot2Loc)] <
382: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
383: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
384: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
385: proc 2 (Robot2) pan_in:375 (state 277) [((fnocon&&(direction==n)))] <
s385: proc 2 (Robot2) pan_in:375 (state 279) [printf('%e',direction)] <
386: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
388: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1389: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
390: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
392: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1393: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
394: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
395: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
396: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
398: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1399: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
400: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
401: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
402: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
404: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1405: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
406: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
408: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1409: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
410: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
412: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
414: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
416: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
418: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
420: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0421: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
422: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
424: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0425: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
426: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
428: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1429: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
430: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
432: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0433: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
434: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
435: proc 2 (Robot2) pan_in:330 (state 177) [(((cohcon&&(direction==s))&&!(inse2)))] <
21435: proc 2 (Robot2) pan_in:330 (state 180) [printf('%d',robot2Loc)] <
436: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
437: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
438: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
439: proc 2 (Robot2) pan_in:390 (state 313) [(((cohcon&&(direction==s))&&(nextDirection==e)))] <
e439: proc 2 (Robot2) pan_in:390 (state 315) [printf('%e',direction)] <
spin: trail ends after 439 steps
#processes: 3
439: proc 2 (Robot2) pan_in:236 (state 351)
439: proc 1 (Robot1) pan_in:35 (state 347)
439: proc 0 (:init:) pan_in:410 (state 4)
MSC: ~G line 426
439: proc - (never_0) pan_in:426 (state 9)
3 processes createdwhich contains a cyclic execution that 'connected2' always changes bewteen 0 and 1 (see step 301, 355, 409), so that satisfies the temporal logic formula. According to my knowledge, SPIN should return a counter-example which doesn't satisfy the temporal logic formula. Is my temporal logic formula representation correct?
> spinroot wrote:
> To enforce synchronous behavior of two separate (asynchronous) processes, you have to provide the mechanism that accomplishes this. By default, processes execute asynchronously. (Other than in nuSMV.)
There is no global 'clock' that can step the system, as one would be able to do in a hardware circuit, because Spin models process systems (where you don't have a global clock -- just a process scheduler that can arbitrarily interleave the asynchronous execution of multiple processes).
So, yes, Spin can execute processes in parallel, but no it cannot do this synchronously. But, you can design synchronization mechanisms to accomplish it (just like you would have to do in any real system with multiple robots: they are asynchronous until you explicitly synchronize their behaviors).
Hi,
Recently I am considering this question again. I am trying to run two SPIN processes in "synchrony". Last time I did this by separating statements of both processes and combining them into a single process. I agree with your 'there is no global clock in SPIN and just a process scheduler that can arbitrarily interleave the asynchronous execution of multiple processes (it looks like run in synchrony), and Spin can execute processes in parallel, but no it cannot do this in pure synchrony '. But I am wondering how to do this in SPIN? how to explicitly 'synchronize' two processes in SPIN, without combining them into a single one?
Many Thanks.
[quote=spinroot]Promela is fundamentally a language for specifying asynchronous process behaviors.
Any type of synchronization that you want to enforce has to be enforced explicitly, just like you would need to do if you were to write it as a C program running as multiple threads or processes in a standard operating system. There's no predefined way to let two processes execute in lock-step. So if you'd like to do that, you do have to specify precisely how you'd enforce that....
Perhaps one simple way out would be to fold the two proctypes that must execute synchronously into a single one -- then you can specify precisely what happens and in what order.[/quote]
sorry, I just notice that if we fold the two proctypes into a single one, we do can specify precisely what happens and in what order. However this does not make two robots move synchronously, it just makes robots move in turn in a particular order, e.g. robot1, robot2, robot1, robot2...... is it possible to make two robots (processes) execute in parallel in SPIN? thanks.
[quote=spinroot]Spin can handle models with up to 255 asynchronous processes, in principle.
A swarm of robots does sound like a fundamentally asynchronous system. (nuSMV would be the best choice for a purely synchronous system, but Spin specifically targets asynchronous system models). Whether the verification with a 20 process system remains tractable depends completely on how the model is constructed (the formalization of the algorithm that you want to verify). In general, you should not expect a 1 to 1 translation of implementation code into Promela code to be very tractable -- a successful model checking run normally requires some abstractions to keep things tractable.
You may be able to abstract the behavior (the externally visible behavior that is) of groups of robots, and use that as part of the model, to see how one robot behaves in the presence of multiple others. That then would lead to a 2 process abstraction (i.e., one robot and its environment as far as it is visible to that one robot). In short: it requires thought....[/quote]
We have already done some abstractions and clever representations to the control algorithm, we simplify robot's behaviour, discretise the arena and etc. and we write the input for NuSMV and SPIN. for 2,3 robots the verification runs well, I am just thinking whether it is worth trying to verify larger say 20 robots case.
[quote=spinroot]remember that this is a verification tool. are there, for instance, any property violations in a system with 20 robots that could not be exhibited by a system with 19 robots? or 10? or 3?
there's no point in making the problem harder if there's no real gain in return of course.
then note also that this is just a tool to assist you in proving something. it's like math: if used well, you can prove interesting things -- if not used well, you wont be able to prove anything.
so, model the system carefully, making abstractions, finding the simplest possible way to express things formally, and then you'll be able to prove interesting properties of your design. it's the principle of the 'smallest sufficient model' that allows you to prove things.
just like in ordinary math: keep things as simple as possible, but no simpler, and you can prove remarkable results. there's no short-cut here -- spin is one of the better tools out there that can handle systems with astounding complexity -- but then again, if you're not careful you can also easily build models that exhibit even greater unnecessary complexity to befuddle even the best of tools.... :-)[/quote]
Yes, my study is a control algorithm for a swarm of robots, and the algorithm is able to at certain level keep all robots in connected. the algorithm's performance will increase as the increasing of robot's population. For instance, the algorithm is not good to keep all robots connected in 3,10 robots case, but it is better to keep connected in 20,40 robots case. actually it doesn't make much sense if we only verify small number of robots. But we have done the same thing using NuSMV and already faced state exploration problem for 3 robots case. So I am just wondering, based on your experience, can SPIN do better than NuSMV for verifying larger robot's population? Thanks.
[quote=spinroot]Promela is fundamentally a language for specifying asynchronous process behaviors.
Any type of synchronization that you want to enforce has to be enforced explicitly, just like you would need to do if you were to write it as a C program running as multiple threads or processes in a standard operating system. There's no predefined way to let two processes execute in lock-step. So if you'd like to do that, you do have to specify precisely how you'd enforce that....
Perhaps one simple way out would be to fold the two proctypes that must execute synchronously into a single one -- then you can specify precisely what happens and in what order.[/quote]
Ok, thanks. By the way, this piece of code is just for two robots case. Do you think the SPIN can deal with say twenty robots case? will it suffer from the state exploration problem ? I mean I write the code for twenty robots case ,and run the verification, will it work?
Many Thanks,
Chengxiu
Dear all,
this is still for my two robots interaction program (attached below). two processes proctype Robot1 and proctype Robot2, corresponds to two robots. and they share several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. In each process, there is a 'do .....od ' and executing the codes in it repeatedly. I verified the never claim property '[] <> (connected1 ==1)' and found out the a counter-example (failing trace, cyclic execution which the 'connected1' remain being 0 forever).
But in fact this property should hold, and I found out the mainly problem is that the two processes do not run concurrently, which let two robots do not move synchronously. e.g. the codes in 'do...od' of proctype Robot2 executes two times but the codes in 'do...od' do not execute once.
Is this possible to let two process run synchronously, that is the codes in 'do .. od' of proctype Robot1 execute once and the codes in 'do..od' executes once and repeat ? through configuring different simulation option or modifying the codes?
Many Thanks.
Chengxiu
bool connected1 = 0;
bool connected2 = 0;
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};
proctype Robot1()
{
int robot1Loc = 0;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0;
bool fcon, fnocon, cohcon, cohnocon;
if /*initially, random direction*/
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
::robot1x = robot1Loc / 10; printf ("%d", robot1x); /*xcoordinate*/
robot1y = robot1Loc % 10; printf("%d", robot1y);/*ycoordinate*/
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected1 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected1);
fcon = (ford ==1 && coh == 0 && connected1 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n ) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fnocon && direction == n) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
::(fnocon && direction == s) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc);
::(fnocon && direction == e) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf (" %d", robot1Loc);
::(fnocon && direction == w) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == n ) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc);
:: (cohcon && direction == n && nextDirection == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc);
:: (cohcon && direction == n && nextDirection == w) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc);
:: (cohcon && direction == s && nextDirection == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc);
:: (cohcon && direction == s && nextDirection == w) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc);
:: (cohcon && direction == e && nextDirection == n) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc);
:: (cohcon && direction == e && nextDirection == s) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
:: (cohcon && direction == w && nextDirection == n) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc);
:: (cohcon && direction == w && nextDirection == s) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n) -> direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == n) -> direction = w; nextDirection = w; printf ("%e", direction);
:: (cohcon && direction == s) -> direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == s) -> direction = w; nextDirection = w; printf ("%e", direction);
:: (cohcon && direction == e) -> direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == e) -> direction = s; nextDirection = s; printf ("%e", direction);
:: (cohcon && direction == w) -> direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == w) -> direction = s; nextDirection = s; printf ("%e", direction);
fi;
od
}
proctype Robot2()
{
int robot2Loc = 11;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0;
bool fcon, fnocon, cohcon, cohnocon;
if
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
::robot2x = robot2Loc / 10; printf ("%d", robot2x);
robot2y = robot2Loc % 10; printf ("%d", robot2y);
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected2 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected2);
fcon = (ford ==1 && coh ==0 && connected2 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected2 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected2== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected2 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
::(fcon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == n) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
::(fnocon && direction == s) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(fnocon && direction == e) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == w) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == n ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
:: (cohcon && direction == n && nextDirection == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
:: (cohcon && direction == n && nextDirection == w) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
:: (cohcon && direction == s && nextDirection == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
:: (cohcon && direction == s && nextDirection == w) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
:: (cohcon && direction == e && nextDirection == n) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
:: (cohcon && direction == e && nextDirection == s) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
:: (cohcon && direction == w && nextDirection == n) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
:: (cohcon && direction == w && nextDirection == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n ) -> direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == n ) -> direction = w; nextDirection = w; printf ("%e", direction);
:: (cohcon && direction == s) -> direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == s) -> direction = w; nextDirection = w; printf ("%e", direction);
:: (cohcon && direction == e ) -> direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == e ) -> direction = s; nextDirection = s; printf ("%e", direction);
:: (cohcon && direction == w ) -> direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == w ) -> direction = s; nextDirection = s; printf ("%e", direction);
fi;
od
}
init { atomic {run Robot1(); run Robot2()} }
never { /* !([] <> (connected1 == 1)) */
T0_init:
if
:: (! ((connected1 == 1))) -> goto accept_S4
:: (1) -> goto T0_init
fi;
accept_S4:
if
:: (! ((connected1 == 1))) -> goto accept_S4
fi;
}[quote=spinroot]i did the following:
- removed "&& connected2" from the property
- spin -a spec.pml
- cc -o pan pan.c
- ./pan -a
this generated a counter-example -- showing that the property does not hold
i.e., there is an execition where connected1 does not eventually return to the value 1, but can permanently remain 0
you then replay the precise steps in that error scenario but saying something like:
- spin -t -p spec.pml
This will print a cyclic execution that can be repeated forever after, with connected1 being zero. The cycle starts at the point in the printout where it says "Start of Cycle".
You can add more detail to the trace with various spin options (see spin -- for a list).
The counter-example I generated is 223 steps long.
Easier perhaps to learn the basics by using these shell command-line steps at first.[/quote]
ok, thanks so much!
[quote=spinroot]did you mean to say that connected1 and connected2 are always eventually *simultaneously* true? (because that's what your property states....)[/quote]
Thanks, I understand your question.
In fact, I want to verify, for each global variable 'connected1' and 'connected2', infinitely often (always eventually) they hold.
so it should verify them separately.
1. verifying never claim for '[] <> (connected1 == 1)' to the program.
2. verifying never claim for '[] <> (connected2 == 1)' to the program.
could you give me some feedback for the results, do them hold? because I don't quite understand
the output, thanks.
Cheers,
Chengxiu
Dear all,
I just finished writing the following code, two processes Robot1 and Robot2, they repeatedly execute and have several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. At the last part, I added the 'never claim' which was automatically generated by system corresponding to the temporal logic formula "[] <> (connected1 && connected2 = 1)", infinitely often the global variables 'connected1' and 'connected2' are true. But when I run this code in Xspin, I don't quite understand the outputs, could anyone run this and give me some feedback, does this 'never claim' property hold?
Cheers,
Chengxiu
bool connected1 = 0;
bool connected2 = 0;
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};
proctype Robot1()
{
int robot1Loc = 0;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
bool ford =1, coh = 0; /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon;
if
:: direction = n;
:: direction = s;
:: direction = e;
:: direction = w;
fi;
do
::robot1x = robot1Loc / 10;
robot1y = robot1Loc % 10;
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected1 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) || ((lenmax - abs12y) <= range));
fcon = (ford ==1 && coh ==0 && connected1 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n ) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf("%d", robot1Loc);
::(fcon && direction == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf("%d", robot1Loc);
::(fcon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf("%d", robot1Loc);
::(fcon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot1Loc);
::(fnocon && direction == n) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf("%d", robot1Loc);
::(fnocon && direction == s) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf("%d", robot1Loc);
::(fnocon && direction == e) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot1Loc);
::(fnocon && direction == w) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf("%d", robot1Loc);
::(cohnocon && direction == n ) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf("%d", robot1Loc);
::(cohnocon && direction == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf("%d", robot1Loc);
::(cohnocon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf("%d", robot1Loc);
::(cohnocon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot1Loc);
:: (cohcon && direction == n) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf("%d", robot1Loc);
:: (cohcon && direction == n) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot1Loc);
:: (cohcon && direction == s) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf("%d", robot1Loc);
:: (cohcon && direction == s) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot1Loc);
:: (cohcon && direction == e) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf("%d", robot1Loc);
:: (cohcon && direction == e) ->10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf("%d", robot1Loc);
:: (cohcon && direction == w) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf("%d", robot1Loc);
:: (cohcon && direction == w) ->10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf("%d", robot1Loc);
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n;
:: (fcon && direction == s) -> direction = s;
:: (fcon && direction == e) -> direction = e;
:: (fcon && direction == w) -> direction = w;
::(fnocon && direction == n) -> direction = s;
::(fnocon && direction == e) -> direction = w;
::(fnocon && direction == s) -> direction = n;
::(fnocon && direction == w) -> direction = e;
:: (cohnocon&& direction == n) -> direction = n;
:: (cohnocon && direction == s) -> direction = s;
:: (cohnocon && direction == e) -> direction = e;
:: (cohnocon && direction == w) -> direction = w;
:: (cohcon && direction == n) -> direction = e;
:: (cohcon && direction == n) -> direction = w;
:: (cohcon && direction == s) -> direction = e;
:: (cohcon && direction == s) -> direction = w;
:: (cohcon && direction == e) -> direction = n;
:: (cohcon && direction == e) -> direction = s;
:: (cohcon && direction == w) -> direction = n;
:: (cohcon && direction == w) -> direction = s;
fi;
od
}
proctype Robot2()
{
int robot2Loc = 11;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
bool ford =1, coh = 0; /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon;
if
:: direction = n;
:: direction = s;
:: direction = e;
:: direction = w;
fi;
do
::robot2x = robot2Loc / 10;
robot2y = robot2Loc % 10;
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected2 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) || ((lenmax - abs12y) <= range));
fcon = (ford ==1 && coh ==0 && connected1 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf("%d", robot2Loc);
::(fcon && direction == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf("%d", robot2Loc);
::(fcon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf("%d", robot2Loc);
::(fcon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot2Loc);
::(fnocon && direction == n) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf("%d", robot2Loc);
::(fnocon && direction == s) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf("%d", robot2Loc);
::(fnocon && direction == e) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot2Loc);
::(fnocon && direction == w) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf("%d", robot2Loc);
::(cohnocon && direction == n ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf("%d", robot2Loc);
::(cohnocon && direction == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf("%d", robot2Loc);
::(cohnocon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf("%d", robot2Loc);
::(cohnocon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot2Loc);
:: (cohcon && direction == n) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf("%d", robot2Loc);
:: (cohcon && direction == n) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot2Loc);
:: (cohcon && direction == s) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf("%d", robot2Loc);
:: (cohcon && direction == s) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf("%d", robot2Loc);
:: (cohcon && direction == e) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf("%d", robot2Loc);
:: (cohcon && direction == e) ->10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf("%d", robot2Loc);
:: (cohcon && direction == w) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf("%d", robot2Loc);
:: (cohcon && direction == w) ->10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf("%d", robot2Loc);
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n;
:: (fcon && direction == s) -> direction = s;
:: (fcon && direction == e) -> direction = e;
:: (fcon && direction == w) -> direction = w;
::(fnocon && direction == n) -> direction = s;
::(fnocon && direction == e) -> direction = w;
::(fnocon && direction == s) -> direction = n;
::(fnocon && direction == w) -> direction = e;
:: (cohnocon&& direction == n) -> direction = n;
:: (cohnocon && direction == s) -> direction = s;
:: (cohnocon && direction == e) -> direction = e;
:: (cohnocon && direction == w) -> direction = w;
:: (cohcon && direction == n) -> direction = e;
:: (cohcon && direction == n) -> direction = w;
:: (cohcon && direction == s) -> direction = e;
:: (cohcon && direction == s) -> direction = w;
:: (cohcon && direction == e) -> direction = n;
:: (cohcon && direction == e) -> direction = s;
:: (cohcon && direction == w) -> direction = n;
:: (cohcon && direction == w) -> direction = s;
fi;
od
}
init { atomic {run Robot1(); run Robot2()} }
never { /* !([] (<> (connected1 && connected2 == 1))) */
T0_init:
if
:: (! ((connected1 && connected2 == 1))) -> goto accept_S4
:: (1) -> goto T0_init
fi;
accept_S4:
if
:: (! ((connected1 && connected2 == 1))) -> goto accept_S4
fi;
}Dear all,
I am trying to do the following program: two processes, named Robot1 and Robot2, they have four global variables, robot1x, robot1y, robot2x, robot2y.
proctype Robot1 assigns robot1x and robot1y, and assigns its internal variable connected1 by comparisons of robot1x, robot1y, robot2x, robot2y.
proctype Robot2 assigns robot2x and robot2y, and assigns its internal variable connected2 by comparisons of robot1x, robot1y, robot2x, robot2y.
the Program is as follows:
--------------------------------------------------------------------------
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};
proctype Robot1()
{
int robot1Loc = 0;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
bool connected1 = 0;
robot1x = robot1Loc / 10;
robot1y = robot1Loc % 10;
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi
connected1 = ((abs12x <= range) || (lenmax - abs12x) <= range)) && ((abs12y <= range) || (lenmax - abs12y) <= range));
}
proctype Robot2()
{
int robot2Loc = 11;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
bool connected2 = 0;
robot2x = robot2Loc / 10;
robot2y = robot2Loc % 10;
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi
connected2 = ((abs12x <= range) || (lenmax - abs12x) <= range)) && ((abs12y <= range) || (lenmax - abs12y) <= range));
}
init { atomic {run Robot1(); run Robot2()} }
-----------------------------------------------------------------------------
when I run the simulation, I hope the result shows both connected1, connected2 = 1.
but the system reports there is syntax errors in process Robot1 at:
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi
I think it is because the system does not know the value of robot2x, which will be later
assigned in process Robot2(), How to solve this problem?
Cheers,
Chengxiu
Ok, thanks.
by the way, is there any online video tutorial about the Promela?
so where will show the output of the "printf" ? for XSPIN
Dear all,
I am a new beginner about the SPIN.
I have tested the codes below:
"
proctype A(){
printf("123");
}
init { run A() }
"
run simulation and found about the result of "printf"
didn't appear in "Data Values" panel, why?
Cheers,
Chengxiu
Pages: 1