probabilistic

//Probability a mix node is bad    
rate badP = 0.7;
rate goodP = 0.3;

const onionLength = 20; //number of hops between source and dest
const userCount = 10;

module entropy

launch:  bool init true;
new:  bool init false;
chosenBad:  bool init true;
done:  bool init false;
bad:  bool init false;
good: bool init false;
end: bool init false;
runCount: [0..onionLength] init onionLength;
state: [1..userCount] init 1;

[] launch -> (launch'=false) & (new'=true);

[] (new & (runCount > 0)) -> (runCount'=runCount - 1) & (new'=false)
    & (chosenBad'=false);

[] (!chosenBad) ->
  goodP: (good'=true) & (chosenBad'=true) +
  badP:  (bad'=true) & (chosenBad'=true);

[] bad & !end -> (end'=true);

[] (good & !end & (userCount = 1)) ->
    1.0: (state'=1) & (end'=true);

[] (good & !end & (userCount = 2)) ->
    0.5: (state'=1) & (end'=true) +
    0.5: (state'=2) & (end'=true);

[] (good & !end & (userCount = 3)) -> 
    0.333: (state'=1) & (end'=true) +
    0.333: (state'=2) & (end'=true) +
    0.334: (state'=3) & (end'=true);

[] (good & !end & (userCount = 5)) -> 
    0.2: (state'=1) & (end'=true) +
    0.2: (state'=2) & (end'=true) +
    0.2: (state'=3) & (end'=true) +
    0.2: (state'=4) & (end'=true) +
    0.2: (state'=5) & (end'=true);

[] (good & !end & (userCount = 10)) -> 
    0.1: (state'=1) & (end'=true) +
    0.1: (state'=2) & (end'=true) +
    0.1: (state'=3) & (end'=true) +
    0.1: (state'=4) & (end'=true) +
    0.1: (state'=5) & (end'=true) +
    0.1: (state'=6) & (end'=true) +
    0.1: (state'=7) & (end'=true) +
    0.1: (state'=8) & (end'=true) +
    0.1: (state'=9) & (end'=true) +
    0.1: (state'=10) & (end'=true);


[] (good & !end & (userCount = 20)) -> 
    0.05: (state'=1) & (end'=true) +
    0.05: (state'=2) & (end'=true) +
    0.05: (state'=3) & (end'=true) +
    0.05: (state'=4) & (end'=true) +
    0.05: (state'=5) & (end'=true) +
    0.05: (state'=6) & (end'=true) +
    0.05: (state'=7) & (end'=true) +
    0.05: (state'=8) & (end'=true) +
    0.05: (state'=9) & (end'=true) +
    0.05: (state'=10) & (end'=true) +
    0.05: (state'=11) & (end'=true) +
    0.05: (state'=12) & (end'=true) +
    0.05: (state'=13) & (end'=true) +
    0.05: (state'=14) & (end'=true) +
    0.05: (state'=15) & (end'=true) +
    0.05: (state'=16) & (end'=true) +
    0.05: (state'=17) & (end'=true) +
    0.05: (state'=18) & (end'=true) +
    0.05: (state'=19) & (end'=true) +
    0.05: (state'=20) & (end'=true);


[] end & (runCount > 0) -> (bad'=false) & (good'=false) & (new'= true)
 & (end'=false);

[] end & (runCount = 0) -> (end'=false) & (bad'=false) & (good'=false) 
& (done'=true);

[] done -> done'=true;

endmodule