|
| | | Tutorial |
Let us describe a small example. We will model a client and a server which communicate through a two unreliable channels (a channel for each way). The client has to send a sequence of M different requests to the server. The server treat the request and send an acknowlegdement. If there is a failure (we suppose that the client can detect it), the client can retry twice to send the request. On completion, the sender emit the message CORR, otherwise the message ERR.
We first declare the set of channels:
channel
S_send,S_receive,S_lost,
A_send,A_receive,A_lost,
START,CORR,ERR;
If we had global variables, we would also declare them here.
Then we define the SendLine and AckLine processes. The keyword sync allows to define the set of channels on which the process synchronize. init defines the root state(s). The sign # is used to refer to a location name. Then the list of locations, together with their outgoing transitions, is described. when introduces the possible guard on variables, sync specifies a possible synchronization channel for the transition, and goto the destination location or the distribution over several destination locations.
process SendLine {
sync
S_send,S_receive,S_lost;
init
#idle;
loc idle:
when true sync S_send goto { sent 0.8; lost 0.2 };
loc sent:
when true sync S_receive goto idle;
loc lost:
when true sync S_lost goto idle;
}
process AckLine {
sync
A_send,A_receive,A_lost;
init
#idle;
loc idle:
when true sync A_send goto { sent 0.9; lost 0.1 };
loc sent:
when true sync A_receive goto idle;
loc lost:
when true sync A_lost goto idle;
}
The more complex process is the Client process. This process owns two local variables. Their type is uint(2), which means: 2-bits unsigned integers. Here the destination locations are possibly followed by an assign instruction which specifies the new values of some variables
process Client {
sync
S_send,S_lost,A_lost,A_receive,
START,CORR,ERR;
var
n,msg : uint(2);
init
#idle;
loc idle:
when true sync START goto msg assign { msg := uint(2)0 };
loc msg:
when true sync S_send goto wait assign { n := uint(2)0 };
loc wait:
when msg < uint(2)3 sync A_receive goto msg assign { msg := msg + uint(2)1 };
when msg = uint(2)3 sync A_receive goto end;
when true sync S_lost goto retry;
when true sync A_lost goto retry;
loc retry:
when n < uint(2)3 sync S_send goto wait assign { n := n + uint(2)1 };
when n = uint(2)3 sync ERR goto idle;
loc end:
when true sync CORR goto idle;
}
Last, we have the (dummy) Server process:
process Server {
sync
S_receive,A_send,A_receive,A_lost;
init
#idle;
loc idle:
when true sync S_receive goto task;
loc task:
when true sync A_send goto wait;
loc wait:
when true sync A_receive goto idle;
when true sync A_lost goto idle;
}
Now we specify the property. We refer to locations and local variables by prefixing them with the name of the owner process. system the set of processes that are composed in parallel, and initial and final two sets of states. Basically, we want to check properties about the probability to reach a final state from an initial state during an execution of the system.
system SendLine,AckLine,Client,Server; initial #Client.idle; final #Client.end;
In this case, what is the probability to successfully send all the messages without any transmission error ?
We will use for this property the version of the tool which uses the CDDLIB LP solver. Let us type probr.opt -exact -goal s0.5 example.prob. We get the following output:
- Syntaxical analysis
- Semantic analysis, transformation into Bdds
** computing processes and expressions
** Boolean composition
** Boolean analysis
Initially: 15 state variables, 32768 states
relation: 396 nodes
Reordering...
Reachability analysis from init: 184 states, 35 nodes
Reachability analysis from initial: 184 states, 35 nodes
psup0: 0 states, 1 nodes
Extending final states
All reachable initial states are also pinf1; pinf = psup = 1.0
Example: (SendLine.loc=idle)(AckLine.loc=idle)(Client.loc=idle)
(Server.loc=idle)
Note: Using Rapture 2.0.0, one gets a slightly different output than the one displayed above, but the essential results remain the same.
The tool discovered by discrete fixpoint analysis that every initial state has a probability 1 to lead eventually to a final state. After some reflexion, it appears that it is perfectly right: as the sender process can send a new message after having emitted ERR and as the failure probability is strictly less than 1, you eventually lead to a final state with probability 1.
What we actually want to check is the probability to send correctly one message. Let's add the following process into the system.
process Sync2 {
sync
START,CORR;
init
#idle;
loc idle:
when true sync START goto run;
loc run:
when true sync CORR goto end;
loc end:
}
and let's write the new property
system SendLine,AckLine,Client,Server,Sync2; initial #Sync2.idle; final #Sync2.end;
We get the following output:
- Syntaxical analysis
- Semantic analysis, transformation into Bdds
** computing processes and expressions
** Boolean composition
** Boolean analysis
Initially: 17 state variables, 131072 states
relation: 469 nodes
Reordering...
Reachability analysis from init: 192 states, 49 nodes
Reachability analysis from initial: 192 states, 49 nodes
psup0: 16 states, 31 nodes
Extending final states
Second reachability analysis from initial: 176 states, 40 nodes
Non-sink state space: 164 states, 57 nodes
Psup=1: 4 states
in 0.08 seconds
** computing global probabilistic transition function
** size of the transition function: 319 nodes, 1550 paths, 6 leaves
System build and analysed (Boolean analysis) in 0.12 seconds
Building initial partition in 0.01 seconds
Step 1, automaton has 10 locations and 12 nails, 5420 bytes
essential automaton has 5 locations and 7 nails
Computing psup: discrete analysis, 1.0
pinf=-inf psup=1 diff=inf
analysis in 0 seconds
refining in 0.01 seconds
Step 2, automaton has 16 locations and 22 nails, 9564 bytes
essential automaton has 9 locations and 15 nails
Computing psup: discrete analysis, 1.0
pinf=-inf psup=1 diff=inf
analysis in 0 seconds
refining in 0.03 seconds
Step 3, automaton has 29 locations and 38 nails, 15784 bytes
essential automaton has 20 locations and 29 nails
Computing psup: discrete analysis, 1.0
pinf=-inf psup=1 diff=inf
analysis in 0 seconds
refining in 0.02 seconds
Step 4, automaton has 44 locations and 48 nails, 20380 bytes
essential automaton has 21 locations and 25 nails
Computing psup: 19 variables, 25 constraints, 13 equalities;
pinf=-inf psup=0.990478425818 diff=inf
analysis in 0.03 seconds
refining in 0.03 seconds
Step 5, automaton has 68 locations and 70 nails, 29748 bytes
essential automaton has 30 locations and 32 nails
Computing psup: 28 variables, 32 constraints, 24 equalities;
pinf=-inf psup=0.981673428381 diff=inf
analysis in 0.02 seconds
refining in 0.02 seconds
Step 6, automaton has 78 locations and 76 nails, 32068 bytes
essential automaton has 34 locations and 32 nails
Computing psup: 32 variables, 32 constraints, 32 equalities;
pinf=-inf psup=0.975639513753 diff=inf
analysis in 0.01 seconds
refining in 0 seconds
** Failure **
After 6 steps and 13 divisions, final automaton has 78 locations
pinf=-inf psup=0.975639513753 diff=inf
Times in seconds:
building: 0.12
analysis: 0.18 (numerical computations: 0.06; refinement: 0.12)
The property is false, because the Psup <= 0.5 on the stabilized partition of the system. As every member of this partition are bisimulation equivalence classes, we get that Psup=.975639513753 on the concrete system.
|
| | | Tutorial |