154 changed files with 55965 additions and 1 deletions
-
116resources/examples/testfiles/ctmc/cluster2.sm
-
151resources/examples/testfiles/ctmc/embedded2.sm
-
126resources/examples/testfiles/ctmc/fms2.sm
-
53resources/examples/testfiles/ctmc/polling2.sm
-
42resources/examples/testfiles/ctmc/tandem5.sm
-
136resources/examples/testfiles/dtmc/brp-16-2.pm
-
69resources/examples/testfiles/dtmc/crowds-5-5.pm
-
69resources/examples/testfiles/dtmc/crowds5_5.pm
-
10resources/examples/testfiles/dtmc/die.lab
-
32resources/examples/testfiles/dtmc/die.pm
-
21resources/examples/testfiles/dtmc/die.tra
-
85resources/examples/testfiles/dtmc/leader-3-5.pm
-
85resources/examples/testfiles/dtmc/leader3_5.pm
-
76resources/examples/testfiles/dtmc/nand-5-2.pm
-
18resources/examples/testfiles/dtmc/test_conditional.pm
-
15resources/examples/testfiles/lab/autoParser.lab
-
5889resources/examples/testfiles/lab/crowds5_5.lab
-
7resources/examples/testfiles/lab/declarationMisspell.lab
-
10resources/examples/testfiles/lab/die.lab
-
14resources/examples/testfiles/lab/doubledLines.lab
-
9resources/examples/testfiles/lab/doubledLinesSkipped.lab
-
11resources/examples/testfiles/lab/dtmc_actionTest.lab
-
11resources/examples/testfiles/lab/dtmc_general.lab
-
11resources/examples/testfiles/lab/dtmc_mismatched.lab
-
6resources/examples/testfiles/lab/endMisspell.lab
-
6resources/examples/testfiles/lab/labelForNonexistentState.lab
-
8resources/examples/testfiles/lab/leader4.lab
-
5resources/examples/testfiles/lab/leader4_8.lab
-
7resources/examples/testfiles/lab/ma_cslFilterTest.lab
-
6resources/examples/testfiles/lab/ma_general.lab
-
7resources/examples/testfiles/lab/ma_mismatched.lab
-
8resources/examples/testfiles/lab/mdp_general.lab
-
7resources/examples/testfiles/lab/mdp_mismatched.lab
-
6resources/examples/testfiles/lab/noDeclarationTag.lab
-
5resources/examples/testfiles/lab/noEndTag.lab
-
2resources/examples/testfiles/lab/noLabelsDecNoneGiven.lab
-
6resources/examples/testfiles/lab/pctl_general.lab
-
6resources/examples/testfiles/lab/swappedStateAndProposition.lab
-
7resources/examples/testfiles/lab/tiny1.lab
-
7resources/examples/testfiles/lab/tiny2.lab
-
40resources/examples/testfiles/lab/two_dice.lab
-
6resources/examples/testfiles/lab/undeclaredLabelsGiven.lab
-
11resources/examples/testfiles/lab/withWhitespaces.lab
-
11resources/examples/testfiles/lab/withoutWhitespaces.lab
-
19resources/examples/testfiles/ma/hybrid_states.ma
-
15resources/examples/testfiles/ma/simple.ma
-
50resources/examples/testfiles/ma/stream2.ma
-
26resources/examples/testfiles/mdp/SmallPrismTest.nm
-
28resources/examples/testfiles/mdp/SmallPrismTest2.nm
-
60resources/examples/testfiles/mdp/coin2-2-illegalSynchronizingWrite.nm
-
60resources/examples/testfiles/mdp/coin2-2.nm
-
60resources/examples/testfiles/mdp/coin2.nm
-
130resources/examples/testfiles/mdp/csma2-2.nm
-
130resources/examples/testfiles/mdp/csma2_2.nm
-
33resources/examples/testfiles/mdp/die_c1.nm
-
45resources/examples/testfiles/mdp/die_selection.nm
-
170resources/examples/testfiles/mdp/firewire.nm
-
170resources/examples/testfiles/mdp/firewire3-0.5.nm
-
91resources/examples/testfiles/mdp/leader3.nm
-
88resources/examples/testfiles/mdp/leader4.nm
-
20resources/examples/testfiles/mdp/multiobjective1.nm
-
20resources/examples/testfiles/mdp/multiobjective2.nm
-
16resources/examples/testfiles/mdp/scheduler_generation.nm
-
30resources/examples/testfiles/mdp/system_composition.nm
-
30resources/examples/testfiles/mdp/system_composition2.nm
-
17resources/examples/testfiles/mdp/tiny_rewards.nm
-
40resources/examples/testfiles/mdp/two_dice.lab
-
40resources/examples/testfiles/mdp/two_dice.nm
-
437resources/examples/testfiles/mdp/two_dice.tra
-
219resources/examples/testfiles/mdp/wlan0-2-2.nm
-
219resources/examples/testfiles/mdp/wlan0_collide.nm
-
148resources/examples/testfiles/pdtmc/brp16_2.pm
-
148resources/examples/testfiles/pdtmc/brp_rewards16_2.pm
-
194resources/examples/testfiles/pdtmc/crowds3_5.pm
-
34resources/examples/testfiles/pdtmc/parametric_die.pm
-
56resources/examples/testfiles/pmdp/coin2_2.pm
-
45resources/examples/testfiles/pmdp/two_dice.nm
-
1resources/examples/testfiles/prctl/apOnly.prctl
-
1resources/examples/testfiles/prctl/complexFormula.prctl
-
1resources/examples/testfiles/prctl/probabilisticFormula.prctl
-
1resources/examples/testfiles/prctl/probabilisticNoBoundFormula.prctl
-
1resources/examples/testfiles/prctl/propositionalFormula.prctl
-
1resources/examples/testfiles/prctl/rewardFormula.prctl
-
1resources/examples/testfiles/prctl/rewardNoBoundFormula.prctl
-
4resources/examples/testfiles/prctl/two_dice.prctl
-
12resources/examples/testfiles/rew/autoParser.state.rew
-
14resources/examples/testfiles/rew/die.coin_flips.trans.rew
-
8resources/examples/testfiles/rew/dtmc_general.state.rew
-
17resources/examples/testfiles/rew/dtmc_general.trans.rew
-
16resources/examples/testfiles/rew/dtmc_mismatched.trans.rew
-
17resources/examples/testfiles/rew/dtmc_mixedStateOrder.trans.rew
-
17resources/examples/testfiles/rew/dtmc_mixedTransitionOrder.trans.rew
-
18resources/examples/testfiles/rew/dtmc_rewardForNonExTrans.trans.rew
-
23resources/examples/testfiles/rew/dtmc_whitespaces.trans.rew
-
661resources/examples/testfiles/rew/leader4.trans.rew
-
4096resources/examples/testfiles/rew/leader4_8.pick.trans.rew
-
6resources/examples/testfiles/rew/ma_general.state.rew
-
7resources/examples/testfiles/rew/ma_mismatched.state.rew
-
6resources/examples/testfiles/rew/mdp_general.state.rew
-
17resources/examples/testfiles/rew/mdp_general.trans.rew
@ -0,0 +1,116 @@ |
|||||
|
// Workstation cluster [HHK00] |
||||
|
// dxp/gxn 11/01/00 |
||||
|
|
||||
|
ctmc |
||||
|
|
||||
|
const int N = 2; // Number of workstations in each cluster |
||||
|
const int left_mx = N; // Number of work stations in left cluster |
||||
|
const int right_mx = N; // Number of work stations in right cluster |
||||
|
|
||||
|
// Failure rates |
||||
|
const double ws_fail = 1/500; // Single workstation: average time to fail = 500 hrs |
||||
|
const double switch_fail = 1/4000; // Switch: average time to fail = 4000 hrs |
||||
|
const double line_fail = 1/5000; // Backbone: average time to fail = 5000 hrs |
||||
|
|
||||
|
// Left cluster |
||||
|
module Left |
||||
|
|
||||
|
left_n : [0..left_mx] init left_mx; // Number of workstations operational |
||||
|
left : bool; // Being repaired? |
||||
|
|
||||
|
[startLeft] !left & (left_n<left_mx) -> 1 : (left'=true); |
||||
|
[repairLeft] left & (left_n<left_mx) -> 1 : (left'=false) & (left_n'=left_n+1); |
||||
|
[] (left_n>0) -> ws_fail*left_n : (left_n'=left_n-1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// Right cluster |
||||
|
module Right = Left[left_n=right_n, |
||||
|
left=right, |
||||
|
left_mx=right_mx, |
||||
|
startLeft=startRight, |
||||
|
repairLeft=repairRight ] |
||||
|
endmodule |
||||
|
|
||||
|
// Repair unit |
||||
|
module Repairman |
||||
|
|
||||
|
r : bool; // Repairing? |
||||
|
|
||||
|
[startLeft] !r -> 10 : (r'=true); // Inspect Left |
||||
|
[startRight] !r -> 10 : (r'=true); // Inspect Right |
||||
|
[startToLeft] !r -> 10 : (r'=true); // Inspect ToLeft |
||||
|
[startToRight] !r -> 10 : (r'=true); // Inspect ToRight |
||||
|
[startLine] !r -> 10 : (r'=true); // Inspect Line |
||||
|
|
||||
|
[repairLeft] r -> 2 : (r'=false); // Repair Left |
||||
|
[repairRight] r -> 2 : (r'=false); // Repair Right |
||||
|
[repairToLeft] r -> 0.25 : (r'=false); // Repair ToLeft |
||||
|
[repairToRight] r -> 0.25 : (r'=false); // Repair ToRight |
||||
|
[repairLine] r -> 0.125 : (r'=false); // Repair Line |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// Line/backbone |
||||
|
module Line |
||||
|
|
||||
|
line : bool; // Being repaired? |
||||
|
line_n : bool init true; // Working? |
||||
|
|
||||
|
[startLine] !line & !line_n -> 1 : (line'=true); |
||||
|
[repairLine] line & !line_n -> 1 : (line'=false) & (line_n'=true); |
||||
|
[] line_n -> line_fail : (line_n'=false); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// Left switch |
||||
|
module ToLeft = Line[line=toleft, |
||||
|
line_n=toleft_n, |
||||
|
line_fail=switch_fail, |
||||
|
startLine=startToLeft, |
||||
|
repairLine=repairToLeft ] |
||||
|
endmodule |
||||
|
|
||||
|
// Right switch |
||||
|
module ToRight = Line[line=toright, |
||||
|
line_n=toright_n, |
||||
|
line_fail=switch_fail, |
||||
|
startLine=startToRight, |
||||
|
repairLine=repairToRight ] |
||||
|
endmodule |
||||
|
|
||||
|
// Formulas + labels |
||||
|
|
||||
|
// Minimum QoS requires 3/4 connected workstations operational |
||||
|
const int k = floor(0.75*N); |
||||
|
// left_operational_i : left_n>=i & toleft_n |
||||
|
// right_operational_i : right_n>=i & toright_n |
||||
|
// operational_i : (left_n+right_n)>=i & toleft_n & line_n & toright_n |
||||
|
// minimum_k : left_operational_k | right_operational_k | operational_k |
||||
|
formula minimum = (left_n>=k & toleft_n) | |
||||
|
(right_n>=k & toright_n) | |
||||
|
((left_n+right_n)>=k & toleft_n & line_n & toright_n); |
||||
|
label "minimum" = (left_n>=k & toleft_n) | (right_n>=k & toright_n) | ((left_n+right_n)>=k & toleft_n & line_n & toright_n); |
||||
|
// premium = minimum_N |
||||
|
label "premium" = (left_n>=left_mx & toleft_n) | (right_n>=right_mx & toright_n) | ((left_n+right_n)>=left_mx & toleft_n & line_n & toright_n); |
||||
|
|
||||
|
// Reward structures |
||||
|
|
||||
|
// Percentage of operational workstations stations |
||||
|
//rewards "percent_op" |
||||
|
// true : 100*(left_n+right_n)/(2*N); |
||||
|
//endrewards |
||||
|
|
||||
|
// Time that the system is not delivering at least minimum QoS |
||||
|
//rewards "time_not_min" |
||||
|
// !minimum : 1; |
||||
|
//endrewards |
||||
|
|
||||
|
// Number of repairs |
||||
|
rewards "num_repairs" |
||||
|
[repairLeft] true : 1; |
||||
|
[repairRight] true : 1; |
||||
|
[repairToLeft] true : 1; |
||||
|
[repairToRight] true : 1; |
||||
|
[repairLine] true : 1; |
||||
|
endrewards |
@ -0,0 +1,151 @@ |
|||||
|
ctmc |
||||
|
|
||||
|
// constants |
||||
|
const int MAX_COUNT = 2; |
||||
|
const int MIN_SENSORS = 2; |
||||
|
const int MIN_ACTUATORS = 1; |
||||
|
|
||||
|
// rates |
||||
|
const double lambda_p = 1/(365*24*60*60); // 1 year |
||||
|
const double lambda_s = 1/(30*24*60*60); // 1 month |
||||
|
const double lambda_a = 1/(2*30*24*60*60); // 2 months |
||||
|
const double tau = 1/60; // 1 min |
||||
|
const double delta_f = 1/(24*60*60); // 1 day |
||||
|
const double delta_r = 1/30; // 30 secs |
||||
|
|
||||
|
// sensors |
||||
|
module sensors |
||||
|
|
||||
|
s : [0..3] init 3; // number of sensors working |
||||
|
|
||||
|
[] s>1 -> s*lambda_s : (s'=s-1); // failure of a single sensor |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// input processor |
||||
|
// (takes data from sensors and passes onto main processor) |
||||
|
module proci |
||||
|
|
||||
|
i : [0..2] init 2; // 2=ok, 1=transient fault, 0=failed |
||||
|
|
||||
|
[] i>0 & s>=MIN_SENSORS -> lambda_p : (i'=0); // failure of processor |
||||
|
[] i=2 & s>=MIN_SENSORS -> delta_f : (i'=1); // transient fault |
||||
|
[input_reboot] i=1 & s>=MIN_SENSORS -> delta_r : (i'=2); // reboot after transient fault |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// actuators |
||||
|
module actuators |
||||
|
|
||||
|
a : [0..2] init 2; // number of actuators working |
||||
|
|
||||
|
[] a>0 -> a*lambda_a : (a'=a-1); // failure of a single actuator |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// output processor |
||||
|
// (receives instructions from main processor and passes onto actuators) |
||||
|
module proco = proci [ i=o, s=a, input_reboot=output_reboot, MIN_SENSORS=MIN_ACTUATORS ] endmodule |
||||
|
|
||||
|
// main processor |
||||
|
// (takes data from proci, processes it, and passes instructions to proco) |
||||
|
module procm |
||||
|
|
||||
|
m : [0..1] init 1; // 1=ok, 0=failed |
||||
|
count : [0..MAX_COUNT+1] init 0; // number of consecutive skipped cycles |
||||
|
|
||||
|
// failure of processor |
||||
|
[] m=1 -> lambda_p : (m'=0); |
||||
|
// processing completed before timer expires - reset skipped cycle counter |
||||
|
[timeout] comp -> tau : (count'=0); |
||||
|
// processing not completed before timer expires - increment skipped cycle counter |
||||
|
[timeout] !comp -> tau : (count'=min(count+1, MAX_COUNT+1)); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// connecting bus |
||||
|
module bus |
||||
|
|
||||
|
// flags |
||||
|
// main processor has processed data from input processor |
||||
|
// and sent corresponding instructions to output processor (since last timeout) |
||||
|
comp : bool init true; |
||||
|
// input processor has data ready to send |
||||
|
reqi : bool init true; |
||||
|
// output processor has instructions ready to be processed |
||||
|
reqo : bool init false; |
||||
|
|
||||
|
// input processor reboots |
||||
|
[input_reboot] true -> 1 : |
||||
|
// performs a computation if has already done so or |
||||
|
// it is up and ouput clear (i.e. nothing waiting) |
||||
|
(comp'=(comp | (m=1 & !reqo))) |
||||
|
// up therefore something to process |
||||
|
& (reqi'=true) |
||||
|
// something to process if not functioning and either |
||||
|
// there is something already pending |
||||
|
// or the main processor sends a request |
||||
|
& (reqo'=!(o=2 & a>=1) & (reqo | m=1)); |
||||
|
|
||||
|
// output processor reboots |
||||
|
[output_reboot] true -> 1 : |
||||
|
// performs a computation if it has already or |
||||
|
// something waiting and is up |
||||
|
// (can be processes as the output has come up and cleared pending requests) |
||||
|
(comp'=(comp | (reqi & m=1))) |
||||
|
// something to process it they are up or |
||||
|
// there was already something and the main processor acts |
||||
|
// (output now up must be due to main processor being down) |
||||
|
& (reqi'=(i=2 & s>=2) | (reqi & m=0)) |
||||
|
// output and actuators up therefore nothing can be pending |
||||
|
& (reqo'=false); |
||||
|
|
||||
|
// main processor times out |
||||
|
[timeout] true -> 1 : |
||||
|
// performs a computation if it is up something was pending |
||||
|
// and nothing is waiting for the output |
||||
|
(comp'=(reqi & !reqo & m=1)) |
||||
|
// something to process if up or |
||||
|
// already something and main process cannot act |
||||
|
// (down or outputs pending) |
||||
|
& (reqi'=(i=2 & s>=2) | (reqi & (reqo | m=0))) |
||||
|
// something to process if they are not functioning and |
||||
|
// either something is already pending |
||||
|
// or the main processor acts |
||||
|
& (reqo'=!(o=2 & a>=1) & (reqo | (reqi & m=1))); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
|
||||
|
// the system is down |
||||
|
formula down = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0); |
||||
|
// transient failure has occured but the system is not down |
||||
|
formula danger = !down & (i=1 | o=1); |
||||
|
// the system is operational |
||||
|
formula up = !down & !danger; |
||||
|
|
||||
|
|
||||
|
// reward structures |
||||
|
|
||||
|
rewards "up" |
||||
|
up : 1/3600; |
||||
|
endrewards |
||||
|
|
||||
|
rewards "danger" |
||||
|
danger : 1/3600; |
||||
|
endrewards |
||||
|
rewards "down" |
||||
|
down : 1/3600; |
||||
|
endrewards |
||||
|
|
||||
|
//labels |
||||
|
// causes of failues |
||||
|
label "fail_sensors" = i=2&s<MIN_SENSORS; // sensors have failed |
||||
|
label "fail_actuators" = o=2&a<MIN_ACTUATORS; // actuators have failed |
||||
|
label "fail_io" = count=MAX_COUNT+1; // IO has failed |
||||
|
label "fail_main" = m=0; // ,main processor has failed |
||||
|
|
||||
|
// system status |
||||
|
label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0); // system has shutdown |
||||
|
label "danger" = !down & (i=1 | o=1); // transient fault has occured |
||||
|
label "up" = !down & !danger; |
@ -0,0 +1,126 @@ |
|||||
|
// flexible manufacturing system [CT93] |
||||
|
// gxn/dxp 11/06/01 |
||||
|
|
||||
|
ctmc // model is a ctmc |
||||
|
|
||||
|
const int n = 2; // number of tokens |
||||
|
|
||||
|
// rates from Pi equal #(Pi) * min(1, np/r) |
||||
|
// where np = (3n)/2 and r = P1+P2+P3+P12 |
||||
|
const int np=floor((3*n)/2); |
||||
|
formula r = P1+P2+P3+P12; |
||||
|
|
||||
|
module machine1 |
||||
|
|
||||
|
P1 : [0..n] init n; |
||||
|
P1wM1 : [0..n]; |
||||
|
P1M1 : [0..3]; |
||||
|
P1d : [0..n]; |
||||
|
P1s : [0..n]; |
||||
|
P1wP2 : [0..n]; |
||||
|
M1 : [0..3] init 3; |
||||
|
|
||||
|
[t1] (P1>0) & (M1>0) & (P1M1<3) -> P1*min(1,np/r) : (P1'=P1-1) & (P1M1'=P1M1+1) & (M1'=M1-1); |
||||
|
[t1] (P1>0) & (M1=0) & (P1wM1<n) -> P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1); |
||||
|
|
||||
|
[] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s<n) -> 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1); |
||||
|
[] (P1M1>0) & (P1wM1>0) & (P1s<n) -> 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1); |
||||
|
|
||||
|
[] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2<n) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1); |
||||
|
[] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2<n) -> 0.05*P1M1 : (P1wM1'=P1wM1-1) & (P1wP2'=P1wP2+1); |
||||
|
|
||||
|
[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1=0) & (M1<3) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1); |
||||
|
[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1>0) -> 0.05*P1M1 : (P1wM1'=P1wM1-1); |
||||
|
|
||||
|
[p1p2] (P1wP2>0) -> 1: (P1wP2'=P1wP2-1); |
||||
|
[] (P1s>0) & (P1+P1s<=n) -> 1/60 : (P1s'=0) & (P1'=P1+P1s); |
||||
|
[fp12] (P1+P12s<=n) -> 1: (P1'=P1+P12s); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module machine2 |
||||
|
|
||||
|
P2 : [0..n] init n; |
||||
|
P2wM2 : [0..n]; |
||||
|
P2M2 : [0..1]; |
||||
|
P2s : [0..n]; |
||||
|
P2wP1 : [0..n]; |
||||
|
M2 : [0..1] init 1; |
||||
|
|
||||
|
[t2] (P2>0) & (M2>0) & (P2M2<1) -> P2*min(1,np/r) : (P2'=P2-1) & (P2M2'=P2M2+1) & (M2'=M2-1); |
||||
|
[t2] (P2>0) & (M2=0) & (P2wM2<n) -> P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1); |
||||
|
|
||||
|
[] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s<n) -> 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1); |
||||
|
[] (P2M2>0) & (P2wM2>0) & (P2s<n) -> 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1); |
||||
|
|
||||
|
[] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1<n) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1); |
||||
|
[] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1<n) -> 1/15: (P2wM2'=P2wM2-1) & (P2wP1'=P2wP1+1); |
||||
|
|
||||
|
[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2=0) & (M2<1) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1); |
||||
|
[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2>0) -> 1/15: (P2wM2'=P2wM2-1); |
||||
|
|
||||
|
[p1p2] (P2wP1>0) -> 1 : (P2wP1'=P2wP1-1); |
||||
|
[] (P2s>0) & (P2+P2s<=n) -> 1/60 : (P2s'=0) & (P2'=P2+P2s); |
||||
|
[fp12] (P2+P12s<=n) -> 1 : (P2'=P2+P12s); |
||||
|
[p2p3] (M2>0) -> 1 : (M2'=M2); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module machine3 |
||||
|
|
||||
|
P3 : [0..n] init n; |
||||
|
P3M2 : [0..n]; |
||||
|
P3s : [0..n]; |
||||
|
|
||||
|
[t3] (P3>0) & (P3M2<n) -> P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1); |
||||
|
|
||||
|
[p2p3] (P3M2>0) & (P3s<n) -> 1/2 : (P3M2'=P3M2-1) & (P3s'=P3s+1); |
||||
|
[] (P3s>0) & (P3+P3s<=n) -> 1/60 : (P3s'=0) & (P3'=P3+P3s); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module machine12 |
||||
|
|
||||
|
P12 : [0..n]; |
||||
|
P12wM3 : [0..n]; |
||||
|
P12M3 : [0..2]; |
||||
|
P12s : [0..n]; |
||||
|
M3 : [0..2] init 2; |
||||
|
|
||||
|
[p1p2] (P12<n) -> 1: (P12'=P12+1); |
||||
|
|
||||
|
[t12] (P12>0) & (M3>0) & (P12M3<2) -> P12*min(1,np/r) : (P12'=P12-1) & (P12M3'=P12M3+1) & (M3'=M3-1); |
||||
|
[t12] (P12>0) & (M3=0) & (P12wM3<n) -> P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1); |
||||
|
|
||||
|
[] (P12M3>0) & (P12wM3=0) & (P12s<n) & (M3<2) -> P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1); |
||||
|
[] (P12M3>0) & (P12wM3>0) & (P12s<n) -> P12M3 : (P12wM3'=P12wM3-1) & (P12s'=P12s+1); |
||||
|
|
||||
|
[fp12] (P12s>0) -> 1/60 : (P12s'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// reward structures |
||||
|
|
||||
|
// throughput of machine1 |
||||
|
rewards "throughput_m1" |
||||
|
[t1] true : 1; |
||||
|
endrewards |
||||
|
// throughput of machine2 |
||||
|
rewards "throughput_m2" |
||||
|
[t2] true : 1; |
||||
|
endrewards |
||||
|
// throughput of machine3 |
||||
|
rewards "throughput_m3" |
||||
|
[t3] true : 1; |
||||
|
endrewards |
||||
|
// throughput of machine12 |
||||
|
rewards "throughput_m12" |
||||
|
[t12] true : 1; |
||||
|
endrewards |
||||
|
// productivity of the system |
||||
|
rewards "productivity" |
||||
|
[t1] true : 400; |
||||
|
[t2] true : 600; |
||||
|
[t3] true : 100; |
||||
|
[t12] true : 1100; |
||||
|
endrewards |
@ -0,0 +1,53 @@ |
|||||
|
// polling example [IT90] |
||||
|
// gxn/dxp 26/01/00 |
||||
|
|
||||
|
ctmc |
||||
|
|
||||
|
const int N = 2; |
||||
|
|
||||
|
const double mu = 1; |
||||
|
const double gamma = 200; |
||||
|
const double lambda = mu/N; |
||||
|
|
||||
|
module server |
||||
|
|
||||
|
s : [1..2]; // station |
||||
|
a : [0..1]; // action: 0=polling, 1=serving |
||||
|
|
||||
|
[loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); |
||||
|
[loop1b] (s=1)&(a=0) -> gamma : (a'=1); |
||||
|
[serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); |
||||
|
|
||||
|
[loop2a] (s=2)&(a=0) -> gamma : (s'=1); |
||||
|
[loop2b] (s=2)&(a=0) -> gamma : (a'=1); |
||||
|
[serve2] (s=2)&(a=1) -> mu : (s'=1)&(a'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module station1 |
||||
|
|
||||
|
s1 : [0..1]; // state of station: 0=empty, 1=full |
||||
|
|
||||
|
[loop1a] (s1=0) -> 1 : (s1'=0); |
||||
|
[] (s1=0) -> lambda : (s1'=1); |
||||
|
[loop1b] (s1=1) -> 1 : (s1'=1); |
||||
|
[serve1] (s1=1) -> 1 : (s1'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct further stations through renaming |
||||
|
|
||||
|
module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule |
||||
|
// (cumulative) rewards |
||||
|
|
||||
|
// expected time station 1 is waiting to be served |
||||
|
rewards "waiting" |
||||
|
s1=1 & !(s=1 & a=1) : 1; |
||||
|
endrewards |
||||
|
|
||||
|
// expected number of times station 1 is served |
||||
|
rewards "served" |
||||
|
[serve1] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=1&a=0; |
@ -0,0 +1,42 @@ |
|||||
|
// tandem queueing network [HKMKS99] |
||||
|
// gxn/dxp 25/01/00 |
||||
|
|
||||
|
ctmc |
||||
|
|
||||
|
const int c = 5; // queue capacity |
||||
|
|
||||
|
const double lambda = 4*c; |
||||
|
const double mu1a = 0.1*2; |
||||
|
const double mu1b = 0.9*2; |
||||
|
const double mu2 = 2; |
||||
|
const double kappa = 4; |
||||
|
|
||||
|
module serverC |
||||
|
|
||||
|
sc : [0..c]; |
||||
|
ph : [1..2]; |
||||
|
|
||||
|
[] (sc<c) -> lambda: (sc'=sc+1); |
||||
|
[route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1); |
||||
|
[] (sc>0) & (ph=1) -> mu1a: (ph'=2); |
||||
|
[route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module serverM |
||||
|
|
||||
|
sm : [0..c]; |
||||
|
|
||||
|
[route] (sm<c) -> 1: (sm'=sm+1); |
||||
|
[] (sm>0) -> kappa: (sm'=sm-1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// reward - number of customers in network |
||||
|
rewards "customers" |
||||
|
true : sc + sm; |
||||
|
endrewards |
||||
|
|
||||
|
label "network_full" = sc=c&sm=c&ph=2; |
||||
|
label "first_queue_full" = sc=c; |
||||
|
label "second_queue_full" = sm=c; |
@ -0,0 +1,136 @@ |
|||||
|
// bounded retransmission protocol [D'AJJL01] |
||||
|
// gxn/dxp 23/05/2001 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// number of chunks |
||||
|
const int N = 16; |
||||
|
// maximum number of retransmissions |
||||
|
const int MAX = 2; |
||||
|
|
||||
|
module sender |
||||
|
|
||||
|
s : [0..6]; |
||||
|
// 0 idle |
||||
|
// 1 next_frame |
||||
|
// 2 wait_ack |
||||
|
// 3 retransmit |
||||
|
// 4 success |
||||
|
// 5 error |
||||
|
// 6 wait sync |
||||
|
srep : [0..3]; |
||||
|
// 0 bottom |
||||
|
// 1 not ok (nok) |
||||
|
// 2 do not know (dk) |
||||
|
// 3 ok (ok) |
||||
|
nrtr : [0..MAX]; |
||||
|
i : [0..N]; |
||||
|
bs : bool; |
||||
|
s_ab : bool; |
||||
|
fs : bool; |
||||
|
ls : bool; |
||||
|
|
||||
|
// idle |
||||
|
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); |
||||
|
// next_frame |
||||
|
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); |
||||
|
// wait_ack |
||||
|
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); |
||||
|
[TO_Msg] (s=2) -> (s'=3); |
||||
|
[TO_Ack] (s=2) -> (s'=3); |
||||
|
// retransmit |
||||
|
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); |
||||
|
// success |
||||
|
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1); |
||||
|
[] (s=4) & (i=N) -> (s'=0) & (srep'=3); |
||||
|
// error |
||||
|
[SyncWait] (s=5) -> (s'=6); |
||||
|
// wait sync |
||||
|
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module receiver |
||||
|
|
||||
|
r : [0..5]; |
||||
|
// 0 new_file |
||||
|
// 1 fst_safe |
||||
|
// 2 frame_received |
||||
|
// 3 frame_reported |
||||
|
// 4 idle |
||||
|
// 5 resync |
||||
|
rrep : [0..4]; |
||||
|
// 0 bottom |
||||
|
// 1 fst |
||||
|
// 2 inc |
||||
|
// 3 ok |
||||
|
// 4 nok |
||||
|
fr : bool; |
||||
|
lr : bool; |
||||
|
br : bool; |
||||
|
r_ab : bool; |
||||
|
recv : bool; |
||||
|
|
||||
|
|
||||
|
// new_file |
||||
|
[SyncWait] (r=0) -> (r'=0); |
||||
|
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
// fst_safe_frame |
||||
|
[] (r=1) -> (r'=2) & (r_ab'=br); |
||||
|
// frame_received |
||||
|
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); |
||||
|
[aA] (r=2) & !(r_ab=br) -> (r'=4); |
||||
|
// frame_reported |
||||
|
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); |
||||
|
// idle |
||||
|
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
[SyncWait] (r=4) & (ls=true) -> (r'=5); |
||||
|
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); |
||||
|
// resync |
||||
|
[SyncWait] (r=5) -> (r'=0) & (rrep'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module checker // prevents more than one frame being set |
||||
|
|
||||
|
T : bool; |
||||
|
|
||||
|
[NewFile] (T=false) -> (T'=true); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelK |
||||
|
|
||||
|
k : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2); |
||||
|
// sending |
||||
|
[aG] (k=1) -> (k'=0); |
||||
|
// lost |
||||
|
[TO_Msg] (k=2) -> (k'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelL |
||||
|
|
||||
|
l : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2); |
||||
|
// sending |
||||
|
[aB] (l=1) -> (l'=0); |
||||
|
// lost |
||||
|
[TO_Ack] (l=2) -> (l'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
[aF] i=1 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=5; |
@ -0,0 +1,69 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
// probability of forwarding |
||||
|
const double PF = 0.8; |
||||
|
const double notPF = .2; // must be 1-PF |
||||
|
// probability that a crowd member is bad |
||||
|
const double badC = .167; |
||||
|
// probability that a crowd member is good |
||||
|
const double goodC = 0.833; |
||||
|
// Total number of protocol runs to analyze |
||||
|
const int TotalRuns = 5; |
||||
|
// size of the crowd |
||||
|
const int CrowdSize = 5; |
||||
|
|
||||
|
module crowds |
||||
|
// protocol phase |
||||
|
phase: [0..4] init 0; |
||||
|
|
||||
|
// crowd member good (or bad) |
||||
|
good: bool init false; |
||||
|
|
||||
|
// number of protocol runs |
||||
|
runCount: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// observe_i is the number of times the attacker observed crowd member i |
||||
|
observe0: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe1: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe2: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe3: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe4: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// the last seen crowd member |
||||
|
lastSeen: [0..CrowdSize - 1] init 0; |
||||
|
|
||||
|
// get the protocol started |
||||
|
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); |
||||
|
|
||||
|
// decide whether crowd member is good or bad according to given probabilities |
||||
|
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); |
||||
|
|
||||
|
// if the current member is a good member, update the last seen index (chosen uniformly) |
||||
|
[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); |
||||
|
|
||||
|
// if the current member is a bad member, record the most recently seen index |
||||
|
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
||||
|
|
||||
|
// good crowd members forward with probability PF and deliver otherwise |
||||
|
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); |
||||
|
|
||||
|
// deliver the message and start over |
||||
|
[] phase=4 -> 1: (phase'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "observe0Greater1" = observe0>1; |
||||
|
label "observe1Greater1" = observe1>1; |
||||
|
label "observe2Greater1" = observe2>1; |
||||
|
label "observe3Greater1" = observe3>1; |
||||
|
label "observe4Greater1" = observe4>1; |
||||
|
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; |
||||
|
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; |
@ -0,0 +1,69 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
// probability of forwarding |
||||
|
const double PF = 4/5; |
||||
|
const double notPF = 1/5; // must be 1-PF |
||||
|
// probability that a crowd member is bad |
||||
|
const double badC = 167/1000; |
||||
|
// probability that a crowd member is good |
||||
|
const double goodC = 833/1000; |
||||
|
// Total number of protocol runs to analyze |
||||
|
const int TotalRuns = 5; |
||||
|
// size of the crowd |
||||
|
const int CrowdSize = 5; |
||||
|
|
||||
|
module crowds |
||||
|
// protocol phase |
||||
|
phase: [0..4] init 0; |
||||
|
|
||||
|
// crowd member good (or bad) |
||||
|
good: bool init false; |
||||
|
|
||||
|
// number of protocol runs |
||||
|
runCount: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// observe_i is the number of times the attacker observed crowd member i |
||||
|
observe0: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe1: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe2: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe3: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe4: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// the last seen crowd member |
||||
|
lastSeen: [0..CrowdSize - 1] init 0; |
||||
|
|
||||
|
// get the protocol started |
||||
|
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); |
||||
|
|
||||
|
// decide whether crowd member is good or bad according to given probabilities |
||||
|
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); |
||||
|
|
||||
|
// if the current member is a good member, update the last seen index (chosen uniformly) |
||||
|
[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); |
||||
|
|
||||
|
// if the current member is a bad member, record the most recently seen index |
||||
|
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
||||
|
|
||||
|
// good crowd members forward with probability PF and deliver otherwise |
||||
|
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); |
||||
|
|
||||
|
// deliver the message and start over |
||||
|
[] phase=4 -> 1: (phase'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "observe0Greater1" = observe0>1; |
||||
|
label "observe1Greater1" = observe1>1; |
||||
|
label "observe2Greater1" = observe2>1; |
||||
|
label "observe3Greater1" = observe3>1; |
||||
|
label "observe4Greater1" = observe4>1; |
||||
|
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; |
||||
|
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; |
@ -0,0 +1,10 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock one two three four five six done |
||||
|
#END |
||||
|
0 init |
||||
|
7 one done |
||||
|
8 two done |
||||
|
9 three done |
||||
|
10 four done |
||||
|
11 five done |
||||
|
12 six done |
@ -0,0 +1,32 @@ |
|||||
|
// Knuth's model of a fair die using only fair coins |
||||
|
dtmc |
||||
|
|
||||
|
module die |
||||
|
|
||||
|
// local state |
||||
|
s : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d : [0..6] init 0; |
||||
|
|
||||
|
[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
||||
|
[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); |
||||
|
[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); |
||||
|
[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); |
||||
|
[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); |
||||
|
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); |
||||
|
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); |
||||
|
[] s=7 -> 1: (s'=7); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards "coin_flips" |
||||
|
[] s<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "one" = s=7&d=1; |
||||
|
label "two" = s=7&d=2; |
||||
|
label "three" = s=7&d=3; |
||||
|
label "four" = s=7&d=4; |
||||
|
label "five" = s=7&d=5; |
||||
|
label "six" = s=7&d=6; |
||||
|
label "done" = s=7; |
@ -0,0 +1,21 @@ |
|||||
|
dtmc |
||||
|
0 1 0.5 |
||||
|
0 2 0.5 |
||||
|
1 3 0.5 |
||||
|
1 4 0.5 |
||||
|
2 5 0.5 |
||||
|
2 6 0.5 |
||||
|
3 1 0.5 |
||||
|
3 7 0.5 |
||||
|
4 8 0.5 |
||||
|
4 9 0.5 |
||||
|
5 10 0.5 |
||||
|
5 11 0.5 |
||||
|
6 2 0.5 |
||||
|
6 12 0.5 |
||||
|
7 7 1 |
||||
|
8 8 1 |
||||
|
9 9 1 |
||||
|
10 10 1 |
||||
|
11 11 1 |
||||
|
12 12 1 |
@ -0,0 +1,85 @@ |
|||||
|
// synchronous leader election protocol (itai & Rodeh) |
||||
|
// dxp/gxn 25/01/01 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// CONSTANTS |
||||
|
const int N = 3; // number of processes |
||||
|
const int K = 5; // range of probabilistic choice |
||||
|
|
||||
|
// counter module used to count the number of processes that have been read |
||||
|
// and to know when a process has decided |
||||
|
module counter |
||||
|
|
||||
|
// counter (c=i means process j reading process (i-1)+j next) |
||||
|
c : [1..N-1]; |
||||
|
|
||||
|
// reading |
||||
|
[read] c<N-1 -> 1:(c'=c+1); |
||||
|
// finished reading |
||||
|
[read] c=N-1 -> 1:(c'=c); |
||||
|
//decide |
||||
|
[done] u1|u2|u3 -> 1:(c'=c); |
||||
|
// pick again reset counter |
||||
|
[retry] !(u1|u2|u3) -> 1:(c'=1); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(c'=c); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// processes form a ring and suppose: |
||||
|
// process 1 reads process 2 |
||||
|
// process 2 reads process 3 |
||||
|
// process 3 reads process 1 |
||||
|
module process1 |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..3]; |
||||
|
// s1=0 make random choice |
||||
|
// s1=1 reading |
||||
|
// s1=2 deciding |
||||
|
// s1=3 finished |
||||
|
|
||||
|
// has a unique id so far (initially true) |
||||
|
u1 : bool; |
||||
|
|
||||
|
// value to be sent to next process in the ring (initially sets this to its own value) |
||||
|
v1 : [0..K-1]; |
||||
|
|
||||
|
// random choice |
||||
|
p1 : [0..K-1]; |
||||
|
|
||||
|
// pick value |
||||
|
[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); |
||||
|
// read |
||||
|
[read] s1=1 & u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2); |
||||
|
[read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0); |
||||
|
// read and move to decide |
||||
|
[read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
||||
|
[read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); |
||||
|
// deciding |
||||
|
// done |
||||
|
[done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
//retry |
||||
|
[retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(s1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule |
||||
|
module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule |
||||
|
|
||||
|
// expected number of rounds |
||||
|
rewards "num_rounds" |
||||
|
[pick] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
// labels |
||||
|
label "elected" = s1=3&s2=3&s3=3; |
||||
|
|
@ -0,0 +1,85 @@ |
|||||
|
// synchronous leader election protocol (itai & Rodeh) |
||||
|
// dxp/gxn 25/01/01 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// CONSTANTS |
||||
|
const int N = 3; // number of processes |
||||
|
const int K = 5; // range of probabilistic choice |
||||
|
|
||||
|
// counter module used to count the number of processes that have been read |
||||
|
// and to know when a process has decided |
||||
|
module counter |
||||
|
|
||||
|
// counter (c=i means process j reading process (i-1)+j next) |
||||
|
c : [1..N-1]; |
||||
|
|
||||
|
// reading |
||||
|
[read] c<N-1 -> 1:(c'=c+1); |
||||
|
// finished reading |
||||
|
[read] c=N-1 -> 1:(c'=c); |
||||
|
//decide |
||||
|
[done] u1|u2|u3 -> 1:(c'=c); |
||||
|
// pick again reset counter |
||||
|
[retry] !(u1|u2|u3) -> 1:(c'=1); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(c'=c); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// processes form a ring and suppose: |
||||
|
// process 1 reads process 2 |
||||
|
// process 2 reads process 3 |
||||
|
// process 3 reads process 1 |
||||
|
module process1 |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..3]; |
||||
|
// s1=0 make random choice |
||||
|
// s1=1 reading |
||||
|
// s1=2 deciding |
||||
|
// s1=3 finished |
||||
|
|
||||
|
// has a unique id so far (initially true) |
||||
|
u1 : bool; |
||||
|
|
||||
|
// value to be sent to next process in the ring (initially sets this to its own value) |
||||
|
v1 : [0..K-1]; |
||||
|
|
||||
|
// random choice |
||||
|
p1 : [0..K-1]; |
||||
|
|
||||
|
// pick value |
||||
|
[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); |
||||
|
// read |
||||
|
[read] s1=1 & u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2); |
||||
|
[read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0); |
||||
|
// read and move to decide |
||||
|
[read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
||||
|
[read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); |
||||
|
// deciding |
||||
|
// done |
||||
|
[done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
//retry |
||||
|
[retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(s1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule |
||||
|
module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule |
||||
|
|
||||
|
// expected number of rounds |
||||
|
rewards "num_rounds" |
||||
|
[pick] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
// labels |
||||
|
label "elected" = s1=3&s2=3&s3=3; |
||||
|
|
@ -0,0 +1,76 @@ |
|||||
|
// nand multiplex system |
||||
|
// gxn/dxp 20/03/03 |
||||
|
|
||||
|
// U (correctly) performs a random permutation of the outputs of the previous stage |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
const int N = 5; // number of inputs in each bundle |
||||
|
const int K = 2; // number of restorative stages |
||||
|
|
||||
|
const int M = 2*K+1; // total number of multiplexing units |
||||
|
|
||||
|
// parameters taken from the following paper |
||||
|
// A system architecture solution for unreliable nanoelectric devices |
||||
|
// J. Han & P. Jonker |
||||
|
// IEEEE trans. on nanotechnology vol 1(4) 2002 |
||||
|
|
||||
|
const double perr = 0.02; // probability nand works correctly |
||||
|
const double prob1 = 0.9; // probability initial inputs are stimulated |
||||
|
|
||||
|
// model whole system as a single module by resuing variables |
||||
|
// to decrease the state space |
||||
|
module multiplex |
||||
|
|
||||
|
u : [1..M]; // number of stages |
||||
|
c : [0..N]; // counter (number of copies of the nand done) |
||||
|
|
||||
|
s : [0..4]; // local state |
||||
|
// 0 - initial state |
||||
|
// 1 - set x inputs |
||||
|
// 2 - set y inputs |
||||
|
// 3 - set outputs |
||||
|
// 4 - done |
||||
|
|
||||
|
z : [0..N]; // number of new outputs equal to 1 |
||||
|
zx : [0..N]; // number of old outputs equal to 1 |
||||
|
zy : [0..N]; // need second copy for y |
||||
|
// initially 9 since initially probability of stimulated state is 0.9 |
||||
|
|
||||
|
x : [0..1]; // value of first input |
||||
|
y : [0..1]; // value of second input |
||||
|
|
||||
|
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet |
||||
|
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished |
||||
|
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space) |
||||
|
|
||||
|
// choose x permute selection (have zx stimulated inputs) |
||||
|
// note only need y to be random |
||||
|
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random |
||||
|
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1); |
||||
|
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2); |
||||
|
|
||||
|
// choose x randomly from selection (have zy stimulated inputs) |
||||
|
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random |
||||
|
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3); |
||||
|
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1); |
||||
|
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3); |
||||
|
|
||||
|
// use nand gate |
||||
|
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty |
||||
|
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault |
||||
|
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty |
||||
|
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault |
||||
|
|
||||
|
[] s=4 -> (s'=s); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// rewards: final value of gate |
||||
|
rewards |
||||
|
// [] s=0 & (c=N) & (u=M) : z/N; |
||||
|
s=0 & (c=N) & (u=M) : z/N; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=4 & z/N<0.1; |
||||
|
label "end" = s=4; |
@ -0,0 +1,18 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
module test |
||||
|
s : [0 .. 3] init 0; |
||||
|
|
||||
|
[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
||||
|
[] s=1 -> 1 : true; |
||||
|
[] s=2 -> 1 : (s'=3); |
||||
|
[] s=3 -> 1 : true; |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
s=2 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "condition" = s=2; |
||||
|
label "target" = s=3; |
@ -0,0 +1,15 @@ |
|||||
|
#DECLARATION |
||||
|
init one two three four |
||||
|
#END |
||||
|
0 init one two three four |
||||
|
1 one |
||||
|
2 two |
||||
|
3 three |
||||
|
4 four |
||||
|
5 one |
||||
|
6 one |
||||
|
7 two |
||||
|
8 two |
||||
|
9 three four |
||||
|
10 three |
||||
|
11 four |
5889
resources/examples/testfiles/lab/crowds5_5.lab
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,7 @@ |
|||||
|
#DECLAATION |
||||
|
phi |
||||
|
#END |
||||
|
1 phi |
||||
|
2 phi |
||||
|
3 phi |
||||
|
|
@ -0,0 +1,10 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock one two three four five six done |
||||
|
#END |
||||
|
0 init |
||||
|
7 one done |
||||
|
8 two done |
||||
|
9 three done |
||||
|
10 four done |
||||
|
11 five done |
||||
|
12 six done |
@ -0,0 +1,14 @@ |
|||||
|
#DECLARATION |
||||
|
one two three |
||||
|
#END |
||||
|
1 one |
||||
|
1 two |
||||
|
2 two |
||||
|
3 one |
||||
|
4 three |
||||
|
2 two |
||||
|
5 two three |
||||
|
2 three |
||||
|
5 two |
||||
|
4 one |
||||
|
1 three |
@ -0,0 +1,9 @@ |
|||||
|
#DECLARATION |
||||
|
one two three |
||||
|
#END |
||||
|
1 one |
||||
|
0 two |
||||
|
2 two |
||||
|
3 one |
||||
|
4 three |
||||
|
5 two three |
@ -0,0 +1,11 @@ |
|||||
|
#DECLARATION |
||||
|
init a b c d |
||||
|
#END |
||||
|
0 init c |
||||
|
1 c |
||||
|
2 c d |
||||
|
3 c |
||||
|
4 c |
||||
|
5 a |
||||
|
6 b |
||||
|
7 b |
@ -0,0 +1,11 @@ |
|||||
|
#DECLARATION |
||||
|
init one two three four |
||||
|
#END |
||||
|
0 init one two three four |
||||
|
1 one |
||||
|
2 two |
||||
|
3 three |
||||
|
4 four |
||||
|
5 one |
||||
|
6 one two |
||||
|
7 init one four |
@ -0,0 +1,11 @@ |
|||||
|
#DECLARATION |
||||
|
init one two three four |
||||
|
#END |
||||
|
0 init one two three four |
||||
|
1 one |
||||
|
2 two |
||||
|
3 three |
||||
|
4 four |
||||
|
5 one |
||||
|
6 one two |
||||
|
7 init one four |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
phi |
||||
|
#EDN |
||||
|
1 phi |
||||
|
2 phi |
||||
|
3 phi |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
one two |
||||
|
#END |
||||
|
1 one |
||||
|
2 two |
||||
|
354 one |
@ -0,0 +1,8 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock elected |
||||
|
#END |
||||
|
0 init |
||||
|
2595 elected |
||||
|
2596 elected |
||||
|
2599 elected |
||||
|
2969 elected |
@ -0,0 +1,5 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock elected |
||||
|
#END |
||||
|
0 init |
||||
|
12399 elected |
@ -0,0 +1,7 @@ |
|||||
|
#DECLARATION |
||||
|
init r1 r2 err |
||||
|
#END |
||||
|
0 init |
||||
|
2 err |
||||
|
6 r1 |
||||
|
7 r2 |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
init goal err |
||||
|
#END |
||||
|
0 init |
||||
|
3 err |
||||
|
5 goal |
@ -0,0 +1,7 @@ |
|||||
|
#DECLARATION |
||||
|
init goal err |
||||
|
#END |
||||
|
0 init |
||||
|
3 err |
||||
|
5 goal |
||||
|
9 err |
@ -0,0 +1,8 @@ |
|||||
|
#DECLARATION |
||||
|
init one two three |
||||
|
#END |
||||
|
0 init one three |
||||
|
2 two three |
||||
|
3 one |
||||
|
4 init |
||||
|
5 two |
@ -0,0 +1,7 @@ |
|||||
|
#DECLARATION |
||||
|
init one two three |
||||
|
#END |
||||
|
0 init one three |
||||
|
2 two three |
||||
|
3 one |
||||
|
4 init |
@ -0,0 +1,6 @@ |
|||||
|
phi |
||||
|
#END |
||||
|
1 phi |
||||
|
2 phi |
||||
|
3 phi |
||||
|
|
@ -0,0 +1,5 @@ |
|||||
|
#DECLARATION |
||||
|
phi |
||||
|
1 phi |
||||
|
2 phi |
||||
|
3 phi |
@ -0,0 +1,2 @@ |
|||||
|
#DECLARATION |
||||
|
#END |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
phi psi smth |
||||
|
#END |
||||
|
0 phi |
||||
|
1 phi |
||||
|
2 smth phi |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
phi |
||||
|
#END |
||||
|
1 phi |
||||
|
phi 2 |
||||
|
3 phi |
@ -0,0 +1,7 @@ |
|||||
|
#DECLARATION |
||||
|
init goal |
||||
|
#END |
||||
|
0 init |
||||
|
7 goal |
||||
|
8 goal |
||||
|
|
@ -0,0 +1,7 @@ |
|||||
|
#DECLARATION |
||||
|
init goal |
||||
|
#END |
||||
|
0 init |
||||
|
7 goal |
||||
|
8 goal |
||||
|
|
@ -0,0 +1,40 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock done two three four five six seven eight nine ten eleven twelve |
||||
|
#END |
||||
|
0 init |
||||
|
98 done two |
||||
|
99 done three |
||||
|
100 done four |
||||
|
101 done five |
||||
|
102 done six |
||||
|
103 done seven |
||||
|
111 done three |
||||
|
112 done four |
||||
|
113 done five |
||||
|
114 done six |
||||
|
115 done seven |
||||
|
116 done eight |
||||
|
124 done four |
||||
|
125 done five |
||||
|
126 done six |
||||
|
127 done seven |
||||
|
128 done eight |
||||
|
129 done nine |
||||
|
137 done five |
||||
|
138 done six |
||||
|
139 done seven |
||||
|
140 done eight |
||||
|
141 done nine |
||||
|
142 done ten |
||||
|
150 done six |
||||
|
151 done seven |
||||
|
152 done eight |
||||
|
153 done nine |
||||
|
154 done ten |
||||
|
155 done eleven |
||||
|
163 done seven |
||||
|
164 done eight |
||||
|
165 done nine |
||||
|
166 done ten |
||||
|
167 done eleven |
||||
|
168 done twelve |
@ -0,0 +1,6 @@ |
|||||
|
#DECLARATION |
||||
|
psi |
||||
|
#END |
||||
|
1 phi |
||||
|
2 phi |
||||
|
3 phi |
@ -0,0 +1,11 @@ |
|||||
|
#DECLARATION |
||||
|
one 9 & two " three |
||||
|
#END |
||||
|
1 one three |
||||
|
2 two " |
||||
|
3 three two |
||||
|
4 one one |
||||
|
5 two three one two three three two one |
||||
|
7 one 9 two |
||||
|
11 two & |
||||
|
12 one |
@ -0,0 +1,11 @@ |
|||||
|
#DECLARATION |
||||
|
one 9 & two " three |
||||
|
#END |
||||
|
1 one three |
||||
|
2 two " |
||||
|
3 three two |
||||
|
4 one |
||||
|
5 two three one |
||||
|
7 one 9 two |
||||
|
11 two & |
||||
|
12 one |
@ -0,0 +1,19 @@ |
|||||
|
|
||||
|
ma |
||||
|
|
||||
|
module hybrid_states |
||||
|
|
||||
|
s : [0..4]; |
||||
|
|
||||
|
[] (s=0) -> 0.8 : (s'=0) + 0.2 : (s'=2); |
||||
|
[] (s=0) -> 1 : (s' = 1); |
||||
|
<> (s=0) -> 3 : (s' = 1); |
||||
|
<> (s=1) -> 9 : (s'=0) + 1 : (s'=3); |
||||
|
<> (s=2) -> 12 : (s'=4); |
||||
|
[] (s=3) -> 1 : true; |
||||
|
[] (s=3) -> 1 : (s'=4); |
||||
|
<> (s=3) -> 2 : (s'=3) + 2 : (s'=4); |
||||
|
[] (s=4) -> 1 : true; |
||||
|
<> (s=4) -> 3 : (s'=3); |
||||
|
|
||||
|
endmodule |
@ -0,0 +1,15 @@ |
|||||
|
|
||||
|
ma |
||||
|
|
||||
|
module simple |
||||
|
|
||||
|
s : [0..4]; |
||||
|
|
||||
|
|
||||
|
[alpha] (s=0) -> 1 : (s' = 1); |
||||
|
[beta] (s=0) -> 0.8 : (s'=0) + 0.2 : (s'=2); |
||||
|
<> (s=1) -> 9 : (s'=0) + 1 : (s'=3); |
||||
|
<> (s=2) -> 12 : (s'=4); |
||||
|
<> (s>2) -> 1 : true; |
||||
|
|
||||
|
endmodule |
@ -0,0 +1,50 @@ |
|||||
|
|
||||
|
ma |
||||
|
|
||||
|
const int N = 2; // num packages |
||||
|
|
||||
|
const double inRate = 4; |
||||
|
const double processingRate = 5; |
||||
|
|
||||
|
module streamingclient |
||||
|
|
||||
|
s : [0..3]; // current state: |
||||
|
// 0: decide whether to start |
||||
|
// 1: buffering |
||||
|
// 2: running |
||||
|
// 3: done |
||||
|
|
||||
|
n : [0..N]; // number of received packages |
||||
|
k : [0..N]; // number of processed packages |
||||
|
|
||||
|
[buffer] s=0 & n<N -> 1 : (s'=1); |
||||
|
[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1); |
||||
|
|
||||
|
<> s=1 -> inRate : (n'=n+1) & (s'=0); |
||||
|
|
||||
|
<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1); |
||||
|
<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); |
||||
|
<> s=2 & n=N & k<n -> processingRate : (k'=k+1); |
||||
|
<> s=2 & n=N & k=N -> processingRate : (s'=3); |
||||
|
|
||||
|
<> s=3 -> 1 : true; |
||||
|
endmodule |
||||
|
|
||||
|
// All packages received and buffer empty |
||||
|
label "done" = (s=3); |
||||
|
|
||||
|
rewards "buffering" |
||||
|
s=1 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
rewards "initialbuffering" |
||||
|
s=1 & k = 0: 1; |
||||
|
endrewards |
||||
|
|
||||
|
rewards "intermediatebuffering" |
||||
|
s=1 & k > 0: 1; |
||||
|
endrewards |
||||
|
|
||||
|
rewards "numRestarts" |
||||
|
[start] k > 0 : 1; |
||||
|
endrewards |
@ -0,0 +1,26 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module one |
||||
|
s1 : [0 .. 3]; |
||||
|
|
||||
|
[a] s1=0 -> (s1'=1); |
||||
|
|
||||
|
[c] s1=1 -> (s1'=2); |
||||
|
|
||||
|
[d] s1=1 -> (s1'=3); |
||||
|
endmodule |
||||
|
|
||||
|
module two |
||||
|
s2 : [0 .. 2]; |
||||
|
|
||||
|
[b] s2=0 -> (s2'=1); |
||||
|
|
||||
|
[c] s2=1 -> (s2'=2); |
||||
|
endmodule |
||||
|
|
||||
|
module three |
||||
|
s3 : [0 .. 2]; |
||||
|
|
||||
|
[c] s3=0 -> (s3'=1); |
||||
|
endmodule |
||||
|
|
@ -0,0 +1,28 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module one |
||||
|
s1 : [0 .. 3]; |
||||
|
|
||||
|
[a] s1=0 -> (s1'=1); |
||||
|
|
||||
|
[c] s1=1 -> (s1'=2); |
||||
|
|
||||
|
[d] s1=1 -> (s1'=3); |
||||
|
endmodule |
||||
|
|
||||
|
module two |
||||
|
s2 : [0 .. 2]; |
||||
|
|
||||
|
[b] s2=0 -> (s2'=1); |
||||
|
|
||||
|
[c] s2=1 -> (s2'=2); |
||||
|
endmodule |
||||
|
|
||||
|
module three |
||||
|
s3 : [0 .. 2]; |
||||
|
|
||||
|
[c] s3=0 -> (s3'=1); |
||||
|
|
||||
|
[a] s3=2 -> (s3'=2); |
||||
|
endmodule |
||||
|
|
@ -0,0 +1,60 @@ |
|||||
|
// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] |
||||
|
// gxn/dxp 20/11/00 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// constants |
||||
|
const int N=2; |
||||
|
const int K=2; |
||||
|
const int range = 2*(K+1)*N; |
||||
|
const int counter_init = (K+1)*N; |
||||
|
const int left = N; |
||||
|
const int right = 2*(K+1)*N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
global counter : [0..range] init counter_init; |
||||
|
|
||||
|
module process1 |
||||
|
|
||||
|
// program counter |
||||
|
pc1 : [0..3]; |
||||
|
// 0 - flip |
||||
|
// 1 - write |
||||
|
// 2 - check |
||||
|
// 3 - finished |
||||
|
|
||||
|
// local coin |
||||
|
coin1 : [0..1]; |
||||
|
|
||||
|
// flip coin |
||||
|
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); |
||||
|
// write tails -1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); |
||||
|
// write heads +1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); |
||||
|
// check |
||||
|
// decide tails |
||||
|
[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); |
||||
|
// decide heads |
||||
|
[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); |
||||
|
// flip again |
||||
|
[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); |
||||
|
// loop (all loop together when done) |
||||
|
[done] (pc1=3) -> 1 : (pc1'=3)&(counter'=counter); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1[pc1=pc2,coin1=coin2] endmodule |
||||
|
|
||||
|
// labels |
||||
|
label "finished" = pc1=3 & pc2=3 ; |
||||
|
label "all_coins_equal_0" = coin1=0 & coin2=0 ; |
||||
|
label "all_coins_equal_1" = coin1=1 & coin2=1 ; |
||||
|
label "agree" = coin1=coin2 ; |
||||
|
|
||||
|
// rewards |
||||
|
rewards "steps" |
||||
|
true : 1; |
||||
|
endrewards |
||||
|
|
@ -0,0 +1,60 @@ |
|||||
|
// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] |
||||
|
// gxn/dxp 20/11/00 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// constants |
||||
|
const int N=2; |
||||
|
const int K=2; |
||||
|
const int range = 2*(K+1)*N; |
||||
|
const int counter_init = (K+1)*N; |
||||
|
const int left = N; |
||||
|
const int right = 2*(K+1)*N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
global counter : [0..range] init counter_init; |
||||
|
|
||||
|
module process1 |
||||
|
|
||||
|
// program counter |
||||
|
pc1 : [0..3]; |
||||
|
// 0 - flip |
||||
|
// 1 - write |
||||
|
// 2 - check |
||||
|
// 3 - finished |
||||
|
|
||||
|
// local coin |
||||
|
coin1 : [0..1]; |
||||
|
|
||||
|
// flip coin |
||||
|
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); |
||||
|
// write tails -1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); |
||||
|
// write heads +1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); |
||||
|
// check |
||||
|
// decide tails |
||||
|
[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); |
||||
|
// decide heads |
||||
|
[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); |
||||
|
// flip again |
||||
|
[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); |
||||
|
// loop (all loop together when done) |
||||
|
[done] (pc1=3) -> 1 : (pc1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1[pc1=pc2,coin1=coin2] endmodule |
||||
|
|
||||
|
// labels |
||||
|
label "finished" = pc1=3 & pc2=3 ; |
||||
|
label "all_coins_equal_0" = coin1=0 & coin2=0 ; |
||||
|
label "all_coins_equal_1" = coin1=1 & coin2=1 ; |
||||
|
label "agree" = coin1=coin2 ; |
||||
|
|
||||
|
// rewards |
||||
|
rewards "steps" |
||||
|
true : 1; |
||||
|
endrewards |
||||
|
|
@ -0,0 +1,60 @@ |
|||||
|
// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] |
||||
|
// gxn/dxp 20/11/00 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// constants |
||||
|
const int N=2; |
||||
|
const int K; |
||||
|
const int range = 2*(K+1)*N; |
||||
|
const int counter_init = (K+1)*N; |
||||
|
const int left = N; |
||||
|
const int right = 2*(K+1)*N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
global counter : [0..range] init counter_init; |
||||
|
|
||||
|
module process1 |
||||
|
|
||||
|
// program counter |
||||
|
pc1 : [0..3]; |
||||
|
// 0 - flip |
||||
|
// 1 - write |
||||
|
// 2 - check |
||||
|
// 3 - finished |
||||
|
|
||||
|
// local coin |
||||
|
coin1 : [0..1]; |
||||
|
|
||||
|
// flip coin |
||||
|
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); |
||||
|
// write tails -1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); |
||||
|
// write heads +1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); |
||||
|
// check |
||||
|
// decide tails |
||||
|
[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); |
||||
|
// decide heads |
||||
|
[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); |
||||
|
// flip again |
||||
|
[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); |
||||
|
// loop (all loop together when done) |
||||
|
[done] (pc1=3) -> 1 : (pc1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1[pc1=pc2,coin1=coin2] endmodule |
||||
|
|
||||
|
// labels |
||||
|
label "finished" = pc1=3 & pc2=3 ; |
||||
|
label "all_coins_equal_0" = coin1=0 & coin2=0 ; |
||||
|
label "all_coins_equal_1" = coin1=1 & coin2=1 ; |
||||
|
label "agree" = coin1=coin2 ; |
||||
|
|
||||
|
// rewards |
||||
|
rewards "steps" |
||||
|
true : 1; |
||||
|
endrewards |
||||
|
|
@ -0,0 +1,130 @@ |
|||||
|
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
||||
|
// gxn/dxp 04/12/01 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// note made changes since cannot have strict inequalities |
||||
|
// in digital clocks approach and suppose a station only sends one message |
||||
|
|
||||
|
// simplified parameters scaled |
||||
|
const int sigma=1; // time for messages to propagate along the bus |
||||
|
const int lambda=30; // time to send a message |
||||
|
|
||||
|
// actual parameters |
||||
|
const int N = 2; // number of processes |
||||
|
const int K = 2; // exponential backoff limit |
||||
|
const int slot = 2*sigma; // length of slot |
||||
|
// const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
||||
|
const int M = 3 ; // max number of slots to wait |
||||
|
//const int lambda=782; |
||||
|
//const int sigma=26; |
||||
|
|
||||
|
// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); |
||||
|
// formula min_collisions = min(cd1,cd2); |
||||
|
// formula max_collisions = max(cd1,cd2); |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
// the bus |
||||
|
module bus |
||||
|
|
||||
|
b : [0..2]; |
||||
|
// b=0 - idle |
||||
|
// b=1 - active |
||||
|
// b=2 - collision |
||||
|
|
||||
|
// clocks of bus |
||||
|
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
||||
|
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
||||
|
|
||||
|
// a sender sends (ok - no other message being sent) |
||||
|
[send1] (b=0) -> (b'=1); |
||||
|
[send2] (b=0) -> (b'=1); |
||||
|
|
||||
|
// a sender sends (bus busy - collision) |
||||
|
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
||||
|
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
||||
|
|
||||
|
// finish sending |
||||
|
[end1] (b=1) -> (b'=0) & (y1'=0); |
||||
|
[end2] (b=1) -> (b'=0) & (y1'=0); |
||||
|
|
||||
|
// bus busy |
||||
|
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
||||
|
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
||||
|
|
||||
|
// collision detected |
||||
|
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
||||
|
|
||||
|
// time passage |
||||
|
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
||||
|
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
||||
|
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
// model of first sender |
||||
|
module station1 |
||||
|
|
||||
|
// LOCAL STATE |
||||
|
s1 : [0..5]; |
||||
|
// s1=0 - initial state |
||||
|
// s1=1 - transmit |
||||
|
// s1=2 - collision (set backoff) |
||||
|
// s1=3 - wait (bus busy) |
||||
|
// s1=4 - successfully sent |
||||
|
|
||||
|
// LOCAL CLOCK |
||||
|
x1 : [0..max(lambda,slot)]; |
||||
|
|
||||
|
// BACKOFF COUNTER (number of slots to wait) |
||||
|
bc1 : [0..M]; |
||||
|
|
||||
|
// COLLISION COUNTER |
||||
|
cd1 : [0..K]; |
||||
|
|
||||
|
// start sending |
||||
|
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
||||
|
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
||||
|
|
||||
|
// transmitting |
||||
|
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
||||
|
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
||||
|
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
||||
|
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
||||
|
|
||||
|
// set backoff (no time can pass in this state) |
||||
|
// probability depends on which transmission this is (cd1) |
||||
|
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
||||
|
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
||||
|
|
||||
|
// wait until backoff counter reaches 0 then send again |
||||
|
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
||||
|
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
||||
|
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
||||
|
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
||||
|
|
||||
|
// once finished nothing matters |
||||
|
[time] (s1>=4) -> (x1'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// construct further stations through renaming |
||||
|
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// reward structure for expected time |
||||
|
rewards "time" |
||||
|
[time] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// labels/formulae |
||||
|
label "all_delivered" = s1=4&s2=4; |
||||
|
label "one_delivered" = s1=4|s2=4; |
||||
|
label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); |
||||
|
|
@ -0,0 +1,130 @@ |
|||||
|
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
||||
|
// gxn/dxp 04/12/01 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// note made changes since cannot have strict inequalities |
||||
|
// in digital clocks approach and suppose a station only sends one message |
||||
|
|
||||
|
// simplified parameters scaled |
||||
|
const int sigma=1; // time for messages to propagate along the bus |
||||
|
const int lambda=30; // time to send a message |
||||
|
|
||||
|
// actual parameters |
||||
|
const int N = 2; // number of processes |
||||
|
const int K = 2; // exponential backoff limit |
||||
|
const int slot = 2*sigma; // length of slot |
||||
|
// const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
||||
|
const int M = 3 ; // max number of slots to wait |
||||
|
//const int lambda=782; |
||||
|
//const int sigma=26; |
||||
|
|
||||
|
// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); |
||||
|
// formula min_collisions = min(cd1,cd2); |
||||
|
// formula max_collisions = max(cd1,cd2); |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
// the bus |
||||
|
module bus |
||||
|
|
||||
|
b : [0..2]; |
||||
|
// b=0 - idle |
||||
|
// b=1 - active |
||||
|
// b=2 - collision |
||||
|
|
||||
|
// clocks of bus |
||||
|
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
||||
|
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
||||
|
|
||||
|
// a sender sends (ok - no other message being sent) |
||||
|
[send1] (b=0) -> (b'=1); |
||||
|
[send2] (b=0) -> (b'=1); |
||||
|
|
||||
|
// a sender sends (bus busy - collision) |
||||
|
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
||||
|
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
||||
|
|
||||
|
// finish sending |
||||
|
[end1] (b=1) -> (b'=0) & (y1'=0); |
||||
|
[end2] (b=1) -> (b'=0) & (y1'=0); |
||||
|
|
||||
|
// bus busy |
||||
|
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
||||
|
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
||||
|
|
||||
|
// collision detected |
||||
|
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
||||
|
|
||||
|
// time passage |
||||
|
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
||||
|
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
||||
|
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
// model of first sender |
||||
|
module station1 |
||||
|
|
||||
|
// LOCAL STATE |
||||
|
s1 : [0..5]; |
||||
|
// s1=0 - initial state |
||||
|
// s1=1 - transmit |
||||
|
// s1=2 - collision (set backoff) |
||||
|
// s1=3 - wait (bus busy) |
||||
|
// s1=4 - successfully sent |
||||
|
|
||||
|
// LOCAL CLOCK |
||||
|
x1 : [0..max(lambda,slot)]; |
||||
|
|
||||
|
// BACKOFF COUNTER (number of slots to wait) |
||||
|
bc1 : [0..M]; |
||||
|
|
||||
|
// COLLISION COUNTER |
||||
|
cd1 : [0..K]; |
||||
|
|
||||
|
// start sending |
||||
|
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
||||
|
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
||||
|
|
||||
|
// transmitting |
||||
|
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
||||
|
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
||||
|
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
||||
|
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
||||
|
|
||||
|
// set backoff (no time can pass in this state) |
||||
|
// probability depends on which transmission this is (cd1) |
||||
|
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
||||
|
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
||||
|
|
||||
|
// wait until backoff counter reaches 0 then send again |
||||
|
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
||||
|
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
||||
|
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
||||
|
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
||||
|
|
||||
|
// once finished nothing matters |
||||
|
[time] (s1>=4) -> (x1'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// construct further stations through renaming |
||||
|
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// reward structure for expected time |
||||
|
rewards "time" |
||||
|
[time] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// labels/formulae |
||||
|
label "all_delivered" = s1=4&s2=4; |
||||
|
label "one_delivered" = s1=4|s2=4; |
||||
|
label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); |
||||
|
|
@ -0,0 +1,33 @@ |
|||||
|
// Knuth's model of a fair die using only fair coins |
||||
|
mdp |
||||
|
|
||||
|
module die |
||||
|
|
||||
|
// local state |
||||
|
s : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d : [0..6] init 0; |
||||
|
|
||||
|
[a] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
||||
|
[b] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=2); |
||||
|
[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); |
||||
|
[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); |
||||
|
[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); |
||||
|
[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); |
||||
|
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); |
||||
|
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); |
||||
|
[] s=7 -> 1: (s'=7); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards "coin_flips" |
||||
|
[] s<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "one" = s=7&d=1; |
||||
|
label "two" = s=7&d=2; |
||||
|
label "three" = s=7&d=3; |
||||
|
label "four" = s=7&d=4; |
||||
|
label "five" = s=7&d=5; |
||||
|
label "six" = s=7&d=6; |
||||
|
label "done" = s=7; |
@ -0,0 +1,45 @@ |
|||||
|
// Knuth's model of a fair die using only fair coins |
||||
|
mdp |
||||
|
|
||||
|
module die |
||||
|
|
||||
|
// local state |
||||
|
s : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d : [0..6] init 0; |
||||
|
|
||||
|
[fair] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
||||
|
[ufair1] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2); |
||||
|
[ufair2] s=0 -> 0.7 : (s'=1) + 0.3 : (s'=2); |
||||
|
[fair] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); |
||||
|
[ufair1] s=1 -> 0.6 : (s'=3) + 0.4 : (s'=4); |
||||
|
[ufair2] s=1 -> 0.7 : (s'=3) + 0.3 : (s'=4); |
||||
|
[fair] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); |
||||
|
[ufair1] s=2 -> 0.6 : (s'=5) + 0.4 : (s'=6); |
||||
|
[ufair2] s=2 -> 0.7 : (s'=5) + 0.3 : (s'=6); |
||||
|
[fair] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); |
||||
|
[ufair1] s=3 -> 0.6 : (s'=1) + 0.4 : (s'=7) & (d'=1); |
||||
|
[ufair2] s=3 -> 0.7 : (s'=1) + 0.3 : (s'=7) & (d'=1); |
||||
|
[fair] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); |
||||
|
[ufair1] s=4 -> 0.6 : (s'=7) & (d'=2) + 0.4 : (s'=7) & (d'=3); |
||||
|
[ufair2] s=4 -> 0.7 : (s'=7) & (d'=2) + 0.3 : (s'=7) & (d'=3); |
||||
|
[fair] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); |
||||
|
[ufair1] s=5 -> 0.6 : (s'=2) + 0.4 : (s'=7) & (d'=6); |
||||
|
[ufair2] s=5 -> 0.7 : (s'=2) + 0.3 : (s'=7) & (d'=6); |
||||
|
[] s=7 -> 1: (s'=7); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards "coin_flips" |
||||
|
[fair] s<7 : 1; |
||||
|
[ufair1] s<7 : 1; |
||||
|
[ufair2] s<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "one" = s=7&d=1; |
||||
|
label "two" = s=7&d=2; |
||||
|
label "three" = s=7&d=3; |
||||
|
label "four" = s=7&d=4; |
||||
|
label "five" = s=7&d=5; |
||||
|
label "six" = s=7&d=6; |
||||
|
label "done" = s=7; |
@ -0,0 +1,170 @@ |
|||||
|
// firewire protocol with integer semantics |
||||
|
// dxp/gxn 14/06/01 |
||||
|
|
||||
|
// CLOCKS |
||||
|
// x1 (x2) clock for node1 (node2) |
||||
|
// y1 and y2 (z1 and z2) clocks for wire12 (wire21) |
||||
|
mdp |
||||
|
|
||||
|
// maximum and minimum delays |
||||
|
// fast |
||||
|
const int rc_fast_max = 85; |
||||
|
const int rc_fast_min = 76; |
||||
|
// slow |
||||
|
const int rc_slow_max = 167; |
||||
|
const int rc_slow_min = 159; |
||||
|
// delay caused by the wire length |
||||
|
const int delay; |
||||
|
// probability of choosing fast |
||||
|
const double fast; |
||||
|
const double slow=1-fast; |
||||
|
|
||||
|
module wire12 |
||||
|
|
||||
|
// local state |
||||
|
w12 : [0..9]; |
||||
|
// 0 - empty |
||||
|
// 1 - rec_req |
||||
|
// 2 - rec_req_ack |
||||
|
// 3 - rec_ack |
||||
|
// 4 - rec_ack_idle |
||||
|
// 5 - rec_idle |
||||
|
// 6 - rec_idle_req |
||||
|
// 7 - rec_ack_req |
||||
|
// 8 - rec_req_idle |
||||
|
// 9 - rec_idle_ack |
||||
|
|
||||
|
// clock for wire12 |
||||
|
y1 : [0..delay+1]; |
||||
|
y2 : [0..delay+1]; |
||||
|
|
||||
|
// empty |
||||
|
// do not need y1 and y2 to increase as always reset when this state is left |
||||
|
// similarly can reset y1 and y2 when we re-enter this state |
||||
|
[snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); |
||||
|
[snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); |
||||
|
[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); |
||||
|
[time] w12=0 -> (w12'=w12); |
||||
|
// rec_req |
||||
|
[snd_req12] w12=1 -> (w12'=1); |
||||
|
[rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_ack12] w12=1 -> (w12'=2) & (y2'=0); |
||||
|
[snd_idle12] w12=1 -> (w12'=8) & (y2'=0); |
||||
|
[time] w12=1 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_req_ack |
||||
|
[snd_ack12] w12=2 -> (w12'=2); |
||||
|
[rec_req12] w12=2 -> (w12'=3); |
||||
|
[time] w12=2 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack |
||||
|
[snd_ack12] w12=3 -> (w12'=3); |
||||
|
[rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_idle12] w12=3 -> (w12'=4) & (y2'=0); |
||||
|
[snd_req12] w12=3 -> (w12'=7) & (y2'=0); |
||||
|
[time] w12=3 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack_idle |
||||
|
[snd_idle12] w12=4 -> (w12'=4); |
||||
|
[rec_ack12] w12=4 -> (w12'=5); |
||||
|
[time] w12=4 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle |
||||
|
[snd_idle12] w12=5 -> (w12'=5); |
||||
|
[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_req12] w12=5 -> (w12'=6) & (y2'=0); |
||||
|
[snd_ack12] w12=5 -> (w12'=9) & (y2'=0); |
||||
|
[time] w12=5 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle_req |
||||
|
[snd_req12] w12=6 -> (w12'=6); |
||||
|
[rec_idle12] w12=6 -> (w12'=1); |
||||
|
[time] w12=6 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack_req |
||||
|
[snd_req12] w12=7 -> (w12'=7); |
||||
|
[rec_ack12] w12=7 -> (w12'=1); |
||||
|
[time] w12=7 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_req_idle |
||||
|
[snd_idle12] w12=8 -> (w12'=8); |
||||
|
[rec_req12] w12=8 -> (w12'=5); |
||||
|
[time] w12=8 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle_ack |
||||
|
[snd_ack12] w12=9 -> (w12'=9); |
||||
|
[rec_idle12] w12=9 -> (w12'=3); |
||||
|
[time] w12=9 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module node1 |
||||
|
|
||||
|
// clock for node1 |
||||
|
x1 : [0..168]; |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..8]; |
||||
|
// 0 - root contention |
||||
|
// 1 - rec_idle |
||||
|
// 2 - rec_req_fast |
||||
|
// 3 - rec_req_slow |
||||
|
// 4 - rec_idle_fast |
||||
|
// 5 - rec_idle_slow |
||||
|
// 6 - snd_req |
||||
|
// 7- almost_root |
||||
|
// 8 - almost_child |
||||
|
|
||||
|
// added resets to x1 when not considered again until after rest |
||||
|
// removed root and child (using almost root and almost child) |
||||
|
|
||||
|
// root contention immediate state) |
||||
|
[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); |
||||
|
[rec_idle21] s1=0 -> (s1'=1); |
||||
|
// rec_idle immediate state) |
||||
|
[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); |
||||
|
[rec_req21] s1=1 -> (s1'=0); |
||||
|
// rec_req_fast |
||||
|
[rec_idle21] s1=2 -> (s1'=4); |
||||
|
[snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); |
||||
|
[time] s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_req_slow |
||||
|
[rec_idle21] s1=3 -> (s1'=5); |
||||
|
[snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); |
||||
|
[time] s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_idle_fast |
||||
|
[rec_req21] s1=4 -> (s1'=2); |
||||
|
[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); |
||||
|
[time] s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_idle_slow |
||||
|
[rec_req21] s1=5 -> (s1'=3); |
||||
|
[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); |
||||
|
[time] s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
||||
|
// snd_req |
||||
|
// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 |
||||
|
// also can set x1 to 0 upon entering this state |
||||
|
[rec_req21] s1=6 -> (s1'=0); |
||||
|
[rec_ack21] s1=6 -> (s1'=8); |
||||
|
[time] s1=6 -> (s1'=s1); |
||||
|
// almost root (immediate) |
||||
|
// loop in final states to remove deadlock |
||||
|
[] s1=7 & s2=8 -> (s1'=s1); |
||||
|
[] s1=8 & s2=7 -> (s1'=s1); |
||||
|
[time] s1=7 -> (s1'=s1); |
||||
|
[time] s1=8 -> (s1'=s1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining automata through renaming |
||||
|
module wire21=wire12[w12=w21, y1=z1, y2=z2, |
||||
|
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, |
||||
|
rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] |
||||
|
endmodule |
||||
|
module node2=node1[s1=s2, s2=s1, x1=x2, |
||||
|
rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, |
||||
|
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] |
||||
|
endmodule |
||||
|
|
||||
|
// reward structures |
||||
|
// time |
||||
|
rewards "time" |
||||
|
[time] true : 1; |
||||
|
endrewards |
||||
|
// time nodes sending |
||||
|
rewards "time_sending" |
||||
|
[time] (w12>0 | w21>0) : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)); |
@ -0,0 +1,170 @@ |
|||||
|
// firewire protocol with integer semantics |
||||
|
// dxp/gxn 14/06/01 |
||||
|
|
||||
|
// CLOCKS |
||||
|
// x1 (x2) clock for node1 (node2) |
||||
|
// y1 and y2 (z1 and z2) clocks for wire12 (wire21) |
||||
|
mdp |
||||
|
|
||||
|
// maximum and minimum delays |
||||
|
// fast |
||||
|
const int rc_fast_max = 85; |
||||
|
const int rc_fast_min = 76; |
||||
|
// slow |
||||
|
const int rc_slow_max = 167; |
||||
|
const int rc_slow_min = 159; |
||||
|
// delay caused by the wire length |
||||
|
const int delay = 3; |
||||
|
// probability of choosing fast |
||||
|
const double fast = 0.5; |
||||
|
const double slow=1-fast; |
||||
|
|
||||
|
module wire12 |
||||
|
|
||||
|
// local state |
||||
|
w12 : [0..9]; |
||||
|
// 0 - empty |
||||
|
// 1 - rec_req |
||||
|
// 2 - rec_req_ack |
||||
|
// 3 - rec_ack |
||||
|
// 4 - rec_ack_idle |
||||
|
// 5 - rec_idle |
||||
|
// 6 - rec_idle_req |
||||
|
// 7 - rec_ack_req |
||||
|
// 8 - rec_req_idle |
||||
|
// 9 - rec_idle_ack |
||||
|
|
||||
|
// clock for wire12 |
||||
|
y1 : [0..delay+1]; |
||||
|
y2 : [0..delay+1]; |
||||
|
|
||||
|
// empty |
||||
|
// do not need y1 and y2 to increase as always reset when this state is left |
||||
|
// similarly can reset y1 and y2 when we re-enter this state |
||||
|
[snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); |
||||
|
[snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); |
||||
|
[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); |
||||
|
[time] w12=0 -> (w12'=w12); |
||||
|
// rec_req |
||||
|
[snd_req12] w12=1 -> (w12'=1); |
||||
|
[rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_ack12] w12=1 -> (w12'=2) & (y2'=0); |
||||
|
[snd_idle12] w12=1 -> (w12'=8) & (y2'=0); |
||||
|
[time] w12=1 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_req_ack |
||||
|
[snd_ack12] w12=2 -> (w12'=2); |
||||
|
[rec_req12] w12=2 -> (w12'=3); |
||||
|
[time] w12=2 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack |
||||
|
[snd_ack12] w12=3 -> (w12'=3); |
||||
|
[rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_idle12] w12=3 -> (w12'=4) & (y2'=0); |
||||
|
[snd_req12] w12=3 -> (w12'=7) & (y2'=0); |
||||
|
[time] w12=3 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack_idle |
||||
|
[snd_idle12] w12=4 -> (w12'=4); |
||||
|
[rec_ack12] w12=4 -> (w12'=5); |
||||
|
[time] w12=4 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle |
||||
|
[snd_idle12] w12=5 -> (w12'=5); |
||||
|
[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); |
||||
|
[snd_req12] w12=5 -> (w12'=6) & (y2'=0); |
||||
|
[snd_ack12] w12=5 -> (w12'=9) & (y2'=0); |
||||
|
[time] w12=5 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle_req |
||||
|
[snd_req12] w12=6 -> (w12'=6); |
||||
|
[rec_idle12] w12=6 -> (w12'=1); |
||||
|
[time] w12=6 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_ack_req |
||||
|
[snd_req12] w12=7 -> (w12'=7); |
||||
|
[rec_ack12] w12=7 -> (w12'=1); |
||||
|
[time] w12=7 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_req_idle |
||||
|
[snd_idle12] w12=8 -> (w12'=8); |
||||
|
[rec_req12] w12=8 -> (w12'=5); |
||||
|
[time] w12=8 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
// rec_idle_ack |
||||
|
[snd_ack12] w12=9 -> (w12'=9); |
||||
|
[rec_idle12] w12=9 -> (w12'=3); |
||||
|
[time] w12=9 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module node1 |
||||
|
|
||||
|
// clock for node1 |
||||
|
x1 : [0..168]; |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..8]; |
||||
|
// 0 - root contention |
||||
|
// 1 - rec_idle |
||||
|
// 2 - rec_req_fast |
||||
|
// 3 - rec_req_slow |
||||
|
// 4 - rec_idle_fast |
||||
|
// 5 - rec_idle_slow |
||||
|
// 6 - snd_req |
||||
|
// 7- almost_root |
||||
|
// 8 - almost_child |
||||
|
|
||||
|
// added resets to x1 when not considered again until after rest |
||||
|
// removed root and child (using almost root and almost child) |
||||
|
|
||||
|
// root contention immediate state) |
||||
|
[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); |
||||
|
[rec_idle21] s1=0 -> (s1'=1); |
||||
|
// rec_idle immediate state) |
||||
|
[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); |
||||
|
[rec_req21] s1=1 -> (s1'=0); |
||||
|
// rec_req_fast |
||||
|
[rec_idle21] s1=2 -> (s1'=4); |
||||
|
[snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); |
||||
|
[time] s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_req_slow |
||||
|
[rec_idle21] s1=3 -> (s1'=5); |
||||
|
[snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); |
||||
|
[time] s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_idle_fast |
||||
|
[rec_req21] s1=4 -> (s1'=2); |
||||
|
[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); |
||||
|
[time] s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
||||
|
// rec_idle_slow |
||||
|
[rec_req21] s1=5 -> (s1'=3); |
||||
|
[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); |
||||
|
[time] s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
||||
|
// snd_req |
||||
|
// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 |
||||
|
// also can set x1 to 0 upon entering this state |
||||
|
[rec_req21] s1=6 -> (s1'=0); |
||||
|
[rec_ack21] s1=6 -> (s1'=8); |
||||
|
[time] s1=6 -> (s1'=s1); |
||||
|
// almost root (immediate) |
||||
|
// loop in final states to remove deadlock |
||||
|
[] s1=7 & s2=8 -> (s1'=s1); |
||||
|
[] s1=8 & s2=7 -> (s1'=s1); |
||||
|
[time] s1=7 -> (s1'=s1); |
||||
|
[time] s1=8 -> (s1'=s1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining automata through renaming |
||||
|
module wire21=wire12[w12=w21, y1=z1, y2=z2, |
||||
|
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, |
||||
|
rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] |
||||
|
endmodule |
||||
|
module node2=node1[s1=s2, s2=s1, x1=x2, |
||||
|
rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, |
||||
|
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] |
||||
|
endmodule |
||||
|
|
||||
|
// reward structures |
||||
|
// time |
||||
|
rewards "time" |
||||
|
[time] true : 1; |
||||
|
endrewards |
||||
|
// time nodes sending |
||||
|
rewards "time_sending" |
||||
|
[time] (w12>0 | w21>0) : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)); |
@ -0,0 +1,91 @@ |
|||||
|
// asynchronous leader election |
||||
|
// 4 processes |
||||
|
// gxn/dxp 29/01/01 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
const int N = 3; // number of processes |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
module process1 |
||||
|
|
||||
|
// COUNTER |
||||
|
c1 : [0..3-1]; |
||||
|
|
||||
|
// STATES |
||||
|
s1 : [0..4]; |
||||
|
// 0 make choice |
||||
|
// 1 have not received neighbours choice |
||||
|
// 2 active |
||||
|
// 3 inactive |
||||
|
// 4 leader |
||||
|
|
||||
|
// PREFERENCE |
||||
|
p1 : [0..1]; |
||||
|
|
||||
|
// VARIABLES FOR SENDING AND RECEIVING |
||||
|
receive1 : [0..2]; |
||||
|
// not received anything |
||||
|
// received choice |
||||
|
// received counter |
||||
|
sent1 : [0..2]; |
||||
|
// not send anything |
||||
|
// sent choice |
||||
|
// sent counter |
||||
|
|
||||
|
// pick value |
||||
|
[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); |
||||
|
|
||||
|
// send preference |
||||
|
[p12] (s1=1) & (sent1=0) -> (sent1'=1); |
||||
|
// receive preference |
||||
|
// stay active |
||||
|
[p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1); |
||||
|
// become inactive |
||||
|
[p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1); |
||||
|
|
||||
|
// send preference (can now reset preference) |
||||
|
[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); |
||||
|
// send counter (already sent preference) |
||||
|
// not received counter yet |
||||
|
[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); |
||||
|
// received counter (pick again) |
||||
|
[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// receive counter and not sent yet (note in this case do not pass it on as will send own counter) |
||||
|
[c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); |
||||
|
// receive counter and sent counter |
||||
|
// only active process (decide) |
||||
|
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
// other active process (pick again) |
||||
|
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// send preference (must have received preference) and can now reset |
||||
|
[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); |
||||
|
// send counter (must have received counter first) and can now reset |
||||
|
[c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// receive preference |
||||
|
[p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1); |
||||
|
// receive counter |
||||
|
[c31] (s1=3) & (receive1=1) & (c3<N-1) -> (c1'=c3+1) & (receive1'=2); |
||||
|
|
||||
|
// done |
||||
|
[done] (s1=4) -> (s1'=s1); |
||||
|
// add loop for processes who are inactive |
||||
|
[done] (s1=3) -> (s1'=s1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
// construct further stations through renaming |
||||
|
module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule |
||||
|
module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
|
||||
|
//---------------------------------------------------------------------------------------------------------------------------- |
||||
|
formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); |
||||
|
label "elected" = s1=4|s2=4|s3=4; |
||||
|
|
@ -0,0 +1,88 @@ |
|||||
|
// asynchronous leader election |
||||
|
// 4 processes |
||||
|
// gxn/dxp 29/01/01 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
const int N = 4; // number of processes |
||||
|
|
||||
|
module process1 |
||||
|
|
||||
|
// COUNTER |
||||
|
c1 : [0..N-1]; |
||||
|
|
||||
|
// STATES |
||||
|
s1 : [0..4]; |
||||
|
// 0 make choice |
||||
|
// 1 have not received neighbours choice |
||||
|
// 2 active |
||||
|
// 3 inactive |
||||
|
// 4 leader |
||||
|
|
||||
|
// PREFERENCE |
||||
|
p1 : [0..1]; |
||||
|
|
||||
|
// VARIABLES FOR SENDING AND RECEIVING |
||||
|
receive1 : [0..2]; |
||||
|
// not received anything |
||||
|
// received choice |
||||
|
// received counter |
||||
|
sent1 : [0..2]; |
||||
|
// not send anything |
||||
|
// sent choice |
||||
|
// sent counter |
||||
|
|
||||
|
// pick value |
||||
|
[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); |
||||
|
|
||||
|
// send preference |
||||
|
[p12] (s1=1) & (sent1=0) -> (sent1'=1); |
||||
|
// receive preference |
||||
|
// stay active |
||||
|
[p41] (s1=1) & (receive1=0) & !( (p1=0) & (p4=1) ) -> (s1'=2) & (receive1'=1); |
||||
|
// become inactive |
||||
|
[p41] (s1=1) & (receive1=0) & (p1=0) & (p4=1) -> (s1'=3) & (receive1'=1); |
||||
|
|
||||
|
// send preference (can now reset preference) |
||||
|
[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); |
||||
|
// send counter (already sent preference) |
||||
|
// not received counter yet |
||||
|
[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); |
||||
|
// received counter (pick again) |
||||
|
[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// receive counter and not sent yet (note in this case do not pass it on as will send own counter) |
||||
|
[c41] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); |
||||
|
// receive counter and sent counter |
||||
|
// only active process (decide) |
||||
|
[c41] (s1=2) & (receive1=1) & (sent1=2) & (c4=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
// other active process (pick again) |
||||
|
[c41] (s1=2) & (receive1=1) & (sent1=2) & (c4<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// send preference (must have received preference) and can now reset |
||||
|
[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); |
||||
|
// send counter (must have received counter first) and can now reset |
||||
|
[c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
||||
|
|
||||
|
// receive preference |
||||
|
[p41] (s1=3) & (receive1=0) -> (p1'=p4) & (receive1'=1); |
||||
|
// receive counter |
||||
|
[c41] (s1=3) & (receive1=1) & (c4<N-1) -> (c1'=c4+1) & (receive1'=2); |
||||
|
|
||||
|
// done |
||||
|
[done] (s1=4) -> (s1'=s1); |
||||
|
// add loop for processes who are inactive |
||||
|
[done] (s1=3) -> (s1'=s1); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p41=p12,c12=c23,c41=c12,p4=p1,c4=c1] endmodule |
||||
|
module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p41=p23,c12=c34,c41=c23,p4=p2,c4=c2] endmodule |
||||
|
module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p41,p41=p34,c12=c41,c41=c34,p4=p3,c4=c3] endmodule |
||||
|
|
||||
|
// reward - expected number of rounds (equals the number of times a process receives a counter) |
||||
|
rewards "rounds" |
||||
|
[c12] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "elected" = s1=4|s2=4|s3=4|s4=4; |
@ -0,0 +1,20 @@ |
|||||
|
|
||||
|
mdp |
||||
|
|
||||
|
module module1 |
||||
|
|
||||
|
// local state |
||||
|
s : [0..2] init 0; |
||||
|
|
||||
|
[A] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2); |
||||
|
[B] s=0 -> 0.3 : (s'=0) + 0.7 : (s'=1); |
||||
|
[C] s=0 -> 0.2 : (s'=0) + 0.8 : (s'=2); |
||||
|
[D] s=1 -> 0.25 : (s'=0) + 0.75 : (s'=2); |
||||
|
[] s=2 -> 1 : (s'=s); |
||||
|
endmodule |
||||
|
|
||||
|
rewards "rew" |
||||
|
[A] true : 10; |
||||
|
[D] true : 4; |
||||
|
endrewards |
||||
|
|
@ -0,0 +1,20 @@ |
|||||
|
|
||||
|
mdp |
||||
|
|
||||
|
module module1 |
||||
|
|
||||
|
s : [0..2] init 0; |
||||
|
|
||||
|
[A] s=0 -> 1 : (s'=1); |
||||
|
[B] s=0 -> 1 : (s'=2); |
||||
|
[C] s=1 -> 1 : true; |
||||
|
[D] s=1 -> 1 : (s'=2); |
||||
|
[E] s=2 -> 1 : true; |
||||
|
endmodule |
||||
|
|
||||
|
rewards "rew" |
||||
|
[A] true : 10; |
||||
|
[C] true : 3; |
||||
|
[E] true : 1; |
||||
|
endrewards |
||||
|
|
@ -0,0 +1,16 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module one |
||||
|
|
||||
|
s : [0 .. 5] init 0; |
||||
|
|
||||
|
[] s=0 -> 0.5: (s'=1) + 0.5: (s'=3); |
||||
|
[] s=1 -> 0.4 : (s'=4) + 0.6: (s'=3); |
||||
|
[] s=1 -> 1: (s'=4); |
||||
|
[] s=1 -> 0.8: (s'=3) + 0.2: (s'=4); |
||||
|
[] s=0 | s = 2 -> 0.9: (s'=s) + 0.1 : (s'=3); |
||||
|
[] 3 <= s & s <= 4 -> 1: true; |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "target" = s=3; |
@ -0,0 +1,30 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module one |
||||
|
x : [0 .. 2] init 0; |
||||
|
|
||||
|
[a] x=0 -> (x'=1); |
||||
|
[] x>=0 -> (x'=2); |
||||
|
[done] x>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
module two |
||||
|
y : [0 .. 2] init 0; |
||||
|
|
||||
|
[b] y=0 -> (y'=1); |
||||
|
[] y>=0 -> (y'=2); |
||||
|
[done] y>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
module three |
||||
|
z : [0 .. 2] init 0; |
||||
|
|
||||
|
[a] z=0 -> (z'=1); |
||||
|
[] x=0&y=0&z=1 -> (z'=2); |
||||
|
[loop] z>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
system |
||||
|
((one || two {b <- a}) / {a}) {done <- loop} || three |
||||
|
endsystem |
||||
|
|
@ -0,0 +1,30 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module one |
||||
|
x : [0 .. 2] init 0; |
||||
|
|
||||
|
[a] x=0 -> (x'=1); |
||||
|
[] x>=0 -> (x'=2); |
||||
|
[done] x>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
module two |
||||
|
y : [0 .. 2] init 0; |
||||
|
|
||||
|
[b] y=0 -> (y'=1); |
||||
|
[] y>=0 -> (y'=2); |
||||
|
[done] y>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
module three |
||||
|
z : [0 .. 2] init 0; |
||||
|
|
||||
|
[a] z=0 -> (z'=1); |
||||
|
[] x=0&y=0&z=1 -> (z'=2); |
||||
|
[loop] z>=1 -> true; |
||||
|
endmodule |
||||
|
|
||||
|
system |
||||
|
((one || two {b <- a})) {done <- loop} || three |
||||
|
endsystem |
||||
|
|
@ -0,0 +1,17 @@ |
|||||
|
mdp |
||||
|
|
||||
|
module mod1 |
||||
|
|
||||
|
s : [0..2] init 0; |
||||
|
[] s=0 -> true; |
||||
|
[] s=0 -> (s'=1); |
||||
|
[] s=1 -> (s'=2); |
||||
|
[] s=2 -> (s'=2); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
[] s=1 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=2; |
@ -0,0 +1,40 @@ |
|||||
|
#DECLARATION |
||||
|
init deadlock done two three four five six seven eight nine ten eleven twelve |
||||
|
#END |
||||
|
0 init |
||||
|
98 done two |
||||
|
99 done three |
||||
|
100 done four |
||||
|
101 done five |
||||
|
102 done six |
||||
|
103 done seven |
||||
|
111 done three |
||||
|
112 done four |
||||
|
113 done five |
||||
|
114 done six |
||||
|
115 done seven |
||||
|
116 done eight |
||||
|
124 done four |
||||
|
125 done five |
||||
|
126 done six |
||||
|
127 done seven |
||||
|
128 done eight |
||||
|
129 done nine |
||||
|
137 done five |
||||
|
138 done six |
||||
|
139 done seven |
||||
|
140 done eight |
||||
|
141 done nine |
||||
|
142 done ten |
||||
|
150 done six |
||||
|
151 done seven |
||||
|
152 done eight |
||||
|
153 done nine |
||||
|
154 done ten |
||||
|
155 done eleven |
||||
|
163 done seven |
||||
|
164 done eight |
||||
|
165 done nine |
||||
|
166 done ten |
||||
|
167 done eleven |
||||
|
168 done twelve |
@ -0,0 +1,40 @@ |
|||||
|
// sum of two dice as the asynchronous parallel composition of |
||||
|
// two copies of Knuth's model of a fair die using only fair coins |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
module die1 |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d1 : [0..6] init 0; |
||||
|
|
||||
|
[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2); |
||||
|
[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4); |
||||
|
[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6); |
||||
|
[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1); |
||||
|
[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); |
||||
|
[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); |
||||
|
[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); |
||||
|
[] s1=7 & s2=7 -> 1: (s1'=7); |
||||
|
endmodule |
||||
|
|
||||
|
module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule |
||||
|
|
||||
|
rewards "coinflips" |
||||
|
[] s1<7 | s2<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "done" = s1=7 & s2=7; |
||||
|
label "two" = s1=7 & s2=7 & d1+d2=2; |
||||
|
label "three" = s1=7 & s2=7 & d1+d2=3; |
||||
|
label "four" = s1=7 & s2=7 & d1+d2=4; |
||||
|
label "five" = s1=7 & s2=7 & d1+d2=5; |
||||
|
label "six" = s1=7 & s2=7 & d1+d2=6; |
||||
|
label "seven" = s1=7 & s2=7 & d1+d2=7; |
||||
|
label "eight" = s1=7 & s2=7 & d1+d2=8; |
||||
|
label "nine" = s1=7 & s2=7 & d1+d2=9; |
||||
|
label "ten" = s1=7 & s2=7 & d1+d2=10; |
||||
|
label "eleven" = s1=7 & s2=7 & d1+d2=11; |
||||
|
label "twelve" = s1=7 & s2=7 & d1+d2=12; |
@ -0,0 +1,437 @@ |
|||||
|
mdp |
||||
|
0 0 13 0.5 |
||||
|
0 0 26 0.5 |
||||
|
0 1 1 0.5 |
||||
|
0 1 2 0.5 |
||||
|
1 0 14 0.5 |
||||
|
1 0 27 0.5 |
||||
|
1 1 3 0.5 |
||||
|
1 1 4 0.5 |
||||
|
2 0 15 0.5 |
||||
|
2 0 28 0.5 |
||||
|
2 1 5 0.5 |
||||
|
2 1 6 0.5 |
||||
|
3 0 16 0.5 |
||||
|
3 0 29 0.5 |
||||
|
3 1 1 0.5 |
||||
|
3 1 7 0.5 |
||||
|
4 0 17 0.5 |
||||
|
4 0 30 0.5 |
||||
|
4 1 8 0.5 |
||||
|
4 1 9 0.5 |
||||
|
5 0 18 0.5 |
||||
|
5 0 31 0.5 |
||||
|
5 1 10 0.5 |
||||
|
5 1 11 0.5 |
||||
|
6 0 19 0.5 |
||||
|
6 0 32 0.5 |
||||
|
6 1 2 0.5 |
||||
|
6 1 12 0.5 |
||||
|
7 0 20 0.5 |
||||
|
7 0 33 0.5 |
||||
|
8 0 21 0.5 |
||||
|
8 0 34 0.5 |
||||
|
9 0 22 0.5 |
||||
|
9 0 35 0.5 |
||||
|
10 0 23 0.5 |
||||
|
10 0 36 0.5 |
||||
|
11 0 24 0.5 |
||||
|
11 0 37 0.5 |
||||
|
12 0 25 0.5 |
||||
|
12 0 38 0.5 |
||||
|
13 0 39 0.5 |
||||
|
13 0 52 0.5 |
||||
|
13 1 14 0.5 |
||||
|
13 1 15 0.5 |
||||
|
14 0 40 0.5 |
||||
|
14 0 53 0.5 |
||||
|
14 1 16 0.5 |
||||
|
14 1 17 0.5 |
||||
|
15 0 41 0.5 |
||||
|
15 0 54 0.5 |
||||
|
15 1 18 0.5 |
||||
|
15 1 19 0.5 |
||||
|
16 0 42 0.5 |
||||
|
16 0 55 0.5 |
||||
|
16 1 14 0.5 |
||||
|
16 1 20 0.5 |
||||
|
17 0 43 0.5 |
||||
|
17 0 56 0.5 |
||||
|
17 1 21 0.5 |
||||
|
17 1 22 0.5 |
||||
|
18 0 44 0.5 |
||||
|
18 0 57 0.5 |
||||
|
18 1 23 0.5 |
||||
|
18 1 24 0.5 |
||||
|
19 0 45 0.5 |
||||
|
19 0 58 0.5 |
||||
|
19 1 15 0.5 |
||||
|
19 1 25 0.5 |
||||
|
20 0 46 0.5 |
||||
|
20 0 59 0.5 |
||||
|
21 0 47 0.5 |
||||
|
21 0 60 0.5 |
||||
|
22 0 48 0.5 |
||||
|
22 0 61 0.5 |
||||
|
23 0 49 0.5 |
||||
|
23 0 62 0.5 |
||||
|
24 0 50 0.5 |
||||
|
24 0 63 0.5 |
||||
|
25 0 51 0.5 |
||||
|
25 0 64 0.5 |
||||
|
26 0 65 0.5 |
||||
|
26 0 78 0.5 |
||||
|
26 1 27 0.5 |
||||
|
26 1 28 0.5 |
||||
|
27 0 66 0.5 |
||||
|
27 0 79 0.5 |
||||
|
27 1 29 0.5 |
||||
|
27 1 30 0.5 |
||||
|
28 0 67 0.5 |
||||
|
28 0 80 0.5 |
||||
|
28 1 31 0.5 |
||||
|
28 1 32 0.5 |
||||
|
29 0 68 0.5 |
||||
|
29 0 81 0.5 |
||||
|
29 1 27 0.5 |
||||
|
29 1 33 0.5 |
||||
|
30 0 69 0.5 |
||||
|
30 0 82 0.5 |
||||
|
30 1 34 0.5 |
||||
|
30 1 35 0.5 |
||||
|
31 0 70 0.5 |
||||
|
31 0 83 0.5 |
||||
|
31 1 36 0.5 |
||||
|
31 1 37 0.5 |
||||
|
32 0 71 0.5 |
||||
|
32 0 84 0.5 |
||||
|
32 1 28 0.5 |
||||
|
32 1 38 0.5 |
||||
|
33 0 72 0.5 |
||||
|
33 0 85 0.5 |
||||
|
34 0 73 0.5 |
||||
|
34 0 86 0.5 |
||||
|
35 0 74 0.5 |
||||
|
35 0 87 0.5 |
||||
|
36 0 75 0.5 |
||||
|
36 0 88 0.5 |
||||
|
37 0 76 0.5 |
||||
|
37 0 89 0.5 |
||||
|
38 0 77 0.5 |
||||
|
38 0 90 0.5 |
||||
|
39 0 13 0.5 |
||||
|
39 0 91 0.5 |
||||
|
39 1 40 0.5 |
||||
|
39 1 41 0.5 |
||||
|
40 0 14 0.5 |
||||
|
40 0 92 0.5 |
||||
|
40 1 42 0.5 |
||||
|
40 1 43 0.5 |
||||
|
41 0 15 0.5 |
||||
|
41 0 93 0.5 |
||||
|
41 1 44 0.5 |
||||
|
41 1 45 0.5 |
||||
|
42 0 16 0.5 |
||||
|
42 0 94 0.5 |
||||
|
42 1 40 0.5 |
||||
|
42 1 46 0.5 |
||||
|
43 0 17 0.5 |
||||
|
43 0 95 0.5 |
||||
|
43 1 47 0.5 |
||||
|
43 1 48 0.5 |
||||
|
44 0 18 0.5 |
||||
|
44 0 96 0.5 |
||||
|
44 1 49 0.5 |
||||
|
44 1 50 0.5 |
||||
|
45 0 19 0.5 |
||||
|
45 0 97 0.5 |
||||
|
45 1 41 0.5 |
||||
|
45 1 51 0.5 |
||||
|
46 0 20 0.5 |
||||
|
46 0 98 0.5 |
||||
|
47 0 21 0.5 |
||||
|
47 0 99 0.5 |
||||
|
48 0 22 0.5 |
||||
|
48 0 100 0.5 |
||||
|
49 0 23 0.5 |
||||
|
49 0 101 0.5 |
||||
|
50 0 24 0.5 |
||||
|
50 0 102 0.5 |
||||
|
51 0 25 0.5 |
||||
|
51 0 103 0.5 |
||||
|
52 0 104 0.5 |
||||
|
52 0 117 0.5 |
||||
|
52 1 53 0.5 |
||||
|
52 1 54 0.5 |
||||
|
53 0 105 0.5 |
||||
|
53 0 118 0.5 |
||||
|
53 1 55 0.5 |
||||
|
53 1 56 0.5 |
||||
|
54 0 106 0.5 |
||||
|
54 0 119 0.5 |
||||
|
54 1 57 0.5 |
||||
|
54 1 58 0.5 |
||||
|
55 0 107 0.5 |
||||
|
55 0 120 0.5 |
||||
|
55 1 53 0.5 |
||||
|
55 1 59 0.5 |
||||
|
56 0 108 0.5 |
||||
|
56 0 121 0.5 |
||||
|
56 1 60 0.5 |
||||
|
56 1 61 0.5 |
||||
|
57 0 109 0.5 |
||||
|
57 0 122 0.5 |
||||
|
57 1 62 0.5 |
||||
|
57 1 63 0.5 |
||||
|
58 0 110 0.5 |
||||
|
58 0 123 0.5 |
||||
|
58 1 54 0.5 |
||||
|
58 1 64 0.5 |
||||
|
59 0 111 0.5 |
||||
|
59 0 124 0.5 |
||||
|
60 0 112 0.5 |
||||
|
60 0 125 0.5 |
||||
|
61 0 113 0.5 |
||||
|
61 0 126 0.5 |
||||
|
62 0 114 0.5 |
||||
|
62 0 127 0.5 |
||||
|
63 0 115 0.5 |
||||
|
63 0 128 0.5 |
||||
|
64 0 116 0.5 |
||||
|
64 0 129 0.5 |
||||
|
65 0 130 0.5 |
||||
|
65 0 143 0.5 |
||||
|
65 1 66 0.5 |
||||
|
65 1 67 0.5 |
||||
|
66 0 131 0.5 |
||||
|
66 0 144 0.5 |
||||
|
66 1 68 0.5 |
||||
|
66 1 69 0.5 |
||||
|
67 0 132 0.5 |
||||
|
67 0 145 0.5 |
||||
|
67 1 70 0.5 |
||||
|
67 1 71 0.5 |
||||
|
68 0 133 0.5 |
||||
|
68 0 146 0.5 |
||||
|
68 1 66 0.5 |
||||
|
68 1 72 0.5 |
||||
|
69 0 134 0.5 |
||||
|
69 0 147 0.5 |
||||
|
69 1 73 0.5 |
||||
|
69 1 74 0.5 |
||||
|
70 0 135 0.5 |
||||
|
70 0 148 0.5 |
||||
|
70 1 75 0.5 |
||||
|
70 1 76 0.5 |
||||
|
71 0 136 0.5 |
||||
|
71 0 149 0.5 |
||||
|
71 1 67 0.5 |
||||
|
71 1 77 0.5 |
||||
|
72 0 137 0.5 |
||||
|
72 0 150 0.5 |
||||
|
73 0 138 0.5 |
||||
|
73 0 151 0.5 |
||||
|
74 0 139 0.5 |
||||
|
74 0 152 0.5 |
||||
|
75 0 140 0.5 |
||||
|
75 0 153 0.5 |
||||
|
76 0 141 0.5 |
||||
|
76 0 154 0.5 |
||||
|
77 0 142 0.5 |
||||
|
77 0 155 0.5 |
||||
|
78 0 26 0.5 |
||||
|
78 0 156 0.5 |
||||
|
78 1 79 0.5 |
||||
|
78 1 80 0.5 |
||||
|
79 0 27 0.5 |
||||
|
79 0 157 0.5 |
||||
|
79 1 81 0.5 |
||||
|
79 1 82 0.5 |
||||
|
80 0 28 0.5 |
||||
|
80 0 158 0.5 |
||||
|
80 1 83 0.5 |
||||
|
80 1 84 0.5 |
||||
|
81 0 29 0.5 |
||||
|
81 0 159 0.5 |
||||
|
81 1 79 0.5 |
||||
|
81 1 85 0.5 |
||||
|
82 0 30 0.5 |
||||
|
82 0 160 0.5 |
||||
|
82 1 86 0.5 |
||||
|
82 1 87 0.5 |
||||
|
83 0 31 0.5 |
||||
|
83 0 161 0.5 |
||||
|
83 1 88 0.5 |
||||
|
83 1 89 0.5 |
||||
|
84 0 32 0.5 |
||||
|
84 0 162 0.5 |
||||
|
84 1 80 0.5 |
||||
|
84 1 90 0.5 |
||||
|
85 0 33 0.5 |
||||
|
85 0 163 0.5 |
||||
|
86 0 34 0.5 |
||||
|
86 0 164 0.5 |
||||
|
87 0 35 0.5 |
||||
|
87 0 165 0.5 |
||||
|
88 0 36 0.5 |
||||
|
88 0 166 0.5 |
||||
|
89 0 37 0.5 |
||||
|
89 0 167 0.5 |
||||
|
90 0 38 0.5 |
||||
|
90 0 168 0.5 |
||||
|
91 0 92 0.5 |
||||
|
91 0 93 0.5 |
||||
|
92 0 94 0.5 |
||||
|
92 0 95 0.5 |
||||
|
93 0 96 0.5 |
||||
|
93 0 97 0.5 |
||||
|
94 0 92 0.5 |
||||
|
94 0 98 0.5 |
||||
|
95 0 99 0.5 |
||||
|
95 0 100 0.5 |
||||
|
96 0 101 0.5 |
||||
|
96 0 102 0.5 |
||||
|
97 0 93 0.5 |
||||
|
97 0 103 0.5 |
||||
|
98 0 98 1 |
||||
|
98 1 98 1 |
||||
|
99 0 99 1 |
||||
|
99 1 99 1 |
||||
|
100 0 100 1 |
||||
|
100 1 100 1 |
||||
|
101 0 101 1 |
||||
|
101 1 101 1 |
||||
|
102 0 102 1 |
||||
|
102 1 102 1 |
||||
|
103 0 103 1 |
||||
|
103 1 103 1 |
||||
|
104 0 105 0.5 |
||||
|
104 0 106 0.5 |
||||
|
105 0 107 0.5 |
||||
|
105 0 108 0.5 |
||||
|
106 0 109 0.5 |
||||
|
106 0 110 0.5 |
||||
|
107 0 105 0.5 |
||||
|
107 0 111 0.5 |
||||
|
108 0 112 0.5 |
||||
|
108 0 113 0.5 |
||||
|
109 0 114 0.5 |
||||
|
109 0 115 0.5 |
||||
|
110 0 106 0.5 |
||||
|
110 0 116 0.5 |
||||
|
111 0 111 1 |
||||
|
111 1 111 1 |
||||
|
112 0 112 1 |
||||
|
112 1 112 1 |
||||
|
113 0 113 1 |
||||
|
113 1 113 1 |
||||
|
114 0 114 1 |
||||
|
114 1 114 1 |
||||
|
115 0 115 1 |
||||
|
115 1 115 1 |
||||
|
116 0 116 1 |
||||
|
116 1 116 1 |
||||
|
117 0 118 0.5 |
||||
|
117 0 119 0.5 |
||||
|
118 0 120 0.5 |
||||
|
118 0 121 0.5 |
||||
|
119 0 122 0.5 |
||||
|
119 0 123 0.5 |
||||
|
120 0 118 0.5 |
||||
|
120 0 124 0.5 |
||||
|
121 0 125 0.5 |
||||
|
121 0 126 0.5 |
||||
|
122 0 127 0.5 |
||||
|
122 0 128 0.5 |
||||
|
123 0 119 0.5 |
||||
|
123 0 129 0.5 |
||||
|
124 0 124 1 |
||||
|
124 1 124 1 |
||||
|
125 0 125 1 |
||||
|
125 1 125 1 |
||||
|
126 0 126 1 |
||||
|
126 1 126 1 |
||||
|
127 0 127 1 |
||||
|
127 1 127 1 |
||||
|
128 0 128 1 |
||||
|
128 1 128 1 |
||||
|
129 0 129 1 |
||||
|
129 1 129 1 |
||||
|
130 0 131 0.5 |
||||
|
130 0 132 0.5 |
||||
|
131 0 133 0.5 |
||||
|
131 0 134 0.5 |
||||
|
132 0 135 0.5 |
||||
|
132 0 136 0.5 |
||||
|
133 0 131 0.5 |
||||
|
133 0 137 0.5 |
||||
|
134 0 138 0.5 |
||||
|
134 0 139 0.5 |
||||
|
135 0 140 0.5 |
||||
|
135 0 141 0.5 |
||||
|
136 0 132 0.5 |
||||
|
136 0 142 0.5 |
||||
|
137 0 137 1 |
||||
|
137 1 137 1 |
||||
|
138 0 138 1 |
||||
|
138 1 138 1 |
||||
|
139 0 139 1 |
||||
|
139 1 139 1 |
||||
|
140 0 140 1 |
||||
|
140 1 140 1 |
||||
|
141 0 141 1 |
||||
|
141 1 141 1 |
||||
|
142 0 142 1 |
||||
|
142 1 142 1 |
||||
|
143 0 144 0.5 |
||||
|
143 0 145 0.5 |
||||
|
144 0 146 0.5 |
||||
|
144 0 147 0.5 |
||||
|
145 0 148 0.5 |
||||
|
145 0 149 0.5 |
||||
|
146 0 144 0.5 |
||||
|
146 0 150 0.5 |
||||
|
147 0 151 0.5 |
||||
|
147 0 152 0.5 |
||||
|
148 0 153 0.5 |
||||
|
148 0 154 0.5 |
||||
|
149 0 145 0.5 |
||||
|
149 0 155 0.5 |
||||
|
150 0 150 1 |
||||
|
150 1 150 1 |
||||
|
151 0 151 1 |
||||
|
151 1 151 1 |
||||
|
152 0 152 1 |
||||
|
152 1 152 1 |
||||
|
153 0 153 1 |
||||
|
153 1 153 1 |
||||
|
154 0 154 1 |
||||
|
154 1 154 1 |
||||
|
155 0 155 1 |
||||
|
155 1 155 1 |
||||
|
156 0 157 0.5 |
||||
|
156 0 158 0.5 |
||||
|
157 0 159 0.5 |
||||
|
157 0 160 0.5 |
||||
|
158 0 161 0.5 |
||||
|
158 0 162 0.5 |
||||
|
159 0 157 0.5 |
||||
|
159 0 163 0.5 |
||||
|
160 0 164 0.5 |
||||
|
160 0 165 0.5 |
||||
|
161 0 166 0.5 |
||||
|
161 0 167 0.5 |
||||
|
162 0 158 0.5 |
||||
|
162 0 168 0.5 |
||||
|
163 0 163 1 |
||||
|
163 1 163 1 |
||||
|
164 0 164 1 |
||||
|
164 1 164 1 |
||||
|
165 0 165 1 |
||||
|
165 1 165 1 |
||||
|
166 0 166 1 |
||||
|
166 1 166 1 |
||||
|
167 0 167 1 |
||||
|
167 1 167 1 |
||||
|
168 0 168 1 |
||||
|
168 1 168 1 |
@ -0,0 +1,219 @@ |
|||||
|
// WLAN PROTOCOL (two stations) |
||||
|
// discrete time model |
||||
|
// gxn/jzs 20/02/02 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// COLLISIONS |
||||
|
const int COL = 2; // maximum number of collisions |
||||
|
|
||||
|
// TIMING CONSTRAINTS |
||||
|
// we have used the FHSS parameters |
||||
|
// then scaled by the value of ASLOTTIME |
||||
|
const int ASLOTTIME = 1; |
||||
|
const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
||||
|
const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
const int TRANS_TIME_MAX = 2; // scaling up |
||||
|
const int TRANS_TIME_MIN = 4; // scaling down |
||||
|
const int ACK_TO = 6; |
||||
|
const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
||||
|
const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
// maximum constant used in timing constraints + 1 |
||||
|
const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; |
||||
|
|
||||
|
// CONTENTION WINDOW |
||||
|
// CWMIN =15 & CWMAX =16 |
||||
|
// this means that MAX_BACKOFF IS 2 |
||||
|
const int MAX_BACKOFF = 0; |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// THE MEDIUM/CHANNEL |
||||
|
|
||||
|
// FORMULAE FOR THE CHANNEL |
||||
|
// channel is busy |
||||
|
formula busy = c1>0 | c2>0; |
||||
|
// channel is free |
||||
|
formula free = c1=0 & c2=0; |
||||
|
|
||||
|
module medium |
||||
|
|
||||
|
// number of collisions |
||||
|
col : [0..COL]; |
||||
|
|
||||
|
// medium status |
||||
|
c1 : [0..2]; |
||||
|
c2 : [0..2]; |
||||
|
// ci corresponds to messages associated with station i |
||||
|
// 0 nothing being sent |
||||
|
// 1 being sent correctly |
||||
|
// 2 being sent garbled |
||||
|
|
||||
|
// begin sending message and nothing else currently being sent |
||||
|
[send1] c1=0 & c2=0 -> (c1'=1); |
||||
|
[send2] c2=0 & c1=0 -> (c2'=1); |
||||
|
|
||||
|
// begin sending message and something is already being sent |
||||
|
// in this case both messages become garbled |
||||
|
[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
|
||||
|
// finish sending message |
||||
|
[finish1] c1>0 -> (c1'=0); |
||||
|
[finish2] c2>0 -> (c2'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// STATION 1 |
||||
|
module station1 |
||||
|
// clock for station 1 |
||||
|
x1 : [0..TIME_MAX]; |
||||
|
|
||||
|
// local state |
||||
|
s1 : [1..12]; |
||||
|
// 1 sense |
||||
|
// 2 wait until free before setting backoff |
||||
|
// 3 wait for DIFS then set slot |
||||
|
// 4 set backoff |
||||
|
// 5 backoff |
||||
|
// 6 wait until free in backoff |
||||
|
// 7 wait for DIFS then resume backoff |
||||
|
// 8 vulnerable |
||||
|
// 9 transmit |
||||
|
// 11 wait for SIFS and then ACK |
||||
|
// 10 wait for ACT_TO |
||||
|
// 12 done |
||||
|
// BACKOFF |
||||
|
// separate into slots |
||||
|
slot1 : [0..1]; |
||||
|
backoff1 : [0..15]; |
||||
|
|
||||
|
// BACKOFF COUNTER |
||||
|
bc1 : [0..1]; |
||||
|
// SENSE |
||||
|
// let time pass |
||||
|
[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ready to transmit |
||||
|
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=1 & busy -> (s1'=2) & (x1'=0); |
||||
|
// WAIT UNTIL FREE BEFORE SETTING BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=2 & busy -> (s1'=2); |
||||
|
// find that channel is free so check its free for DIFS before setting backoff |
||||
|
[] s1=2 & free -> (s1'=3); |
||||
|
// WAIT FOR DIFS THEN SET BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=3 & busy -> (s1'=2) & (x1'=0); |
||||
|
// start backoff first uniformly choose slot |
||||
|
// backoff counter 0 |
||||
|
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
||||
|
// SET BACKOFF (no time can pass) |
||||
|
// chosen slot now set backoff |
||||
|
[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=1 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=2 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=3 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=4 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=5 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=6 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=7 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=8 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=9 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=10) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=11) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=12) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=13) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=14) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=15); |
||||
|
// BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// decrement backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); |
||||
|
// finish backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=5 & busy -> (s1'=6) & (x1'=0); |
||||
|
// WAIT UNTIL FREE IN BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=6 & busy -> (s1'=6); |
||||
|
// find that channel is free |
||||
|
[] s1=6 & free -> (s1'=7); |
||||
|
|
||||
|
// WAIT FOR DIFS THEN RESUME BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// resume backoff (start again from previous backoff) |
||||
|
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=7 & busy -> (s1'=6) & (x1'=0); |
||||
|
|
||||
|
// VULNERABLE |
||||
|
// let time pass |
||||
|
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// move to transmit |
||||
|
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); |
||||
|
// TRANSMIT |
||||
|
// let time pass |
||||
|
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// finish transmission successful |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); |
||||
|
// finish transmission garbled |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); |
||||
|
// WAIT FOR SIFS THEN WAIT FOR ACK |
||||
|
|
||||
|
// WAIT FOR SIFS i.e. c1=0 |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
// following guard is always false as SIFS=1 |
||||
|
// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) |
||||
|
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK i.e. c1=1 |
||||
|
// let time pass |
||||
|
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// get acknowledgement so packet sent correctly and move to done |
||||
|
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK_TO |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=11 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// no acknowledgement (go to backoff waiting DIFS first) |
||||
|
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); |
||||
|
|
||||
|
// DONE |
||||
|
[time] s1=12 -> (s1'=12); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
// STATION 2 (rename STATION 1) |
||||
|
module |
||||
|
station2=station1[x1=x2, |
||||
|
s1=s2, |
||||
|
s2=s1, |
||||
|
c1=c2, |
||||
|
c2=c1, |
||||
|
slot1=slot2, |
||||
|
backoff1=backoff2, |
||||
|
bc1=bc2, |
||||
|
send1=send2, |
||||
|
finish1=finish2] |
||||
|
endmodule |
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
|
||||
|
label "twoCollisions" = col=2; |
||||
|
label "fourCollisions" = col=4; |
||||
|
label "sixCollisions" = col=6; |
@ -0,0 +1,219 @@ |
|||||
|
// WLAN PROTOCOL (two stations) |
||||
|
// discrete time model |
||||
|
// gxn/jzs 20/02/02 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// COLLISIONS |
||||
|
const int COL; // maximum number of collisions |
||||
|
|
||||
|
// TIMING CONSTRAINTS |
||||
|
// we have used the FHSS parameters |
||||
|
// then scaled by the value of ASLOTTIME |
||||
|
const int ASLOTTIME = 1; |
||||
|
const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
||||
|
const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
const int TRANS_TIME_MAX; // scaling up |
||||
|
const int TRANS_TIME_MIN = 4; // scaling down |
||||
|
const int ACK_TO = 6; |
||||
|
const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
||||
|
const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
// maximum constant used in timing constraints + 1 |
||||
|
const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; |
||||
|
|
||||
|
// CONTENTION WINDOW |
||||
|
// CWMIN =15 & CWMAX =16 |
||||
|
// this means that MAX_BACKOFF IS 2 |
||||
|
const int MAX_BACKOFF = 0; |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// THE MEDIUM/CHANNEL |
||||
|
|
||||
|
// FORMULAE FOR THE CHANNEL |
||||
|
// channel is busy |
||||
|
formula busy = c1>0 | c2>0; |
||||
|
// channel is free |
||||
|
formula free = c1=0 & c2=0; |
||||
|
|
||||
|
module medium |
||||
|
|
||||
|
// number of collisions |
||||
|
col : [0..COL]; |
||||
|
|
||||
|
// medium status |
||||
|
c1 : [0..2]; |
||||
|
c2 : [0..2]; |
||||
|
// ci corresponds to messages associated with station i |
||||
|
// 0 nothing being sent |
||||
|
// 1 being sent correctly |
||||
|
// 2 being sent garbled |
||||
|
|
||||
|
// begin sending message and nothing else currently being sent |
||||
|
[send1] c1=0 & c2=0 -> (c1'=1); |
||||
|
[send2] c2=0 & c1=0 -> (c2'=1); |
||||
|
|
||||
|
// begin sending message and something is already being sent |
||||
|
// in this case both messages become garbled |
||||
|
[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
|
||||
|
// finish sending message |
||||
|
[finish1] c1>0 -> (c1'=0); |
||||
|
[finish2] c2>0 -> (c2'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// STATION 1 |
||||
|
module station1 |
||||
|
// clock for station 1 |
||||
|
x1 : [0..TIME_MAX]; |
||||
|
|
||||
|
// local state |
||||
|
s1 : [1..12]; |
||||
|
// 1 sense |
||||
|
// 2 wait until free before setting backoff |
||||
|
// 3 wait for DIFS then set slot |
||||
|
// 4 set backoff |
||||
|
// 5 backoff |
||||
|
// 6 wait until free in backoff |
||||
|
// 7 wait for DIFS then resume backoff |
||||
|
// 8 vulnerable |
||||
|
// 9 transmit |
||||
|
// 11 wait for SIFS and then ACK |
||||
|
// 10 wait for ACT_TO |
||||
|
// 12 done |
||||
|
// BACKOFF |
||||
|
// separate into slots |
||||
|
slot1 : [0..1]; |
||||
|
backoff1 : [0..15]; |
||||
|
|
||||
|
// BACKOFF COUNTER |
||||
|
bc1 : [0..1]; |
||||
|
// SENSE |
||||
|
// let time pass |
||||
|
[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ready to transmit |
||||
|
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=1 & busy -> (s1'=2) & (x1'=0); |
||||
|
// WAIT UNTIL FREE BEFORE SETTING BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=2 & busy -> (s1'=2); |
||||
|
// find that channel is free so check its free for DIFS before setting backoff |
||||
|
[] s1=2 & free -> (s1'=3); |
||||
|
// WAIT FOR DIFS THEN SET BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=3 & busy -> (s1'=2) & (x1'=0); |
||||
|
// start backoff first uniformly choose slot |
||||
|
// backoff counter 0 |
||||
|
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
||||
|
// SET BACKOFF (no time can pass) |
||||
|
// chosen slot now set backoff |
||||
|
[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=1 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=2 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=3 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=4 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=5 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=6 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=7 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=8 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=9 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=10) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=11) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=12) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=13) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=14) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=15); |
||||
|
// BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// decrement backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); |
||||
|
// finish backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=5 & busy -> (s1'=6) & (x1'=0); |
||||
|
// WAIT UNTIL FREE IN BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=6 & busy -> (s1'=6); |
||||
|
// find that channel is free |
||||
|
[] s1=6 & free -> (s1'=7); |
||||
|
|
||||
|
// WAIT FOR DIFS THEN RESUME BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// resume backoff (start again from previous backoff) |
||||
|
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=7 & busy -> (s1'=6) & (x1'=0); |
||||
|
|
||||
|
// VULNERABLE |
||||
|
// let time pass |
||||
|
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// move to transmit |
||||
|
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); |
||||
|
// TRANSMIT |
||||
|
// let time pass |
||||
|
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// finish transmission successful |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); |
||||
|
// finish transmission garbled |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); |
||||
|
// WAIT FOR SIFS THEN WAIT FOR ACK |
||||
|
|
||||
|
// WAIT FOR SIFS i.e. c1=0 |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
// following guard is always false as SIFS=1 |
||||
|
// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) |
||||
|
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK i.e. c1=1 |
||||
|
// let time pass |
||||
|
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// get acknowledgement so packet sent correctly and move to done |
||||
|
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK_TO |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=11 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// no acknowledgement (go to backoff waiting DIFS first) |
||||
|
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); |
||||
|
|
||||
|
// DONE |
||||
|
[time] s1=12 -> (s1'=12); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
// STATION 2 (rename STATION 1) |
||||
|
module |
||||
|
station2=station1[x1=x2, |
||||
|
s1=s2, |
||||
|
s2=s1, |
||||
|
c1=c2, |
||||
|
c2=c1, |
||||
|
slot1=slot2, |
||||
|
backoff1=backoff2, |
||||
|
bc1=bc2, |
||||
|
send1=send2, |
||||
|
finish1=finish2] |
||||
|
endmodule |
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
|
||||
|
label "twoCollisions" = col=2; |
||||
|
label "fourCollisions" = col=4; |
||||
|
label "sixCollisions" = col=6; |
@ -0,0 +1,148 @@ |
|||||
|
// bounded retransmission protocol [D'AJJL01] |
||||
|
// gxn/dxp 23/05/2001 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// number of chunks |
||||
|
const int N = 16; |
||||
|
// maximum number of retransmissions |
||||
|
const int MAX = 2; |
||||
|
|
||||
|
// reliability of channels |
||||
|
const double pL; |
||||
|
const double pK; |
||||
|
|
||||
|
// timeouts |
||||
|
const double TOMsg; |
||||
|
const double TOAck; |
||||
|
|
||||
|
module sender |
||||
|
|
||||
|
s : [0..6]; |
||||
|
// 0 idle |
||||
|
// 1 next_frame |
||||
|
// 2 wait_ack |
||||
|
// 3 retransmit |
||||
|
// 4 success |
||||
|
// 5 error |
||||
|
// 6 wait sync |
||||
|
srep : [0..3]; |
||||
|
// 0 bottom |
||||
|
// 1 not ok (nok) |
||||
|
// 2 do not know (dk) |
||||
|
// 3 ok (ok) |
||||
|
nrtr : [0..MAX]; |
||||
|
i : [0..N]; |
||||
|
bs : bool; |
||||
|
s_ab : bool; |
||||
|
fs : bool; |
||||
|
ls : bool; |
||||
|
|
||||
|
// idle |
||||
|
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); |
||||
|
// next_frame |
||||
|
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); |
||||
|
// wait_ack |
||||
|
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); |
||||
|
[TO_Msg] (s=2) -> (s'=3); |
||||
|
[TO_Ack] (s=2) -> (s'=3); |
||||
|
// retransmit |
||||
|
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); |
||||
|
// success |
||||
|
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1); |
||||
|
[] (s=4) & (i=N) -> (s'=0) & (srep'=3); |
||||
|
// error |
||||
|
[SyncWait] (s=5) -> (s'=6); |
||||
|
// wait sync |
||||
|
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module receiver |
||||
|
|
||||
|
r : [0..5]; |
||||
|
// 0 new_file |
||||
|
// 1 fst_safe |
||||
|
// 2 frame_received |
||||
|
// 3 frame_reported |
||||
|
// 4 idle |
||||
|
// 5 resync |
||||
|
rrep : [0..4]; |
||||
|
// 0 bottom |
||||
|
// 1 fst |
||||
|
// 2 inc |
||||
|
// 3 ok |
||||
|
// 4 nok |
||||
|
fr : bool; |
||||
|
lr : bool; |
||||
|
br : bool; |
||||
|
r_ab : bool; |
||||
|
recv : bool; |
||||
|
|
||||
|
|
||||
|
// new_file |
||||
|
[SyncWait] (r=0) -> (r'=0); |
||||
|
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
// fst_safe_frame |
||||
|
[] (r=1) -> (r'=2) & (r_ab'=br); |
||||
|
// frame_received |
||||
|
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); |
||||
|
[aA] (r=2) & !(r_ab=br) -> (r'=4); |
||||
|
// frame_reported |
||||
|
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); |
||||
|
// idle |
||||
|
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
[SyncWait] (r=4) & (ls=true) -> (r'=5); |
||||
|
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); |
||||
|
// resync |
||||
|
[SyncWait] (r=5) -> (r'=0) & (rrep'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// prevents more than one file being sent |
||||
|
module tester |
||||
|
|
||||
|
T : bool; |
||||
|
|
||||
|
[NewFile] (T=false) -> (T'=true); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelK |
||||
|
|
||||
|
k : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); |
||||
|
// sending |
||||
|
[aG] (k=1) -> (k'=0); |
||||
|
// lost |
||||
|
[TO_Msg] (k=2) -> (k'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelL |
||||
|
|
||||
|
l : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); |
||||
|
// sending |
||||
|
[aB] (l=1) -> (l'=0); |
||||
|
// lost |
||||
|
[TO_Ack] (l=2) -> (l'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "error" = s=5; |
||||
|
|
||||
|
rewards |
||||
|
[TO_Msg] true : TOMsg; |
||||
|
[TO_Ack] true : TOAck; |
||||
|
endrewards |
||||
|
|
||||
|
|
@ -0,0 +1,148 @@ |
|||||
|
// bounded retransmission protocol [D'AJJL01] |
||||
|
// gxn/dxp 23/05/2001 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// number of chunks |
||||
|
const int N = 16; |
||||
|
// maximum number of retransmissions |
||||
|
const int MAX = 2; |
||||
|
|
||||
|
// reliability of channels |
||||
|
const double pL; |
||||
|
const double pK; |
||||
|
|
||||
|
// timeouts |
||||
|
const double TOMsg; |
||||
|
const double TOAck; |
||||
|
|
||||
|
module sender |
||||
|
|
||||
|
s : [0..6]; |
||||
|
// 0 idle |
||||
|
// 1 next_frame |
||||
|
// 2 wait_ack |
||||
|
// 3 retransmit |
||||
|
// 4 success |
||||
|
// 5 error |
||||
|
// 6 wait sync |
||||
|
srep : [0..3]; |
||||
|
// 0 bottom |
||||
|
// 1 not ok (nok) |
||||
|
// 2 do not know (dk) |
||||
|
// 3 ok (ok) |
||||
|
nrtr : [0..MAX]; |
||||
|
i : [0..N]; |
||||
|
bs : bool; |
||||
|
s_ab : bool; |
||||
|
fs : bool; |
||||
|
ls : bool; |
||||
|
|
||||
|
// idle |
||||
|
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); |
||||
|
// next_frame |
||||
|
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); |
||||
|
// wait_ack |
||||
|
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); |
||||
|
[TO_Msg] (s=2) -> (s'=3); |
||||
|
[TO_Ack] (s=2) -> (s'=3); |
||||
|
// retransmit |
||||
|
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); |
||||
|
// success |
||||
|
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1); |
||||
|
[] (s=4) & (i=N) -> (s'=0) & (srep'=3); |
||||
|
// error |
||||
|
[SyncWait] (s=5) -> (s'=6); |
||||
|
// wait sync |
||||
|
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module receiver |
||||
|
|
||||
|
r : [0..5]; |
||||
|
// 0 new_file |
||||
|
// 1 fst_safe |
||||
|
// 2 frame_received |
||||
|
// 3 frame_reported |
||||
|
// 4 idle |
||||
|
// 5 resync |
||||
|
rrep : [0..4]; |
||||
|
// 0 bottom |
||||
|
// 1 fst |
||||
|
// 2 inc |
||||
|
// 3 ok |
||||
|
// 4 nok |
||||
|
fr : bool; |
||||
|
lr : bool; |
||||
|
br : bool; |
||||
|
r_ab : bool; |
||||
|
recv : bool; |
||||
|
|
||||
|
|
||||
|
// new_file |
||||
|
[SyncWait] (r=0) -> (r'=0); |
||||
|
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
// fst_safe_frame |
||||
|
[] (r=1) -> (r'=2) & (r_ab'=br); |
||||
|
// frame_received |
||||
|
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); |
||||
|
[aA] (r=2) & !(r_ab=br) -> (r'=4); |
||||
|
// frame_reported |
||||
|
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); |
||||
|
// idle |
||||
|
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
[SyncWait] (r=4) & (ls=true) -> (r'=5); |
||||
|
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); |
||||
|
// resync |
||||
|
[SyncWait] (r=5) -> (r'=0) & (rrep'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// prevents more than one file being sent |
||||
|
module tester |
||||
|
|
||||
|
T : bool; |
||||
|
|
||||
|
[NewFile] (T=false) -> (T'=true); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelK |
||||
|
|
||||
|
k : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); |
||||
|
// sending |
||||
|
[aG] (k=1) -> (k'=0); |
||||
|
// lost |
||||
|
[TO_Msg] (k=2) -> (k'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelL |
||||
|
|
||||
|
l : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); |
||||
|
// sending |
||||
|
[aB] (l=1) -> (l'=0); |
||||
|
// lost |
||||
|
[TO_Ack] (l=2) -> (l'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
[TO_Msg] true : TOMsg; |
||||
|
[TO_Ack] true : TOAck; |
||||
|
endrewards |
||||
|
|
||||
|
|
||||
|
|
||||
|
label "target" = s=5; |
@ -0,0 +1,194 @@ |
|||||
|
// CROWDS [Reiter,Rubin] |
||||
|
// Vitaly Shmatikov, 2002 |
||||
|
// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) |
||||
|
|
||||
|
// note: |
||||
|
// Change everything marked CWDSIZ when changing the size of the crowd |
||||
|
// Change everything marked CWDMAX when increasing max size of the crowd |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// Model parameters |
||||
|
const double PF; // forwarding probability |
||||
|
const double badC; // probability that member is untrustworthy |
||||
|
|
||||
|
// Probability of forwarding |
||||
|
// const double PF = 0.8; |
||||
|
// const double notPF = 0.2; // must be 1-PF |
||||
|
|
||||
|
// Probability that a crowd member is bad |
||||
|
// const double badC = 0.1; |
||||
|
// const double badC = 0.091; |
||||
|
// const double badC = 0.167; |
||||
|
// const double goodC = 0.909; // must be 1-badC |
||||
|
// const double goodC = 0.833; // must be 1-badC |
||||
|
|
||||
|
const int CrowdSize = 3; // CWDSIZ: actual number of good crowd members |
||||
|
const int TotalRuns = 5; // Total number of protocol runs to analyze |
||||
|
const int MaxGood=20; // CWDMAX: maximum number of good crowd members |
||||
|
|
||||
|
// Process definitions |
||||
|
module crowds |
||||
|
|
||||
|
// Auxiliary variables |
||||
|
launch: bool init true; // Start modeling? |
||||
|
newInstance: bool init false; // Initialize a new protocol instance? |
||||
|
runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances |
||||
|
start: bool init false; // Start the protocol? |
||||
|
run: bool init false; // Run the protocol? |
||||
|
lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg |
||||
|
good: bool init false; // Crowd member is good? |
||||
|
bad: bool init false; // ... bad? |
||||
|
recordLast: bool init false; // Record last seen crowd member? |
||||
|
badObserve: bool init false; // Bad members observes who sent msg? |
||||
|
deliver: bool init false; // Deliver message to destination? |
||||
|
done: bool init false; // Protocol instance finished? |
||||
|
|
||||
|
// Counters for attackers' observations |
||||
|
// CWDMAX: 1 counter per each good crowd member |
||||
|
observe0: [0..TotalRuns]; |
||||
|
observe1: [0..TotalRuns]; |
||||
|
observe2: [0..TotalRuns]; |
||||
|
observe3: [0..TotalRuns]; |
||||
|
observe4: [0..TotalRuns]; |
||||
|
observe5: [0..TotalRuns]; |
||||
|
observe6: [0..TotalRuns]; |
||||
|
observe7: [0..TotalRuns]; |
||||
|
observe8: [0..TotalRuns]; |
||||
|
observe9: [0..TotalRuns]; |
||||
|
observe10: [0..TotalRuns]; |
||||
|
observe11: [0..TotalRuns]; |
||||
|
observe12: [0..TotalRuns]; |
||||
|
observe13: [0..TotalRuns]; |
||||
|
observe14: [0..TotalRuns]; |
||||
|
observe15: [0..TotalRuns]; |
||||
|
observe16: [0..TotalRuns]; |
||||
|
observe17: [0..TotalRuns]; |
||||
|
observe18: [0..TotalRuns]; |
||||
|
observe19: [0..TotalRuns]; |
||||
|
|
||||
|
[] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false); |
||||
|
// Set up a newInstance protocol instance |
||||
|
[] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true); |
||||
|
|
||||
|
// SENDER |
||||
|
// Start the protocol |
||||
|
[] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); |
||||
|
|
||||
|
// CROWD MEMBERS |
||||
|
// Good or bad crowd member? |
||||
|
[] !good & !bad & !deliver & run -> |
||||
|
1-badC : (good'=true) & (recordLast'=true) & (run'=false) + |
||||
|
badC : (bad'=true) & (badObserve'=true) & (run'=false); |
||||
|
|
||||
|
// GOOD MEMBERS |
||||
|
// Forward with probability PF, else deliver |
||||
|
[] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); |
||||
|
// Record the last crowd member who touched the msg; |
||||
|
// all good members may appear with equal probability |
||||
|
// Note: This is backward. In the real protocol, each honest |
||||
|
// forwarder randomly chooses the next forwarder. |
||||
|
// Here, the identity of an honest forwarder is randomly |
||||
|
// chosen *after* it has forwarded the message. |
||||
|
[] recordLast & CrowdSize=2 -> |
||||
|
1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=3 -> |
||||
|
1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=4 -> |
||||
|
1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + |
||||
|
1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=5 -> |
||||
|
1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + |
||||
|
1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + |
||||
|
1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=10 -> |
||||
|
1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + |
||||
|
1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=15 -> |
||||
|
1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + |
||||
|
1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); |
||||
|
[] recordLast & CrowdSize=20 -> |
||||
|
1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + |
||||
|
1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); |
||||
|
|
||||
|
// BAD MEMBERS |
||||
|
// Remember from whom the message was received and deliver |
||||
|
// CWDMAX: 1 rule per each good crowd member |
||||
|
[] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
[] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false); |
||||
|
|
||||
|
// RECIPIENT |
||||
|
// Delivery to destination |
||||
|
[] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); |
||||
|
// Start a newInstance instance |
||||
|
[] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "observe0Greater1" = observe0 > 1; |
||||
|
label "observeIGreater1" = observe1>1|observe2>1; |
||||
|
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1; |
@ -0,0 +1,34 @@ |
|||||
|
// Knuth's model of a fair die using only fair coins |
||||
|
dtmc |
||||
|
|
||||
|
const double p; |
||||
|
|
||||
|
module die |
||||
|
|
||||
|
// local state |
||||
|
s : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d : [0..6] init 0; |
||||
|
|
||||
|
[] s=0 -> p : (s'=1) + (1-p) : (s'=2); |
||||
|
[] s=1 -> p : (s'=3) + (1-p) : (s'=4); |
||||
|
[] s=2 -> p : (s'=5) + (1-p) : (s'=6); |
||||
|
[] s=3 -> p : (s'=1) + (1-p) : (s'=7) & (d'=1); |
||||
|
[] s=4 -> p : (s'=7) & (d'=2) + (1-p) : (s'=7) & (d'=3); |
||||
|
[] s=5 -> p : (s'=7) & (d'=4) + (1-p) : (s'=7) & (d'=5); |
||||
|
[] s=6 -> p : (s'=2) + (1-p) : (s'=7) & (d'=6); |
||||
|
[] s=7 -> 1: (s'=7); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards "coin_flips" |
||||
|
[] s<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "one" = s=7&d=1; |
||||
|
label "two" = s=7&d=2; |
||||
|
label "three" = s=7&d=3; |
||||
|
label "four" = s=7&d=4; |
||||
|
label "five" = s=7&d=5; |
||||
|
label "six" = s=7&d=6; |
||||
|
label "done" = s=7; |
@ -0,0 +1,56 @@ |
|||||
|
//Randomised Consensus Protocol |
||||
|
|
||||
|
mdp |
||||
|
const double p1; // in [0.2 , 0.8] |
||||
|
const double p2; // in [0.2 , 0.8] |
||||
|
|
||||
|
|
||||
|
const int N=2; |
||||
|
const int K=2; |
||||
|
const int range = 2*(K+1)*N; |
||||
|
const int counter_init = (K+1)*N; |
||||
|
const int left = N; |
||||
|
const int right = 2*(K+1)*N - N; |
||||
|
|
||||
|
// shared coin |
||||
|
global counter : [0..range] init counter_init; |
||||
|
|
||||
|
module process1 |
||||
|
|
||||
|
// program counter |
||||
|
pc1 : [0..3]; |
||||
|
// 0 - flip |
||||
|
// 1 - write |
||||
|
// 2 - check |
||||
|
// 3 - finished |
||||
|
|
||||
|
// local coin |
||||
|
coin1 : [0..1]; |
||||
|
|
||||
|
// flip coin |
||||
|
[] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); |
||||
|
// write tails -1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); |
||||
|
// write heads +1 (reset coin to add regularity) |
||||
|
[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); |
||||
|
// check |
||||
|
// decide tails |
||||
|
[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); |
||||
|
// decide heads |
||||
|
[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); |
||||
|
// flip again |
||||
|
[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); |
||||
|
// loop (all loop together when done) |
||||
|
[done] (pc1=3) -> (pc1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule |
||||
|
label "finished" = pc1=3 &pc2=3 ; |
||||
|
label "all_coins_equal_1" = coin1=1 &coin2=1 ; |
||||
|
rewards "steps" |
||||
|
true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
|
||||
|
|
@ -0,0 +1,45 @@ |
|||||
|
// sum of two dice as the asynchronous parallel composition of |
||||
|
// two copies of Knuth's model of a fair die using only fair coins |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
//Coin Probabilities |
||||
|
const double p1; |
||||
|
const double p2; |
||||
|
|
||||
|
module die1 |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d1 : [0..6] init 0; |
||||
|
|
||||
|
[] s1=0 -> p1 : (s1'=1) + 1-p1 : (s1'=2); |
||||
|
[] s1=1 -> p1 : (s1'=3) + 1-p1 : (s1'=4); |
||||
|
[] s1=2 -> p1 : (s1'=5) + 1-p1 : (s1'=6); |
||||
|
[] s1=3 -> p1 : (s1'=1) + 1-p1 : (s1'=7) & (d1'=1); |
||||
|
[] s1=4 -> p1 : (s1'=7) & (d1'=2) + 1-p1 : (s1'=7) & (d1'=3); |
||||
|
[] s1=5 -> p1 : (s1'=7) & (d1'=4) + 1-p1 : (s1'=7) & (d1'=5); |
||||
|
[] s1=6 -> p1 : (s1'=2) + 1-p1 : (s1'=7) & (d1'=6); |
||||
|
[] s1=7 & s2=7 -> 1: (s1'=7); |
||||
|
endmodule |
||||
|
|
||||
|
module die2 = die1 [ s1=s2, s2=s1, d1=d2, p1=p2 ] endmodule |
||||
|
|
||||
|
rewards "coinflips" |
||||
|
[] s1<7 | s2<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "done" = s1=7 & s2=7; |
||||
|
label "two" = s1=7 & s2=7 & d1+d2=2; |
||||
|
label "three" = s1=7 & s2=7 & d1+d2=3; |
||||
|
label "four" = s1=7 & s2=7 & d1+d2=4; |
||||
|
label "five" = s1=7 & s2=7 & d1+d2=5; |
||||
|
label "six" = s1=7 & s2=7 & d1+d2=6; |
||||
|
label "seven" = s1=7 & s2=7 & d1+d2=7; |
||||
|
label "eight" = s1=7 & s2=7 & d1+d2=8; |
||||
|
label "nine" = s1=7 & s2=7 & d1+d2=9; |
||||
|
label "ten" = s1=7 & s2=7 & d1+d2=10; |
||||
|
label "eleven" = s1=7 & s2=7 & d1+d2=11; |
||||
|
label "twelve" = s1=7 & s2=7 & d1+d2=12; |
||||
|
label "doubles" = s1=7 & s2=7 & d1=d2; |
@ -0,0 +1 @@ |
|||||
|
P |
@ -0,0 +1 @@ |
|||||
|
P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ]) |
@ -0,0 +1 @@ |
|||||
|
P > 0.5 [ F a ] |
@ -0,0 +1 @@ |
|||||
|
P = ? [ F <= 42 !a ] |
@ -0,0 +1 @@ |
|||||
|
!(a & b) | a & ! c |
@ -0,0 +1 @@ |
|||||
|
R >= 15 [ a U !b ] |
@ -0,0 +1 @@ |
|||||
|
R = ? [ a U <= 4 b & (!c) ] |
@ -0,0 +1,4 @@ |
|||||
|
P<=0.17 [ F "doubles" ] |
||||
|
|
||||
|
|
||||
|
|
@ -0,0 +1,12 @@ |
|||||
|
0 0 |
||||
|
1 1 |
||||
|
2 2 |
||||
|
3 3 |
||||
|
4 4 |
||||
|
5 10 |
||||
|
6 10 |
||||
|
7 5 |
||||
|
8 20 |
||||
|
9 0 |
||||
|
10 0 |
||||
|
11 1000 |
@ -0,0 +1,14 @@ |
|||||
|
0 1 1 |
||||
|
0 2 1 |
||||
|
1 3 1 |
||||
|
1 4 1 |
||||
|
2 5 1 |
||||
|
2 6 1 |
||||
|
3 1 1 |
||||
|
3 7 1 |
||||
|
4 8 1 |
||||
|
4 9 1 |
||||
|
5 10 1 |
||||
|
5 11 1 |
||||
|
6 2 1 |
||||
|
6 12 1 |
@ -0,0 +1,8 @@ |
|||||
|
0 0 |
||||
|
1 1 |
||||
|
2 2 |
||||
|
3 3.32 |
||||
|
4 4 |
||||
|
5 110 |
||||
|
6 101 |
||||
|
7 42 |
@ -0,0 +1,17 @@ |
|||||
|
0 1 10 |
||||
|
1 2 5 |
||||
|
1 3 5.5 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
2 5 2 |
||||
|
3 3 1 |
||||
|
4 3 1 |
||||
|
5 3 0.1 |
||||
|
5 4 1.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
6 0 1 |
||||
|
6 5 0 |
||||
|
6 6 12 |
||||
|
7 6 35.224653 |
||||
|
7 7 9.875347 |
@ -0,0 +1,16 @@ |
|||||
|
0 1 10 |
||||
|
0 5 13 |
||||
|
1 2 5 |
||||
|
1 3 5.5 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
2 5 2 |
||||
|
3 3 1 |
||||
|
4 3 1 |
||||
|
5 3 0.1 |
||||
|
5 4 1.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
6 0 1 |
||||
|
6 5 0 |
||||
|
6 6 12 |
@ -0,0 +1,17 @@ |
|||||
|
0 1 10 |
||||
|
1 2 5 |
||||
|
1 3 5.5 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
2 5 2 |
||||
|
3 3 1 |
||||
|
5 3 0.1 |
||||
|
5 4 1.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
4 3 1 |
||||
|
6 0 1 |
||||
|
6 5 0 |
||||
|
6 6 12 |
||||
|
7 6 35.224653 |
||||
|
7 7 9.875347 |
@ -0,0 +1,17 @@ |
|||||
|
0 1 10 |
||||
|
1 3 5.5 |
||||
|
1 2 5 |
||||
|
2 5 2 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
3 3 1 |
||||
|
4 3 1 |
||||
|
5 3 0.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
5 4 1.1 |
||||
|
6 0 1 |
||||
|
6 5 0 |
||||
|
6 6 12 |
||||
|
7 7 9.875347 |
||||
|
7 6 35.224653 |
@ -0,0 +1,18 @@ |
|||||
|
0 1 10 |
||||
|
1 2 5 |
||||
|
1 3 5.5 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
2 5 2 |
||||
|
3 3 1 |
||||
|
4 3 1 |
||||
|
5 3 0.1 |
||||
|
5 4 1.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
6 0 1 |
||||
|
6 4 42 |
||||
|
6 5 0 |
||||
|
6 6 12 |
||||
|
7 6 35.224653 |
||||
|
7 7 9.875347 |
@ -0,0 +1,23 @@ |
|||||
|
|
||||
|
|
||||
|
0 1 10 |
||||
|
1 2 5 |
||||
|
1 3 5.5 |
||||
|
2 3 21.4 |
||||
|
2 4 4 |
||||
|
2 5 2 |
||||
|
3 3 1 |
||||
|
4 3 1 |
||||
|
5 3 0.1 |
||||
|
|
||||
|
|
||||
|
5 4 1.1 |
||||
|
5 5 9.5 |
||||
|
5 6 6.7 |
||||
|
6 0 1 |
||||
|
6 5 0 |
||||
|
6 6 12 |
||||
|
7 6 35.224653 |
||||
|
7 7 9.875347 |
||||
|
|
||||
|
|
@ -0,0 +1,661 @@ |
|||||
|
1214 1 1486 1 |
||||
|
1215 2 1487 1 |
||||
|
1216 2 1488 1 |
||||
|
1217 1 1489 1 |
||||
|
1218 2 1490 1 |
||||
|
1219 1 1491 1 |
||||
|
1220 1 1492 1 |
||||
|
1221 2 1493 1 |
||||
|
1222 3 1494 1 |
||||
|
1223 3 1495 1 |
||||
|
1224 2 1496 1 |
||||
|
1225 2 1497 1 |
||||
|
1226 2 1498 1 |
||||
|
1227 2 1499 1 |
||||
|
1228 2 1500 1 |
||||
|
1229 2 1501 1 |
||||
|
1230 3 1502 1 |
||||
|
1231 3 1503 1 |
||||
|
1232 2 1504 1 |
||||
|
1233 2 1505 1 |
||||
|
1234 2 1506 1 |
||||
|
1235 2 1507 1 |
||||
|
1236 2 1508 1 |
||||
|
1237 2 1509 1 |
||||
|
1238 2 1510 1 |
||||
|
1239 2 1511 1 |
||||
|
1240 1 1512 1 |
||||
|
1241 2 1513 1 |
||||
|
1242 2 1514 1 |
||||
|
1243 2 1384 1 |
||||
|
1244 2 1385 1 |
||||
|
1245 2 1386 1 |
||||
|
1246 1 1387 1 |
||||
|
1247 1 1388 1 |
||||
|
1248 1 1389 1 |
||||
|
1249 1 1390 1 |
||||
|
1250 1 1391 1 |
||||
|
1251 1 1392 1 |
||||
|
1252 1 1393 1 |
||||
|
1253 2 1394 1 |
||||
|
1254 2 1395 1 |
||||
|
1255 1 1396 1 |
||||
|
1256 1 1397 1 |
||||
|
1257 1 1398 1 |
||||
|
1258 2 1399 1 |
||||
|
1259 2 1400 1 |
||||
|
1260 1 1401 1 |
||||
|
1261 1 1402 1 |
||||
|
1262 1 1403 1 |
||||
|
1263 1 1404 1 |
||||
|
1264 1 1405 1 |
||||
|
1265 1 1406 1 |
||||
|
1266 2 1407 1 |
||||
|
1267 2 1408 1 |
||||
|
1268 1 1409 1 |
||||
|
1269 1 1410 1 |
||||
|
1270 1 1411 1 |
||||
|
1271 1 1515 1 |
||||
|
1272 1 1516 1 |
||||
|
1273 2 1517 1 |
||||
|
1274 2 1518 1 |
||||
|
1275 2 1519 1 |
||||
|
1276 2 1520 1 |
||||
|
1277 1 1521 1 |
||||
|
1278 2 1522 1 |
||||
|
1279 2 1523 1 |
||||
|
1280 2 1524 1 |
||||
|
1281 2 1525 1 |
||||
|
1282 1 1526 1 |
||||
|
1283 1 1527 1 |
||||
|
1284 1 1528 1 |
||||
|
1285 3 1529 1 |
||||
|
1286 3 1530 1 |
||||
|
1287 2 1531 1 |
||||
|
1288 2 1532 1 |
||||
|
1289 2 1533 1 |
||||
|
1290 2 1534 1 |
||||
|
1291 2 1535 1 |
||||
|
1292 2 1536 1 |
||||
|
1293 3 1537 1 |
||||
|
1294 3 1538 1 |
||||
|
1295 2 1539 1 |
||||
|
1296 2 1540 1 |
||||
|
1297 2 1541 1 |
||||
|
1298 2 1542 1 |
||||
|
1299 2 1543 1 |
||||
|
1300 2 1544 1 |
||||
|
1301 2 1545 1 |
||||
|
1302 2 1546 1 |
||||
|
1303 1 1547 1 |
||||
|
1304 2 1548 1 |
||||
|
1305 2 1549 1 |
||||
|
1306 2 1384 1 |
||||
|
1307 2 1385 1 |
||||
|
1308 2 1386 1 |
||||
|
1309 1 1387 1 |
||||
|
1310 1 1388 1 |
||||
|
1311 1 1389 1 |
||||
|
1312 1 1390 1 |
||||
|
1313 1 1391 1 |
||||
|
1314 1 1392 1 |
||||
|
1315 2 1394 1 |
||||
|
1316 2 1395 1 |
||||
|
1317 1 1396 1 |
||||
|
1318 1 1397 1 |
||||
|
1319 1 1398 1 |
||||
|
1320 2 1399 1 |
||||
|
1321 2 1400 1 |
||||
|
1322 1 1401 1 |
||||
|
1323 1 1402 1 |
||||
|
1324 1 1403 1 |
||||
|
1325 1 1404 1 |
||||
|
1326 1 1405 1 |
||||
|
1327 1 1406 1 |
||||
|
1328 2 1407 1 |
||||
|
1329 2 1408 1 |
||||
|
1330 1 1409 1 |
||||
|
1331 1 1410 1 |
||||
|
1332 1 1411 1 |
||||
|
1333 1 1579 1 |
||||
|
1334 1 1580 1 |
||||
|
1335 2 1581 1 |
||||
|
1336 2 1582 1 |
||||
|
1337 2 1583 1 |
||||
|
1338 2 1584 1 |
||||
|
1339 1 1585 1 |
||||
|
1340 2 1586 1 |
||||
|
1341 2 1587 1 |
||||
|
1342 2 1588 1 |
||||
|
1343 2 1589 1 |
||||
|
1344 1 1590 1 |
||||
|
1345 1 1591 1 |
||||
|
1346 1 1592 1 |
||||
|
1347 1 1593 1 |
||||
|
1348 1 1594 1 |
||||
|
1349 2 1595 1 |
||||
|
1350 2 1596 1 |
||||
|
1351 1 1597 1 |
||||
|
1352 1 1598 1 |
||||
|
1353 1 1599 1 |
||||
|
1354 1 1600 1 |
||||
|
1355 1 1601 1 |
||||
|
1356 1 1602 1 |
||||
|
1357 2 1603 1 |
||||
|
1358 2 1604 1 |
||||
|
1359 1 1605 1 |
||||
|
1360 1 1606 1 |
||||
|
1361 1 1607 1 |
||||
|
1362 1 1608 1 |
||||
|
1363 1 1609 1 |
||||
|
1364 1 1610 1 |
||||
|
1365 1 1611 1 |
||||
|
1366 1 1612 1 |
||||
|
1367 0 1613 1 |
||||
|
1368 1 1614 1 |
||||
|
1369 1 1615 1 |
||||
|
1370 1 1616 1 |
||||
|
1371 1 1617 1 |
||||
|
1372 2 1618 1 |
||||
|
1373 2 1619 1 |
||||
|
1374 2 1620 1 |
||||
|
1375 2 1621 1 |
||||
|
1376 1 1622 1 |
||||
|
1377 2 1623 1 |
||||
|
1378 2 1624 1 |
||||
|
1379 2 1625 1 |
||||
|
1380 2 1626 1 |
||||
|
1381 1 1627 1 |
||||
|
1382 1 1628 1 |
||||
|
1383 1 1629 1 |
||||
|
1644 1 141 1 |
||||
|
1645 2 142 1 |
||||
|
1646 2 143 1 |
||||
|
1647 2 144 1 |
||||
|
1648 1 145 1 |
||||
|
1649 1 146 1 |
||||
|
1650 1 147 1 |
||||
|
1651 2 148 1 |
||||
|
1652 2 149 1 |
||||
|
1653 2 150 1 |
||||
|
1654 1 151 1 |
||||
|
1655 1 152 1 |
||||
|
1656 1 153 1 |
||||
|
1657 1 154 1 |
||||
|
1658 1 155 1 |
||||
|
1659 2 0 1 |
||||
|
1660 1 1 1 |
||||
|
1661 1 2 1 |
||||
|
1662 1 3 1 |
||||
|
1663 1 4 1 |
||||
|
1664 1 5 1 |
||||
|
1665 1 6 1 |
||||
|
1666 1 7 1 |
||||
|
1667 0 8 1 |
||||
|
1668 0 9 1 |
||||
|
1669 0 10 1 |
||||
|
1670 1 11 1 |
||||
|
1671 1 12 1 |
||||
|
1672 1 13 1 |
||||
|
1673 1 14 1 |
||||
|
1674 0 15 1 |
||||
|
1675 0 16 1 |
||||
|
1676 0 17 1 |
||||
|
1677 1 18 1 |
||||
|
1678 1 19 1 |
||||
|
1679 1 20 1 |
||||
|
1680 1 21 1 |
||||
|
1681 1 22 1 |
||||
|
1682 0 23 1 |
||||
|
1683 0 24 1 |
||||
|
1684 0 25 1 |
||||
|
1685 1 26 1 |
||||
|
1686 1 27 1 |
||||
|
1687 1 156 1 |
||||
|
1688 1 157 1 |
||||
|
1689 1 158 1 |
||||
|
1690 1 159 1 |
||||
|
1691 2 160 1 |
||||
|
1692 2 161 1 |
||||
|
1693 2 162 1 |
||||
|
1694 1 163 1 |
||||
|
1695 1 164 1 |
||||
|
1696 1 165 1 |
||||
|
1697 2 166 1 |
||||
|
1698 2 167 1 |
||||
|
1699 2 168 1 |
||||
|
1700 1 169 1 |
||||
|
1701 1 170 1 |
||||
|
1702 1 171 1 |
||||
|
1703 1 172 1 |
||||
|
1704 1 173 1 |
||||
|
1705 2 0 1 |
||||
|
1706 1 1 1 |
||||
|
1707 1 2 1 |
||||
|
1708 1 3 1 |
||||
|
1709 1 4 1 |
||||
|
1710 1 5 1 |
||||
|
1711 1 6 1 |
||||
|
1712 1 7 1 |
||||
|
1713 0 8 1 |
||||
|
1714 0 9 1 |
||||
|
1715 0 10 1 |
||||
|
1716 1 11 1 |
||||
|
1717 1 12 1 |
||||
|
1718 1 13 1 |
||||
|
1719 1 14 1 |
||||
|
1720 0 15 1 |
||||
|
1721 0 16 1 |
||||
|
1722 0 17 1 |
||||
|
1723 1 18 1 |
||||
|
1724 1 19 1 |
||||
|
1725 1 20 1 |
||||
|
1726 1 21 1 |
||||
|
1727 1 22 1 |
||||
|
1728 0 23 1 |
||||
|
1729 0 24 1 |
||||
|
1730 0 25 1 |
||||
|
1731 1 26 1 |
||||
|
1732 1 27 1 |
||||
|
1733 1 201 1 |
||||
|
1734 1 202 1 |
||||
|
1735 1 203 1 |
||||
|
1736 1 204 1 |
||||
|
1737 1 205 1 |
||||
|
1738 1 206 1 |
||||
|
1739 1 207 1 |
||||
|
1740 0 208 1 |
||||
|
1741 0 209 1 |
||||
|
1742 0 210 1 |
||||
|
1743 1 211 1 |
||||
|
1744 1 212 1 |
||||
|
1745 1 213 1 |
||||
|
1746 0 214 1 |
||||
|
1747 0 215 1 |
||||
|
1748 0 216 1 |
||||
|
1749 0 217 1 |
||||
|
1750 0 218 1 |
||||
|
1751 1 219 1 |
||||
|
1752 1 220 1 |
||||
|
1753 1 221 1 |
||||
|
1754 1 222 1 |
||||
|
1865 3 2122 1 |
||||
|
1866 3 2123 1 |
||||
|
1867 2 2124 1 |
||||
|
1868 2 2125 1 |
||||
|
1869 2 2126 1 |
||||
|
1870 2 2127 1 |
||||
|
1871 2 2128 1 |
||||
|
1872 2 2129 1 |
||||
|
1873 3 2130 1 |
||||
|
1874 3 2131 1 |
||||
|
1875 2 2132 1 |
||||
|
1876 2 2133 1 |
||||
|
1877 2 2134 1 |
||||
|
1878 2 2135 1 |
||||
|
1879 2 2136 1 |
||||
|
1880 2 2137 1 |
||||
|
1881 2 2138 1 |
||||
|
1882 2 2139 1 |
||||
|
1883 1 2140 1 |
||||
|
1884 2 2141 1 |
||||
|
1885 2 2142 1 |
||||
|
1886 2 2023 1 |
||||
|
1887 2 2024 1 |
||||
|
1888 2 2025 1 |
||||
|
1889 1 2026 1 |
||||
|
1890 1 2027 1 |
||||
|
1891 1 2028 1 |
||||
|
1892 1 2029 1 |
||||
|
1893 1 2030 1 |
||||
|
1894 1 2031 1 |
||||
|
1895 2 2032 1 |
||||
|
1896 2 2033 1 |
||||
|
1897 1 2034 1 |
||||
|
1898 1 2035 1 |
||||
|
1899 1 2036 1 |
||||
|
1900 2 2037 1 |
||||
|
1901 2 2038 1 |
||||
|
1902 1 2039 1 |
||||
|
1903 1 2040 1 |
||||
|
1904 1 2041 1 |
||||
|
1905 1 2042 1 |
||||
|
1906 1 2043 1 |
||||
|
1907 1 2044 1 |
||||
|
1908 2 2045 1 |
||||
|
1909 2 2046 1 |
||||
|
1910 1 2047 1 |
||||
|
1911 1 2048 1 |
||||
|
1912 1 2049 1 |
||||
|
1913 1 2143 1 |
||||
|
1914 1 2144 1 |
||||
|
1915 2 2145 1 |
||||
|
1916 2 2146 1 |
||||
|
1917 2 2147 1 |
||||
|
1918 2 2148 1 |
||||
|
1919 1 2149 1 |
||||
|
1920 2 2150 1 |
||||
|
1921 2 2151 1 |
||||
|
1922 2 2152 1 |
||||
|
1923 2 2153 1 |
||||
|
1924 1 2154 1 |
||||
|
1925 1 2155 1 |
||||
|
1926 1 2156 1 |
||||
|
1927 3 2157 1 |
||||
|
1928 3 2158 1 |
||||
|
1929 2 2159 1 |
||||
|
1930 2 2160 1 |
||||
|
1931 2 2161 1 |
||||
|
1932 2 2162 1 |
||||
|
1933 2 2163 1 |
||||
|
1934 2 2164 1 |
||||
|
1935 3 2165 1 |
||||
|
1936 2 2166 1 |
||||
|
1937 2 2167 1 |
||||
|
1938 2 2168 1 |
||||
|
1939 2 2169 1 |
||||
|
1940 2 2170 1 |
||||
|
1941 2 2171 1 |
||||
|
1942 2 2172 1 |
||||
|
1943 1 2173 1 |
||||
|
1944 2 2174 1 |
||||
|
1945 2 2175 1 |
||||
|
1946 2 2023 1 |
||||
|
1947 2 2024 1 |
||||
|
1948 2 2025 1 |
||||
|
1949 1 2026 1 |
||||
|
1950 1 2027 1 |
||||
|
1951 1 2028 1 |
||||
|
1952 1 2029 1 |
||||
|
1953 1 2030 1 |
||||
|
1954 1 2031 1 |
||||
|
1955 2 2032 1 |
||||
|
1956 2 2033 1 |
||||
|
1957 1 2034 1 |
||||
|
1958 1 2035 1 |
||||
|
1959 1 2036 1 |
||||
|
1960 2 2037 1 |
||||
|
1961 1 2039 1 |
||||
|
1962 1 2040 1 |
||||
|
1963 1 2041 1 |
||||
|
1964 1 2042 1 |
||||
|
1965 1 2043 1 |
||||
|
1966 1 2044 1 |
||||
|
1967 2 2045 1 |
||||
|
1968 2 2046 1 |
||||
|
1969 1 2047 1 |
||||
|
1970 1 2048 1 |
||||
|
1971 1 2049 1 |
||||
|
1972 1 2205 1 |
||||
|
1973 1 2206 1 |
||||
|
1974 2 2207 1 |
||||
|
1975 2 2208 1 |
||||
|
1976 2 2209 1 |
||||
|
1977 2 2210 1 |
||||
|
1978 1 2211 1 |
||||
|
1979 2 2212 1 |
||||
|
1980 2 2213 1 |
||||
|
1981 2 2214 1 |
||||
|
1982 2 2215 1 |
||||
|
1983 1 2216 1 |
||||
|
1984 1 2217 1 |
||||
|
1985 1 2218 1 |
||||
|
1986 1 2219 1 |
||||
|
1987 1 2220 1 |
||||
|
1988 2 2221 1 |
||||
|
1989 2 2222 1 |
||||
|
1990 1 2223 1 |
||||
|
1991 1 2224 1 |
||||
|
1992 1 2225 1 |
||||
|
1993 1 2226 1 |
||||
|
1994 1 2227 1 |
||||
|
1995 1 2228 1 |
||||
|
1996 2 2229 1 |
||||
|
1997 2 2230 1 |
||||
|
1998 1 2231 1 |
||||
|
1999 1 2232 1 |
||||
|
2000 1 2233 1 |
||||
|
2001 1 2234 1 |
||||
|
2002 1 2235 1 |
||||
|
2003 1 2236 1 |
||||
|
2004 1 2237 1 |
||||
|
2005 1 2238 1 |
||||
|
2006 0 2239 1 |
||||
|
2007 1 2240 1 |
||||
|
2008 1 2241 1 |
||||
|
2009 1 2242 1 |
||||
|
2010 1 2243 1 |
||||
|
2011 2 2244 1 |
||||
|
2012 2 2245 1 |
||||
|
2013 2 2246 1 |
||||
|
2014 2 2247 1 |
||||
|
2015 1 2248 1 |
||||
|
2016 2 2249 1 |
||||
|
2017 2 2250 1 |
||||
|
2018 2 2251 1 |
||||
|
2019 2 2252 1 |
||||
|
2020 1 2253 1 |
||||
|
2021 1 2254 1 |
||||
|
2022 1 2255 1 |
||||
|
2300 2 142 1 |
||||
|
2301 2 143 1 |
||||
|
2302 2 144 1 |
||||
|
2303 1 145 1 |
||||
|
2304 1 146 1 |
||||
|
2305 1 147 1 |
||||
|
2306 2 148 1 |
||||
|
2307 2 149 1 |
||||
|
2308 2 150 1 |
||||
|
2309 1 151 1 |
||||
|
2310 1 152 1 |
||||
|
2311 1 153 1 |
||||
|
2312 1 154 1 |
||||
|
2313 1 155 1 |
||||
|
2314 2 0 1 |
||||
|
2315 1 1 1 |
||||
|
2316 1 2 1 |
||||
|
2317 1 3 1 |
||||
|
2318 1 4 1 |
||||
|
2319 1 5 1 |
||||
|
2320 1 6 1 |
||||
|
2321 1 7 1 |
||||
|
2322 0 8 1 |
||||
|
2323 0 9 1 |
||||
|
2324 0 10 1 |
||||
|
2325 1 11 1 |
||||
|
2326 1 12 1 |
||||
|
2327 1 13 1 |
||||
|
2328 1 14 1 |
||||
|
2329 0 15 1 |
||||
|
2330 0 16 1 |
||||
|
2331 0 17 1 |
||||
|
2332 1 18 1 |
||||
|
2333 1 19 1 |
||||
|
2334 1 20 1 |
||||
|
2335 1 21 1 |
||||
|
2336 1 22 1 |
||||
|
2337 0 23 1 |
||||
|
2338 0 24 1 |
||||
|
2339 0 25 1 |
||||
|
2340 1 26 1 |
||||
|
2341 1 27 1 |
||||
|
2342 1 156 1 |
||||
|
2343 1 157 1 |
||||
|
2344 1 158 1 |
||||
|
2345 1 159 1 |
||||
|
2346 2 160 1 |
||||
|
2347 2 161 1 |
||||
|
2348 2 162 1 |
||||
|
2349 1 163 1 |
||||
|
2350 1 164 1 |
||||
|
2351 1 165 1 |
||||
|
2352 2 166 1 |
||||
|
2353 2 168 1 |
||||
|
2354 1 169 1 |
||||
|
2355 1 170 1 |
||||
|
2356 1 171 1 |
||||
|
2357 1 172 1 |
||||
|
2358 1 173 1 |
||||
|
2359 2 0 1 |
||||
|
2360 1 1 1 |
||||
|
2361 1 2 1 |
||||
|
2362 1 3 1 |
||||
|
2363 1 4 1 |
||||
|
2364 1 5 1 |
||||
|
2365 1 6 1 |
||||
|
2366 1 7 1 |
||||
|
2367 0 8 1 |
||||
|
2368 0 9 1 |
||||
|
2369 0 10 1 |
||||
|
2370 1 11 1 |
||||
|
2371 1 12 1 |
||||
|
2372 1 13 1 |
||||
|
2373 1 14 1 |
||||
|
2374 0 15 1 |
||||
|
2375 0 16 1 |
||||
|
2376 0 17 1 |
||||
|
2377 1 18 1 |
||||
|
2378 1 19 1 |
||||
|
2379 1 20 1 |
||||
|
2380 1 22 1 |
||||
|
2381 0 23 1 |
||||
|
2382 0 24 1 |
||||
|
2383 0 25 1 |
||||
|
2384 1 26 1 |
||||
|
2385 1 27 1 |
||||
|
2386 1 201 1 |
||||
|
2387 1 202 1 |
||||
|
2388 1 203 1 |
||||
|
2389 1 204 1 |
||||
|
2390 1 205 1 |
||||
|
2391 1 206 1 |
||||
|
2392 1 207 1 |
||||
|
2393 0 208 1 |
||||
|
2394 0 209 1 |
||||
|
2395 0 210 1 |
||||
|
2396 1 211 1 |
||||
|
2397 1 212 1 |
||||
|
2398 1 213 1 |
||||
|
2399 0 214 1 |
||||
|
2400 0 215 1 |
||||
|
2401 0 216 1 |
||||
|
2402 0 217 1 |
||||
|
2403 0 218 1 |
||||
|
2404 1 219 1 |
||||
|
2405 1 220 1 |
||||
|
2406 1 221 1 |
||||
|
2407 1 222 1 |
||||
|
3010 1 2542 1 |
||||
|
3011 1 2543 1 |
||||
|
3012 1 2544 1 |
||||
|
3013 1 2545 1 |
||||
|
3014 2 2546 1 |
||||
|
3015 2 2547 1 |
||||
|
3016 2 2548 1 |
||||
|
3017 1 2549 1 |
||||
|
3018 1 2550 1 |
||||
|
3019 2 2552 1 |
||||
|
3020 2 2553 1 |
||||
|
3021 2 2554 1 |
||||
|
3022 1 2555 1 |
||||
|
3023 1 2556 1 |
||||
|
3024 1 2558 1 |
||||
|
3025 1 2559 1 |
||||
|
3026 2 2408 1 |
||||
|
3027 1 2409 1 |
||||
|
3028 1 2410 1 |
||||
|
3029 1 2412 1 |
||||
|
3030 1 2413 1 |
||||
|
3031 1 2414 1 |
||||
|
3032 0 2416 1 |
||||
|
3033 0 2417 1 |
||||
|
3034 1 2419 1 |
||||
|
3035 1 2420 1 |
||||
|
3036 1 2421 1 |
||||
|
3037 0 2423 1 |
||||
|
3038 0 2424 1 |
||||
|
3039 1 2426 1 |
||||
|
3040 1 2427 1 |
||||
|
3041 1 2428 1 |
||||
|
3042 1 2429 1 |
||||
|
3043 1 2430 1 |
||||
|
3044 0 2431 1 |
||||
|
3045 0 2432 1 |
||||
|
3046 1 2433 1 |
||||
|
3047 1 2434 1 |
||||
|
3048 1 2560 1 |
||||
|
3049 1 2561 1 |
||||
|
3050 1 2562 1 |
||||
|
3051 1 2563 1 |
||||
|
3052 2 2564 1 |
||||
|
3053 2 2565 1 |
||||
|
3054 2 2566 1 |
||||
|
3055 1 2567 1 |
||||
|
3056 1 2568 1 |
||||
|
3057 2 2570 1 |
||||
|
3058 2 2571 1 |
||||
|
3059 2 2572 1 |
||||
|
3060 1 2573 1 |
||||
|
3061 1 2574 1 |
||||
|
3062 1 2576 1 |
||||
|
3063 1 2577 1 |
||||
|
3064 2 2408 1 |
||||
|
3065 1 2409 1 |
||||
|
3066 1 2410 1 |
||||
|
3067 1 2412 1 |
||||
|
3068 1 2413 1 |
||||
|
3069 1 2414 1 |
||||
|
3070 0 2416 1 |
||||
|
3071 0 2417 1 |
||||
|
3072 1 2419 1 |
||||
|
3073 1 2420 1 |
||||
|
3074 1 2421 1 |
||||
|
3075 0 2423 1 |
||||
|
3076 0 2424 1 |
||||
|
3077 1 2426 1 |
||||
|
3078 1 2427 1 |
||||
|
3079 1 2428 1 |
||||
|
3080 1 2429 1 |
||||
|
3081 1 2430 1 |
||||
|
3082 0 2431 1 |
||||
|
3083 0 2432 1 |
||||
|
3084 1 2433 1 |
||||
|
3085 1 2434 1 |
||||
|
3086 1 2600 1 |
||||
|
3087 1 2601 1 |
||||
|
3088 1 2602 1 |
||||
|
3089 1 2603 1 |
||||
|
3090 1 2604 1 |
||||
|
3091 1 2605 1 |
||||
|
3092 1 2606 1 |
||||
|
3093 0 2607 1 |
||||
|
3094 0 2608 1 |
||||
|
3095 1 2609 1 |
||||
|
3096 1 2610 1 |
||||
|
3097 1 2611 1 |
||||
|
3098 0 2612 1 |
||||
|
3099 0 2613 1 |
||||
|
3100 0 2614 1 |
||||
|
3101 0 2615 1 |
||||
|
3102 1 2616 1 |
||||
|
3103 1 2617 1 |
||||
|
3104 1 2618 1 |
||||
|
3105 1 2619 1 |
||||
|
3150 1 2551 1 |
||||
|
3151 1 2557 1 |
||||
|
3152 1 2411 1 |
||||
|
3153 1 2415 1 |
||||
|
3154 0 2418 1 |
||||
|
3155 1 2422 1 |
||||
|
3156 0 2425 1 |
||||
|
3157 1 2569 1 |
||||
|
3158 1 2575 1 |
||||
|
3159 1 2411 1 |
||||
|
3160 1 2415 1 |
||||
|
3161 0 2418 1 |
||||
|
3162 1 2422 1 |
||||
|
3163 0 2425 1 |
||||
|
3164 0 2620 1 |
||||
|
3165 0 2621 1 |
||||
|
3170 0 2599 1 |
||||
|
3171 0 2599 1 |
4096
resources/examples/testfiles/rew/leader4_8.pick.trans.rew
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,6 @@ |
|||||
|
0 0 |
||||
|
1 1.75774 |
||||
|
2 5.436563657 |
||||
|
3 1.570796327 |
||||
|
4 1000 |
||||
|
5 7 |
@ -0,0 +1,7 @@ |
|||||
|
0 0 |
||||
|
1 1.75774 |
||||
|
2 5.436563657 |
||||
|
3 1.570796327 |
||||
|
4 1000 |
||||
|
5 7 |
||||
|
9 42 |
@ -0,0 +1,6 @@ |
|||||
|
0 0 |
||||
|
1 1 |
||||
|
2 2 |
||||
|
3 3.32 |
||||
|
4 42 |
||||
|
5 110 |
@ -0,0 +1,17 @@ |
|||||
|
0 0 0 1 |
||||
|
0 0 1 30 |
||||
|
0 1 1 15.2 |
||||
|
0 1 2 75 |
||||
|
0 1 5 2.45 |
||||
|
0 2 5 1 |
||||
|
0 3 0 0.114 |
||||
|
0 3 4 90 |
||||
|
1 0 2 1 |
||||
|
2 0 2 55 |
||||
|
2 0 3 87 |
||||
|
3 0 2 13 |
||||
|
3 0 3 999 |
||||
|
4 0 1 0.7 |
||||
|
4 0 4 0.3 |
||||
|
5 0 1 0.1 |
||||
|
5 0 5 6 |
Some files were not shown because too many files changed in this diff
Reference in new issue
xxxxxxxxxx