Commit 31a3707d authored by Thom Badings's avatar Thom Badings
Browse files

Updated drone model

parent f0d20414
......@@ -40,9 +40,9 @@ python3 samplingprism.py --model-file nand/nand_10_5.pm --property-file nand/nan
### NAND (25,5)
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction geq --num_samples '(100,1000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.206 --outfile nand_25-5_sat_output.txt
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.206 --outfile nand_25-5_sat_output.txt
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction leq --num_samples '(100,1000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.744 --outfile nand_25-5_unsat_output.txt
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.744 --outfile nand_25-5_unsat_output.txt
### CONSENSUS (2,2)
......@@ -56,6 +56,18 @@ python3 samplingprism.py --model-file consensus/coin4.pm --property-file consens
python3 samplingprism.py --model-file consensus/coin4.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction leq --num_samples '(100,1000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.888 --outfile consensus_4-2_unsat_output.txt
### DRONE
### DRONE
## Uniform
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism.py --model-file drone/drone_par.nm --property-file drone/drone.prctl --threshold 0.9 --bisimulation none --direction geq --num_samples '1000' --num_iter 1 --beta '0.999999' --outfile drone_output.txt
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
## Wind in positive y direction
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
## Wind in negative x direction
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
// CROWDS [Reiter,Rubin]
// Vitaly Shmatikov, 2002
// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de)
// note:
// Change everything marked CWDSIZ when changing the size of the crowd
// Change everything marked CWDMAX when increasing max size of the crowd
dtmc
// Model parameters
const double PF; // forwarding probability
const double badC; // probability that member is untrustworthy
// Probability of forwarding
// const double PF = 0.8;
// const double notPF = 0.2; // must be 1-PF
// Probability that a crowd member is bad
// const double badC = 0.1;
// const double badC = 0.091;
// const double badC = 0.167;
// const double goodC = 0.909; // must be 1-badC
// const double goodC = 0.833; // must be 1-badC
const int CrowdSize = 15; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 7; // Total number of protocol runs to analyze
const int MaxGood=20; // CWDMAX: maximum number of good crowd members
// Process definitions
module crowds
// Auxiliary variables
launch: bool init true; // Start modeling?
newInstance: bool init false; // Initialize a new protocol instance?
runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances
start: bool init false; // Start the protocol?
run: bool init false; // Run the protocol?
lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg
good: bool init false; // Crowd member is good?
bad: bool init false; // ... bad?
recordLast: bool init false; // Record last seen crowd member?
badObserve: bool init false; // Bad members observes who sent msg?
deliver: bool init false; // Deliver message to destination?
done: bool init false; // Protocol instance finished?
// Counters for attackers' observations
// CWDMAX: 1 counter per each good crowd member
observe0: [0..TotalRuns];
observe1: [0..TotalRuns];
observe2: [0..TotalRuns];
observe3: [0..TotalRuns];
observe4: [0..TotalRuns];
observe5: [0..TotalRuns];
observe6: [0..TotalRuns];
observe7: [0..TotalRuns];
observe8: [0..TotalRuns];
observe9: [0..TotalRuns];
observe10: [0..TotalRuns];
observe11: [0..TotalRuns];
observe12: [0..TotalRuns];
observe13: [0..TotalRuns];
observe14: [0..TotalRuns];
observe15: [0..TotalRuns];
observe16: [0..TotalRuns];
observe17: [0..TotalRuns];
observe18: [0..TotalRuns];
observe19: [0..TotalRuns];
[] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false);
// Set up a newInstance protocol instance
[] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true);
// SENDER
// Start the protocol
[] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false);
// CROWD MEMBERS
// Good or bad crowd member?
[] !good & !bad & !deliver & run ->
1-badC : (good'=true) & (recordLast'=true) & (run'=false) +
badC : (bad'=true) & (badObserve'=true) & (run'=false);
// GOOD MEMBERS
// Forward with probability PF, else deliver
[] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true);
// Record the last crowd member who touched the msg;
// all good members may appear with equal probability
// Note: This is backward. In the real protocol, each honest
// forwarder randomly chooses the next forwarder.
// Here, the identity of an honest forwarder is randomly
// chosen *after* it has forwarded the message.
[] recordLast & CrowdSize=2 ->
1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=3 ->
1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=4 ->
1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=5 ->
1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=10 ->
1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=15 ->
1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=20 ->
1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true);
// BAD MEMBERS
// Remember from whom the message was received and deliver
// CWDMAX: 1 rule per each good crowd member
[] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
// RECIPIENT
// Delivery to destination
[] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false);
// Start a newInstance instance
[] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood);
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1>1|observe2>1;
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1;
......@@ -4,35 +4,35 @@ import numpy as np
template_header = """
mdp
const int MAXX = 10;
const int MAXY = 10;
const int MAXZ = 10;
const int MAXX = 15;
const int MAXY = 15;
const int MAXZ = 15;
formula valid = (1 < x & x < MAXX-1 & 1 < y & y < MAXY-1 & 1 < z & z < MAXZ-1) & ok=1;
formula attarget = x > MAXX - 3;
formula attarget2 = x > MAXX - 1 & y > MAXY - 2 & z > MAXZ - 3;
formula attarget2 = x > MAXX - 3;
formula attarget = x <= 3 & y >= MAXY - 3 & z >= MAXZ - 3;
formula crash = ((xarea4 | xarea5) & (yarea4 | yarea5) & (zarea0 | zarea1)) | ((xarea4 | xarea5) & (yarea0 | yarea1) & (zarea4 | zarea5)) | ((xarea0 | xarea1) & (yarea0 | yarea1) & (zarea0 | zarea1 | zarea2)) | ((xarea0) & (yarea3 | yarea4) & (zarea1 | zarea2 | zarea3));
formula valid = (1 <= x & x <= MAXX-1 & 1 <= y & y <= MAXY-1 & 1 <= z & z <= MAXZ-1) & !crash & ok=1;
"""
control_module = """
module control
c : [0..3] init 0;
c : [0..1] init 0;
[move] c = 0 -> 1: (c'=1);
[env] c = 1 -> 1: (c'=2);
[chc] c = 2 -> 1: (c'=3);
[chd] c = 3 -> 1: (c'=0);
[env] c = 1 -> 1: (c'=0);
endmodule
"""
mod_head = """
module mod
ok : [0..1] init 1;
cond : [0..3] init 0;
wdir : [0..7] init 0;
cond : [0..0] init 0;
wdir : [0..0] init 0;
x : [0..MAXX] init 2;
y : [0..MAXY] init floor(MAXY/2);
z : [0..MAXZ] init floor(MAXZ/2);
x : [0..MAXX] init 14;
y : [0..MAXY] init 2;
z : [0..MAXZ] init 2;
phase : [0..1] init 0;
......@@ -43,17 +43,8 @@ module mod
[move] z < MAXX -> 1: (z'=z+1);
[move] z > 0 -> 1: (z'=z-1);
[move] attarget -> 1: (phase'=1);
[chc] cond = 0 -> p00: (cond' = 0) + p01: (cond' = 1) + p02: (cond' = 2) + p03: (cond' = 3);
[chc] cond = 1 -> p10: (cond' = 0) + p11: (cond' = 1) + p12: (cond' = 2) + p13: (cond' = 3);
[chc] cond = 2 -> p20: (cond' = 0) + p21: (cond' = 1) + p22: (cond' = 2) + p23: (cond' = 3);
[chc] cond = 3 -> p30: (cond' = 0) + p31: (cond' = 1) + p32: (cond' = 2) + p33: (cond' = 3);
[chd] cond = 0 -> c0pdircm2: (wdir' = mod(wdir + 6,8)) + c0pdircm1: (wdir' = mod(wdir + 7,8)) + c0pdirc0: (wdir' = wdir) + c0pdircp1: (wdir' = mod(wdir + 1,8)) + c0pdircp2: (wdir' = mod(wdir + 2,8));
[chd] cond = 1 -> c1pdircm2: (wdir' = mod(wdir + 6,8)) + c1pdircm1: (wdir' = mod(wdir + 7,8)) + c1pdirc0: (wdir' = wdir) + c1pdircp1: (wdir' = mod(wdir + 1,8)) + c1pdircp2: (wdir' = mod(wdir + 2,8));
[chd] cond = 2 -> c2pdircm2: (wdir' = mod(wdir + 6,8)) + c2pdircm1: (wdir' = mod(wdir + 7,8)) + c2pdirc0: (wdir' = wdir) + c2pdircp1: (wdir' = mod(wdir + 1,8)) + c2pdircp2: (wdir' = mod(wdir + 2,8));
[chd] cond = 3 -> c3pdircm2: (wdir' = mod(wdir + 6,8)) + c3pdircm1: (wdir' = mod(wdir + 7,8)) + c3pdirc0: (wdir' = wdir) + c3pdircp1: (wdir' = mod(wdir + 1,8)) + c3pdircp2: (wdir' = mod(wdir + 2,8));
[env] !valid -> 1: (ok'=0) & (x'=0) & (y'=0) & (z'=0) & (phase'=0);
"""
......@@ -78,9 +69,9 @@ labels="""
#for element in itertools.product(*somelists):
# print(element)
xsplits = [4,6]
ysplits = [7]
zsplits = [5]
xsplits = [2,4,7,9,11]
ysplits = [3,5,7,10,13]
zsplits = [2,4,8,10,12]
x_area_splits = [0] + xsplits + ["MAXX"]
y_area_splits = [0] + ysplits + ["MAXY"]
......@@ -95,14 +86,14 @@ y_area_definitions = _areadefinitions("y", y_area_splits)
z_area_definitions = _areadefinitions("z", z_area_splits)
area_definitions = "\n".join([x_area_definitions, y_area_definitions, z_area_definitions])
conditions = [0,1,2,3]
winddirs = [0,1,2,3,4,5,6,7]
conditions = [0]
winddirs = [0]
xzones = list(range(len(xsplits)+1))
yzones = list(range(len(ysplits)+1))
zzones = list(range(len(zsplits)+1))
def get_update(dir,eff):
if dir % 2 == 0:
if dir % 10 == 1:
# straight
affected_var, other_var = ("x","y") if dir in [0,4] else ("y","x")
main_var_sym = "+" if dir < 4 else "-"
......@@ -110,84 +101,110 @@ def get_update(dir,eff):
return "({}' = {}{}{})".format(affected_var, affected_var, main_var_sym, math.ceil(1)) + " & " + "({}' = {}{})".format(other_var,other_var,sec_var_op)
else:
# diagionals
assert dir in [1,3,5,7]
#assert dir in [1,3,5,7]
xsym = "+" if dir in [1,7] else "-"
ysym = "+" if dir < 4 else "-"
if eff == 0:
return "(x'=x) & (y'=y)"
if eff in [3,6]:
return "(x' = x{}{}) & (y' = y{}{})".format(xsym,1,ysym,1)
# if eff in [3,6]:
# return "(x' = x{}{}) & (y' = y{}{})".format(xsym,1,ysym,1)
# if eff == 1:
# if dir == 1:
# return ("(x'=x+1)")
# if dir == 3:
# return ("(y'=y+1)")
# if dir == 5:
# return ("(x'=x-1)")
# if dir == 7:
# return ("(y'=y-1)")
# if eff == 2:
# if dir == 1:
# return ("(y'=y+1)")
# if dir == 3:
# return ("(x'=x-1)")
# if dir == 5:
# return ("(y'=y-1)")
# if dir == 7:
# return ("(x'=x+1)")
# if eff == 4:
# if dir == 1:
# return ("(x'=x+1) & (y'=y+1)")
# if dir == 3:
# return ("(y'=y+1) & (x'=x-1)")
# if dir == 5:
# return ("(x'=x-1) & (y'=y-1)")
# if dir == 7:
# return ("(y'=y-1) & (x'=x+1)")
# if eff == 5:
# if dir == 1:
# return ("(y'=y+1) & (x'=x+1)")
# if dir == 3:
# return ("(x'=x-1) & (y'=y+1)")
# if dir == 5:
# return ("(y'=y-1) & (x'=x-1)")
# if dir == 7:
# return ("(x'=x+1) & (y'=y-1)")
if eff == 1:
if dir == 1:
return ("(x'=x+1)")
if dir == 3:
return ("(y'=y+1)")
if dir == 5:
return ("(x'=x-1)")
if dir == 7:
return ("(y'=y-1)")
return ("(x'=x+1)")
if eff == 2:
if dir == 1:
return ("(y'=y+1)")
if dir == 3:
return ("(x'=x-1)")
if dir == 5:
return ("(y'=y-1)")
if dir == 7:
return ("(x'=x+1)")
return ("(x'=x+2)")
if eff == 3:
return ("(x'=x-1)")
if eff == 4:
if dir == 1:
return ("(x'=x+1) & (y'=y+1)")
if dir == 3:
return ("(y'=y+1) & (x'=x-1)")
if dir == 5:
return ("(x'=x-1) & (y'=y-1)")
if dir == 7:
return ("(y'=y-1) & (x'=x+1)")
return ("(x'=x-2)")
if eff == 5:
if dir == 1:
return ("(y'=y+1) & (x'=x+1)")
if dir == 3:
return ("(x'=x-1) & (y'=y+1)")
if dir == 5:
return ("(y'=y-1) & (x'=x-1)")
if dir == 7:
return ("(x'=x+1) & (y'=y-1)")
return ("(y'=y+1)")
if eff == 6:
return ("(y'=y+2)")
if eff == 7:
return ("(y'=y-1)")
if eff == 8:
return ("(y'=y-2)")
if eff == 9:
return ("(y'=y+1) & (x'=x+1)")
if eff == 10:
return ("(y'=y-1) & (x'=x-1)")
if eff == 11:
return ("(y'=y+1) & (x'=x-1)")
if eff == 12:
return ("(y'=y-1) & (x'=x+1)")
assert False
num_effs=13
def create_command(c,w,x,y,z):
guard = "cond = {} & wdir = {} & xarea{} & yarea{} & zarea{} & valid".format(c, w, x, y, z)
updates = [get_update(w, i) for i in range(7)]
probs = ["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(7)]
updates = [get_update(w, i) for i in range(num_effs)]
probs = ["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(num_effs)]
weighted_updates = ["{}: {}".format(p, u) for p, u in zip(probs, updates)]
update_str = " + ".join(weighted_updates)
return "\t[env] {} -> {};".format(guard, update_str)
commands = [create_command(c,w,x,y,z) for (c,w,x,y,z) in itertools.product(conditions, winddirs, xzones, yzones, zzones)]
def create_reward(w,x,y,z):
guard = "wdir = {} & xarea{} & yarea{} & zarea{} & valid".format(w, x, y, z)
#print(guard)
#updates = [get_update(w, i) for i in range(7)]
#probs = ["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(7)]
rewards = "RewardEnvw{}x{}y{}z{}".format(w, x, y, z,)
#print(rewards)
#weighted_updates = ["{}".format(p,) for p in zip(rewards)]
#update_str = " + ".join(weighted_updates)
return "\t[env] true & {}: {};".format(guard, rewards)
# def create_reward(w,x,y,z):
# guard = "wdir = {} & xarea{} & yarea{} & zarea{} & valid".format(w, x, y, z)
# #print(guard)
# #updates = [get_update(w, i) for i in range(7)]
# #probs = ["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(7)]
# rewards = "RewardEnvw{}x{}y{}z{}".format(w, x, y, z,)
# #print(rewards)
# #weighted_updates = ["{}".format(p,) for p in zip(rewards)]
# #update_str = " + ".join(weighted_updates)
# return "\t[env] true & {}: {};".format(guard, rewards)
rewards = [create_reward(w,x,y,z) for (w,x,y,z) in itertools.product(winddirs, xzones, yzones, zzones)]
# rewards = [create_reward(w,x,y,z) for (w,x,y,z) in itertools.product(winddirs, xzones, yzones, zzones)]
def parameter_groups():
groups = []
for cfrom in range(4):
groups.append(["p{}{}".format(cfrom,cto) for cto in range(4)])
for cfrom in range(4):
groups.append(["c{}pdirc{}".format(cfrom,dirto) for dirto in ["m2","m1","0","p1","p2"]])
# for cfrom in range(1):
# groups.append(["p{}{}".format(cfrom,cto) for cto in range(1)])
# for cfrom in range(1):
# groups.append(["c{}pdirc{}".format(cfrom,dirto) for dirto in ["m2","m1","0","p1","p2"]])
for (c,w,x,y,z) in itertools.product(conditions, winddirs, xzones, yzones, zzones):
groups.append(["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(7)])
groups.append(["pc{}w{}x{}y{}z{}eff{}".format(c, w, x, y, z, i) for i in range(num_effs)])
#for r in range(1):
groups.append(["RewardEnv","RewardChd"])
# groups.append(["RewardEnv","RewardChd"])
#for (w) in (winddirs):
# groups.append(["RewardEnvw{}x{}y{}z{}".format(w,x,y,z) for x,y,z in itertools.product(xzones,yzones,zzones)])
#print(groups)
......@@ -202,23 +219,55 @@ def parameter_definitions(groups,init):
return "\n".join(["const double {};".format(par) for group in groups for par in group])
def parameter_dirichlet_instantiations(groups):
def parameter_dirichlet_instantiations(groups,weather):
instantiations=dict()
for group in groups:
#print(group)
#if there is eff in the parameter group, create dirichlet weights non-uniformly
if any("eff" in group_item for group_item in group):
if weather == "uniform":
array = np.random.random_sample((len(group),))
array[0]=1*array[0]
array[1]=1*array[1]
array[2]=3*array[2]
array[3]=3*array[3]
array[4]=4*array[4]
array[5]=2*array[5]
array[6]=1*array[6]
#create uniformly
elif weather == "x-neg-bias":
if any("eff" in group_item for group_item in group):
array = np.random.random_sample((len(group),))
array[0]=1*array[0]
array[1]=1*array[1]
array[2]=1*array[2]
array[3]=2*array[3]
array[4]=2*array[4]
array[5]=1*array[5]
array[6]=1*array[6]
array[7]=1*array[7]
array[8]=1*array[8]
array[9]=1*array[9]
array[10]=2*array[10]
array[11]=2*array[11]
array[12]=1*array[12]
# print(array,len(array),group)
#create uniformly
else:
array = np.random.random_sample((len(group),))
elif weather == "y-pos-bias":
if any("eff" in group_item for group_item in group):
array = np.random.random_sample((len(group),))
array[0]=1*array[0]
array[1]=1*array[1]
array[2]=1*array[2]
array[3]=1*array[3]
array[4]=1*array[4]
array[5]=1*array[5]
array[6]=1*array[6]
array[7]=2*array[7]
array[8]=2*array[8]
array[9]=1*array[9]
array[10]=2*array[10]
array[11]=1*array[11]
array[12]=2*array[12]
# print(array,len(array),group)
#create uniformly
else:
array = np.random.random_sample((len(group),))
else:
array = np.random.random_sample((len(group),))
raise RuntimeError("Specificed weather is not compatible")
instantiations[tuple(group)]=array
return instantiations
......@@ -246,19 +295,20 @@ def parameter_dirichlet_samples(parameter_instantiations):
return instantiations_sample
groups = parameter_groups()
weather = "uniform"
parameter_defs = parameter_definitions(groups,False)
parameter_instantiations=parameter_dirichlet_instantiations(groups)
parameter_instantiations=parameter_dirichlet_instantiations(groups,weather)
parameter_samples=parameter_dirichlet_samples(parameter_instantiations)
for element in parameter_samples:
print(np.sum(parameter_samples[tuple(element)]))