#!/usr/bin/env python
from itertools import combinations_with_replacement,product
class ModelGenerator_Security():
def __init__(self, parameters):
# def __init__(self, modelFilePath, propertiesFilePath, propertiesProbabilisticFilePath, initAddProb=0.01, initRemProb=0.001, minNumVms=None, maxNumVms=None, maxAdd=None, maxRem=None, num_of_clusters=None, gain=None, latency_threshold=60, alpha="0.2", model_type='mdp', rewards_structure='s', action_selection_type="max", fault_probs=True, norm=False, prob_threshold='0.8',max_steps='5',cumulative=True):
self.initNumVms = int(parameters["initNumVms"]);
self.minNumVms = int(parameters["minNumVms"]);
self.maxNumVms = int(parameters["maxNumVms"]);
self.maxAdd = int(parameters["maxAdd"]);
self.maxRem = int(parameters["maxRem"]);
self.num_of_clusters = int(parameters["num_of_clusters"]);
self.gain = parameters["gain"];
self.latency_threshold = parameters["latency_threshold"];
self.modelFilePath = parameters["modelFilePath"];
self.propertiesFilePath = parameters["propertiesFilePath"];
self.propertiesProbabilisticFilePath = parameters["propertiesProbabilisticFilePath"];
self.max_steps = parameters["max_steps"]
self.cumulative = parameters["cumulative"]
self.gain_punishment = parameters["gain_punishment"]
self.attack = eval(parameters["attack"])
self.transient_counter_limit = int(parameters["transient_counter_limit"]);
self.only_attack = eval(parameters["only_attack"])
self.hourly = parameters["hourly"]
self.weightedReward = parameters["weightedReward"]
self.vm_types = parameters["vm_types"]
self.vm_types_limits = parameters["vm_types_limits"]
# self.repViolationPunishement = parameters["repViolationPunishement"]
self.spot = False
self.new_spot_vm_types = []
# sp_vm_type = ""
for vm_type in self.vm_types:
if("_sp" in vm_type):
self.spot = True
self.new_spot_vm_types.append(vm_type)
# sp_vm_type = vm_type
# self.new_spot_vm_types.append(vm_type+"_1")
# self.new_spot_vm_types.append(vm_type+"_12")
# self.new_spot_vm_types.append(vm_type+"_14")
# if(self.spot):
# self.vm_types.remove(sp_vm_type)
# self.vm_types += self.new_spot_vm_types
self.multiType = False
if(len(self.vm_types) > 0):
self.multiType = True
self.create_throughput = 'throughput' in self.gain
self.LS = "\n";
def generateModel(self):
self.out = open(self.modelFilePath, 'w');
self.out.write("mdp"+self.LS+self.LS);
#generate model parameters
self.generateParameters();
#generate module
self.generateModule();
self.generateProbabilitiesModule();
self.out.write(self.LS);
if self.transient_counter_limit > 0:
self.generateTransientModule();
self.out.write(self.LS);
if self.attack:
self.generateAttackModule();
self.out.write(self.LS);
#generates formulas
self.generateFormulas();
#generates rewards
self.generateRewardsFirst();
self.out.close();
self.generatePropertiesFirst();
#Start of Parameters Generation
def generateParameters(self):
self.generateParameter("latency", False);
#generate prob cluster weights
self.generateParameter("prob", True);
if self.attack:
#generate attack parameters
self.generateAttackParameter();
if self.multiType:
self.generateCostParameter();
#generate cluster specifications
self.out.write("const int min_num_nodes = " + str(self.minNumVms) + ";" + self.LS
+ "const int max_num_nodes = " + str(self.maxNumVms) + ";" + self.LS
+ "const int num_of_clusters = " + str(self.num_of_clusters) + ";" + self.LS
+ "const double latency_threshold = " + str(self.latency_threshold) + ";" + self.LS
+ "const int init_num_nodes;" + self.LS);
for vm_type in self.vm_types:
self.out.write("const int "+vm_type+"_min_num_nodes;" + self.LS
+"const int "+vm_type+"_max_num_nodes;" + self.LS
+"const int "+vm_type+"_init_num_nodes;" + self.LS);
if(self.weightedReward):
self.out.write("const double mean_lat;" + self.LS)
self.out.write("const double std_lat;" + self.LS)
self.out.write("const int max_steps = " + str(self.max_steps) + ";" + self.LS)
self.out.write(self.LS);
if(self.transient_counter_limit > 0):
self.out.write("const int add_transient_counter_limit = "+str(self.transient_counter_limit)+";" + self.LS)
if(self.hourly):
self.generateRemoveStepsParameters();
self.out.write(self.LS);
if(self.spot):
# self.generateRemoveSpotParameters();
# self.out.write(self.LS);
self.generateCostSpotParameters();
self.out.write(self.LS);
self.generateBidSpotParameters();
self.out.write(self.LS);
for i in range(1, self.maxAdd+1):
self.out.write("const bool add_"+str(i)+"_restriction;" + self.LS)
self.out.write("const bool no_op_restriction;" + self.LS)
for i in range(1, self.maxRem+1):
self.out.write("const bool rem_"+str(i)+"_restriction;" + self.LS)
def generateParameter(self, name, weight):
for i in range(self.minNumVms, self.maxNumVms+1):
for j in range(0, self.num_of_clusters):
for k in range(0, int(self.max_steps)+1):
self.out.write("const double "+name+"_vm_"+str(i)+"_cluster_"+str(j)+"_step_"+str(k)+("_w" if weight else "")+";");
self.out.write(self.LS);
self.out.write(self.LS);
self.out.write(self.LS);
def generateAttackParameter(self):
for vm_type in self.vm_types:
self.out.write("const double %s;"%(vm_type + "_attack_prob") + self.LS);
self.out.write(self.LS);
def generateCostParameter(self):
for vm_type in self.vm_types:
if('_sp' not in vm_type):
self.out.write("const double %s;"%(vm_type + "_cost") + self.LS);
self.out.write(self.LS);
def generateRemoveStepsParameters(self):
for i in range(0, int(self.max_steps)+1):
for vm_type in self.vm_types:
self.out.write("const int remove" + vm_type + "_step_" + str(i) + ";" + self.LS);
def generateRemoveSpotParameters(self):
for vm_type in self.vm_types:
if "_sp" in vm_type:
for s in range(0,int(self.max_steps)+1):
self.out.write("const double "+vm_type+"_remove_spot_step_" + str(s) + ";" + self.LS);
def generateCostSpotParameters(self):
for vm_type in self.vm_types:
if ("_sp" in vm_type):
for s in range(0,int(self.max_steps)+1):
self.out.write("const double "+vm_type+"_market_price_step_" + str(s) + ";" + self.LS);
def generateBidSpotParameters(self):
for vm_type in self.vm_types:
if ("_sp" in vm_type):
self.out.write("const double "+vm_type+"_bid_price;" + self.LS);
def generateCostSpotFormula(self):
for vm_type in self.vm_types:
if('_sp' in vm_type):
self.out.write("formula %s = "%(vm_type + "_cost"));
for i in range(0, int(self.max_steps)+1):
self.out.write("steps="+str(i)+"?"+vm_type+"_market_price_step_"+str(i)+":");
self.out.write("0;" + self.LS);
self.out.write(self.LS);
#End of Parameters Generation
#Start of Module Generation
def generateModule(self):
self.out.write("module tiramola" + self.LS
+ "\tcurrent_num_nodes : [min_num_nodes..max_num_nodes] init init_num_nodes;" + self.LS);
# if(self.spot):
# for vm_type in self.vm_types:
# if "_sp" in vm_type:
# self.out.write("\t%s_previous_num_nodes : [%s_min_num_nodes..%s_max_num_nodes] init %s_init_num_nodes;"%(vm_type,vm_type,vm_type,vm_type) + self.LS);
for vm_type in self.vm_types:
if("_pr" in vm_type):
self.out.write("\t"+vm_type+"_current_num_nodes : int init "+vm_type+"_init_num_nodes;" + self.LS)
else:
self.out.write("\t"+vm_type+"_current_num_nodes : ["+vm_type+"_min_num_nodes.."+vm_type+"_max_num_nodes] init "+vm_type+"_init_num_nodes;" + self.LS)
# for vm_type in self.vm_types:
# if("_sp" in vm_type):
# self.out.write("\t"+vm_type+"_rem_candidate : [0.."+vm_type+"_max_num_nodes] init 0;" + self.LS)
self.out.write("\tsteps : [0..max_steps] init 0;" + self.LS)
if self.transient_counter_limit > 0:
self.out.write("\tadd_transient_counter : [0..add_transient_counter_limit] init add_transient_counter_limit;" + self.LS);
if(self.spot):
self.out.write("\tphase : [-1..4] init -1;" + self.LS)
# for vm_type in self.vm_types:
# if("_sp" in vm_type):
# self.out.write("\t%s_removed_spots : [0..max_num_nodes] init 0;"%(vm_type) + self.LS)
else:
self.out.write("\tphase : [0..4] init 0;" + self.LS)
self.out.write(self.LS);
#generates the actions which are checked in the first step
self.generateActions();
self.out.write(self.LS);
if self.multiType:
self.out.write("\t[end] steps = max_steps & phase = 0-> (phase' = 4);" + self.LS);
else:
if self.transient_counter_limit > 0:
self.out.write("\t[end] steps = max_steps & !stop & !get_cluster & !get_transient -> (stop' = true);" + self.LS);
else:
self.out.write("\t[end] steps = max_steps & !stop & !get_cluster -> (stop' = true);" + self.LS);
self.out.write("\t[stop] phase = 4 -> true;" + self.LS);
self.out.write("endmodule" + self.LS + self.LS);
def generateActions(self):
if(self.spot):
self.generatePreSpotActions();
# self.generateSpotActions();
#generate add/remove actions
if(self.multiType):
self.generateMultiTypeAddActions();
self.generateMultiTypeRemoveActions();
self.generateMultiTypeNoOpActions();
else:
self.generateAddActions();
self.generateRemoveActions();
self.generateNoOpActions();
self.out.write(self.LS);
if(self.attack):
self.out.write("\t[attack] phase = 2 ->" + self.LS);
self.out.write("\t\t(phase' = 3);" + self.LS + self.LS);
if self.transient_counter_limit > 0:
self.out.write("\t[cluster] phase = 1 ->" + self.LS);
if(self.attack):
self.out.write("\t\t(phase' = 2);" + self.LS + self.LS);
else:
self.out.write("\t\t(phase' = 3);" + self.LS + self.LS);
self.out.write("\t[transient] phase = 3 ->" + self.LS);
if(self.spot):
self.out.write("\t\t(phase' = -1);" + self.LS + self.LS);
else:
self.out.write("\t\t(phase' = 0);" + self.LS + self.LS);
else:
self.out.write("\t[action] get_cluster & !stop ->" + self.LS);
self.out.write("\t\t(get_cluster' = false);" + self.LS);
#pre spot actions
def generatePreSpotActions(self):
pre_spot_condition_template = '';
for vm_type in self.new_spot_vm_types:
pre_spot_condition_template += vm_type + '_bid_price %s ' + vm_type + '_cost & ';
for i in product(['<','>'], repeat=len(self.new_spot_vm_types)):
#if(i.count('<') != len(i)):
ps = pre_spot_condition_template%i
self.out.write("\t[pre_spot] " + ps + "phase = -1 ->" + self.LS);
pre_spot_result_template = '';
if('<' in i):
pre_spot_result_template += " (current_num_nodes' = current_num_nodes - (";
cnt = 0;
for symbol in i:
if(symbol == '<'):
pre_spot_result_template += self.new_spot_vm_types[cnt] + "_current_num_nodes + ";
cnt += 1;
pre_spot_result_template = pre_spot_result_template[0:len(pre_spot_result_template)-2] + ")) &"
cnt = 0;
for symbol in i:
if(symbol == '<'):
pre_spot_result_template += " (" + self.new_spot_vm_types[cnt] + "_current_num_nodes' = 0) &";
cnt += 1;
self.out.write("\t\t" + pre_spot_result_template + " (phase' = 0);" + self.LS + self.LS);
#spot actions
def generateSpotActions(self):
for vm_type in self.vm_types:
if "_sp" in vm_type:
for i in range(1,self.maxNumVms+1):
self.out.write("\t[spot] %s_remove_spots = %s & %s_current_num_nodes - %s_remove_spots >= %s_min_num_nodes & current_num_nodes - %s_remove_spots >= min_num_nodes & phase = -1 ->"%(vm_type,str(i),vm_type,vm_type,vm_type,vm_type) + self.LS);
self.out.write("\t\t(%s_current_num_nodes' = %s_current_num_nodes - %s) & (%s_rem_candidate' = 0) & (current_num_nodes' = current_num_nodes - %s) & (phase' = -1);"%(vm_type,vm_type,str(i),vm_type,str(i)) + self.LS + self.LS);
spot_condition = "[spot] ";
for vm_type in self.vm_types:
if "_sp" in vm_type:
spot_condition += vm_type + "_rem_candidate = 0 & ";
self.out.write("\t" + spot_condition + "phase = -1 ->" + self.LS);
self.out.write("\t\t(phase' = 0);" + self.LS + self.LS);
def generateAddActions(self):
for j in range(1, self.maxAdd+1):
self.out.write("\t[add_" + str(j) + "] allow_add_" + str(j) + " & (steps < max_steps) & (current_num_nodes + "+str(j)+") <= max_num_nodes & !stop & !get_cluster "+("& add_transient_counter = add_transient_counter_limit " if self.transient_counter_limit > 0 else "")+"->" + self.LS);
self.out.write("\t\t(current_num_nodes' = current_num_nodes + " + str(j) + ") & (steps' = steps + 1) & (get_cluster' = true)"+("& (get_transient' = true) & (add_transient_counter' = 0) " if self.transient_counter_limit > 0 else "")+";" + self.LS);
self.out.write(self.LS);
self.out.write(self.LS);
def generateRemoveActions(self):
for j in range(1, self.maxRem+1):
self.out.write("\t[remove_" + str(j) + "] allow_rem_" + str(j) + " (steps < max_steps) & (current_num_nodes - "+str(j)+") >= min_num_nodes & "+("(allow_to_remove >= " + str(j) + ") &" if self.hourly else "")+" !stop & !get_cluster "+("& add_transient_counter = add_transient_counter_limit " if self.transient_counter_limit > 0 else "")+"->" + self.LS);
self.out.write("\t\t(current_num_nodes' = current_num_nodes - " + str(j) + ") & (steps' = steps + 1) & (get_cluster' = true);" + self.LS);
self.out.write(self.LS);
self.out.write(self.LS);
def generateNoOpActions(self):
self.out.write("\t[no_op] allow_no_op !stop & steps < max_steps & !get_cluster "+("& !get_transient " if self.transient_counter_limit > 0 else "")+" -> " + self.LS);
self.out.write("\t\t(current_num_nodes' = current_num_nodes) & (steps' = steps + 1) & (get_cluster' = true);" + self.LS + self.LS);
#multiType
def generateMultiTypeAddActions(self):
for j in range(1, self.maxAdd+1):
for comb in combinations_with_replacement(self.vm_types,j):
self.out.write("\t[add_" + str(j) + ''.join(comb) + "] "+ "allow_add_" + str(j) + " & steps < max_steps & ");
cnt = 0
met = []
for vm_type in comb:
if vm_type not in met:
if(vm_type in self.vm_types_limits):
if(cnt < len(comb)):
self.out.write("(" + vm_type + "_current_num_nodes + "+str(comb.count(vm_type))+") <= " + vm_type + "_max_num_nodes & ");
cnt = cnt + comb.count(vm_type);
met.append(vm_type)
self.out.write("(current_num_nodes + "+str(j)+") <= max_num_nodes & add_transient_counter = add_transient_counter_limit & phase = 0 ->" + self.LS);
self.out.write("\t\t");
cnt = 0
met = []
for vm_type in comb:
if vm_type not in met:
if(cnt < len(comb)):
self.out.write("(" + vm_type + "_current_num_nodes' = " + vm_type + "_current_num_nodes + " + str(comb.count(vm_type)) + ") & ");
# if("_sp" in vm_type):
# self.out.write("(" + vm_type + "_previous_num_nodes' = " + vm_type + "_current_num_nodes) & ");
cnt = cnt + comb.count(vm_type);
met.append(vm_type)
self.out.write("(current_num_nodes' = current_num_nodes + " + str(j) + ") & (steps' = steps + 1) & (phase' = 1) & (add_transient_counter' = 0);" + self.LS);
self.out.write(self.LS);
self.out.write(self.LS);
def generateMultiTypeRemoveActions(self):
for j in range(1, self.maxRem+1):
for comb in combinations_with_replacement(self.vm_types,j):
self.out.write("\t[rem_" + str(j) + ''.join(comb) + "] "+ "allow_rem_"+str(j)+" & steps < max_steps & ");
cnt = 0
met = []
for vm_type in comb:
if(vm_type in self.vm_types_limits):
if vm_type not in met:
if(cnt < len(comb)):
self.out.write("(" + vm_type + "_current_num_nodes - "+str(comb.count(vm_type))+") >= " + vm_type + "_min_num_nodes & "+(str(comb.count(vm_type))+" <= remove"+vm_type+"_limit & " if self.hourly else ""));
cnt = cnt + comb.count(vm_type);
met.append(vm_type)
self.out.write("(current_num_nodes - "+str(j)+") >= min_num_nodes & add_transient_counter = add_transient_counter_limit & phase = 0 ->" + self.LS);
self.out.write("\t\t");
cnt = 0
met = []
for vm_type in comb:
if vm_type not in met:
if(cnt < len(comb)):
self.out.write("(" + vm_type + "_current_num_nodes' = " + vm_type + "_current_num_nodes - " + str(comb.count(vm_type)) + ") & ");
# if("_sp" in vm_type):
# self.out.write("("+vm_type+"_removed_spots' = "+vm_type+"_removed_spots + "+str(comb.count(vm_type))+") & ");
cnt = cnt + comb.count(vm_type);
met.append(vm_type)
self.out.write("(current_num_nodes' = current_num_nodes - " + str(j) + ") & (steps' = steps + 1) & (phase' = 1);" + self.LS);
self.out.write(self.LS);
self.out.write(self.LS);
def generateMultiTypeNoOpActions(self):
self.out.write("\t[no_op] allow_no_op & steps < max_steps & phase = 0 & add_transient_counter = add_transient_counter_limit -> " + self.LS);
self.out.write("\t\t(current_num_nodes' = current_num_nodes) & ");
# for vm_type in self.vm_types:
# if "_sp" in vm_type:
# self.out.write("(" + vm_type + "_previous_num_nodes' = " + vm_type + "_current_num_nodes) & ");
self.out.write("(steps' = steps + 1) & (phase' = 1);" + self.LS + self.LS);
self.out.write("\t[no_op] steps < max_steps & phase = 0 & add_transient_counter < add_transient_counter_limit -> " + self.LS);
self.out.write("\t\t(current_num_nodes' = current_num_nodes) & ");
# for vm_type in self.vm_types:
# if "_sp" in vm_type:
# self.out.write("(" + vm_type + "_previous_num_nodes' = " + vm_type + "_current_num_nodes) & ");
self.out.write("(steps' = steps + 1) & (phase' = 1) & (add_transient_counter' = add_transient_counter + 1);" + self.LS + self.LS);
#End of Module Generation
#Start of Probabilities Module Generation
def generateProbabilitiesModule(self):
self.out.write("module cluster_compute" + self.LS
+ "\tcluster_id : [0..num_of_clusters-1] init 0;" + self.LS + self.LS);
for i in range(self.minNumVms, self.maxNumVms+1):
for k in range(0,int(self.max_steps)+1):
self.out.write("\t[cluster] current_num_nodes = "+str(i)+((" & steps = "+str(k)) if self.max_steps!=0 else "")+" & phase = 1 & (");
for c in range(0, self.num_of_clusters):
self.out.write("prob_vm_"+str(i)+"_cluster_"+str(c)+"_step_"+str(k)+"_w");
if(c == self.num_of_clusters-1):
self.out.write(" != 0)");
else:
self.out.write(" + ");
self.out.write("->" + self.LS + "\t\t");
for c in range(0, self.num_of_clusters):
self.out.write("prob_vm_"+str(i)+"_cluster_"+str(c)+"_step_"+str(k)+"_w : (cluster_id' = "+str(c)+")");
if(c == self.num_of_clusters-1):
self.out.write(";" + self.LS);
else:
self.out.write(self.LS + "\t\t+");
self.out.write(self.LS);
self.out.write(self.LS);
self.out.write("endmodule" + self.LS);
#End of Probabilities Module Generation
#Start of Transient Module Generation
def generateTransientModule(self):
self.out.write("module add_transient" + self.LS
+ "\tadd_tran_current_num_nodes : [min_num_nodes..max_num_nodes] init init_num_nodes;" + self.LS + self.LS);
self.out.write("\t[transient] true ->" + self.LS
+ "\t\t(add_tran_current_num_nodes' = current_num_nodes);" + self.LS + self.LS);
self.out.write("endmodule" + self.LS);
#End of Attack Module Generation
#Start of Attack Module Generation
def generateAttackModule(self):
self.out.write("module attack_prob_compute" + self.LS
+ "\tattack : bool init false;" + self.LS + self.LS);
self.out.write("\t[attack] phase = 2 ->" + self.LS
+ "\t\tattack_prob : (attack' = true)" + self.LS
+ "\t\t+(1 - attack_prob) : (attack' = false);" + self.LS);
self.out.write("endmodule" + self.LS);
#End of Attack Module Generation
#Start of Formulas Generation
def generateFormulas(self):
if self.spot:
# for vm_type in self.vm_types:
# if "_sp" in vm_type:
# self.out.write("formula "+vm_type+"_remove_spots = (");
# for i in range(0, int(self.max_steps)+1):
# self.out.write("steps="+str(i)+"?("+vm_type+"_removed_spots=0?"+vm_type+"_remove_spot_step_"+str(i)+":max(");
# for j in range(0, i+1):
# self.out.write(vm_type+"_remove_spot_step_"+str(j)+"+")
# self.out.write("(-"+vm_type+"_removed_spots),0)):")
# self.out.write("0) + " + vm_type + "_rem_candidate;" + self.LS + self.LS);
# self.out.write("formula total_remove_spots = ");
# rem_spots = ""
# for vm_type in self.vm_types:
# if "_sp" in vm_type:
# rem_spots += vm_type+"_removed_spots +";
# self.out.write(rem_spots[:-1] + ";" + self.LS + self.LS)
self.generateCostSpotFormula();
self.out.write(self.LS);
if self.attack:
self.out.write("formula attack_prob = 1-(");
for vm_type in self.vm_types:
self.out.write("pow(1-%s,%s)*"%(vm_type + "_attack_prob", vm_type + "_current_num_nodes"));
self.out.write("1);" + self.LS + self.LS);
self.out.write("formula min_attack_prob = 1-(");
for vm_type in self.vm_types:
self.out.write("pow(1-%s,%s)*"%(vm_type + "_attack_prob", vm_type + "_min_num_nodes"));
self.out.write("1);" + self.LS + self.LS);
self.out.write("formula max_attack_prob = 1-(");
for vm_type in self.vm_types:
self.out.write("pow(1-%s,%s)*"%(vm_type + "_attack_prob", vm_type + "_max_num_nodes"));
self.out.write("1);" + self.LS + self.LS);
if self.multiType:
i = 0
self.out.write("formula total_cost = ");
for vm_type in self.vm_types:
self.out.write("%s*%s"%(vm_type + "_current_num_nodes", vm_type + "_cost"));
if (i < len(self.vm_types)-1):
self.out.write("+");
i = i + 1
self.out.write(";" + self.LS + self.LS);
i = 0
self.out.write("formula min_total_cost = ");
for vm_type in self.vm_types:
self.out.write("%s*%s"%(vm_type + "_min_num_nodes", vm_type + "_cost"));
if (i < len(self.vm_types)-1):
self.out.write("+");
i = i + 1
self.out.write(";" + self.LS + self.LS);
i = 0
self.out.write("formula max_total_cost = ");
for vm_type in self.vm_types:
self.out.write("%s*%s"%(vm_type + "_max_num_nodes", vm_type + "_cost"));
if (i < len(self.vm_types)-1):
self.out.write("+");
i = i + 1
self.out.write(";" + self.LS + self.LS);
#generates max_throughput formula
if self.create_throughput:
self.out.write("formula max_throughput = max_num_nodes * serv_throughput;" + self.LS + self.LS);
#generates latency formula
self.generateParameterFormula("current_latency","current_num_nodes");
if self.transient_counter_limit > 0:
#generates latency formula
self.generateTransientParameterFormula("add_transient_latency","add_tran_current_num_nodes");
self.out.write(self.LS);
#generates throughput formula
if self.create_throughput:
self.generateParameterFormula("current_throughput","current_num_nodes");
self.out.write(self.LS);
if self.transient_counter_limit > 0:
self.out.write("formula latency = add_transient_counter < add_transient_counter_limit?add_transient_latency:current_latency;" + self.LS);
else:
self.out.write("formula latency = current_latency;" + self.LS);
if self.create_throughput:
self.out.write("formula throughput = current_throughput;" + self.LS);
self.out.write("formula num_nodes = current_num_nodes;" + self.LS + self.LS);
#generates gain and formulas
if self.attack:
if self.only_attack:
self.out.write("formula utility = (attack)?0:(" + self.gain + ");" + self.LS);
else:
# self.out.write("formula utility = (latency>latency_threshold | attack)?0:(" + self.gain + ");" + self.LS);
# self.out.write("formula utility = (latency>latency_threshold & attack)?0:(latency<latency_threshold & attack)?0.5:(latency>latency_threshold & !attack)?1:(latency<latency_threshold & !attack)?1.5+(" + self.gain + "):0;" + self.LS);
if(self.weightedReward):
self.out.write("formula norm_attack_prob = (attack_prob-min_attack_prob)/(max_attack_prob-min_attack_prob);" + self.LS)
self.out.write("formula norm_num_nodes = (num_nodes-min_num_nodes)/(max_num_nodes-min_num_nodes);" + self.LS)
self.out.write("formula norm_total_cost = (total_cost-min_total_cost)/(max_total_cost-min_total_cost);" + self.LS)
self.out.write("formula z_latency = (latency-mean_lat)/std_lat>1?1:(latency-mean_lat)/std_lat<(-1)?-1:(latency-mean_lat)/std_lat;" + self.LS)
self.out.write("formula norm_latency = (z_latency+1)/2;" + self.LS)
self.out.write("formula utility = " + self.gain + ";" + self.LS);
else:
self.out.write("formula utility = (attack)?0:(latency>latency_threshold)?0.5:(" + self.gain + ");" + self.LS);
# self.out.write("formula utility = (latency>latency_threshold & attack)?0:(" + self.gain + ");" + self.LS);
else:
if(self.weightedReward):
self.out.write("formula norm_total_cost = (total_cost-min_total_cost)/(max_total_cost-min_total_cost);" + self.LS)
self.out.write("formula norm_num_nodes = (num_nodes-min_num_nodes)/(max_num_nodes-min_num_nodes);" + self.LS)
self.out.write("formula z_latency = (latency-mean_lat)/std_lat>1?1:(latency-mean_lat)/std_lat<(-1)?-1:(latency-mean_lat)/std_lat;" + self.LS)
self.out.write("formula norm_latency = (z_latency+1)/2;" + self.LS)
self.out.write("formula utility = (latency>latency_threshold)?"+self.gain_punishment+":(" + self.gain + ");" + self.LS);
# self.out.write("formula utility = (" + self.gain + ");" + self.LS);
else:
self.out.write("formula utility = (latency>latency_threshold)?"+self.gain_punishment+":(" + self.gain + ");" + self.LS);
self.out.write("formula state_reward = enableStateReward*(utility<=0?0:utility);"+self.LS+self.LS);
#self.out.write("formula state_reward = utility<=0?0:utility;"+self.LS+self.LS);
self.generateEnableStateRewardsFormula();
self.out.write(self.LS);
if(self.hourly):
for vm_type in self.vm_types:
self.out.write("formula remove"+vm_type+"_limit = ");
for i in range(0, int(self.max_steps)+1):
self.out.write("steps="+str(i)+"?remove"+vm_type+"_step_"+str(i)+":");
self.out.write("0;" + self.LS);
self.out.write(self.LS);
for i in range(1, self.maxAdd+1):
self.out.write("formula allow_add_"+str(i)+" = (steps=0 & add_"+str(i)+"_restriction)?false:true;" + self.LS);
for i in range(1, self.maxRem+1):
self.out.write("formula allow_rem_"+str(i)+" = (steps=0 & rem_"+str(i)+"_restriction)?false:true;" + self.LS);
self.out.write("formula allow_no_op = (steps=0 & no_op_restriction)?false:true;" + self.LS);
def generateParameterFormula(self, name, num_nodes):
formula = "formula "+name+" = ";
for i in range(self.minNumVms,self.maxNumVms+1):
for j in range(0, self.num_of_clusters):
if self.max_steps == 0:
formula += num_nodes+"="+str(i)+" & cluster_id="+str(j)+"?"+name.replace("current_","").replace("previous_","")+"_vm_"+str(i)+"_cluster_"+str(j)+"_step_0:";
else:
for k in range(0,int(self.max_steps)+1):
formula += num_nodes+"="+str(i)+" & cluster_id="+str(j)+" & steps="+str(k)+"?"+name.replace("current_","").replace("previous_","")+"_vm_"+str(i)+"_cluster_"+str(j)+"_step_"+str(k)+":";
formula += "0;";
self.out.write(formula + self.LS);
def generateTransientParameterFormula(self, name, num_nodes):
formula = "formula "+name+" = ";
for i in range(self.minNumVms,self.maxNumVms+1):
for j in range(0, self.num_of_clusters):
for k in range(0,int(self.max_steps)+1):
formula += num_nodes+"="+str(i)+" & cluster_id="+str(j)+" & steps="+str(k)+"?"+name.replace("current_","").replace("previous_","").replace("add_transient_","")+"_vm_"+str(i)+"_cluster_"+str(j)+"_step_"+str(k)+":";
formula += "0;";
self.out.write(formula + self.LS);
def generateStateRewardFormulas(self):
self.out.write("formula state_reward = enableStateReward*utility;"+ self.LS);
def generateEnableStateRewardsFormula(self):
self.out.write("formula enableStateReward = (steps > 0 & phase = 0)?1:0;"+ self.LS);
# if self.spot:
# self.out.write("formula enableSpotPunishment = (steps > 0 & phase = -1)?1:0;"+ self.LS);
#End of Formula Generation
#Start of Rewards Generation
def generateRewardsFirst(self):
self.out.write("rewards \"s_pos\"" + self.LS);
self.out.write("\ttrue : state_reward;" + self.LS);
# for i in range(self.minNumVms, self.maxNumVms+1):
# self.out.write("\tcurrent_num_nodes = "+str(i)+" : state_reward;" + self.LS);
self.out.write("endrewards" + self.LS + self.LS);
#End of Reward Generation
def generatePropertiesFirst(self):
out = open(self.propertiesFilePath, 'w');
if(self.weightedReward):
out.write('R{"s_pos"}min=? [ F phase = 4 ]' + self.LS);
else:
out.write('R{"s_pos"}min=? [ F phase = 4 ]' + self.LS);
out.close();
if __name__ == '__main__':
parameters = {}
parameters["initNumVms"] = "2"
parameters["minNumVms"] = "2"
parameters["maxNumVms"] = "6"
parameters["maxAdd"] = "3"
parameters["maxRem"] = "2"
parameters["num_of_clusters"] = "3"
parameters["gain"] = "max_num_nodes-num_nodes+1"
parameters["latency_threshold"] = "60"
parameters["modelFilePath"] = "models/spots.prism"
parameters["propertiesFilePath"] = "models/generated_properties.csl"
parameters["propertiesProbabilisticFilePath"] = "models/generated_prob_properties.csl"
parameters["max_steps"] = "4"
parameters["cumulative"] = True
parameters["weightedReward"] = True
parameters["attack"] = "False"
parameters["transient_counter_limit"] = "2"
parameters["only_attack"] = "False"
parameters["hourly"] = True
parameters["gain_punishment"] = "2"
parameters["vm_types"] = ['_pr_cl','_pc_od','_pc2_sp1','_pc2_sp12','_pc2_sp14']
parameters["vm_types_limits"] = ['_pr_cl','_pc_od','_pc2_sp1','_pc2_sp12','_pc2_sp14']
pmcb = ModelGenerator_Security(parameters);
pmcb.generateModel();