|
|
@ -7,8 +7,8 @@ mdp |
|
|
// variables to represent whether a process has a token or not |
|
|
// variables to represent whether a process has a token or not |
|
|
// note they are global because they can be updated by other processes |
|
|
// note they are global because they can be updated by other processes |
|
|
#for i=1:N# |
|
|
#for i=1:N# |
|
|
global q#i# : [0..1]; |
|
|
|
|
|
#end# |
|
|
|
|
|
|
|
|
global q#i# : [0..1]; |
|
|
|
|
|
#end# |
|
|
|
|
|
|
|
|
// module of process 1 |
|
|
// module of process 1 |
|
|
module process1 |
|
|
module process1 |
|
|
@ -29,11 +29,12 @@ endrewards |
|
|
|
|
|
|
|
|
// formula, for use here and in properties: number of tokens |
|
|
// formula, for use here and in properties: number of tokens |
|
|
formula num_tokens = #+ i=1:N#q#i##end#; |
|
|
formula num_tokens = #+ i=1:N#q#i##end#; |
|
|
// label - stable configurations (1 token) |
|
|
|
|
|
label "stable" = num_tokens=1; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// label - stable configurations (1 token) |
|
|
|
|
|
label "stable" = num_tokens=1; |
|
|
|
|
|
|
|
|
// initial states (at least one token) |
|
|
// initial states (at least one token) |
|
|
init |
|
|
init |
|
|
num_tokens >= 1 |
|
|
num_tokens >= 1 |
|
|
endinit |
|
|
endinit |
|
|
|
|
|
|
|
|
|
|
|
|