diff --git a/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp b/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp index d658dc6e..aecf9f92 100644 --- a/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp +++ b/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp @@ -7,8 +7,8 @@ mdp // variables to represent whether a process has a token or not // note they are global because they can be updated by other processes #for i=1:N# -global q#i# : [0..1]; -#end# +global q#i# : [0..1]; +#end# // module of process 1 module process1 @@ -29,11 +29,12 @@ endrewards // formula, for use here and in properties: number of tokens 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) init num_tokens >= 1 endinit - +