dehnert
9 years ago
4725 changed files with 213050 additions and 582041 deletions
-
9.gitignore
-
337CMakeLists.txt
-
24README
-
51README.md
-
2cuda/CMakeAlignmentCheck.cpp
-
2cuda/CMakeFloatAlignmentCheck.cpp
-
4doc/build.md
-
52examples/benchmarkRegions.sh
-
52examples/benchmarkRegionsRefinement.sh
-
116examples/ctmc/cluster/cluster.sm
-
151examples/ctmc/embedded/embedded.sm
-
126examples/ctmc/fms/fms.sm
-
51examples/ctmc/polling/polling2.sm
-
66examples/ctmc/polling/polling5.sm
-
42examples/ctmc/tandem/tandem.sm
-
11examples/ctmc/tiny/tiny.sm
-
4examples/dft/and.dft
-
5examples/dft/and_param.dft
-
4examples/dft/be_nonfail.dft
-
21examples/dft/cardiac.dft
-
24examples/dft/cas.dft
-
22examples/dft/cm2.dft
-
41examples/dft/cm4.dft
-
26examples/dft/cps.dft
-
16examples/dft/deathegg.dft
-
8examples/dft/fdep.dft
-
5examples/dft/fdep2.dft
-
5examples/dft/fdep3.dft
-
129examples/dft/ftpp_complex.dft
-
63examples/dft/ftpp_large.dft
-
53examples/dft/ftpp_standard.dft
-
22examples/dft/mcs.dft
-
26examples/dft/mdcs.dft
-
19examples/dft/mdcs2.dft
-
7examples/dft/mp.dft
-
8examples/dft/nonmonoton_param.dft
-
4examples/dft/or.dft
-
4examples/dft/pand.dft
-
6examples/dft/pand_param.dft
-
12examples/dft/pdep.dft
-
9examples/dft/pdep2.dft
-
5examples/dft/pdep3.dft
-
7examples/dft/pdep4.dft
-
11examples/dft/pdep_symmetry.dft
-
5examples/dft/por.dft
-
5examples/dft/seq.dft
-
6examples/dft/seq2.dft
-
6examples/dft/seq3.dft
-
7examples/dft/seq4.dft
-
9examples/dft/seq5.dft
-
5examples/dft/spare.dft
-
8examples/dft/spare2.dft
-
10examples/dft/spare3.dft
-
9examples/dft/spare4.dft
-
9examples/dft/spare5.dft
-
7examples/dft/spare6.dft
-
5examples/dft/spare7.dft
-
7examples/dft/spare8.dft
-
5examples/dft/spare_cold.dft
-
9examples/dft/spare_param.dft
-
9examples/dft/spare_symmetry.dft
-
8examples/dft/symmetry.dft
-
8examples/dft/symmetry2.dft
-
12examples/dft/symmetry3.dft
-
12examples/dft/symmetry4.dft
-
21examples/dft/symmetry5.dft
-
10examples/dft/symmetry_param.dft
-
7examples/dft/symmetry_shared.dft
-
8examples/dft/tripple_and1.dft
-
8examples/dft/tripple_and2.dft
-
6examples/dft/tripple_and2_c.dft
-
7examples/dft/tripple_and_c.dft
-
9examples/dft/tripple_or.dft
-
8examples/dft/tripple_or2.dft
-
6examples/dft/tripple_or2_c.dft
-
7examples/dft/tripple_or_c.dft
-
9examples/dft/tripple_pand.dft
-
8examples/dft/tripple_pand2.dft
-
6examples/dft/tripple_pand2_c.dft
-
7examples/dft/tripple_pand_c.dft
-
5examples/dft/voting.dft
-
5examples/dft/voting2.dft
-
136examples/dtmc/brp/brp.pm
-
139examples/dtmc/brp/brp_2_16.pm
-
3examples/dtmc/crowds/crowds.pctl
-
19examples/dtmc/crowds/crowds.res
-
80examples/dtmc/crowds/crowds10_5.pm
-
95examples/dtmc/crowds/crowds15_5.pm
-
111examples/dtmc/crowds/crowds20_5.pm
-
4examples/dtmc/die/die.pctl
-
31examples/dtmc/die/die.pm
-
4examples/dtmc/die/die.res
-
76examples/dtmc/nand/nand.pm
-
22examples/dtmc/sync/sync.pm
-
4examples/dtmc/synchronous_leader/leader.pctl
-
14examples/dtmc/synchronous_leader/leader.res
-
89examples/dtmc/synchronous_leader/leader4_8.pm
-
90examples/dtmc/synchronous_leader/leader5_8.pm
-
91examples/dtmc/synchronous_leader/leader6_8.pm
-
1examples/dtmc/tiny_lra/tiny_lra.pctl
@ -0,0 +1,24 @@ |
|||
# Create build directory for storm |
|||
mkdir build |
|||
|
|||
# Go to build directory |
|||
cd build |
|||
|
|||
# Configure the project |
|||
cmake .. |
|||
# If you want an interactive configuration, try "ccmake ..". Then you can press "c" to initially configure the project, change your values and then press "g" to generate the Makefile |
|||
|
|||
# After generating the Makefile you can build the resources we need for the project |
|||
make resources |
|||
|
|||
# Now we build the main project for DFTs |
|||
make storm-dft-main |
|||
|
|||
# Last you can run an example |
|||
./src/storm-dft -dft ../examples/dft/and.dft -mttf |
|||
|
|||
# To get a list of all available arguments run |
|||
./src/storm-dft --help |
|||
|
|||
# Example for DFT to Petri net translation |
|||
./src/storm-dft -dft ../examples/dft/and.dft --gspn |
|||
@ -1 +1,52 @@ |
|||
Storm |
|||
============================== |
|||
|
|||
For more instructions, check out the documentation found in [Getting Started](doc/getting-started.md) |
|||
|
|||
|
|||
Benchmarks |
|||
---------------------------- |
|||
|
|||
Example input files for storm can be obtained from |
|||
https://github.com/moves-rwth/storm-examples. |
|||
Running make example-files automatically obtains these files. |
|||
|
|||
Further examples and benchmarks found in the following repositories: |
|||
|
|||
* **Prism files** (DTMC, MDP, CTMC): |
|||
http://www.prismmodelchecker.org/benchmarks/ |
|||
* **Jani files** (DTMC, MDP, CTMC, MA): |
|||
http://jani-spec.org/ |
|||
* **GSPN**s: |
|||
(private, contact: sebastian.junges@cs.rwth-aachen.de) |
|||
* **DFT**s: |
|||
https://github.com/moves-rwth/dft-examples |
|||
* **PGCL**: |
|||
(private, contact: sebastian.junges@cs.rwth-aachen.de) |
|||
|
|||
|
|||
Authors |
|||
----------------------------- |
|||
Storm has been developed at RWTH Aachen University. |
|||
|
|||
###### Principal developers |
|||
* Christian Dehnert |
|||
* Joost-Pieter Katoen |
|||
* Sebastian Junges |
|||
* Matthias Volk |
|||
|
|||
###### Developers (lexicographical order) |
|||
* Philipp Berger |
|||
* David Korzeniewski |
|||
* Tim Quatmann |
|||
|
|||
###### Contributors (lexicographical order) |
|||
* Dimitri Bohlender |
|||
* Harold Bruintjes |
|||
* Michael Deutschen |
|||
* Thomas Heinemann |
|||
* Thomas Henn |
|||
* Tom Janson |
|||
* Gereon Kremer |
|||
* Manuel Sascha Weiand |
|||
* Lukas Westhofen |
|||
@ -1,52 +0,0 @@ |
|||
#!/bin/bash |
|||
|
|||
if [ "$#" != 1 ]; |
|||
then |
|||
echo "Wrong number of arguments! Provide a filename for the results!" |
|||
elif [ -a $1 ]; then |
|||
echo "File for results already exists!" |
|||
else |
|||
|
|||
|
|||
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" |
|||
|
|||
executable=$DIR/../build/src/storm |
|||
|
|||
timeout="timeout 3600" |
|||
|
|||
declare -a modeltypes=("pdtmc" "pmdp") |
|||
|
|||
for modeltype in "${modeltypes[@]}" |
|||
do |
|||
if [ "$modeltype" == "pdtmc" ]; |
|||
then |
|||
declare -a models=("crowds" "nand" "brp_rewards2" "brp_rewards4" "brp") |
|||
dobisim="-bisim" |
|||
else |
|||
declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4") |
|||
dobisim="" |
|||
fi |
|||
for model in "${models[@]}" |
|||
do |
|||
modelfolder="$DIR/$modeltype/$model" |
|||
suffix="-" |
|||
while read instance; |
|||
do |
|||
suffix="1$suffix" |
|||
echo "Working on $modelfolder/$instance" |
|||
echo "___WORKING ON $modeltype: $instance""____________" >>$1$suffix |
|||
echo "_________________________________________________________________________________" >> $1$suffix |
|||
$timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_regions.txt" >> $1$suffix & |
|||
done < "$modelfolder/models" |
|||
wait |
|||
# write logs into result file |
|||
suffix="-" |
|||
while read instance; |
|||
do |
|||
suffix="1$suffix" |
|||
cat $1$suffix >> $1 |
|||
rm $1$suffix |
|||
done < "$modelfolder/models" |
|||
done |
|||
done |
|||
fi |
|||
@ -1,52 +0,0 @@ |
|||
#!/bin/bash |
|||
|
|||
if [ "$#" != 1 ]; |
|||
then |
|||
echo "Wrong number of arguments! Provide a filename for the results!" |
|||
elif [ -a $1 ]; then |
|||
echo "File for results already exists!" |
|||
else |
|||
|
|||
|
|||
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" |
|||
|
|||
executable=$DIR/../build/src/storm |
|||
|
|||
timeout="timeout 3600" |
|||
|
|||
declare -a modeltypes=("pdtmc" "pmdp") |
|||
|
|||
for modeltype in "${modeltypes[@]}" |
|||
do |
|||
if [ "$modeltype" == "pdtmc" ]; |
|||
then |
|||
declare -a models=("crowds" "nand" "brp_rewards2" "brp_rewards4" "brp") |
|||
dobisim="-bisim" |
|||
else |
|||
declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4") |
|||
dobisim="" |
|||
fi |
|||
for model in "${models[@]}" |
|||
do |
|||
modelfolder="$DIR/$modeltype/$model" |
|||
suffix="-" |
|||
while read instance; |
|||
do |
|||
suffix="1$suffix" |
|||
echo "Working on $modelfolder/$instance" |
|||
echo "___WORKING ON $modeltype: $instance""____________" >>$1$suffix |
|||
echo "_________________________________________________________________________________" >> $1$suffix |
|||
$timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_space.txt" --region:refinement 0.05 --region:samplemode off >> "$1$suffix" & |
|||
done < "$modelfolder/models" |
|||
wait |
|||
# write logs into result file |
|||
suffix="-" |
|||
while read instance; |
|||
do |
|||
suffix="1$suffix" |
|||
cat $1$suffix >> $1 |
|||
rm $1$suffix |
|||
done < "$modelfolder/models" |
|||
done |
|||
done |
|||
fi |
|||
@ -1,116 +0,0 @@ |
|||
// Workstation cluster [HHK00] |
|||
// dxp/gxn 11/01/00 |
|||
|
|||
ctmc |
|||
|
|||
const int N; // 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 |
|||
@ -1,151 +0,0 @@ |
|||
ctmc |
|||
|
|||
// constants |
|||
const int MAX_COUNT; |
|||
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; |
|||
@ -1,126 +0,0 @@ |
|||
// flexible manufacturing system [CT93] |
|||
// gxn/dxp 11/06/01 |
|||
|
|||
ctmc // model is a ctmc |
|||
|
|||
const int n; // 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 |
|||
@ -1,51 +0,0 @@ |
|||
// 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 |
|||
@ -1,66 +0,0 @@ |
|||
// polling example [IT90] |
|||
// gxn/dxp 26/01/00 |
|||
|
|||
ctmc |
|||
|
|||
const int N = 5; |
|||
|
|||
const double mu = 1; |
|||
const double gamma = 200; |
|||
const double lambda = mu/N; |
|||
|
|||
module server |
|||
|
|||
s : [1..5]; // 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'=s+1); |
|||
[loop2b] (s=2)&(a=0) -> gamma : (a'=1); |
|||
[serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); |
|||
[loop3b] (s=3)&(a=0) -> gamma : (a'=1); |
|||
[serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); |
|||
[loop4b] (s=4)&(a=0) -> gamma : (a'=1); |
|||
[serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop5a] (s=5)&(a=0) -> gamma : (s'=1); |
|||
[loop5b] (s=5)&(a=0) -> gamma : (a'=1); |
|||
[serve5] (s=5)&(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 |
|||
module station3 = station1 [ s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3 ] endmodule |
|||
module station4 = station1 [ s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4 ] endmodule |
|||
module station5 = station1 [ s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5 ] 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 |
|||
@ -1,42 +0,0 @@ |
|||
// tandem queueing network [HKMKS99] |
|||
// gxn/dxp 25/01/00 |
|||
|
|||
ctmc |
|||
|
|||
const int c; // 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; |
|||
@ -1,11 +0,0 @@ |
|||
ctmc |
|||
|
|||
module one |
|||
s : [0 .. 3] init 0; |
|||
|
|||
[] s<3 -> 3/2 : (s'=s+1); |
|||
[] s>0 -> 3 : (s'=s-1); |
|||
endmodule |
|||
|
|||
label "empty" = s=0; |
|||
label "full" = s=3; |
|||
@ -1,4 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -1,5 +0,0 @@ |
|||
param x; |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=x dorm=0.3; |
|||
@ -1,4 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" lambda=0 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -1,21 +0,0 @@ |
|||
toplevel "SYSTEM"; |
|||
"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS"; |
|||
"FDEP" fdep "TRIGGER" "P" "B"; |
|||
"TRIGGER" or "CS" "SS"; |
|||
"CPU" wsp "P" "B"; |
|||
"MOTOR" or "SWITCH" "MOTORS"; |
|||
"SWITCH" pand "MS" "MA"; |
|||
"MOTORS" csp "MA" "MB"; |
|||
"PUMPS" and "PUMP1" "PUMP2"; |
|||
"PUMP1" csp "PA" "PS"; |
|||
"PUMP2" csp "PB" "PS"; |
|||
"P" lambda=5.0e-5 dorm=0; |
|||
"B" lambda=5.0e-5 dorm=0.5; |
|||
"CS" lambda=2.0e-5 dorm=0; |
|||
"SS" lambda=2.0e-5 dorm=0; |
|||
"MS" lambda=1.0e-6 dorm=0; |
|||
"MA" lambda=1.0e-4 dorm=0; |
|||
"MB" lambda=1.0e-4 dorm=0; |
|||
"PA" lambda=1.0e-4 dorm=0; |
|||
"PB" lambda=1.0e-4 dorm=0; |
|||
"PS" lambda=1.0e-4 dorm=0; |
|||
@ -1,24 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit"; |
|||
|
|||
"CPUfdep" fdep "trigger" "P" "B"; |
|||
"trigger" or "CS" "SS"; |
|||
"CS" lambda=0.2 dorm=0; |
|||
"SS" lambda=0.2 dorm=0; |
|||
"CPUunit" wsp "P" "B"; |
|||
"P" lambda=0.5 dorm=0; |
|||
"B" lambda=0.5 dorm=0.5; |
|||
|
|||
"Motorunit" or "MP" "Motors"; |
|||
"MP" pand "MS" "MA"; |
|||
"Motors" csp "MA" "MB"; |
|||
"MS" lambda=0.01 dorm=0; |
|||
"MA" lambda=1 dorm=0; |
|||
"MB" lambda=1 dorm=0; |
|||
|
|||
"Pumpunit" and "PumpA" "PumpB"; |
|||
"PumpA" csp "PA" "PS"; |
|||
"PumpB" csp "PB" "PS"; |
|||
"PA" lambda=1 dorm=0; |
|||
"PB" lambda=1 dorm=0; |
|||
"PS" lambda=1 dorm=0; |
|||
@ -1,22 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "BUS" "CM"; |
|||
"CM" and "CM1" "CM2"; |
|||
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
|||
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
|||
"DISK1" wsp "D11" "D12"; |
|||
"DISK2" wsp "D21" "D22"; |
|||
"POWER1" or "P1" "PS"; |
|||
"POWER2" or "P2" "PS"; |
|||
"MEMORY1" wsp "M1" "M3"; |
|||
"MEMORY2" wsp "M2" "M3"; |
|||
"BUS" lambda=0.0002 dorm=0; |
|||
"P1" lambda=0.05 dorm=0; |
|||
"P2" lambda=0.05 dorm=0; |
|||
"PS" lambda=0.6 dorm=0; |
|||
"D11" lambda=8.0 dorm=0; |
|||
"D12" lambda=8.0 dorm=0.5; |
|||
"D21" lambda=8.0 dorm=0; |
|||
"D22" lambda=8.0 dorm=0.5; |
|||
"M1" lambda=0.003 dorm=0; |
|||
"M2" lambda=0.003 dorm=0; |
|||
"M3" lambda=0.003 dorm=0.5; |
|||
@ -1,41 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "BUS" "CM"; |
|||
"CM" and "CM1" "CM2" "CM3" "CM4"; |
|||
"CM1" or "DISK1" "POWER1" "MEMORY1"; |
|||
"CM2" or "DISK2" "POWER2" "MEMORY2"; |
|||
"CM3" or "DISK3" "POWER3" "MEMORY3"; |
|||
"CM4" or "DISK4" "POWER4" "MEMORY4"; |
|||
"DISK1" wsp "D11" "D12"; |
|||
"DISK2" wsp "D21" "D22"; |
|||
"DISK3" wsp "D31" "D32"; |
|||
"DISK4" wsp "D41" "D42"; |
|||
"POWER1" or "P1" "PS"; |
|||
"POWER2" or "P2" "PS"; |
|||
"POWER3" or "P3" "PS2"; |
|||
"POWER4" or "P4" "PS2"; |
|||
"MEMORY1" wsp "M1" "M3" "M4"; |
|||
"MEMORY2" wsp "M2" "M3" "M4"; |
|||
"MEMORY3" wsp "M31" "M3"; |
|||
"MEMORY4" wsp "M41" "M4"; |
|||
"BUS" lambda=0.0002 dorm=0; |
|||
"P1" lambda=0.05 dorm=0; |
|||
"P2" lambda=0.05 dorm=0; |
|||
"P3" lambda=0.05 dorm=0; |
|||
"P4" lambda=0.05 dorm=0; |
|||
"PS" lambda=0.6 dorm=0; |
|||
"PS2" lambda=0.6 dorm=0; |
|||
"D11" lambda=8.0 dorm=0; |
|||
"D12" lambda=8.0 dorm=0.5; |
|||
"D21" lambda=8.0 dorm=0; |
|||
"D22" lambda=8.0 dorm=0.5; |
|||
"D31" lambda=8.0 dorm=0; |
|||
"D32" lambda=8.0 dorm=0.5; |
|||
"D41" lambda=8.0 dorm=0; |
|||
"D42" lambda=8.0 dorm=0.5; |
|||
"M1" lambda=0.003 dorm=0; |
|||
"M2" lambda=0.003 dorm=0; |
|||
"M31" lambda=0.003 dorm=0; |
|||
"M41" lambda=0.003 dorm=0; |
|||
"M3" lambda=0.003 dorm=0.5; |
|||
"M4" lambda=0.003 dorm=0.5; |
|||
|
|||
@ -1,26 +0,0 @@ |
|||
toplevel "System"; |
|||
|
|||
"System" pand "A" "B"; |
|||
|
|||
"A" and "AA" "AB" "AC" "AD"; |
|||
|
|||
"B" pand "C" "D"; |
|||
|
|||
"C" and "CA" "CB" "CC" "CD"; |
|||
|
|||
"D" and "DA" "DB" "DC" "DD"; |
|||
|
|||
"AA" lambda=1 dorm=0; |
|||
"AB" lambda=1 dorm=0; |
|||
"AC" lambda=1 dorm=0; |
|||
"AD" lambda=1 dorm=0; |
|||
|
|||
"CA" lambda=1 dorm=0; |
|||
"CB" lambda=1 dorm=0; |
|||
"CC" lambda=1 dorm=0; |
|||
"CD" lambda=1 dorm=0; |
|||
|
|||
"DA" lambda=1 dorm=0; |
|||
"DB" lambda=1 dorm=0; |
|||
"DC" lambda=1 dorm=0; |
|||
"DD" lambda=1 dorm=0; |
|||
@ -1,16 +0,0 @@ |
|||
toplevel "DeathEgg"; |
|||
"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency"; |
|||
"DeathEggServer" or "CampusNET" "DES_Disks"; |
|||
"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2"; |
|||
"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2"; |
|||
"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4"; |
|||
"DeathEggProxy" lambda=0.01 dorm=0; |
|||
"DES_Disk_1" lambda=0.01 dorm=0; |
|||
"DES_Disk_2" lambda=0.01 dorm=0; |
|||
"DES_Disk_3" lambda=0.01 dorm=0; |
|||
"DES_Disk_4" lambda=0.01 dorm=0; |
|||
"CampusPowerDependency" fdep "CampusPower" "DeathEggServer"; |
|||
"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy"; |
|||
"CampusPower" lambda=0.01 dorm=0; |
|||
"CampusNET" lambda=0.01 dorm=0; |
|||
"ProxyPower" lambda=0.01 dorm=0; |
|||
@ -1,8 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "Power" "Machine"; |
|||
"Power" fdep "B_Power" "P" "B"; |
|||
"Machine" or "P" "B"; |
|||
|
|||
"B_Power" lambda=0.5 dorm=0; |
|||
"P" lambda=0.5 dorm=0; |
|||
"B" lambda=0.5 dorm=0.5; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"F" fdep "B" "C"; |
|||
"B" lambda=0.5 dorm=0; |
|||
"C" lambda=0.5 dorm=0; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "F"; |
|||
"F" fdep "B" "C"; |
|||
"B" lambda=0.4 dorm=0; |
|||
"C" lambda=0.8 dorm=0; |
|||
@ -1,129 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
|||
|
|||
"triadA" 2of3 "aA" "bA" "cA"; |
|||
"aA" csp "TAA" "TAS"; |
|||
"bA" csp "TAB" "TAS"; |
|||
"cA" csp "TAC" "TAS"; |
|||
|
|||
"triadB" 2of3 "aB" "bB" "cB"; |
|||
"aB" csp "TBA" "TBS"; |
|||
"bB" csp "TBB" "TBS"; |
|||
"cB" csp "TBC" "TBS"; |
|||
|
|||
"triadC" 2of3 "aC" "bC" "cC"; |
|||
"aC" csp "TCA" "TCS"; |
|||
"bC" csp "TCB" "TCS"; |
|||
"cC" csp "TCC" "TCS"; |
|||
|
|||
"triadD" 2of3 "aD" "bD" "cD"; |
|||
"aD" csp "TDA" "TDS"; |
|||
"bD" csp "TDB" "TDS"; |
|||
"cD" csp "TDC" "TDS"; |
|||
|
|||
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
|||
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
|||
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
|||
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
|||
|
|||
|
|||
"NEA" lambda=0.017 dorm=1; |
|||
"NEB" lambda=0.017 dorm=1; |
|||
"NEC" lambda=0.017 dorm=1; |
|||
"NED" lambda=0.017 dorm=1; |
|||
|
|||
"TAA" or "cpuAA" "memAA"; |
|||
"memAA" csp "memAA1" "memAA2"; |
|||
"cpuAA" lambda=0.11 dorm=0; |
|||
"memAA1" lambda=0.11 dorm=0; |
|||
"memAA2" lambda=0.11 dorm=0; |
|||
|
|||
"TAB" or "cpuAB" "memAB"; |
|||
"memAB" csp "memAB1" "memAB2"; |
|||
"cpuAB" lambda=0.11 dorm=0; |
|||
"memAB1" lambda=0.11 dorm=0; |
|||
"memAB2" lambda=0.11 dorm=0; |
|||
|
|||
"TAC" or "cpuAC" "memAC"; |
|||
"memAC" csp "memAC1" "memAC2"; |
|||
"cpuAC" lambda=0.11 dorm=0; |
|||
"memAC1" lambda=0.11 dorm=0; |
|||
"memAC2" lambda=0.11 dorm=0; |
|||
|
|||
"TAS" or "cpuAS" "memAS"; |
|||
"memAS" csp "memAS1" "memAS2"; |
|||
"cpuAS" lambda=0.11 dorm=0; |
|||
"memAS1" lambda=0.11 dorm=0; |
|||
"memAS2" lambda=0.11 dorm=0; |
|||
|
|||
"TBA" or "cpuBA" "memBA"; |
|||
"memBA" csp "memBA1" "memBA2"; |
|||
"cpuBA" lambda=0.11 dorm=0; |
|||
"memBA1" lambda=0.11 dorm=0; |
|||
"memBA2" lambda=0.11 dorm=0; |
|||
|
|||
"TBB" or "cpuBB" "memBB"; |
|||
"memBB" csp "memBB1" "memBB2"; |
|||
"cpuBB" lambda=0.11 dorm=0; |
|||
"memBB1" lambda=0.11 dorm=0; |
|||
"memBB2" lambda=0.11 dorm=0; |
|||
|
|||
"TBC" or "cpuBC" "memBC"; |
|||
"memBC" csp "memBC1" "memBC2"; |
|||
"cpuBC" lambda=0.11 dorm=0; |
|||
"memBC1" lambda=0.11 dorm=0; |
|||
"memBC2" lambda=0.11 dorm=0; |
|||
|
|||
"TBS" or "cpuBS" "memBS"; |
|||
"memBS" csp "memBS1" "memBS2"; |
|||
"cpuBS" lambda=0.11 dorm=0; |
|||
"memBS1" lambda=0.11 dorm=0; |
|||
"memBS2" lambda=0.11 dorm=0; |
|||
|
|||
"TCA" or "cpuCA" "memCA"; |
|||
"memCA" csp "memCA1" "memCA2"; |
|||
"cpuCA" lambda=0.11 dorm=0; |
|||
"memCA1" lambda=0.11 dorm=0; |
|||
"memCA2" lambda=0.11 dorm=0; |
|||
|
|||
"TCB" or "cpuCB" "memCB"; |
|||
"memCB" csp "memCB1" "memCB2"; |
|||
"cpuCB" lambda=0.11 dorm=0; |
|||
"memCB1" lambda=0.11 dorm=0; |
|||
"memCB2" lambda=0.11 dorm=0; |
|||
|
|||
"TCC" or "cpuCC" "memCC"; |
|||
"memCC" csp "memCC1" "memCC2"; |
|||
"cpuCC" lambda=0.11 dorm=0; |
|||
"memCC1" lambda=0.11 dorm=0; |
|||
"memCC2" lambda=0.11 dorm=0; |
|||
|
|||
"TCS" or "cpuCS" "memCS"; |
|||
"memCS" csp "memCS1" "memCS2"; |
|||
"cpuCS" lambda=0.11 dorm=0; |
|||
"memCS1" lambda=0.11 dorm=0; |
|||
"memCS2" lambda=0.11 dorm=0; |
|||
|
|||
"TDA" or "cpuDA" "memDA"; |
|||
"memDA" csp "memDA1" "memDA2"; |
|||
"cpuDA" lambda=0.11 dorm=0; |
|||
"memDA1" lambda=0.11 dorm=0; |
|||
"memDA2" lambda=0.11 dorm=0; |
|||
|
|||
"TDB" or "cpuDB" "memDB"; |
|||
"memDB" csp "memDB1" "memDB2"; |
|||
"cpuDB" lambda=0.11 dorm=0; |
|||
"memDB1" lambda=0.11 dorm=0; |
|||
"memDB2" lambda=0.11 dorm=0; |
|||
|
|||
"TDC" or "cpuDC" "memDC"; |
|||
"memDC" csp "memDC1" "memDC2"; |
|||
"cpuDC" lambda=0.11 dorm=0; |
|||
"memDC1" lambda=0.11 dorm=0; |
|||
"memDC2" lambda=0.11 dorm=0; |
|||
|
|||
"TDS" or "cpuDS" "memDS"; |
|||
"memDS" csp "memDS1" "memDS2"; |
|||
"cpuDS" lambda=0.11 dorm=0; |
|||
"memDS1" lambda=0.11 dorm=0; |
|||
"memDS2" lambda=0.11 dorm=0; |
|||
@ -1,63 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE"; |
|||
|
|||
"triadA" 3of4 "aA" "bA" "cA" "dA"; |
|||
"aA" csp "TAA" "TAS"; |
|||
"bA" csp "TAB" "TAS"; |
|||
"cA" csp "TAC" "TAS"; |
|||
"dA" csp "TAD" "TAS"; |
|||
|
|||
"triadB" 3of4 "aB" "bB" "cB" "dB"; |
|||
"aB" csp "TBA" "TBS"; |
|||
"bB" csp "TBB" "TBS"; |
|||
"cB" csp "TBC" "TBS"; |
|||
"dB" csp "TBD" "TBS"; |
|||
|
|||
"triadC" 3of4 "aC" "bC" "cC" "dC"; |
|||
"aC" csp "TCA" "TCS"; |
|||
"bC" csp "TCB" "TCS"; |
|||
"cC" csp "TCC" "TCS"; |
|||
"dC" csp "TCD" "TCS"; |
|||
|
|||
"triadD" 3of4 "aD" "bD" "cD" "dD"; |
|||
"aD" csp "TDA" "TDS"; |
|||
"bD" csp "TDB" "TDS"; |
|||
"cD" csp "TDC" "TDS"; |
|||
"dD" csp "TDD" "TDS"; |
|||
|
|||
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
|||
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
|||
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
|||
"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD"; |
|||
"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS"; |
|||
|
|||
|
|||
"NEA" lambda=0.017 dorm=1; |
|||
"NEB" lambda=0.017 dorm=1; |
|||
"NEC" lambda=0.017 dorm=1; |
|||
"NED" lambda=0.017 dorm=1; |
|||
"NEE" lambda=0.017 dorm=1; |
|||
|
|||
"TAA" lambda=0.11 dorm=0; |
|||
"TAB" lambda=0.11 dorm=0; |
|||
"TAC" lambda=0.11 dorm=0; |
|||
"TAD" lambda=0.11 dorm=0; |
|||
"TAS" lambda=0.11 dorm=0; |
|||
|
|||
"TBA" lambda=0.11 dorm=0; |
|||
"TBB" lambda=0.11 dorm=0; |
|||
"TBC" lambda=0.11 dorm=0; |
|||
"TBD" lambda=0.11 dorm=0; |
|||
"TBS" lambda=0.11 dorm=0; |
|||
|
|||
"TCA" lambda=0.11 dorm=0; |
|||
"TCB" lambda=0.11 dorm=0; |
|||
"TCC" lambda=0.11 dorm=0; |
|||
"TCD" lambda=0.11 dorm=0; |
|||
"TCS" lambda=0.11 dorm=0; |
|||
|
|||
"TDA" lambda=0.11 dorm=0; |
|||
"TDB" lambda=0.11 dorm=0; |
|||
"TDC" lambda=0.11 dorm=0; |
|||
"TDD" lambda=0.11 dorm=0; |
|||
"TDS" lambda=0.11 dorm=0; |
|||
@ -1,53 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD"; |
|||
|
|||
"triadA" 2of3 "aA" "bA" "cA"; |
|||
"aA" csp "TAA" "TAS"; |
|||
"bA" csp "TAB" "TAS"; |
|||
"cA" csp "TAC" "TAS"; |
|||
|
|||
"triadB" 2of3 "aB" "bB" "cB"; |
|||
"aB" csp "TBA" "TBS"; |
|||
"bB" csp "TBB" "TBS"; |
|||
"cB" csp "TBC" "TBS"; |
|||
|
|||
"triadC" 2of3 "aC" "bC" "cC"; |
|||
"aC" csp "TCA" "TCS"; |
|||
"bC" csp "TCB" "TCS"; |
|||
"cC" csp "TCC" "TCS"; |
|||
|
|||
"triadD" 2of3 "aD" "bD" "cD"; |
|||
"aD" csp "TDA" "TDS"; |
|||
"bD" csp "TDB" "TDS"; |
|||
"cD" csp "TDC" "TDS"; |
|||
|
|||
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA"; |
|||
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB"; |
|||
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC"; |
|||
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS"; |
|||
|
|||
|
|||
"NEA" lambda=0.017 dorm=1; |
|||
"NEB" lambda=0.017 dorm=1; |
|||
"NEC" lambda=0.017 dorm=1; |
|||
"NED" lambda=0.017 dorm=1; |
|||
|
|||
"TAA" lambda=0.11 dorm=0; |
|||
"TAB" lambda=0.11 dorm=0; |
|||
"TAC" lambda=0.11 dorm=0; |
|||
"TAS" lambda=0.11 dorm=0; |
|||
|
|||
"TBA" lambda=0.11 dorm=0; |
|||
"TBB" lambda=0.11 dorm=0; |
|||
"TBC" lambda=0.11 dorm=0; |
|||
"TBS" lambda=0.11 dorm=0; |
|||
|
|||
"TCA" lambda=0.11 dorm=0; |
|||
"TCB" lambda=0.11 dorm=0; |
|||
"TCC" lambda=0.11 dorm=0; |
|||
"TCS" lambda=0.11 dorm=0; |
|||
|
|||
"TDA" lambda=0.11 dorm=0; |
|||
"TDB" lambda=0.11 dorm=0; |
|||
"TDC" lambda=0.11 dorm=0; |
|||
"TDS" lambda=0.11 dorm=0; |
|||
@ -1,22 +0,0 @@ |
|||
toplevel "n12"; |
|||
"n12" or "n1" "n103" "n7"; |
|||
"n103" wsp "n106" "n14"; |
|||
"n7" and "n18" "n26"; |
|||
"n26" or "n28" "n19" "n23"; |
|||
"n19" wsp "n16" "n13"; |
|||
"n23" wsp "n0" "n17"; |
|||
"n18" or "n15" "n9" "n3"; |
|||
"n3" wsp "n2" "n17"; |
|||
"n9" wsp "n8" "n27"; |
|||
"n16" lambda=8.0 dorm=0.0; |
|||
"n0" lambda=0.003 dorm=0.0; |
|||
"n13" lambda=8.0 dorm=0.5; |
|||
"n2" lambda=0.003 dorm=0.0; |
|||
"n17" lambda=0.003 dorm=0.5; |
|||
"n15" lambda=0.05 dorm=0.0; |
|||
"n106" lambda=1.2 dorm=0.0; |
|||
"n14" lambda=0.6 dorm=0.0; |
|||
"n1" lambda=2.0E-4 dorm=0.0; |
|||
"n27" lambda=8.0 dorm=0.5; |
|||
"n8" lambda=8.0 dorm=0.0; |
|||
"n28" lambda=0.05 dorm=0.0; |
|||
@ -1,26 +0,0 @@ |
|||
toplevel "System"; |
|||
|
|||
"System" or "S" "N"; |
|||
|
|||
"N" lambda=2e-5 dorm=0; |
|||
|
|||
"S" and "CMA" "CMB"; |
|||
|
|||
"CMA" or "DiskA" "PA" "MemA"; |
|||
"DiskA" wsp "DAA" "DAB"; |
|||
"PA" lambda=500e-5 dorm=0; |
|||
"MemA" wsp "MA" "MC"; |
|||
"DAA" lambda=80000e-5 dorm=0.5; |
|||
"DAB" lambda=80000e-5 dorm=0.5; |
|||
"MA" lambda=30e-5 dorm=0; |
|||
|
|||
"CMB" or "DiskB" "PB" "MemB"; |
|||
"DiskB" wsp "DBA" "DBB"; |
|||
"PB" lambda=500e-5 dorm=0; |
|||
"MemB" wsp "MB" "MC"; |
|||
"DBA" lambda=80000e-5 dorm=0.5; |
|||
"DBB" lambda=80000e-5 dorm=0.5; |
|||
"MB" lambda=30e-5 dorm=0; |
|||
|
|||
"MC" lambda=30e-5 dorm=0.5; |
|||
|
|||
@ -1,19 +0,0 @@ |
|||
toplevel "System"; |
|||
"System" or "S" "N"; |
|||
"N" lambda=0.0000200000 dorm=0.0000000000; |
|||
"S" and "CMA" "CMB"; |
|||
"CMA" or "DiskA" "PA" "MemA"; |
|||
"DiskA" wsp "DAA" "DAB"; |
|||
"PA" lambda=0.0049999999 dorm=0.0000000000; |
|||
"MemA" wsp "MA" "MC"; |
|||
"DAA" lambda=0.8000000119 dorm=0.5000000000; |
|||
"DAB" lambda=0.8000000119 dorm=0.5000000000; |
|||
"MA" lambda=0.0003000000 dorm=0.0000000000; |
|||
"CMB" or "DiskB" "PB" "MemB"; |
|||
"DiskB" wsp "DBA" "DBB"; |
|||
"PB" lambda=0.0049999999 dorm=0.0000000000; |
|||
"MemB" wsp "MB" "MC"; |
|||
"DBA" lambda=0.8000000119 dorm=0.5000000000; |
|||
"DBB" lambda=0.8000000119 dorm=0.5000000000; |
|||
"MB" lambda=0.0003000000 dorm=0.0000000000; |
|||
"MC" lambda=0.0003000000 dorm=0.5000000000; |
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" or "D" "E"; |
|||
"C" or "F" "E"; |
|||
"D" lambda=0.1 dorm=0; |
|||
"E" lambda=0.2 dorm=0; |
|||
"F" lambda=0.3 dorm=0; |
|||
@ -1,8 +0,0 @@ |
|||
param x; |
|||
param y; |
|||
toplevel "A"; |
|||
"A" or "B" "Z"; |
|||
"B" pand "D" "S"; |
|||
"Z" lambda=y dorm=0; |
|||
"D" lambda=100 dorm=0; |
|||
"S" lambda=100*x dorm=0; |
|||
@ -1,4 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -1,4 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" pand "B" "C"; |
|||
"B" lambda=0.4 dorm=0.3; |
|||
"C" lambda=0.2 dorm=0.3; |
|||
@ -1,6 +0,0 @@ |
|||
param x; |
|||
param y; |
|||
toplevel "A"; |
|||
"A" pand "B" "C"; |
|||
"B" lambda=x dorm=0.3; |
|||
"C" lambda=y dorm=0.3; |
|||
@ -1,12 +0,0 @@ |
|||
// From Junges2015 |
|||
// Example 3.19 |
|||
|
|||
toplevel "SF"; |
|||
"SF" or "A" "B" "PDEP"; |
|||
"A" pand "S" "MA"; |
|||
"B" and "MA" "MB"; |
|||
"PDEP" pdep=0.2 "MA" "S"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"MA" lambda=0.5 dorm=0; |
|||
"MB" lambda=0.5 dorm=0; |
|||
@ -1,9 +0,0 @@ |
|||
toplevel "SF"; |
|||
"SF" or "A" "B" "PDEP"; |
|||
"A" pand "S" "MA"; |
|||
"B" and "MA" "MB"; |
|||
"PDEP" pdep=0.2 "MA" "S" "MB"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"MA" lambda=0.5 dorm=0; |
|||
"MB" lambda=0.5 dorm=0; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "F"; |
|||
"F" pdep=0.3 "B" "C"; |
|||
"B" lambda=0.4 dorm=0; |
|||
"C" lambda=0.8 dorm=0; |
|||
@ -1,7 +0,0 @@ |
|||
toplevel "SF"; |
|||
"SF" pand "S" "A" "B"; |
|||
"PDEP" pdep=0.2 "S" "A" "B"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"A" lambda=0.5 dorm=0; |
|||
"B" lambda=0.5 dorm=0; |
|||
@ -1,11 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'"; |
|||
"B" and "C" "D" "PDEP"; |
|||
"B'" and "C'" "D'" "PDEP'"; |
|||
"PDEP" pdep=0.6 "C" "D"; |
|||
"PDEP'" pdep=0.6 "C'" "D'"; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=0.5 dorm=0; |
|||
"C'" lambda=0.5 dorm=0; |
|||
"D'" lambda=0.5 dorm=0; |
|||
|
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" por "B" "C" "D"; |
|||
"B" lambda=0.4 dorm=0.0; |
|||
"C" lambda=0.2 dorm=0.0; |
|||
"D" lambda=0.2 dorm=0.0; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"X" seq "B" "C" |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -1,6 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "D"; |
|||
"X" seq "B" "C" "D"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
"D" lambda=0.5 dorm=0.3; |
|||
@ -1,6 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "C" "D"; |
|||
"X" seq "B" "C" "D"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
"D" lambda=0.5 dorm=0.3; |
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "T1" "B3"; |
|||
"T1" or "B1" "B2"; |
|||
"X" seq "B1" "B2" "B3"; |
|||
"B1" lambda=0.5 dorm=0.3; |
|||
"B2" lambda=0.5 dorm=0.3; |
|||
"B3" lambda=0.5 dorm=0.3; |
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "T1" "T2"; |
|||
"T1" pand "B1" "B2"; |
|||
"T2" pand "B3" "B4"; |
|||
"X" seq "B4" "B3"; |
|||
"B1" lambda=0.7 dorm=0.3; |
|||
"B2" lambda=0.5 dorm=0.3; |
|||
"B3" lambda=0.5 dorm=0.3; |
|||
"B4" lambda=0.7 dorm=0.3; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "M"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" wsp "I" "J"; |
|||
"C" wsp "M" "J"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,10 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C" "D"; |
|||
"B" wsp "I" "M"; |
|||
"C" wsp "J" "M"; |
|||
"D" wsp "K" "M"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" wsp "I" "J" "K"; |
|||
"C" wsp "M" "J"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "B"; |
|||
"B" or "C" "J"; |
|||
"C" or "K" "L"; |
|||
"I" lambda=0.5 dorm=0; |
|||
"J" lambda=0.5 dorm=0; |
|||
"K" lambda=0.5 dorm=0; |
|||
"L" lambda=0.5 dorm=0; |
|||
|
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "I" "B"; |
|||
"B" wsp "J" "M"; |
|||
"I" lambda=0.5 dorm=0.5; |
|||
"J" lambda=0.5 dorm=0.5; |
|||
"M" lambda=0.5 dorm=0.5; |
|||
|
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" wsp "K" "J" "I"; |
|||
"I" lambda=0.5 dorm=0.5; |
|||
"J" lambda=1 dorm=0.5; |
|||
"K" lambda=0.5 dorm=0.5; |
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "B"; |
|||
"B" wsp "J" "K"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "M"; |
|||
"I" lambda=0.5 dorm=0.0; |
|||
"M" lambda=0.5 dorm=0.0; |
|||
|
|||
@ -1,9 +0,0 @@ |
|||
param x; |
|||
param y; |
|||
toplevel "SF"; |
|||
"SF" or "FW" "BW"; |
|||
"FW" wsp "W1" "WS"; |
|||
"BW" wsp "W2" "WS"; |
|||
"W1" lambda=x dorm=0; |
|||
"W2" lambda=1 dorm=0; |
|||
"WS" lambda=y dorm=0; |
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" wsp "I" "J"; |
|||
"C" wsp "K" "L"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
"L" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'"; |
|||
"B" and "C" "D"; |
|||
"B'" and "C'" "D'"; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=0.5 dorm=0; |
|||
"C'" lambda=0.5 dorm=0; |
|||
"D'" lambda=0.5 dorm=0; |
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'"; |
|||
"B" and "C" "D"; |
|||
"B'" and "C'" "D'"; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=2 dorm=0; |
|||
"C'" lambda=0.5 dorm=0; |
|||
"D'" lambda=2 dorm=0; |
|||
@ -1,12 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'" "B''"; |
|||
"B" and "C" "D"; |
|||
"B'" and "C'" "D'"; |
|||
"B''" and "C''" "D''"; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=0.5 dorm=0; |
|||
"C'" lambda=0.5 dorm=0; |
|||
"D'" lambda=0.5 dorm=0; |
|||
"C''" lambda=0.5 dorm=0; |
|||
"D''" lambda=0.5 dorm=0; |
|||
|
|||
@ -1,12 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'" "C" "C'"; |
|||
"B" and "D" "E"; |
|||
"B'" and "D'" "E'"; |
|||
"C" or "F"; |
|||
"C'" or "F'"; |
|||
"D" lambda=0.5 dorm=0; |
|||
"E" lambda=0.5 dorm=0; |
|||
"D'" lambda=0.5 dorm=0; |
|||
"E'" lambda=0.5 dorm=0; |
|||
"F" lambda=0.5 dorm=0; |
|||
"F'" lambda=0.5 dorm=0; |
|||
@ -1,21 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "BA" "BB" "BC" "BD" "BE" "BF"; |
|||
"BA" and "CA" "DA"; |
|||
"BB" and "CB" "DB"; |
|||
"BC" and "CC" "DC"; |
|||
"BD" and "CD" "DD"; |
|||
"BE" and "CE" "DE"; |
|||
"BF" and "CF" "DF"; |
|||
"CA" lambda=0.5 dorm=0; |
|||
"DA" lambda=0.5 dorm=0; |
|||
"CB" lambda=0.5 dorm=0; |
|||
"DB" lambda=0.5 dorm=0; |
|||
"CC" lambda=0.5 dorm=0; |
|||
"DC" lambda=0.5 dorm=0; |
|||
"CD" lambda=0.5 dorm=0; |
|||
"DD" lambda=0.5 dorm=0; |
|||
"CE" lambda=0.5 dorm=0; |
|||
"DE" lambda=0.5 dorm=0; |
|||
"CF" lambda=0.5 dorm=0; |
|||
"DF" lambda=0.5 dorm=0; |
|||
|
|||
@ -1,10 +0,0 @@ |
|||
param x; |
|||
param y; |
|||
toplevel "A"; |
|||
"A" and "B" "B'"; |
|||
"B" and "C" "D"; |
|||
"B'" and "C'" "D'"; |
|||
"C" lambda=x dorm=0; |
|||
"D" lambda=y dorm=0; |
|||
"C'" lambda=x dorm=0; |
|||
"D'" lambda=y dorm=0; |
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "B'"; |
|||
"B" wsp "C" "D"; |
|||
"B'" wsp "C'" "D"; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=0.5 dorm=0; |
|||
"C'" lambda=0.5 dorm=0; |
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" and "BE1" "BE2"; |
|||
"C" and "BE3" "BE4"; |
|||
"BE1" lambda=0.5 dorm=0.3; |
|||
"BE2" lambda=0.5 dorm=0.3; |
|||
"BE3" lambda=0.5 dorm=0.3; |
|||
"BE4" lambda=0.5 dorm=0.3; |
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" and "BE1" "BE2"; |
|||
"C" and "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=0.3; |
|||
"BE2" lambda=0.5 dorm=0.3; |
|||
"BE3" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -1,6 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "BE1" "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" and "BE1" "BE2" "BE3" "BE4"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
"BE4" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" or "BE1" "BE2"; |
|||
"C" or "BE3" "BE4"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
"BE4" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" or "BE1" "BE2"; |
|||
"C" or "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,6 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "BE1" "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" or "BE1" "BE2" "BE3" "BE4"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
"BE4" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,9 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" pand "B" "BE4"; |
|||
"B" pand "C" "BE3"; |
|||
"C" pand "BE1" "BE2"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
"BE4" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,8 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" pand "B" "C"; |
|||
"B" pand "BE1" "BE2"; |
|||
"C" pand "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,6 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" pand "BE1" "BE2" "BE3"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,7 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" pand "BE1" "BE2" "BE3" "BE4"; |
|||
"BE1" lambda=0.5 dorm=3; |
|||
"BE2" lambda=0.5 dorm=3; |
|||
"BE3" lambda=0.5 dorm=3; |
|||
"BE4" lambda=0.5 dorm=3; |
|||
|
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" 1of3 "B" "C" "D"; |
|||
"B" lambda=0.1 dorm=0; |
|||
"C" lambda=0.2 dorm=0; |
|||
"D" lambda=0.3 dorm=0; |
|||
@ -1,5 +0,0 @@ |
|||
toplevel "A"; |
|||
"A" 1of3 "B" "C" "D"; |
|||
"B" lambda=0.3 dorm=0; |
|||
"C" lambda=0.4 dorm=0; |
|||
"D" lambda=1 dorm=0; |
|||
@ -1,136 +0,0 @@ |
|||
// bounded retransmission protocol [D'AJJL01] |
|||
// gxn/dxp 23/05/2001 |
|||
|
|||
dtmc |
|||
|
|||
// number of chunks |
|||
const int N; |
|||
// maximum number of retransmissions |
|||
const int MAX; |
|||
|
|||
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; |
|||
@ -1,139 +0,0 @@ |
|||
// bounded retransmission protocol [D'AJJL01] |
|||
// gxn/dxp 23/05/2001 |
|||
|
|||
dtmc |
|||
|
|||
|
|||
// reliability of channels |
|||
const double pL; |
|||
const double pK; |
|||
|
|||
|
|||
// 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 |
|||
|
|||
// 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; |
|||
@ -1,3 +0,0 @@ |
|||
P=? [ F observe0Greater1 ] |
|||
P=? [ F observeIGreater1 ] |
|||
P=? [ F observeOnlyTrueSender ] |
|||
@ -1,19 +0,0 @@ |
|||
// 5/5 |
|||
P=? [ F "observe0Greater1" ] // 0.3328777473921436 |
|||
P=? [ F "observeIGreater1" ] // 0.15221847380560186 |
|||
P=? [ F "observeOnlyTrueSender" ] // 0.3215351607995943 |
|||
|
|||
// 10/5 |
|||
P=? [ F "observe0Greater1" ] // 0.26345583706046355 |
|||
P=? [ F "observeIGreater1" ] // 0.09236405558901994 |
|||
P=? [ F "observeOnlyTrueSender" ] // 0.25849872034453947 |
|||
|
|||
// 15/5 |
|||
P=? [ F "observe0Greater1" ] // 0.2408422942249347 |
|||
P=? [ F "observeIGreater1" ] // 0.0655686905854717 |
|||
P=? [ F "observeOnlyTrueSender" ] // 0.2377298605519743 |
|||
|
|||
// 20/5 |
|||
P=? [ F "observe0Greater1" ] // 0.22967858575985317 |
|||
P=? [ F "observeIGreater1" ] // 0.05073192927314383 |
|||
P=? [ F "observeOnlyTrueSender" ] // 0.22742031678667812 |
|||
@ -1,80 +0,0 @@ |
|||
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 = 10; |
|||
|
|||
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; |
|||
|
|||
observe5: [0..TotalRuns] init 0; |
|||
|
|||
observe6: [0..TotalRuns] init 0; |
|||
|
|||
observe7: [0..TotalRuns] init 0; |
|||
|
|||
observe8: [0..TotalRuns] init 0; |
|||
|
|||
observe9: [0..TotalRuns] init 0; |
|||
|
|||
// the last seen crowd member |
|||
lastSeen: [0..CrowdSize - 1] init 0; |
|||
|
|||
// get the protocol started |
|||
[] phase=0 & runCount<TotalRuns -> (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/10 : (lastSeen'=0) & (phase'=3) + 1/10 : (lastSeen'=1) & (phase'=3) + 1/10 : (lastSeen'=2) & (phase'=3) + 1/10 : (lastSeen'=3) & (phase'=3) + 1/10 : (lastSeen'=4) & (phase'=3) + 1/10 : (lastSeen'=5) & (phase'=3) + 1/10 : (lastSeen'=6) & (phase'=3) + 1/10 : (lastSeen'=7) & (phase'=3) + 1/10 : (lastSeen'=8) & (phase'=3) + 1/10 : (lastSeen'=9) & (phase'=3); |
|||
|
|||
// if the current member is a bad member, record the most recently seen index |
|||
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+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 -> (phase'=0); |
|||
|
|||
endmodule |
|||
|
|||
label "observe0Greater1" = observe0 > 1; |
|||
label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1; |
|||
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1; |
|||
@ -1,95 +0,0 @@ |
|||
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 = 15; |
|||
|
|||
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; |
|||
|
|||
observe5: [0..TotalRuns] init 0; |
|||
|
|||
observe6: [0..TotalRuns] init 0; |
|||
|
|||
observe7: [0..TotalRuns] init 0; |
|||
|
|||
observe8: [0..TotalRuns] init 0; |
|||
|
|||
observe9: [0..TotalRuns] init 0; |
|||
|
|||
observe10: [0..TotalRuns] init 0; |
|||
|
|||
observe11: [0..TotalRuns] init 0; |
|||
|
|||
observe12: [0..TotalRuns] init 0; |
|||
|
|||
observe13: [0..TotalRuns] init 0; |
|||
|
|||
observe14: [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/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (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); |
|||
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1: (observe10'=observe10+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1: (observe11'=observe11+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1: (observe12'=observe12+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1: (observe13'=observe13+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1: (observe14'=observe14+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 "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1; |
|||
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; |
|||
@ -1,111 +0,0 @@ |
|||
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 = 20; |
|||
|
|||
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; |
|||
|
|||
observe5: [0..TotalRuns] init 0; |
|||
|
|||
observe6: [0..TotalRuns] init 0; |
|||
|
|||
observe7: [0..TotalRuns] init 0; |
|||
|
|||
observe8: [0..TotalRuns] init 0; |
|||
|
|||
observe9: [0..TotalRuns] init 0; |
|||
|
|||
observe10: [0..TotalRuns] init 0; |
|||
|
|||
observe11: [0..TotalRuns] init 0; |
|||
|
|||
observe12: [0..TotalRuns] init 0; |
|||
|
|||
observe13: [0..TotalRuns] init 0; |
|||
|
|||
observe14: [0..TotalRuns] init 0; |
|||
|
|||
observe15: [0..TotalRuns] init 0; |
|||
|
|||
observe16: [0..TotalRuns] init 0; |
|||
|
|||
observe17: [0..TotalRuns] init 0; |
|||
|
|||
observe18: [0..TotalRuns] init 0; |
|||
|
|||
observe19: [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/20 : (lastSeen'=0) & (phase'=3) + 1/20 : (lastSeen'=1) & (phase'=3) + 1/20 : (lastSeen'=2) & (phase'=3) + 1/20 : (lastSeen'=3) & (phase'=3) + 1/20 : (lastSeen'=4) & (phase'=3) + 1/20 : (lastSeen'=5) & (phase'=3) + 1/20 : (lastSeen'=6) & (phase'=3) + 1/20 : (lastSeen'=7) & (phase'=3) + 1/20 : (lastSeen'=8) & (phase'=3) + 1/20 : (lastSeen'=9) & (phase'=3) + 1/20 : (lastSeen'=10) & (phase'=3) + 1/20 : (lastSeen'=11) & (phase'=3) + 1/20 : (lastSeen'=12) & (phase'=3) + 1/20 : (lastSeen'=13) & (phase'=3) + 1/20 : (lastSeen'=14) & (phase'=3) + 1/20 : (lastSeen'=15) & (phase'=3) + 1/20 : (lastSeen'=16) & (phase'=3) + 1/20 : (lastSeen'=17) & (phase'=3) + 1/20 : (lastSeen'=18) & (phase'=3) + 1/20 : (lastSeen'=19) & (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); |
|||
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1:(observe5'=observe5+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1:(observe6'=observe6+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1:(observe7'=observe7+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1:(observe8'=observe8+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1:(observe9'=observe9+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1:(observe10'=observe10+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1:(observe11'=observe11+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1:(observe12'=observe12+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1:(observe13'=observe13+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1:(observe14'=observe14+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> 1:(observe15'=observe15+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> 1:(observe16'=observe16+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> 1:(observe17'=observe17+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> 1:(observe18'=observe18+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> 1:(observe19'=observe19+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 "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1; |
|||
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1; |
|||
|
|||
@ -1,4 +0,0 @@ |
|||
P=? [ F one ] |
|||
P=? [ F two ] |
|||
P=? [ F three ] |
|||
R=? [ F done ] |
|||
@ -1,31 +0,0 @@ |
|||
// 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; |
|||
@ -1,4 +0,0 @@ |
|||
P=? [ F "one" ] // 0.16666650772094727 |
|||
P=? [ F "two" ] // 0.16666650772094727 |
|||
P=? [ F "three" ] // 0.16666650772094727 |
|||
R=? [ F "done" ] // 3.6666650772094727 |
|||
@ -1,76 +0,0 @@ |
|||
// 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; // number of inputs in each bundle |
|||
const int K; // 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; |
|||
@ -1,22 +0,0 @@ |
|||
// A simple model using synchronization |
|||
dtmc |
|||
|
|||
module generator |
|||
|
|||
s : [0..2] init 0; |
|||
|
|||
[] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0); |
|||
[yield] s=1 -> 1 : (s'=2); |
|||
[] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=2); |
|||
|
|||
endmodule |
|||
|
|||
module consumer |
|||
|
|||
t : [0..2] init 0; |
|||
|
|||
[] t=0 -> 0.8 : (t'=1) + 0.2 : (t'=0); |
|||
[yield] t=1 -> 1 : (t'=2); |
|||
[] t=2 -> 0.2 : (t'=0) + 0.8 : (t'=2); |
|||
|
|||
endmodule |
|||
@ -1,4 +0,0 @@ |
|||
P=? [ F elected ] |
|||
// P=? [ F<=(4*(N+1)) elected ] |
|||
P=? [ F<=28 elected ] |
|||
R=? [ F elected ] |
|||
@ -1,14 +0,0 @@ |
|||
// 3/5 |
|||
P=? [ F "elected" ] // 1.0 |
|||
P=? [ F<=(4*(N+1)) "elected" ] // 0.999997440000001 |
|||
R=? [ F "elected" ] // 1.0416666623999995 |
|||
|
|||
// 4/8 |
|||
P=? [ F "elected" ] // 1.0 |
|||
P=? [ F<=(4*(N+1)) "elected" ] // 0.9999965911265463 |
|||
R=? [ F "elected" ] // 1.0448979526072435 |
|||
|
|||
// 5/8 |
|||
P=? [ F "elected" ] // 1.0 |
|||
P=? [ F<=(4*(N+1)) "elected" ] // 0.9999999097195733 |
|||
R=? [ F "elected" ] // 1.0176397499602707 |
|||
@ -1,89 +0,0 @@ |
|||
// synchronous leader election protocol (itai & Rodeh) |
|||
// dxp/gxn 25/01/01 |
|||
|
|||
dtmc |
|||
|
|||
// CONSTANTS |
|||
const int N = 4; // number of processes |
|||
const int K = 8; // 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 -> (c'=c+1); |
|||
// finished reading |
|||
[read] c=N-1 -> (c'=c); |
|||
//decide |
|||
[done] u1|u2|u3|u4 -> (c'=c); |
|||
// pick again reset counter |
|||
[retry] !(u1|u2|u3|u4) -> (c'=1); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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) |
|||
+ 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); |
|||
// read |
|||
[read] s1=1 & u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0); |
|||
// read and move to decide |
|||
[read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
|||
[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); |
|||
// deciding |
|||
// done |
|||
[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
//retry |
|||
[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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=v4 ] endmodule |
|||
module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v1 ] endmodule |
|||
|
|||
// expected number of rounds |
|||
rewards "num_rounds" |
|||
[pick] true : 1; |
|||
endrewards |
|||
|
|||
// labels |
|||
label "elected" = s1=3&s2=3&s3=3&s4=3; |
|||
|
|||
@ -1,90 +0,0 @@ |
|||
// synchronous leader election protocol (itai & Rodeh) |
|||
// dxp/gxn 25/01/01 |
|||
|
|||
dtmc |
|||
|
|||
// CONSTANTS |
|||
const int N = 5; // number of processes |
|||
const int K = 8; // 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 -> (c'=c+1); |
|||
// finished reading |
|||
[read] c=N-1 -> (c'=c); |
|||
//decide |
|||
[done] u1|u2|u3|u4|u5 -> (c'=c); |
|||
// pick again reset counter |
|||
[retry] !(u1|u2|u3|u4|u5) -> (c'=1); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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) |
|||
+ 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); |
|||
// read |
|||
[read] s1=1 & u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0); |
|||
// read and move to decide |
|||
[read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
|||
[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); |
|||
// deciding |
|||
// done |
|||
[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
//retry |
|||
[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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=v4 ] endmodule |
|||
module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule |
|||
module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule |
|||
|
|||
// expected number of rounds |
|||
rewards "num_rounds" |
|||
[pick] true : 1; |
|||
endrewards |
|||
|
|||
// labels |
|||
label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; |
|||
|
|||
@ -1,91 +0,0 @@ |
|||
// synchronous leader election protocol (itai & Rodeh) |
|||
// dxp/gxn 25/01/01 |
|||
|
|||
dtmc |
|||
|
|||
// CONSTANTS |
|||
const int N = 6; // number of processes |
|||
const int K = 8; // 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 -> (c'=c+1); |
|||
// finished reading |
|||
[read] c=N-1 -> (c'=c); |
|||
//decide |
|||
[done] u1|u2|u3|u4|u5|u6 -> (c'=c); |
|||
// pick again reset counter |
|||
[retry] !(u1|u2|u3|u4|u5|u6) -> (c'=1); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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) |
|||
+ 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); |
|||
// read |
|||
[read] s1=1 & u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0); |
|||
// read and move to decide |
|||
[read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
|||
[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); |
|||
// deciding |
|||
// done |
|||
[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
//retry |
|||
[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> (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=v4 ] endmodule |
|||
module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule |
|||
module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v6 ] endmodule |
|||
module process6 = process1 [ s1=s6,p1=p6,v1=v6,u1=u6,v2=v1 ] endmodule |
|||
|
|||
// expected number of rounds |
|||
rewards "num_rounds" |
|||
[pick] true : 1; |
|||
endrewards |
|||
|
|||
// labels |
|||
label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3&s6=3; |
|||
|
|||
@ -1 +0,0 @@ |
|||
LRA=? [ "a" ] |
|||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue