From 293f41c44b8c5181bd2f9e4a1a29ebc414f59c9c Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 2 Jan 2024 01:23:21 +0100 Subject: [PATCH 1/4] Policy search using CEG start --- paynt/synthesizer/policy_tree.py | 38 +++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index d9fe10740..78a256b84 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/paynt/synthesizer/policy_tree.py @@ -960,6 +960,40 @@ def synthesize_policy_for_family_using_ceg(self, family, prop): return unsat_mdp_families, sat_mdp_families, sat_mdp_policies, sat_mdp_to_policy_map + + def policy_search_ceg(self, family, prop): + + action_family = paynt.family.family.DesignSpace(self.action_coloring_family) + smt_solver = paynt.family.smt.SmtSolver(action_family) + + mdp_subfamilies = [] + + # create MDP subfamilies + for hole_assignment in family.all_combinations(): + subfamily = family.copy() + for hole_index, hole_option in enumerate(hole_assignment): + subfamily.hole_set_options(hole_index, [hole_option]) + mdp_subfamilies.append(subfamily) + + policy_family = smt_solver.pick_assignment(action_family) + + while policy_family is not None: + + self.quotient.build_with_second_coloring(family, self.action_coloring, policy_family) # maybe copy to new family? + + primary_result = policy_family.mdp.model_check_property(prop) + self.stat.iteration(policy_family.mdp) + + print(primary_result) + + exit() + + + + policy_family = smt_solver.pick_assignment(family) + + + #### POLICY SEARCH SECTION END #### ################################### @@ -971,7 +1005,9 @@ def evaluate_all(self, family, prop, keep_value_only=False): policy_tree = PolicyTree(family) ### POLICY SEARCH TESTING - #self.create_action_coloring() + self.create_action_coloring() + + self.policy_search_ceg(policy_tree.root.family, prop) # choose policy search method # unsat, sat, policies, policy_map = self.synthesize_policy_for_family_linear(policy_tree.root.family, prop) From 9c73eef008c1c4cd1c1b868f78f21e8f15032ccb Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 2 Jan 2024 16:56:52 +0100 Subject: [PATCH 2/4] first version of CEG policy search --- paynt/synthesizer/policy_tree.py | 64 ++++++++++++++++++++++++++++---- paynt/synthesizer/statistic.py | 2 +- 2 files changed, 57 insertions(+), 9 deletions(-) diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index 78a256b84..8bc6b9611 100644 --- a/paynt/synthesizer/policy_tree.py +++ b/paynt/synthesizer/policy_tree.py @@ -976,21 +976,69 @@ def policy_search_ceg(self, family, prop): mdp_subfamilies.append(subfamily) policy_family = smt_solver.pick_assignment(action_family) + pruned_overall = 0 + counter = 0 while policy_family is not None: + counter += 1 self.quotient.build_with_second_coloring(family, self.action_coloring, policy_family) # maybe copy to new family? - primary_result = policy_family.mdp.model_check_property(prop) - self.stat.iteration(policy_family.mdp) + # primary_result = policy_family.mdp.model_check_property(prop) + # self.stat.iteration(policy_family.mdp) - print(primary_result) + # if not primary_result.sat: + # print("unsat") - exit() + for mdp_subfamily in mdp_subfamilies: + + self.quotient.build_with_second_coloring(mdp_subfamily, self.action_coloring, policy_family) + self.quotient.build_with_second_coloring(mdp_subfamily, self.action_coloring, action_family) + + dtmc = self.quotient.mdp_to_dtmc(policy_family.mdp.model) + policy_dtmc = paynt.quotient.models.DTMC(dtmc,self.quotient,policy_family.mdp.quotient_state_map,policy_family.mdp.quotient_choice_map) + + dtmc_result = policy_dtmc.model_check_property(prop) + self.stat.iteration(policy_dtmc) + + if not dtmc_result.sat: + self.quotient.build(mdp_subfamily) + action_quotient_assignment = self.action_coloring.getChoiceToAssignment() + choice_to_hole_options = [] + for choice in range(mdp_subfamily.mdp.choices): + quotient_choice = mdp_subfamily.mdp.quotient_choice_map[choice] + choice_to_hole_options.append(action_quotient_assignment[quotient_choice]) + + coloring = payntbind.synthesis.Coloring(action_family.family, mdp_subfamily.mdp.model.nondeterministic_choice_indices, choice_to_hole_options) + quotient_container = paynt.quotient.quotient.DtmcFamilyQuotient(mdp_subfamily.mdp.model, action_family, coloring, self.quotient.specification) + + conflict_generator = paynt.synthesizer.conflict_generator.dtmc.ConflictGeneratorDtmc(quotient_container) + conflict_generator.initialize() + requests = [(0, quotient_container.specification.all_properties()[0], None)] + + # dtmc = self.quotient.mdp_to_dtmc(policy_family.mdp) + # policy_dtmc = paynt.quotient.models.DTMC(dtmc,self.quotient,policy_family.mdp.state_map,policy_family.mdp.choice_map) + + model = quotient_container.build_assignment(policy_family) + + conflicts = conflict_generator.construct_conflicts(action_family, policy_family, model, requests) + pruned = smt_solver.exclude_conflicts(action_family, policy_family, conflicts) + pruned_overall += pruned + # print(conflicts) + # print(pruned) + + break + else: + policy = self.quotient.scheduler_to_policy(dtmc_result.result.scheduler, mdp_subfamily.mdp) + return policy + if counter % 100 == 0: + print(f'{round(pruned_overall/action_family.size*100,2)}%') + + policy_family = smt_solver.pick_assignment(action_family) - policy_family = smt_solver.pick_assignment(family) + return False @@ -1005,9 +1053,9 @@ def evaluate_all(self, family, prop, keep_value_only=False): policy_tree = PolicyTree(family) ### POLICY SEARCH TESTING - self.create_action_coloring() - - self.policy_search_ceg(policy_tree.root.family, prop) + # self.create_action_coloring() + # policy = self.policy_search_ceg(policy_tree.root.family, prop) + # print(policy) # choose policy search method # unsat, sat, policies, policy_map = self.synthesize_policy_for_family_linear(policy_tree.root.family, prop) diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 3f6493818..66a002429 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -203,7 +203,7 @@ def get_summary_synthesis(self): return f"feasible: {feasible}" def get_summary_evaluation(self): - if not isinstance(self.evaluations[0], paynt.synthesizer.synthesizer.FamilyEvaluation): + if not self.evaluations or not isinstance(self.evaluations[0], paynt.synthesizer.synthesizer.FamilyEvaluation): return "" members_sat = sum( [evaluation.family.size for evaluation in self.evaluations if evaluation.sat ]) members_total = self.quotient.design_space.size From 52f5cc8632d1fb5a8bd76b9ecf7cd2bd90d5926a Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 2 Jan 2024 16:57:17 +0100 Subject: [PATCH 3/4] added new versions of models --- .../dpm/switch-rates-big-q10-old/sketch.props | 1 + .../dpm/switch-rates-big-q10-old/sketch.templ | 143 ++++++++ .../dpm/switch-rates-big-q10/sketch.props | 1 + .../dpm/switch-rates-big-q10/sketch.templ | 143 ++++++++ .../dpm/switch-rates-big/sketch.templ | 4 +- .../dpm/switch-rates-q10-old/sketch.props | 1 + .../dpm/switch-rates-q10-old/sketch.templ | 142 ++++++++ .../sketches/dpm/switch-rates/sketch.templ | 6 +- .../rover/{rover => rover-big}/sketch.props | 0 .../mdp/sketches/rover/rover-big/sketch.templ | 112 +++++++ .../rover/rover-constant-success/sketch.props | 1 + .../sketch.templ | 0 models/mdp/sketches/virus-new/sketch.props | 1 + models/mdp/sketches/virus-new/sketch.templ | 308 ++++++++++++++++++ 14 files changed, 858 insertions(+), 5 deletions(-) create mode 100644 models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props create mode 100644 models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ create mode 100644 models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props create mode 100644 models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ create mode 100644 models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props create mode 100644 models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ rename models/mdp/sketches/rover/{rover => rover-big}/sketch.props (100%) create mode 100755 models/mdp/sketches/rover/rover-big/sketch.templ create mode 100755 models/mdp/sketches/rover/rover-constant-success/sketch.props rename models/mdp/sketches/rover/{rover => rover-constant-success}/sketch.templ (100%) create mode 100644 models/mdp/sketches/virus-new/sketch.props create mode 100644 models/mdp/sketches/virus-new/sketch.templ diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props b/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props new file mode 100644 index 000000000..07851960d --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props @@ -0,0 +1 @@ +P >= 0.9 [ F (bat = 0 & lost = 0) ] diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ b/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ new file mode 100644 index 000000000..92bbb275c --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ @@ -0,0 +1,143 @@ +mdp + +// timing: +// tick-0: +// queue state is observed and state change is planned (pm) +// request are generated (if service requester is active) +// tick-1: +// requests are served +// state change is executed +// service requester changes its state +// battery depletes + +// initial queue size +const int q_init = 0; + +// ----- synthesized parameters ------------------------------------------------ + +// requester profiles +hole int P1 in {0,1,2}; +hole int P2 in {0,1,2}; +hole int P3 in {0,1,2}; +hole int P4 in {0,1,2}; + +// queue size +hole int QMAX in {10}; + +// observation level thresholds +hole double T1 in {0.0,0.1,0.2,0.3,0.4}; +hole double T2 in {0.5}; +hole double T3 in {0.6,0.7,0.8,0.9}; + +// switching probabilities +hole double WP1 in {0.9,0.8,0.7}; +hole double WP2 in {0.7,0.6,0.5}; + +// ----- modules --------------------------------------------------------------- + + +// clock + +module CLOCK + c : [0..1] init 0; + [tick00] c=0 -> (c'=1); + [tick01] c=0 -> (c'=1); + [tick02] c=0 -> (c'=1); + [tick1] c=1 -> (c'=0); +endmodule + + +// power manager + +module PM + pm : [0..2] init 0; // 0 - sleep, 1 - idle, 2 - active + [tick00] bat=1 -> (pm'=0); + [tick01] bat=1 -> (pm'=1); + [tick02] bat=1 -> (pm'=2); +endmodule + + +// service provider + +module SP + sp : [0..4] init 0; + // 0 - sleep, 1 - idle, 2 - active + // waiting states: 3 - sleep to idle, 4 - idle to active + + // immediate transitions - change to lower-energy (or same) state + [tick1] sp <= 2 & pm <= sp -> (sp'=pm); + + // transitions through waiting states - change to higher-energy state (sleep to idle or idle to active) + [tick1] sp <= 2 & pm > sp -> (sp'=sp+3); + + // waiting states + [tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true; + [tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true; + +endmodule + + +// service requester + +module SR + sr : [0..1] init 0; // 0 - idle, 1 - active + + [tick00] bat=1 -> 1: (sr'=0); + [tick01] bat=1 -> 1: (sr'=0); + [tick02] bat=1 -> 1: (sr'=0); + + [tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1); + + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1); + + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1); + + [tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1); + [tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1); + [tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1); + +endmodule + + +// service request queue +const int MAX_LOST = 10; + +module SRQ + q : [0..10000] init q_init; + lost : [0..MAX_LOST] init 0; + + [tick00] sr=1 & q < QMAX -> (q'=q+1); // request + [tick01] sr=1 & q < QMAX -> (q'=q+1); // request + [tick02] sr=1 & q < QMAX -> (q'=q+1); // request + + [tick00] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + [tick01] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + [tick02] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + + [tick00] sr!=1 -> true; + [tick01] sr!=1 -> true; + [tick02] sr!=1 -> true; + + [tick1] sp=2 -> 1: (q'=max(q-1,0)); // serve + [tick1] sp!=2 -> true; + +endmodule + + +// battery + +module BAT + bat : [0..2] init 1; // 0 empty, 1 - operational, 2 - failed + [tick1] bat=0 -> true; + [tick1] bat=1 & sp!=2 -> 0.01 : (bat'=0) + 0.99 : true; + [tick1] bat=1 & sp=2 -> 0.01 : (bat'=0) + 0.01 : (bat'=2) + 0.98 : true; + [tick1] bat=2 -> true; +endmodule + +label "goal" = (bat = 0 & lost < MAX_LOST); diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props b/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props new file mode 100644 index 000000000..07851960d --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props @@ -0,0 +1 @@ +P >= 0.9 [ F (bat = 0 & lost = 0) ] diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ b/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ new file mode 100644 index 000000000..06353deac --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ @@ -0,0 +1,143 @@ +mdp + +// timing: +// tick-0: +// queue state is observed and state change is planned (pm) +// request are generated (if service requester is active) +// tick-1: +// requests are served +// state change is executed +// service requester changes its state +// battery depletes + +// initial queue size +const int q_init = 0; + +// ----- synthesized parameters ------------------------------------------------ + +// requester profiles +hole int P1 in {0,1,2}; +hole int P2 in {0,1,2}; +hole int P3 in {0,1,2}; +hole int P4 in {0,1,2}; + +// queue size +hole int QMAX in {10}; + +// observation level thresholds +hole double T1 in {0.0,0.1,0.2,0.3,0.4}; +hole double T2 in {0.5}; +hole double T3 in {0.6,0.7,0.8,0.9}; + +// switching probabilities +hole double WP1 in {0.5..0.9:0.05}; +hole double WP2 in {0.5..0.9:0.05}; + +// ----- modules --------------------------------------------------------------- + + +// clock + +module CLOCK + c : [0..1] init 0; + [tick00] c=0 -> (c'=1); + [tick01] c=0 -> (c'=1); + [tick02] c=0 -> (c'=1); + [tick1] c=1 -> (c'=0); +endmodule + + +// power manager + +module PM + pm : [0..2] init 0; // 0 - sleep, 1 - idle, 2 - active + [tick00] bat=1 -> (pm'=0); + [tick01] bat=1 -> (pm'=1); + [tick02] bat=1 -> (pm'=2); +endmodule + + +// service provider + +module SP + sp : [0..4] init 0; + // 0 - sleep, 1 - idle, 2 - active + // waiting states: 3 - sleep to idle, 4 - idle to active + + // immediate transitions - change to lower-energy (or same) state + [tick1] sp <= 2 & pm <= sp -> (sp'=pm); + + // transitions through waiting states - change to higher-energy state (sleep to idle or idle to active) + [tick1] sp <= 2 & pm > sp -> (sp'=sp+3); + + // waiting states + [tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true; + [tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true; + +endmodule + + +// service requester + +module SR + sr : [0..1] init 0; // 0 - idle, 1 - active + + [tick00] bat=1 -> 1: (sr'=0); + [tick01] bat=1 -> 1: (sr'=0); + [tick02] bat=1 -> 1: (sr'=0); + + [tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1); + + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1); + + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1); + + [tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1); + [tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1); + [tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1); + +endmodule + + +// service request queue +const int MAX_LOST = 10; + +module SRQ + q : [0..10000] init q_init; + lost : [0..MAX_LOST] init 0; + + [tick00] sr=1 & q < QMAX -> (q'=q+1); // request + [tick01] sr=1 & q < QMAX -> (q'=q+1); // request + [tick02] sr=1 & q < QMAX -> (q'=q+1); // request + + [tick00] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + [tick01] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + [tick02] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost + + [tick00] sr!=1 -> true; + [tick01] sr!=1 -> true; + [tick02] sr!=1 -> true; + + [tick1] sp=2 -> 1: (q'=max(q-1,0)); // serve + [tick1] sp!=2 -> true; + +endmodule + + +// battery + +module BAT + bat : [0..2] init 1; // 0 empty, 1 - operational, 2 - failed + [tick1] bat=0 -> true; + [tick1] bat=1 & sp!=2 -> 0.01 : (bat'=0) + 0.99 : true; + [tick1] bat=1 & sp=2 -> 0.01 : (bat'=0) + 0.01 : (bat'=2) + 0.98 : true; + [tick1] bat=2 -> true; +endmodule + +label "goal" = (bat = 0 & lost < MAX_LOST); diff --git a/models/mdp/sketches/dpm/switch-rates-big/sketch.templ b/models/mdp/sketches/dpm/switch-rates-big/sketch.templ index 92bbb275c..b93c0d394 100644 --- a/models/mdp/sketches/dpm/switch-rates-big/sketch.templ +++ b/models/mdp/sketches/dpm/switch-rates-big/sketch.templ @@ -30,8 +30,8 @@ hole double T2 in {0.5}; hole double T3 in {0.6,0.7,0.8,0.9}; // switching probabilities -hole double WP1 in {0.9,0.8,0.7}; -hole double WP2 in {0.7,0.6,0.5}; +hole double WP1 in {0.5..0.9:0.1}; +hole double WP2 in {0.5..0.9:0.1}; // ----- modules --------------------------------------------------------------- diff --git a/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props b/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props new file mode 100644 index 000000000..3a5cf8353 --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props @@ -0,0 +1 @@ +P >= 0.95 [ F (bat = 0 & lost = 0) ] diff --git a/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ b/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ new file mode 100644 index 000000000..c3cd18db6 --- /dev/null +++ b/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ @@ -0,0 +1,142 @@ +mdp + +// timing: +// tick-0: +// queue state is observed and state change is planned (pm) +// request are generated (if service requester is active) +// tick-1: +// requests are served +// state change is executed +// service requester changes its state +// battery depletes + +// initial queue size +const int q_init = 0; + +// ----- synthesized parameters ------------------------------------------------ + +// requester profiles +hole int P1 in {0,1,2}; +hole int P2 in {0,1,2}; +hole int P3 in {0,1,2}; +hole int P4 in {0,1,2}; + +// queue size +hole int QMAX in {10}; + +// observation level thresholds +hole double T1 in {0.0,0.1,0.2,0.3,0.4}; +hole double T2 in {0.5}; +hole double T3 in {0.6,0.7,0.8,0.9}; + +// switching probabilities +hole double WP1 in {0.9,0.8,0.7}; +hole double WP2 in {0.7,0.6,0.5}; + +// ----- modules --------------------------------------------------------------- + + +// clock + +module CLOCK + c : [0..1] init 0; + [tick00] c=0 -> (c'=1); + [tick01] c=0 -> (c'=1); + [tick02] c=0 -> (c'=1); + [tick1] c=1 -> (c'=0); +endmodule + + +// power manager + +module PM + pm : [0..2] init 0; // 0 - sleep, 1 - idle, 2 - active + [tick00] bat=1 -> (pm'=0); + [tick01] bat=1 -> (pm'=1); + [tick02] bat=1 -> (pm'=2); +endmodule + + +// service provider + +module SP + sp : [0..4] init 0; + // 0 - sleep, 1 - idle, 2 - active + // waiting states: 3 - sleep to idle, 4 - idle to active + + // immediate transitions - change to lower-energy (or same) state + [tick1] sp <= 2 & pm <= sp -> (sp'=pm); + + // transitions through waiting states - change to higher-energy state (sleep to idle or idle to active) + [tick1] sp <= 2 & pm > sp -> (sp'=sp+3); + + // waiting states + [tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true; + [tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true; + +endmodule + + +// service requester + +module SR + sr : [0..1] init 0; // 0 - idle, 1 - active + + [tick00] bat=1 -> 1: (sr'=0); + [tick01] bat=1 -> 1: (sr'=0); + [tick02] bat=1 -> 1: (sr'=0); + + [tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1); + [tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1); + + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1); + [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1); + + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1); + [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1); + + [tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1); + [tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1); + [tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1); + +endmodule + + +// service request queue + +module SRQ + q : [0..10000] init q_init; + lost : [0..1] init 0; + + [tick00] sr=1 & q < QMAX -> (q'=q+1); // request + [tick01] sr=1 & q < QMAX -> (q'=q+1); // request + [tick02] sr=1 & q < QMAX -> (q'=q+1); // request + + [tick00] sr=1 & q = QMAX -> (lost'=1); // request lost + [tick01] sr=1 & q = QMAX -> (lost'=1); // request lost + [tick02] sr=1 & q = QMAX -> (lost'=1); // request lost + + [tick00] sr!=1 -> true; + [tick01] sr!=1 -> true; + [tick02] sr!=1 -> true; + + [tick1] sp=2 -> 1: (q'=max(q-1,0)); // serve + [tick1] sp!=2 -> true; + +endmodule + + +// battery + +module BAT + bat : [0..2] init 1; // 0 empty, 1 - operational, 2 - failed + [tick1] bat=0 -> true; + [tick1] bat=1 & sp!=2 -> 0.05 : (bat'=0) + 0.95 : true; + [tick1] bat=1 & sp=2 -> 0.05 : (bat'=0) + 0.05 : (bat'=2) + 0.9 : true; + [tick1] bat=2 -> true; +endmodule + +label "goal" = (bat = 0 & lost = 0); diff --git a/models/mdp/sketches/dpm/switch-rates/sketch.templ b/models/mdp/sketches/dpm/switch-rates/sketch.templ index c3cd18db6..9e90a3b0b 100644 --- a/models/mdp/sketches/dpm/switch-rates/sketch.templ +++ b/models/mdp/sketches/dpm/switch-rates/sketch.templ @@ -22,7 +22,7 @@ hole int P3 in {0,1,2}; hole int P4 in {0,1,2}; // queue size -hole int QMAX in {10}; +hole int QMAX in {1..10}; // observation level thresholds hole double T1 in {0.0,0.1,0.2,0.3,0.4}; @@ -30,8 +30,8 @@ hole double T2 in {0.5}; hole double T3 in {0.6,0.7,0.8,0.9}; // switching probabilities -hole double WP1 in {0.9,0.8,0.7}; -hole double WP2 in {0.7,0.6,0.5}; +hole double WP1 in {0.5..0.9:0.1}; +hole double WP2 in {0.5..0.9:0.1}; // ----- modules --------------------------------------------------------------- diff --git a/models/mdp/sketches/rover/rover/sketch.props b/models/mdp/sketches/rover/rover-big/sketch.props similarity index 100% rename from models/mdp/sketches/rover/rover/sketch.props rename to models/mdp/sketches/rover/rover-big/sketch.props diff --git a/models/mdp/sketches/rover/rover-big/sketch.templ b/models/mdp/sketches/rover/rover-big/sketch.templ new file mode 100755 index 000000000..f9bcbfc1a --- /dev/null +++ b/models/mdp/sketches/rover/rover-big/sketch.templ @@ -0,0 +1,112 @@ +// Simplified model of a mars rover +// Encoding by Tim Quatmann and Sebastian Junges +// RWTH Aachen University + +mdp + + +const int num_tasks = 4; + +// time (in minutes) +//const int time_low = 5; +//const int time_medium = 8; +//const int time_high = 10; + +// Energy (in percent) +//const double energy_low = 0.99; +//const double energy_medium = 0.95; +//const double energy_high = 0.9; + +hole double energy_low in {0.999..0.9995:0.0001}; +hole double energy_medium in {0.996..0.9985:0.0005}; +hole double energy_high in {0.99..0.994:0.001}; + +// Scientific Value +//const int value_low = 2; +//const int value_medium = 10; +//const int value_high = 30; + +hole int value_low in {0..5:1}; +hole int value_medium in {10..20:2}; +hole int value_high in {25..50:5}; + +// Success probabilities +//const double task1_success_pr = 0.5; +//const double task2_success_pr = 0.6; +//const double task3_success_pr = 0.8; +//const double task4_success_pr = 0.2; + +hole double task1_success_pr in {0.4..0.6:0.1}; +hole double task2_success_pr in {0.5..0.7:0.1}; +hole double task3_success_pr in {0.8..1.0:0.1}; +hole double task4_success_pr in {0.1..0.3:0.1}; + +formula low_time_task = (task=2 | task=3); +formula medium_time_task = false; +formula high_time_task = (task=1 | task=4); + +formula low_energy_task = (task=1 | task=3); +formula medium_energy_task = (task=2); +formula high_energy_task = (task=4); + +formula low_value_task = (task=3); +formula medium_value_task = (task=1 | task=2); +formula high_value_task = (task=4); + +module rover + // The current task (0 means no task) + task : [0..num_tasks] init 0; + success : bool init false; + + [task1_start] task=0 -> task1_success_pr : (task'=1) & (success'=true) + (1-task1_success_pr) : (task'=1) & (success'=false); + [task2_start] task=0 -> task2_success_pr : (task'=2) & (success'=true) + (1-task2_success_pr) : (task'=2) & (success'=false); + [task3_start] task=0 -> task3_success_pr : (task'=3) & (success'=true) + (1-task3_success_pr) : (task'=3) & (success'=false); + [task4_start] task=0 -> task4_success_pr : (task'=4) & (success'=true) + (1-task4_success_pr) : (task'=4) & (success'=false); + + [task_done] task>0 -> (task'= 0) & (success'=false); +endmodule + + + +module battery + increased_energy : bool init false; + empty: bool init false; + + [task1_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task2_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task3_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task4_start] !empty -> (increased_energy' = false); + [task_done] !empty & low_energy_task & !increased_energy -> energy_low : (increased_energy' = false) + (1-energy_low) : (empty'=true); + [task_done] !empty & low_energy_task & increased_energy -> energy_medium : (increased_energy' = false) + (1-energy_medium) : (empty'=true); + [task_done] !empty & medium_energy_task & !increased_energy -> energy_medium : (increased_energy' = false) + (1-energy_medium) : (empty'=true); + [task_done] !empty & medium_energy_task & increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); + [task_done] !empty & high_energy_task & !increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); + [task_done] !empty & high_energy_task & increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); +endmodule + +const int V = 1000; +module value_counting_module + val : [0..V] init 0; + [task_done] low_value_task -> (val'=min(V,val + (success ? value_low : 0))); + [task_done] medium_value_task -> (val'=min(V,val + (success ? value_medium : 0))); + [task_done] high_value_task -> (val'=min(V,val + (success ? value_high : 0))); +endmodule + +//rewards "time" +// [task_done] low_time_task : time_low; +// [task_done] medium_time_task : time_medium; +// [task_done] high_time_task : time_high; +//endrewards +// +//rewards "energy" +// [task_done] low_energy_task & !increased_energy : energy_low; +// [task_done] low_energy_task & increased_energy : energy_medium; +// [task_done] medium_energy_task & !increased_energy : energy_medium; +// [task_done] medium_energy_task & increased_energy : energy_high; +// [task_done] high_energy_task & !increased_energy : energy_high; +// [task_done] high_energy_task & increased_energy : energy_high; +//endrewards + + +label "goal" = val = V; + diff --git a/models/mdp/sketches/rover/rover-constant-success/sketch.props b/models/mdp/sketches/rover/rover-constant-success/sketch.props new file mode 100755 index 000000000..8e528602a --- /dev/null +++ b/models/mdp/sketches/rover/rover-constant-success/sketch.props @@ -0,0 +1 @@ +P>=0.75 [F "goal"] diff --git a/models/mdp/sketches/rover/rover/sketch.templ b/models/mdp/sketches/rover/rover-constant-success/sketch.templ similarity index 100% rename from models/mdp/sketches/rover/rover/sketch.templ rename to models/mdp/sketches/rover/rover-constant-success/sketch.templ diff --git a/models/mdp/sketches/virus-new/sketch.props b/models/mdp/sketches/virus-new/sketch.props new file mode 100644 index 000000000..4f85f5011 --- /dev/null +++ b/models/mdp/sketches/virus-new/sketch.props @@ -0,0 +1 @@ +P>=0.5 [F s11=2] \ No newline at end of file diff --git a/models/mdp/sketches/virus-new/sketch.templ b/models/mdp/sketches/virus-new/sketch.templ new file mode 100644 index 000000000..018b6a479 --- /dev/null +++ b/models/mdp/sketches/virus-new/sketch.templ @@ -0,0 +1,308 @@ +mdp + +// probabilities +//const double infect=0.5; // probability virus infects a node +//const double detect1=0.5; // probability virus detected by firewall of high/low node +//const double detect2=0.8; // probability virus detected by firewall of barrier node + +hole double infect in {0.5..1.0: 0.1}; +hole double detect1 in {0.0..0.5 : 0.1}; +hole double detect2 in {0.5..1.0 : 0.1}; + +hole int level11 in {0,1}; +hole int level12 in {0,1}; +hole int level13 in {0,1}; + +hole int level21 in {0,1}; +hole int level22 in {0,1}; +hole int level23 in {0,1}; + +hole int level31 in {0,1}; +hole int level32 in {0,1}; +hole int level33 in {0,1}; + +// low nodes (those above the ceil(N/2) row) + +const double detect11= level11=0 ? detect1 : detect2; +const double detect12= level12=0 ? detect1 : detect2; +const double detect13= level13=0 ? detect1 : detect2; + +// barrier nodes (those in the ceil(N/2) row) + +const double detect21= level21=0 ? detect1 : detect2; +const double detect22= level22=0 ? detect1 : detect2; +const double detect23= level23=0 ? detect1 : detect2; + +// high nodes (those below the ceil(N/2) row) + +const double detect31= level31=0 ? detect1 : detect2; +const double detect32= level32=0 ? detect1 : detect2; +const double detect33= level33=0 ? detect1 : detect2; + +hole double fail_rate in {1.0}; + +// node1 that cannot be infected +hole int node1x in {1..2}; +hole int node1y in {2..3}; + +// node2 that cannot be infected +hole int node2x in {2..3}; +hole int node2y in {1..2}; + + +module strategy + step : [0..2] init 0; + + // Alternate between horizontal and vertical attack. Unclear how to start. + [attack23_33] step=0 & s33 = 2 & s11 != 2 & s21 != 2 & s31 != 2 & s12 != 2 & s22 != 2 & s32 != 2 & s13 != 2 & s23 != 2 -> (step'=1); + [attack32_33] step=0 & s33 = 2 & s11 != 2 & s21 != 2 & s31 != 2 & s12 != 2 & s22 != 2 & s32 != 2 & s13 != 2 & s23 != 2 -> (step'=1); + + // This part is clear. We just attack target if possible. + [attack11_21] step=0 & s21 = 2 -> (step'=1); + [attack11_12] step=0 & s12 = 2 -> (step'=1); + + [attack13_12] false -> true; + [attack23_22] false -> true; + [attack31_21] false -> true; + [attack32_22] false -> true; + + + // This part is also rather clear, we just have to decide whether we attack horizontal or vertical. No need to attack a non-neighbour. + [attack21_22] step=0 & s22 = 2 -> (step'=1); + [attack12_22] step=0 & s22 = 2 -> (step'=1); + + // s33 and s23 + [attack32_33] step=0 & s23 = 2 & s22 != 2 & s32 != 2 & s13 != 2 -> (step'=1); + [attack13_23] step=0 & s23 = 2 & s22 != 2 & s32 != 2 & s13 != 2 -> (step'=1); + [attack22_23] step=0 & s23 = 2 & s22 != 2 & s32 != 2 & s13 != 2 -> (step'=1); + + // s33 and s32 + [attack23_33] step=0 & s32 = 2 & s22 != 2 & s23 != 2 & s31 != 2 -> (step'=1); + [attack31_32] step=0 & s32 = 2 & s22 != 2 & s23 != 2 & s31 != 2 -> (step'=1); + [attack22_32] step=0 & s32 = 2 & s22 != 2 & s23 != 2 & s31 != 2 -> (step'=1); + + // s33 and s23 and s13 + [attack32_33] step=0 & s13 = 2 & s22 != 2 & s32 != 2 & s12 != 2 -> (step'=1); + [attack12_13] step=0 & s13 = 2 & s22 != 2 & s32 != 2 & s12 != 2 -> (step'=1); + [attack22_23] step=0 & s13 = 2 & s22 != 2 & s32 != 2 & s12 != 2 -> (step'=1); + + // s33 and s32 and s31 + [attack23_33] step=0 & s31 = 2 & s22 != 2 & s23 != 2 & s12 != 2 -> (step'=1); + [attack21_31] step=0 & s31 = 2 & s22 != 2 & s23 != 2 & s12 != 2 -> (step'=1); + [attack22_32] step=0 & s31 = 2 & s22 != 2 & s23 != 2 & s12 != 2 -> (step'=1); + + + // s33 and s32 and s23 + [attack31_32] step=0 & s32 = 2 & s23 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + [attack13_23] step=0 & s32 = 2 & s23 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + [attack22_32] step=0 & s32 = 2 & s23 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + + + // s33 and s32 and s31 and s23 + [attack13_23] step=0 & s31 = 2 & s23 = 2 & s22 != 2 & s21 != 2 & s13 != 2 -> (step'=1); + [attack21_31] step=0 & s31 = 2 & s23 = 2 & s22 != 2 & s21 != 2 & s13 != 2 -> (step'=1); + [attack22_23] step=0 & s31 = 2 & s23 = 2 & s22 != 2 & s21 != 2 & s13 != 2 -> (step'=1); + + + // s33 and s32 and s13 and s23 + [attack12_13] step=0 & s13 = 2 & s32 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + [attack31_32] step=0 & s13 = 2 & s32 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + [attack22_23] step=0 & s13 = 2 & s32 = 2 & s22 != 2 & s31 != 2 & s12 != 2 -> (step'=1); + + // s33 and s32 and s31 and s23 and s13 + [attack12_13] step=0 & s31 = 2 & s13 = 2 & s22 != 2 & s21 != 2 & s12 != 2 -> (step'=1); + [attack21_31] step=0 & s31 = 2 & s13 = 2 & s22 != 2 & s21 != 2 & s12 != 2 -> (step'=1); + [attack22_23] step=0 & s31 = 2 & s13 = 2 & s22 != 2 & s21 != 2 & s12 != 2 -> (step'=1); + + + [eval] step=1 -> (step'=2); + [report] step=2 -> (step'=0); + + [] s11 = 2 -> true; +endmodule + + +// first column (1..N) +module n11 + + s11 : [0..4]; // node uninfected + // 0 - node uninfected + // 1 - node uninfected but firewall breached + // 2 - node infected + // 3 - save mode + // 4 - infection taking place right now. + + // firewall attacked (from an infected neighbour) + [attack11_21] (s11=0) -> detect11 : true + (1-detect11) : (s11'=1); + [attack11_12] (s11=0) -> detect11 : true + (1-detect11) : (s11'=1); + // if the firewall has been breached tries to infect the node + [eval] (s11=1) -> infect : (s11'=4) + (1-infect) : (s11'=3); + // restore save mode + [eval] (s11=3) -> (s11'=0); + // never block eval. + [eval] (s11!=1) & (s11!=3) -> true; + + [report] (s11=4) -> (s11'=2); + [report] (s11!=4) -> true; + // if the node is infected, then it tries to attack its neighbouring nodes + [attack21_11] (s11=2) -> true; + [attack12_11] (s11=2) -> true; + +endmodule + +module n21 + + s21 : [0..4]; // node uninfected + // 0 - node uninfected + // 1 - node uninfected but firewall breached + // 2 - node infected + + // firewall attacked (from an infected neighbour) + [attack21_31] (s21=0) -> detect21 : true + (1-detect21) : (s21'=1); + [attack21_22] (s21=0) -> detect21 : true + (1-detect21) : (s21'=1); + [attack21_11] (s21=0) -> detect21 : true + (1-detect21) : (s21'=1); + // if the firewall has been breached tries to infect the node + [eval] (s21=1) -> infect : (s21'=4) + (1-infect) : (s21'=3); + // restore save mode + [eval] (s21=3) -> (s21'=0); + // never block eval. + [eval] (s21!=1) & (s21!=3) -> true; + [report] (s21=4) -> (s21'=2); + [report] (s21!=4) -> true; + + // if the node is infected, then it tries to attack its neighbouring nodes + [attack31_21] (s21=2) -> true; + [attack22_21] (s21=2) -> true; + [attack11_21] (s21=2) -> true; + +endmodule + +module n31=n11[s11=s31,detect11=detect31,attack21_11=attack21_31,attack12_11=attack32_31,attack11_21=attack31_21,attack11_12=attack31_32] endmodule + +// second column +module n12=n21[s21=s12,detect21=detect12,attack31_21=attack13_12,attack22_21=attack22_12,attack11_21=attack11_12,attack21_31=attack12_13,attack21_22=attack12_22,attack21_11=attack12_11] endmodule + +module n22 + + s22 : [0..4]; // node uninfected + // 0 - node uninfected + // 1 - node uninfected but firewall breached + // 2 - node infected + + // firewall attacked (from an infected neighbour) + [attack22_32] (s22=0) -> detect22 : true + (1-detect22) : (s22'=1); + [attack22_23] (s22=0) -> detect22 : true + (1-detect22) : (s22'=1); + [attack22_12] (s22=0) -> detect22 : true + (1-detect22) : (s22'=1); + [attack22_21] (s22=0) -> detect22 : true + (1-detect22) : (s22'=1); + // if the firewall has been breached tries to infect the node + [eval] (s22=1) -> infect : (s22'=4) + (1-infect) : (s22'=3); + // restore save mode + [eval] (s22=3) -> (s22'=0); + // never block eval. + [eval] (s22!=1) & (s22!=3) -> true; + [report] (s22=4) -> (s22'=2); + [report] (s22!=4) -> true; + // if the node is infected, then it tries to attack its neighbouring nodes + [attack32_22] (s22=2) -> true; + [attack23_22] (s22=2) -> true; + [attack12_22] (s22=2) -> true; + [attack21_22] (s22=2) -> true; + +endmodule + +module n32=n21[s21=s32,detect21=detect32,attack31_21=attack33_32,attack22_21=attack22_32,attack11_21=attack31_32,attack21_31=attack32_33,attack21_22=attack32_22,attack21_11=attack32_31] endmodule + +// columns 3..N-1 + +// column N +module n13=n11[s11=s13,detect11=detect13,attack21_11=attack23_13,attack12_11=attack12_13,attack11_21=attack13_23,attack11_12=attack13_12] endmodule +module n23=n21[s21=s23,detect21=detect23,attack31_21=attack33_23,attack22_21=attack22_23,attack11_21=attack13_23,attack21_31=attack23_33,attack21_22=attack23_22,attack21_11=attack23_13] endmodule + +module n33 + + s33 : [0..4] init 2; // node infected; + // 0 - node uninfected + // 1 - node uninfected but firewall breached + // 2 - node infected + + // firewall attacked (from an infected neighbour) + [attack33_32] (s33=0) -> detect33 : true + (1-detect33) : (s33'=1); + [attack33_23] (s33=0) -> detect33 : true + (1-detect33) : (s33'=1); + // if the firewall has been breached tries to infect the node + [eval] (s33=1) -> infect : (s33'=4) + (1-infect) : (s33'=3); + // restore save mode + [eval] (s33=3) -> (s33'=0); + // never block eval. + [eval] (s33!=1) & (s33!=3) -> true; + [report] (s33=4) -> (s33'=2); + [report] (s33!=4) -> true; + // if the node is infected, then it tries to attack its neighbouring nodes + [attack32_33] (s33=2) -> true; + [attack23_33] (s33=2) -> true; + +endmodule + + +module infect_fail + + fail : bool init false; + + [eval] !fail & (node1x = 1) & (node1y = 2) & (s12 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node1x = 1) & (node1y = 2) & (s12 <= 1) -> true; + [eval] !fail & (node1x = 2) & (node1y = 2) & (s22 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node1x = 2) & (node1y = 2) & (s22 <= 1) -> true; + [eval] !fail & (node1x = 1) & (node1y = 3) & (s13 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node1x = 1) & (node1y = 3) & (s13 <= 1) -> true; + [eval] !fail & (node1x = 2) & (node1y = 3) & (s23 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node1x = 2) & (node1y = 3) & (s23 <= 1) -> true; + + [eval] !fail & (node2x = 2) & (node2y = 1) & (s21 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node2x = 2) & (node2y = 1) & (s21 <= 1) -> true; + [eval] !fail & (node2x = 2) & (node2y = 2) & (s22 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node2x = 2) & (node2y = 2) & (s22 <= 1) -> true; + [eval] !fail & (node2x = 3) & (node2y = 1) & (s31 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node2x = 3) & (node2y = 1) & (s31 <= 1) -> true; + [eval] !fail & (node2x = 3) & (node2y = 2) & (s32 > 1) -> fail_rate: (fail'=true) + (1-fail_rate): true; + [eval] !fail & (node2x = 3) & (node2y = 2) & (s32 <= 1) -> true; + + [] fail -> true; + +endmodule + +// reward structure (number of attacks) +//rewards "attacks" +// +// // corner nodes +// +// [attack11_12] true : 1; +// [attack11_21] true : 1; +// [attack31_21] true : 1; +// [attack31_32] true : 1; +// [attack13_12] true : 1; +// [attack13_23] true : 1; +// [attack33_32] true : 1; +// [attack33_23] true : 1; +// +// // edge nodes +// +// [attack12_13] true : 1; +// [attack12_11] true : 1; +// [attack12_22] true : 1; +// [attack21_31] true : 1; +// [attack21_11] true : 1; +// [attack21_22] true : 1; +// [attack32_33] true : 1; +// [attack32_31] true : 1; +// [attack32_22] true : 1; +// [attack23_33] true : 1; +// [attack23_13] true : 1; +// [attack23_22] true : 1; +// +// // middle nodes +// +// [attack22_32] true : 1; +// [attack22_23] true : 1; +// [attack22_12] true : 1; +// [attack22_21] true : 1; +// +//endrewards \ No newline at end of file From 622893536a3cd396df0b9e2b60b023333222ac66 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 3 Jan 2024 01:49:24 +0100 Subject: [PATCH 4/4] added new mdp sketches --- .../sketch.props | 0 .../sketch.templ | 0 .../sketch.props | 0 .../sketch.templ | 0 .../sketch.props | 0 .../sketch.templ | 0 .../dpm/switch-rates-big/sketch.props | 1 - .../dpm/switch-rates-big/sketch.templ | 143 -------- .../dpm/{switch-rates => switch}/sketch.props | 0 .../dpm/{switch-rates => switch}/sketch.templ | 4 +- .../mdp/sketches/rover/100-big/sketch.props | 1 + .../mdp/sketches/rover/100-big/sketch.templ | 113 +++++++ .../rover/{rover-big => 100}/sketch.props | 0 .../rover/{rover-small => 100}/sketch.templ | 0 .../sketch.props | 0 .../sketch.templ | 0 models/mdp/sketches/rover/1000/sketch.props | 1 + .../rover/{rover-big => 1000}/sketch.templ | 8 +- .../sketches/rover/rover-small/sketch.props | 1 - .../sketches/uav/operator-big/sketch.props | 1 + .../sketches/uav/operator-big/sketch.templ | 312 +++++++++++++++++ .../uav/operator-roz-big/sketch.props | 1 + .../uav/operator-roz-big/sketch.templ | 315 ++++++++++++++++++ .../uav/operator-roz-workload/sketch.props | 1 + .../uav/operator-roz-workload/sketch.templ | 315 ++++++++++++++++++ .../sketches/uav/operator-roz/sketch.props | 2 +- .../sketches/uav/operator-roz/sketch.templ | 8 +- models/mdp/sketches/uav/operator/sketch.props | 2 +- models/mdp/sketches/uav/roz-big/sketch.props | 1 + models/mdp/sketches/uav/roz-big/sketch.templ | 313 +++++++++++++++++ models/mdp/sketches/uav/roz/sketch.props | 2 +- models/mdp/sketches/uav/roz/sketch.templ | 4 +- 32 files changed, 1389 insertions(+), 160 deletions(-) rename models/mdp/sketches/dpm/{switch-rates-big-q10-old => switch-big-q10-old}/sketch.props (100%) rename models/mdp/sketches/dpm/{switch-rates-big-q10-old => switch-big-q10-old}/sketch.templ (100%) rename models/mdp/sketches/dpm/{switch-rates-big-q10 => switch-big-q10}/sketch.props (100%) rename models/mdp/sketches/dpm/{switch-rates-big-q10 => switch-big-q10}/sketch.templ (100%) rename models/mdp/sketches/dpm/{switch-rates-q10-old => switch-q10-old}/sketch.props (100%) rename models/mdp/sketches/dpm/{switch-rates-q10-old => switch-q10-old}/sketch.templ (100%) delete mode 100644 models/mdp/sketches/dpm/switch-rates-big/sketch.props delete mode 100644 models/mdp/sketches/dpm/switch-rates-big/sketch.templ rename models/mdp/sketches/dpm/{switch-rates => switch}/sketch.props (100%) rename models/mdp/sketches/dpm/{switch-rates => switch}/sketch.templ (98%) create mode 100755 models/mdp/sketches/rover/100-big/sketch.props create mode 100755 models/mdp/sketches/rover/100-big/sketch.templ rename models/mdp/sketches/rover/{rover-big => 100}/sketch.props (100%) rename models/mdp/sketches/rover/{rover-small => 100}/sketch.templ (100%) rename models/mdp/sketches/rover/{rover-constant-success => 1000-constant-success}/sketch.props (100%) rename models/mdp/sketches/rover/{rover-constant-success => 1000-constant-success}/sketch.templ (100%) create mode 100755 models/mdp/sketches/rover/1000/sketch.props rename models/mdp/sketches/rover/{rover-big => 1000}/sketch.templ (96%) delete mode 100755 models/mdp/sketches/rover/rover-small/sketch.props create mode 100644 models/mdp/sketches/uav/operator-big/sketch.props create mode 100644 models/mdp/sketches/uav/operator-big/sketch.templ create mode 100644 models/mdp/sketches/uav/operator-roz-big/sketch.props create mode 100644 models/mdp/sketches/uav/operator-roz-big/sketch.templ create mode 100644 models/mdp/sketches/uav/operator-roz-workload/sketch.props create mode 100644 models/mdp/sketches/uav/operator-roz-workload/sketch.templ create mode 100644 models/mdp/sketches/uav/roz-big/sketch.props create mode 100644 models/mdp/sketches/uav/roz-big/sketch.templ diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props b/models/mdp/sketches/dpm/switch-big-q10-old/sketch.props similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.props rename to models/mdp/sketches/dpm/switch-big-q10-old/sketch.props diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ b/models/mdp/sketches/dpm/switch-big-q10-old/sketch.templ similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-big-q10-old/sketch.templ rename to models/mdp/sketches/dpm/switch-big-q10-old/sketch.templ diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props b/models/mdp/sketches/dpm/switch-big-q10/sketch.props similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-big-q10/sketch.props rename to models/mdp/sketches/dpm/switch-big-q10/sketch.props diff --git a/models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ b/models/mdp/sketches/dpm/switch-big-q10/sketch.templ similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-big-q10/sketch.templ rename to models/mdp/sketches/dpm/switch-big-q10/sketch.templ diff --git a/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props b/models/mdp/sketches/dpm/switch-q10-old/sketch.props similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-q10-old/sketch.props rename to models/mdp/sketches/dpm/switch-q10-old/sketch.props diff --git a/models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ b/models/mdp/sketches/dpm/switch-q10-old/sketch.templ similarity index 100% rename from models/mdp/sketches/dpm/switch-rates-q10-old/sketch.templ rename to models/mdp/sketches/dpm/switch-q10-old/sketch.templ diff --git a/models/mdp/sketches/dpm/switch-rates-big/sketch.props b/models/mdp/sketches/dpm/switch-rates-big/sketch.props deleted file mode 100644 index 07851960d..000000000 --- a/models/mdp/sketches/dpm/switch-rates-big/sketch.props +++ /dev/null @@ -1 +0,0 @@ -P >= 0.9 [ F (bat = 0 & lost = 0) ] diff --git a/models/mdp/sketches/dpm/switch-rates-big/sketch.templ b/models/mdp/sketches/dpm/switch-rates-big/sketch.templ deleted file mode 100644 index b93c0d394..000000000 --- a/models/mdp/sketches/dpm/switch-rates-big/sketch.templ +++ /dev/null @@ -1,143 +0,0 @@ -mdp - -// timing: -// tick-0: -// queue state is observed and state change is planned (pm) -// request are generated (if service requester is active) -// tick-1: -// requests are served -// state change is executed -// service requester changes its state -// battery depletes - -// initial queue size -const int q_init = 0; - -// ----- synthesized parameters ------------------------------------------------ - -// requester profiles -hole int P1 in {0,1,2}; -hole int P2 in {0,1,2}; -hole int P3 in {0,1,2}; -hole int P4 in {0,1,2}; - -// queue size -hole int QMAX in {10}; - -// observation level thresholds -hole double T1 in {0.0,0.1,0.2,0.3,0.4}; -hole double T2 in {0.5}; -hole double T3 in {0.6,0.7,0.8,0.9}; - -// switching probabilities -hole double WP1 in {0.5..0.9:0.1}; -hole double WP2 in {0.5..0.9:0.1}; - -// ----- modules --------------------------------------------------------------- - - -// clock - -module CLOCK - c : [0..1] init 0; - [tick00] c=0 -> (c'=1); - [tick01] c=0 -> (c'=1); - [tick02] c=0 -> (c'=1); - [tick1] c=1 -> (c'=0); -endmodule - - -// power manager - -module PM - pm : [0..2] init 0; // 0 - sleep, 1 - idle, 2 - active - [tick00] bat=1 -> (pm'=0); - [tick01] bat=1 -> (pm'=1); - [tick02] bat=1 -> (pm'=2); -endmodule - - -// service provider - -module SP - sp : [0..4] init 0; - // 0 - sleep, 1 - idle, 2 - active - // waiting states: 3 - sleep to idle, 4 - idle to active - - // immediate transitions - change to lower-energy (or same) state - [tick1] sp <= 2 & pm <= sp -> (sp'=pm); - - // transitions through waiting states - change to higher-energy state (sleep to idle or idle to active) - [tick1] sp <= 2 & pm > sp -> (sp'=sp+3); - - // waiting states - [tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true; - [tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true; - -endmodule - - -// service requester - -module SR - sr : [0..1] init 0; // 0 - idle, 1 - active - - [tick00] bat=1 -> 1: (sr'=0); - [tick01] bat=1 -> 1: (sr'=0); - [tick02] bat=1 -> 1: (sr'=0); - - [tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1); - [tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1); - [tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1); - - [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1); - [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1); - [tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1); - - [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1); - [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1); - [tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1); - - [tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1); - [tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1); - [tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1); - -endmodule - - -// service request queue -const int MAX_LOST = 10; - -module SRQ - q : [0..10000] init q_init; - lost : [0..MAX_LOST] init 0; - - [tick00] sr=1 & q < QMAX -> (q'=q+1); // request - [tick01] sr=1 & q < QMAX -> (q'=q+1); // request - [tick02] sr=1 & q < QMAX -> (q'=q+1); // request - - [tick00] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost - [tick01] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost - [tick02] sr=1 & q = QMAX -> (lost'=min(lost+1,MAX_LOST)); // request lost - - [tick00] sr!=1 -> true; - [tick01] sr!=1 -> true; - [tick02] sr!=1 -> true; - - [tick1] sp=2 -> 1: (q'=max(q-1,0)); // serve - [tick1] sp!=2 -> true; - -endmodule - - -// battery - -module BAT - bat : [0..2] init 1; // 0 empty, 1 - operational, 2 - failed - [tick1] bat=0 -> true; - [tick1] bat=1 & sp!=2 -> 0.01 : (bat'=0) + 0.99 : true; - [tick1] bat=1 & sp=2 -> 0.01 : (bat'=0) + 0.01 : (bat'=2) + 0.98 : true; - [tick1] bat=2 -> true; -endmodule - -label "goal" = (bat = 0 & lost < MAX_LOST); diff --git a/models/mdp/sketches/dpm/switch-rates/sketch.props b/models/mdp/sketches/dpm/switch/sketch.props similarity index 100% rename from models/mdp/sketches/dpm/switch-rates/sketch.props rename to models/mdp/sketches/dpm/switch/sketch.props diff --git a/models/mdp/sketches/dpm/switch-rates/sketch.templ b/models/mdp/sketches/dpm/switch/sketch.templ similarity index 98% rename from models/mdp/sketches/dpm/switch-rates/sketch.templ rename to models/mdp/sketches/dpm/switch/sketch.templ index 9e90a3b0b..50e74118b 100644 --- a/models/mdp/sketches/dpm/switch-rates/sketch.templ +++ b/models/mdp/sketches/dpm/switch/sketch.templ @@ -30,8 +30,8 @@ hole double T2 in {0.5}; hole double T3 in {0.6,0.7,0.8,0.9}; // switching probabilities -hole double WP1 in {0.5..0.9:0.1}; -hole double WP2 in {0.5..0.9:0.1}; +hole double WP1 in {0.5..0.9:0.05}; +hole double WP2 in {0.5..0.9:0.05}; // ----- modules --------------------------------------------------------------- diff --git a/models/mdp/sketches/rover/100-big/sketch.props b/models/mdp/sketches/rover/100-big/sketch.props new file mode 100755 index 000000000..ba9053303 --- /dev/null +++ b/models/mdp/sketches/rover/100-big/sketch.props @@ -0,0 +1 @@ +P>=0.8 [F "goal"] diff --git a/models/mdp/sketches/rover/100-big/sketch.templ b/models/mdp/sketches/rover/100-big/sketch.templ new file mode 100755 index 000000000..eb3cf4f23 --- /dev/null +++ b/models/mdp/sketches/rover/100-big/sketch.templ @@ -0,0 +1,113 @@ +// Simplified model of a mars rover +// Encoding by Tim Quatmann and Sebastian Junges +// RWTH Aachen University + +mdp + + +const int num_tasks = 4; + +// time (in minutes) +//const int time_low = 5; +//const int time_medium = 8; +//const int time_high = 10; + +// Energy (in percent) +//const double energy_low = 0.99; +//const double energy_medium = 0.95; +//const double energy_high = 0.9; + +hole double energy_low in {0.99..0.995:0.001}; +hole double energy_medium in {0.96..0.985:0.005}; +hole double energy_high in {0.9..0.94:0.01}; + +// Scientific Value +//const int value_low = 2; +//const int value_medium = 10; +//const int value_high = 30; + +hole int value_low in {0..5:1}; +hole int value_medium in {10..20:2}; +hole int value_high in {40..65:5}; + +// Success probabilities +//const double task1_success_pr = 0.5; +//const double task2_success_pr = 0.6; +//const double task3_success_pr = 0.8; +//const double task4_success_pr = 0.2; + +hole double task1_success_pr in {0.4..0.6:0.05}; +hole double task2_success_pr in {0.5..0.7:0.05}; +hole double task3_success_pr in {0.8..1.0:0.05}; +hole double task4_success_pr in {0.1..0.3:0.05}; + +formula low_time_task = (task=2 | task=3); +formula medium_time_task = false; +formula high_time_task = (task=1 | task=4); + +formula low_energy_task = (task=1 | task=3); +formula medium_energy_task = (task=2); +formula high_energy_task = (task=4); + +formula low_value_task = (task=3); +formula medium_value_task = (task=1 | task=2); +formula high_value_task = (task=4); + +module rover + // The current task (0 means no task) + task : [0..num_tasks] init 0; + success : bool init false; + + [task1_start] task=0 -> task1_success_pr : (task'=1) & (success'=true) + (1-task1_success_pr) : (task'=1) & (success'=false); + [task2_start] task=0 -> task2_success_pr : (task'=2) & (success'=true) + (1-task2_success_pr) : (task'=2) & (success'=false); + [task3_start] task=0 -> task3_success_pr : (task'=3) & (success'=true) + (1-task3_success_pr) : (task'=3) & (success'=false); + [task4_start] task=0 -> task4_success_pr : (task'=4) & (success'=true) + (1-task4_success_pr) : (task'=4) & (success'=false); + + [task_done] task>0 -> (task'= 0) & (success'=false); +endmodule + + + +module battery + increased_energy : bool init false; + empty: bool init false; + + [task1_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task2_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task3_start] !empty -> 0.5 : (increased_energy' = false) + (0.5) : (increased_energy' = true); + [task4_start] !empty -> (increased_energy' = false); + [task_done] !empty & low_energy_task & !increased_energy -> energy_low : (increased_energy' = false) + (1-energy_low) : (empty'=true); + [task_done] !empty & low_energy_task & increased_energy -> energy_medium : (increased_energy' = false) + (1-energy_medium) : (empty'=true); + [task_done] !empty & medium_energy_task & !increased_energy -> energy_medium : (increased_energy' = false) + (1-energy_medium) : (empty'=true); + [task_done] !empty & medium_energy_task & increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); + [task_done] !empty & high_energy_task & !increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); + [task_done] !empty & high_energy_task & increased_energy -> energy_high : (increased_energy' = false) + (1-energy_high) : (empty'=true); +endmodule + + +const int V = 100; +module value_counting_module + val : [0..V] init 0; + [task_done] low_value_task -> (val'=min(V,val + (success ? value_low : 0))); + [task_done] medium_value_task -> (val'=min(V,val + (success ? value_medium : 0))); + [task_done] high_value_task -> (val'=min(V,val + (success ? value_high : 0))); +endmodule + +//rewards "time" +// [task_done] low_time_task : time_low; +// [task_done] medium_time_task : time_medium; +// [task_done] high_time_task : time_high; +//endrewards +// +//rewards "energy" +// [task_done] low_energy_task & !increased_energy : energy_low; +// [task_done] low_energy_task & increased_energy : energy_medium; +// [task_done] medium_energy_task & !increased_energy : energy_medium; +// [task_done] medium_energy_task & increased_energy : energy_high; +// [task_done] high_energy_task & !increased_energy : energy_high; +// [task_done] high_energy_task & increased_energy : energy_high; +//endrewards + + +label "goal" = val = V; + diff --git a/models/mdp/sketches/rover/rover-big/sketch.props b/models/mdp/sketches/rover/100/sketch.props similarity index 100% rename from models/mdp/sketches/rover/rover-big/sketch.props rename to models/mdp/sketches/rover/100/sketch.props diff --git a/models/mdp/sketches/rover/rover-small/sketch.templ b/models/mdp/sketches/rover/100/sketch.templ similarity index 100% rename from models/mdp/sketches/rover/rover-small/sketch.templ rename to models/mdp/sketches/rover/100/sketch.templ diff --git a/models/mdp/sketches/rover/rover-constant-success/sketch.props b/models/mdp/sketches/rover/1000-constant-success/sketch.props similarity index 100% rename from models/mdp/sketches/rover/rover-constant-success/sketch.props rename to models/mdp/sketches/rover/1000-constant-success/sketch.props diff --git a/models/mdp/sketches/rover/rover-constant-success/sketch.templ b/models/mdp/sketches/rover/1000-constant-success/sketch.templ similarity index 100% rename from models/mdp/sketches/rover/rover-constant-success/sketch.templ rename to models/mdp/sketches/rover/1000-constant-success/sketch.templ diff --git a/models/mdp/sketches/rover/1000/sketch.props b/models/mdp/sketches/rover/1000/sketch.props new file mode 100755 index 000000000..ba9053303 --- /dev/null +++ b/models/mdp/sketches/rover/1000/sketch.props @@ -0,0 +1 @@ +P>=0.8 [F "goal"] diff --git a/models/mdp/sketches/rover/rover-big/sketch.templ b/models/mdp/sketches/rover/1000/sketch.templ similarity index 96% rename from models/mdp/sketches/rover/rover-big/sketch.templ rename to models/mdp/sketches/rover/1000/sketch.templ index f9bcbfc1a..e66e898b8 100755 --- a/models/mdp/sketches/rover/rover-big/sketch.templ +++ b/models/mdp/sketches/rover/1000/sketch.templ @@ -18,8 +18,8 @@ const int num_tasks = 4; //const double energy_high = 0.9; hole double energy_low in {0.999..0.9995:0.0001}; -hole double energy_medium in {0.996..0.9985:0.0005}; -hole double energy_high in {0.99..0.994:0.001}; +hole double energy_medium in {0.997..0.9995:0.0005}; +hole double energy_high in {0.994..0.999:0.001}; // Scientific Value //const int value_low = 2; @@ -27,8 +27,8 @@ hole double energy_high in {0.99..0.994:0.001}; //const int value_high = 30; hole int value_low in {0..5:1}; -hole int value_medium in {10..20:2}; -hole int value_high in {25..50:5}; +hole int value_medium in {20..30:2}; +hole int value_high in {75..100:5}; // Success probabilities //const double task1_success_pr = 0.5; diff --git a/models/mdp/sketches/rover/rover-small/sketch.props b/models/mdp/sketches/rover/rover-small/sketch.props deleted file mode 100755 index 8e528602a..000000000 --- a/models/mdp/sketches/rover/rover-small/sketch.props +++ /dev/null @@ -1 +0,0 @@ -P>=0.75 [F "goal"] diff --git a/models/mdp/sketches/uav/operator-big/sketch.props b/models/mdp/sketches/uav/operator-big/sketch.props new file mode 100644 index 000000000..c962fd94f --- /dev/null +++ b/models/mdp/sketches/uav/operator-big/sketch.props @@ -0,0 +1 @@ +P>=0.8 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-big/sketch.templ b/models/mdp/sketches/uav/operator-big/sketch.templ new file mode 100644 index 000000000..bf1366a8f --- /dev/null +++ b/models/mdp/sketches/uav/operator-big/sketch.templ @@ -0,0 +1,312 @@ +mdp + +// operator parameters +const double p=0.5; // probability of increasing workload due to other uncertain tasks +//const double accu_load1=0.5; // accuracy at the low workload level (real numbers between 0 and 1) +//const double accu_load2=0.9; // accuracy at the high workload level (real numbers between 0 and 1) +//const double fd=0.5; // accuracy discount due to fatigue (real numbers between 0 and 1) +//const int COUNTER; // fatigue threshold (integers, e.g, 10) +//const double risky2=0.5; // at w2: probability of choosing a risky route +//const double risky6=0.5; // at w6: probability of choosing a risky route + +global stop : bool init false; // done visiting all waypoints +formula roz = (r=8) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones + +hole int COUNTER in {1..20}; +hole double fd in {0.1..0.9 : 0.2}; +hole double accu_load1 in {0.7..1.0 : 0.1}; +hole double accu_load2 in {0.1..0.4 : 0.1}; + +hole double risky2 in {0.4..0.6:0.05}; +hole double risky6 in {0.4..0.6:0.05}; + +// OPERATOR MODEL +module operator + + k:[0..100] init 0; // fatigue level measured by completetd tasks + t:[0..2] init 0; // workload level + s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad + c:[0..3] init 0; // choices at the check point + + // image processing, the workload may increase due to other unknown tasks + [image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0); + // not fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1); + // fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2); + // not fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1); + // fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=2); + + // image analysis is bad, UAV need to wait at the waypoint and take another image + [wait] !stop & s=2 -> (t'=0) & (s'=0); + + // if image analysis is good, UAV can continue flying + // at check points, operator may suggest route for the UAV + + // w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3) + [go] !stop & s=1 & w=2 -> risky2:(c'=2) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=3) & (t'=0) & (s'=0) + +(1-risky2)/3:(c'=1) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=0) & (t'=0) & (s'=0); + + // w5 -> r3 (c=0)| r4 (c=1)| w4 (c=2) + [go] !stop & s=1 & w=5 -> 1/3:(c'=2) & (t'=0) & (s'=0) + 1/3:(c'=1) & (t'=0) & (s'=0) + + 1/3:(c'=0) & (t'=0) & (s'=0); + + // w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2) + [go] !stop & s=1 & w=6 -> risky6:(c'=2) & (t'=0) & (s'=0) + (1-risky6)/2:(c'=1) & (t'=0) & (s'=0) + + (1-risky6)/2:(c'=0) & (t'=0) & (s'=0); + + // at non-check-points, UAV has full autonomy to choose flying route + [go] !stop & s=1 & (w!=2 & w!=5 & w!=6) -> (t'=0) & (s'=0); + + // operator stops + [] !stop & w1 & w2 & w6 -> (stop'=true); + [operator_stop] stop -> true; + +endmodule + + +// UAV MODEL +module UAV + // UAV positions: + // inside a waypoint: w!=0, a=0, r=0 + // fly through certain angle of a waypoint: w!=0, a!=0, r=0 + // fly through a road point: w=0, a=0, r!=0 + w:[0..6] init 1; // waypoint + a:[0..8] init 0; // angle points + r:[0..9] init 0; // road points + send: bool init true; + in: bool init true; + // flag that a waypoint has been visited + w1: bool init true; + w2: bool init false; + w3: bool init false; + w4: bool init false; + w5: bool init false; + w6: bool init false; + + // at any waypoint: + // send image to human operator for analysis + [image] w!=0 & a=0 & r=0 & send -> (send'=false); + // wait at the waypoint and send another image + [wait] !send -> (send'=true); + // fly into a waypoint and take an image + [camera] w=1 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w1'=true); + [camera] w=2 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w2'=true); + [camera] w=3 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w3'=true); + [camera] w=4 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w4'=true); + [camera] w=5 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w5'=true); + [camera] w=6 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w6'=true); + // fly out of the waypoint via any angle point + [go] w!=0 & a=0 & r=0 -> 1/8:(a'=1) & (in'=false) + + 1/8:(a'=2) & (in'=false) + + 1/8:(a'=3) & (in'=false) + + 1/8:(a'=4) & (in'=false) + + 1/8:(a'=5) & (in'=false) + + 1/8:(a'=6) & (in'=false) + + 1/8:(a'=7) & (in'=false) + + 1/8:(a'=8) & (in'=false); + + + // UAV flying plans (based on the road map) + // check points: receiving commands from the operator + // w2 -> r5 |r6 |r7 |r9 + [flyw] c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5); + [flyw] c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6); + [flyw] c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7); + [flyw] c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9); + // w5 -> r3 | r4 | w4 (at any angle point) + [flyw] c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4); + [flyw] c=2 & w=5 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + // w6 -> r2 | r3 |r8 + [flyw] c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2); + [flyw] c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8); + + // non check points: fly autonomy + // w1 -> r1 | r9 + [flyw1] w=1 & (a!=0) & r=0 & !in -> (r'=1); + [flyw2] w=1 & (a!=0) & r=0 & !in -> (r'=9); + // w3 -> r6 | w4 (any angle point) + [flyw1] w=3 & (a!=0) & r=0 & !in -> (r'=6); + [flyw2] w=3 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + + // w4 -> w3 | w5 + [flyw1] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + + [flyw2] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r1 -> r2 | w1 + [fly1] r=1 -> (r'=2); + [fly2] r=1 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + // r2 -> r1 | w6 + [fly1] r=2 -> (r'=1); + [fly2] r=2 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r3 -> w5 | w6 + [fly1] r=3 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=3 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r4 -> r5 | w5 + [fly1] r=4 -> (r'=5); + [fly2] r=4 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r5 -> r4 | w2 + [fly1] r=5 -> (r'=4); + [fly2] r=5 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + // r6 -> w2 | w3 + [fly1] r=6 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=6 -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + // r7 -> w2 | r8 + [fly1] r=7 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=7 -> (r'=8); + // r8 -> w6 | r7 + [fly1] r=8 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=8 -> (r'=7); + // r9 -> w1 | w2 + [fly1] r=9 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=9 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + +endmodule + +module flight + + [wait] !roz -> 0.99: true + 0.01: (stop'=true); + [wait] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw1] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw2] roz -> 0.9: true + 0.1: (stop'=true); + + [fly1] !roz -> 0.99: true + 0.01: (stop'=true); + [fly1] roz -> 0.9: true + 0.1: (stop'=true); + + [fly2] !roz -> 0.99: true + 0.01: (stop'=true); + [fly2] roz -> 0.9: true + 0.1: (stop'=true); + +endmodule + + +// rewards "time" // flight time +// [wait] true: 10; +// [fly] true: 60; +// endrewards +// +// rewards "ROZ" // ROZ occupancy +// [fly] roz : 1; +// endrewards \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz-big/sketch.props b/models/mdp/sketches/uav/operator-roz-big/sketch.props new file mode 100644 index 000000000..ad2078aa1 --- /dev/null +++ b/models/mdp/sketches/uav/operator-roz-big/sketch.props @@ -0,0 +1 @@ +P>=0.75 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz-big/sketch.templ b/models/mdp/sketches/uav/operator-roz-big/sketch.templ new file mode 100644 index 000000000..e27a46c2c --- /dev/null +++ b/models/mdp/sketches/uav/operator-roz-big/sketch.templ @@ -0,0 +1,315 @@ +mdp + +// operator parameters +const double p=0.5; // probability of increasing workload due to other uncertain tasks +//const double accu_load1=0.5; // accuracy at the low workload level (real numbers between 0 and 1) +//const double accu_load2=0.9; // accuracy at the high workload level (real numbers between 0 and 1) +//const double fd=0.5; // accuracy discount due to fatigue (real numbers between 0 and 1) +//const int COUNTER; // fatigue threshold (integers, e.g, 10) +//const double risky2=0.5; // at w2: probability of choosing a risky route +//const double risky6=0.5; // at w6: probability of choosing a risky route + +global stop : bool init false; // done visiting all waypoints +formula roz = (r=roz_r_1) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones + +hole int COUNTER in {1..20}; +hole double fd in {0.1..0.9:0.2}; +hole double accu_load1 in {0.7..1.0:0.1}; +hole double accu_load2 in {0.1..0.4:0.1}; +//hole double p in {0.1..0.5:0.1}; + +hole double risky2 in {0.4..0.6:0.05}; +hole double risky6 in {0.4..0.6:0.05}; + +hole int roz_r_1 in {1..9}; + +// OPERATOR MODEL +module operator + + k:[0..100] init 0; // fatigue level measured by completetd tasks + t:[0..2] init 0; // workload level + s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad + c:[0..3] init 0; // choices at the check point + + // image processing, the workload may increase due to other unknown tasks + [image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0); + // not fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1); + // fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2); + // not fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1); + // fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=2); + + // image analysis is bad, UAV need to wait at the waypoint and take another image + [wait] !stop & s=2 -> (t'=0) & (s'=0); + + // if image analysis is good, UAV can continue flying + // at check points, operator may suggest route for the UAV + + // w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3) + [go] !stop & s=1 & w=2 -> risky2:(c'=2) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=3) & (t'=0) & (s'=0) + +(1-risky2)/3:(c'=1) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=0) & (t'=0) & (s'=0); + + // w5 -> r3 (c=0)| r4 (c=1)| w4 (c=2) + [go] !stop & s=1 & w=5 -> 1/3:(c'=2) & (t'=0) & (s'=0) + 1/3:(c'=1) & (t'=0) & (s'=0) + + 1/3:(c'=0) & (t'=0) & (s'=0); + + // w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2) + [go] !stop & s=1 & w=6 -> risky6:(c'=2) & (t'=0) & (s'=0) + (1-risky6)/2:(c'=1) & (t'=0) & (s'=0) + + (1-risky6)/2:(c'=0) & (t'=0) & (s'=0); + + // at non-check-points, UAV has full autonomy to choose flying route + [go] !stop & s=1 & (w!=2 & w!=5 & w!=6) -> (t'=0) & (s'=0); + + // operator stops + [] !stop & w1 & w2 & w6 -> (stop'=true); + [operator_stop] stop -> true; + +endmodule + + +// UAV MODEL +module UAV + // UAV positions: + // inside a waypoint: w!=0, a=0, r=0 + // fly through certain angle of a waypoint: w!=0, a!=0, r=0 + // fly through a road point: w=0, a=0, r!=0 + w:[0..6] init 1; // waypoint + a:[0..8] init 0; // angle points + r:[0..9] init 0; // road points + send: bool init true; + in: bool init true; + // flag that a waypoint has been visited + w1: bool init true; + w2: bool init false; + w3: bool init false; + w4: bool init false; + w5: bool init false; + w6: bool init false; + + // at any waypoint: + // send image to human operator for analysis + [image] w!=0 & a=0 & r=0 & send -> (send'=false); + // wait at the waypoint and send another image + [wait] !send -> (send'=true); + // fly into a waypoint and take an image + [camera] w=1 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w1'=true); + [camera] w=2 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w2'=true); + [camera] w=3 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w3'=true); + [camera] w=4 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w4'=true); + [camera] w=5 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w5'=true); + [camera] w=6 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w6'=true); + // fly out of the waypoint via any angle point + [go] w!=0 & a=0 & r=0 -> 1/8:(a'=1) & (in'=false) + + 1/8:(a'=2) & (in'=false) + + 1/8:(a'=3) & (in'=false) + + 1/8:(a'=4) & (in'=false) + + 1/8:(a'=5) & (in'=false) + + 1/8:(a'=6) & (in'=false) + + 1/8:(a'=7) & (in'=false) + + 1/8:(a'=8) & (in'=false); + + + // UAV flying plans (based on the road map) + // check points: receiving commands from the operator + // w2 -> r5 |r6 |r7 |r9 + [flyw] c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5); + [flyw] c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6); + [flyw] c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7); + [flyw] c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9); + // w5 -> r3 | r4 | w4 (at any angle point) + [flyw] c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4); + [flyw] c=2 & w=5 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + // w6 -> r2 | r3 |r8 + [flyw] c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2); + [flyw] c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8); + + // non check points: fly autonomy + // w1 -> r1 | r9 + [flyw1] w=1 & (a!=0) & r=0 & !in -> (r'=1); + [flyw2] w=1 & (a!=0) & r=0 & !in -> (r'=9); + // w3 -> r6 | w4 (any angle point) + [flyw1] w=3 & (a!=0) & r=0 & !in -> (r'=6); + [flyw2] w=3 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + + // w4 -> w3 | w5 + [flyw1] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + + [flyw2] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r1 -> r2 | w1 + [fly1] r=1 -> (r'=2); + [fly2] r=1 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + // r2 -> r1 | w6 + [fly1] r=2 -> (r'=1); + [fly2] r=2 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r3 -> w5 | w6 + [fly1] r=3 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=3 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r4 -> r5 | w5 + [fly1] r=4 -> (r'=5); + [fly2] r=4 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r5 -> r4 | w2 + [fly1] r=5 -> (r'=4); + [fly2] r=5 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + // r6 -> w2 | w3 + [fly1] r=6 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=6 -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + // r7 -> w2 | r8 + [fly1] r=7 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=7 -> (r'=8); + // r8 -> w6 | r7 + [fly1] r=8 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=8 -> (r'=7); + // r9 -> w1 | w2 + [fly1] r=9 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=9 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + +endmodule + +module flight + + [wait] !roz -> 0.99: true + 0.01: (stop'=true); + [wait] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw1] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw2] roz -> 0.9: true + 0.1: (stop'=true); + + [fly1] !roz -> 0.99: true + 0.01: (stop'=true); + [fly1] roz -> 0.9: true + 0.1: (stop'=true); + + [fly2] !roz -> 0.99: true + 0.01: (stop'=true); + [fly2] roz -> 0.9: true + 0.1: (stop'=true); + +endmodule + + +// rewards "time" // flight time +// [wait] true: 10; +// [fly] true: 60; +// endrewards +// +// rewards "ROZ" // ROZ occupancy +// [fly] roz : 1; +// endrewards \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz-workload/sketch.props b/models/mdp/sketches/uav/operator-roz-workload/sketch.props new file mode 100644 index 000000000..41d21ecfa --- /dev/null +++ b/models/mdp/sketches/uav/operator-roz-workload/sketch.props @@ -0,0 +1 @@ +P>=0.7 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz-workload/sketch.templ b/models/mdp/sketches/uav/operator-roz-workload/sketch.templ new file mode 100644 index 000000000..c97816d7c --- /dev/null +++ b/models/mdp/sketches/uav/operator-roz-workload/sketch.templ @@ -0,0 +1,315 @@ +mdp + +// operator parameters +//const double p=0.5; // probability of increasing workload due to other uncertain tasks +//const double accu_load1=0.5; // accuracy at the low workload level (real numbers between 0 and 1) +//const double accu_load2=0.9; // accuracy at the high workload level (real numbers between 0 and 1) +//const double fd=0.5; // accuracy discount due to fatigue (real numbers between 0 and 1) +//const int COUNTER; // fatigue threshold (integers, e.g, 10) +//const double risky2=0.5; // at w2: probability of choosing a risky route +//const double risky6=0.5; // at w6: probability of choosing a risky route + +global stop : bool init false; // done visiting all waypoints +formula roz = (r=roz_r_1) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones + +hole int COUNTER in {1..10}; +hole double fd in {0.1..0.9:0.1}; +hole double accu_load1 in {0.7..1.0:0.1}; +hole double accu_load2 in {0.1..0.4:0.1}; +hole double p in {0.1..0.5:0.1}; + +hole double risky2 in {0.4..0.6:0.05}; +hole double risky6 in {0.4..0.6:0.05}; + +hole int roz_r_1 in {1..9}; + +// OPERATOR MODEL +module operator + + k:[0..100] init 0; // fatigue level measured by completetd tasks + t:[0..2] init 0; // workload level + s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad + c:[0..3] init 0; // choices at the check point + + // image processing, the workload may increase due to other unknown tasks + [image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0); + // not fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1); + // fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2); + // not fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1); + // fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=2); + + // image analysis is bad, UAV need to wait at the waypoint and take another image + [wait] !stop & s=2 -> (t'=0) & (s'=0); + + // if image analysis is good, UAV can continue flying + // at check points, operator may suggest route for the UAV + + // w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3) + [go] !stop & s=1 & w=2 -> risky2:(c'=2) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=3) & (t'=0) & (s'=0) + +(1-risky2)/3:(c'=1) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=0) & (t'=0) & (s'=0); + + // w5 -> r3 (c=0)| r4 (c=1)| w4 (c=2) + [go] !stop & s=1 & w=5 -> 1/3:(c'=2) & (t'=0) & (s'=0) + 1/3:(c'=1) & (t'=0) & (s'=0) + + 1/3:(c'=0) & (t'=0) & (s'=0); + + // w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2) + [go] !stop & s=1 & w=6 -> risky6:(c'=2) & (t'=0) & (s'=0) + (1-risky6)/2:(c'=1) & (t'=0) & (s'=0) + + (1-risky6)/2:(c'=0) & (t'=0) & (s'=0); + + // at non-check-points, UAV has full autonomy to choose flying route + [go] !stop & s=1 & (w!=2 & w!=5 & w!=6) -> (t'=0) & (s'=0); + + // operator stops + [] !stop & w1 & w2 & w6 -> (stop'=true); + [operator_stop] stop -> true; + +endmodule + + +// UAV MODEL +module UAV + // UAV positions: + // inside a waypoint: w!=0, a=0, r=0 + // fly through certain angle of a waypoint: w!=0, a!=0, r=0 + // fly through a road point: w=0, a=0, r!=0 + w:[0..6] init 1; // waypoint + a:[0..8] init 0; // angle points + r:[0..9] init 0; // road points + send: bool init true; + in: bool init true; + // flag that a waypoint has been visited + w1: bool init true; + w2: bool init false; + w3: bool init false; + w4: bool init false; + w5: bool init false; + w6: bool init false; + + // at any waypoint: + // send image to human operator for analysis + [image] w!=0 & a=0 & r=0 & send -> (send'=false); + // wait at the waypoint and send another image + [wait] !send -> (send'=true); + // fly into a waypoint and take an image + [camera] w=1 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w1'=true); + [camera] w=2 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w2'=true); + [camera] w=3 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w3'=true); + [camera] w=4 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w4'=true); + [camera] w=5 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w5'=true); + [camera] w=6 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w6'=true); + // fly out of the waypoint via any angle point + [go] w!=0 & a=0 & r=0 -> 1/8:(a'=1) & (in'=false) + + 1/8:(a'=2) & (in'=false) + + 1/8:(a'=3) & (in'=false) + + 1/8:(a'=4) & (in'=false) + + 1/8:(a'=5) & (in'=false) + + 1/8:(a'=6) & (in'=false) + + 1/8:(a'=7) & (in'=false) + + 1/8:(a'=8) & (in'=false); + + + // UAV flying plans (based on the road map) + // check points: receiving commands from the operator + // w2 -> r5 |r6 |r7 |r9 + [flyw] c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5); + [flyw] c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6); + [flyw] c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7); + [flyw] c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9); + // w5 -> r3 | r4 | w4 (at any angle point) + [flyw] c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4); + [flyw] c=2 & w=5 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + // w6 -> r2 | r3 |r8 + [flyw] c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2); + [flyw] c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8); + + // non check points: fly autonomy + // w1 -> r1 | r9 + [flyw1] w=1 & (a!=0) & r=0 & !in -> (r'=1); + [flyw2] w=1 & (a!=0) & r=0 & !in -> (r'=9); + // w3 -> r6 | w4 (any angle point) + [flyw1] w=3 & (a!=0) & r=0 & !in -> (r'=6); + [flyw2] w=3 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + + // w4 -> w3 | w5 + [flyw1] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + + [flyw2] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r1 -> r2 | w1 + [fly1] r=1 -> (r'=2); + [fly2] r=1 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + // r2 -> r1 | w6 + [fly1] r=2 -> (r'=1); + [fly2] r=2 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r3 -> w5 | w6 + [fly1] r=3 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=3 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r4 -> r5 | w5 + [fly1] r=4 -> (r'=5); + [fly2] r=4 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r5 -> r4 | w2 + [fly1] r=5 -> (r'=4); + [fly2] r=5 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + // r6 -> w2 | w3 + [fly1] r=6 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=6 -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + // r7 -> w2 | r8 + [fly1] r=7 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=7 -> (r'=8); + // r8 -> w6 | r7 + [fly1] r=8 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=8 -> (r'=7); + // r9 -> w1 | w2 + [fly1] r=9 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=9 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + +endmodule + +module flight + + [wait] !roz -> 0.99: true + 0.01: (stop'=true); + [wait] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw1] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw2] roz -> 0.9: true + 0.1: (stop'=true); + + [fly1] !roz -> 0.99: true + 0.01: (stop'=true); + [fly1] roz -> 0.9: true + 0.1: (stop'=true); + + [fly2] !roz -> 0.99: true + 0.01: (stop'=true); + [fly2] roz -> 0.9: true + 0.1: (stop'=true); + +endmodule + + +// rewards "time" // flight time +// [wait] true: 10; +// [fly] true: 60; +// endrewards +// +// rewards "ROZ" // ROZ occupancy +// [fly] roz : 1; +// endrewards \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz/sketch.props b/models/mdp/sketches/uav/operator-roz/sketch.props index 8f96513d6..ad2078aa1 100644 --- a/models/mdp/sketches/uav/operator-roz/sketch.props +++ b/models/mdp/sketches/uav/operator-roz/sketch.props @@ -1 +1 @@ -P>=0.9 [ F w1&w2&w6 ] \ No newline at end of file +P>=0.75 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/operator-roz/sketch.templ b/models/mdp/sketches/uav/operator-roz/sketch.templ index 8d5964847..7c37d832a 100644 --- a/models/mdp/sketches/uav/operator-roz/sketch.templ +++ b/models/mdp/sketches/uav/operator-roz/sketch.templ @@ -13,10 +13,10 @@ global stop : bool init false; // done visiting all waypoints formula roz = (r=roz_r_1) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones hole int COUNTER in {1..20}; -hole double fd in {0.1,0.3,0.5,0.7,0.9}; -hole double accu_load1 in {0.7,0.8,0.9,1.0}; -hole double accu_load2 in {0.1,0.2,0.3,0.4}; -//hole double p in {0.1,0.2,0.3,0.4,0.5}; +hole double fd in {0.1..0.9:0.2}; +hole double accu_load1 in {0.7..1.0:0.1}; +hole double accu_load2 in {0.1..0.4:0.1}; +//hole double p in {0.1..0.5:0.1}; hole int roz_r_1 in {1..9}; diff --git a/models/mdp/sketches/uav/operator/sketch.props b/models/mdp/sketches/uav/operator/sketch.props index 8f96513d6..c962fd94f 100644 --- a/models/mdp/sketches/uav/operator/sketch.props +++ b/models/mdp/sketches/uav/operator/sketch.props @@ -1 +1 @@ -P>=0.9 [ F w1&w2&w6 ] \ No newline at end of file +P>=0.8 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/roz-big/sketch.props b/models/mdp/sketches/uav/roz-big/sketch.props new file mode 100644 index 000000000..ad2078aa1 --- /dev/null +++ b/models/mdp/sketches/uav/roz-big/sketch.props @@ -0,0 +1 @@ +P>=0.75 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/roz-big/sketch.templ b/models/mdp/sketches/uav/roz-big/sketch.templ new file mode 100644 index 000000000..78f043170 --- /dev/null +++ b/models/mdp/sketches/uav/roz-big/sketch.templ @@ -0,0 +1,313 @@ +mdp + +// operator parameters +//const double p=0.5; // probability of increasing workload due to other uncertain tasks +const double accu_load1=0.8; // accuracy at the low workload level (real numbers between 0 and 1) +const double accu_load2=0.2; // accuracy at the high workload level (real numbers between 0 and 1) +//const double fd=0.5; // accuracy discount due to fatigue (real numbers between 0 and 1) +//const int COUNTER; // fatigue threshold (integers, e.g, 10) +//const double risky2=0.5; // at w2: probability of choosing a risky route +//const double risky6=0.5; // at w6: probability of choosing a risky route + +global stop : bool init false; // done visiting all waypoints +formula roz = (r=roz_r_1) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones + +hole int COUNTER in {1..20}; +hole double fd in {0.1..0.9:0.2}; +hole double p in {0.1..0.5:0.1}; + +hole double risky2 in {0.4..0.6:0.1}; +hole double risky6 in {0.4..0.6:0.1}; + +hole int roz_r_1 in {1..9}; + +// OPERATOR MODEL +module operator + + k:[0..100] init 0; // fatigue level measured by completetd tasks + t:[0..2] init 0; // workload level + s:[0..2] init 0; // status of image processing, 0: init, 1: good, 2: bad + c:[0..3] init 0; // choices at the check point + + // image processing, the workload may increase due to other unknown tasks + [image] !stop & t=0 & s=0 -> (1-p):(t'=1) & (s'=0) + p:(t'=2) & (s'=0); + // not fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k<=COUNTER -> accu_load1:(s'=1)&(k'=k+1) + (1-accu_load1):(s'=2)&(k'=k+1); + // fatigue, workload level 1 + [process] !stop & t=1 & s=0 & k>COUNTER -> accu_load1*fd:(s'=1) + (1-accu_load1*fd):(s'=2); + // not fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k<=COUNTER -> accu_load2:(s'=1)&(k'=k+1) + (1-accu_load2):(s'=2)&(k'=k+1); + // fatigue, workload level 2 + [process] !stop & t=2 & s=0 & k>COUNTER -> accu_load2*fd:(s'=1) + (1-accu_load2*fd):(s'=2); + + // image analysis is bad, UAV need to wait at the waypoint and take another image + [wait] !stop & s=2 -> (t'=0) & (s'=0); + + // if image analysis is good, UAV can continue flying + // at check points, operator may suggest route for the UAV + + // w2 -> r5 (c=0) |r6 (c=1) |r7 (c=2)|r9 (c=3) + [go] !stop & s=1 & w=2 -> risky2:(c'=2) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=3) & (t'=0) & (s'=0) + +(1-risky2)/3:(c'=1) & (t'=0) & (s'=0) + (1-risky2)/3:(c'=0) & (t'=0) & (s'=0); + + // w5 -> r3 (c=0)| r4 (c=1)| w4 (c=2) + [go] !stop & s=1 & w=5 -> 1/3:(c'=2) & (t'=0) & (s'=0) + 1/3:(c'=1) & (t'=0) & (s'=0) + + 1/3:(c'=0) & (t'=0) & (s'=0); + + // w6 -> r2 (c=0)| r3 (c=1) |r8 (c=2) + [go] !stop & s=1 & w=6 -> risky6:(c'=2) & (t'=0) & (s'=0) + (1-risky6)/2:(c'=1) & (t'=0) & (s'=0) + + (1-risky6)/2:(c'=0) & (t'=0) & (s'=0); + + // at non-check-points, UAV has full autonomy to choose flying route + [go] !stop & s=1 & (w!=2 & w!=5 & w!=6) -> (t'=0) & (s'=0); + + // operator stops + [] !stop & w1 & w2 & w6 -> (stop'=true); + [operator_stop] stop -> true; + +endmodule + + +// UAV MODEL +module UAV + // UAV positions: + // inside a waypoint: w!=0, a=0, r=0 + // fly through certain angle of a waypoint: w!=0, a!=0, r=0 + // fly through a road point: w=0, a=0, r!=0 + w:[0..6] init 1; // waypoint + a:[0..8] init 0; // angle points + r:[0..9] init 0; // road points + send: bool init true; + in: bool init true; + // flag that a waypoint has been visited + w1: bool init true; + w2: bool init false; + w3: bool init false; + w4: bool init false; + w5: bool init false; + w6: bool init false; + + // at any waypoint: + // send image to human operator for analysis + [image] w!=0 & a=0 & r=0 & send -> (send'=false); + // wait at the waypoint and send another image + [wait] !send -> (send'=true); + // fly into a waypoint and take an image + [camera] w=1 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w1'=true); + [camera] w=2 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w2'=true); + [camera] w=3 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w3'=true); + [camera] w=4 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w4'=true); + [camera] w=5 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w5'=true); + [camera] w=6 & a!=0 & r=0 & in -> (a'=0) & (send'=true) & (w6'=true); + // fly out of the waypoint via any angle point + [go] w!=0 & a=0 & r=0 -> 1/8:(a'=1) & (in'=false) + + 1/8:(a'=2) & (in'=false) + + 1/8:(a'=3) & (in'=false) + + 1/8:(a'=4) & (in'=false) + + 1/8:(a'=5) & (in'=false) + + 1/8:(a'=6) & (in'=false) + + 1/8:(a'=7) & (in'=false) + + 1/8:(a'=8) & (in'=false); + + + // UAV flying plans (based on the road map) + // check points: receiving commands from the operator + // w2 -> r5 |r6 |r7 |r9 + [flyw] c=0 & w=2 & (a!=0) & r=0 & !in -> (r'=5); + [flyw] c=1 & w=2 & (a!=0) & r=0 & !in -> (r'=6); + [flyw] c=2 & w=2 & (a!=0) & r=0 & !in -> (r'=7); + [flyw] c=3 & w=2 & (a!=0) & r=0 & !in -> (r'=9); + // w5 -> r3 | r4 | w4 (at any angle point) + [flyw] c=0 & w=5 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=1 & w=5 & (a!=0) & r=0 & !in -> (r'=4); + [flyw] c=2 & w=5 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + // w6 -> r2 | r3 |r8 + [flyw] c=0 & w=6 & (a!=0) & r=0 & !in -> (r'=2); + [flyw] c=1 & w=6 & (a!=0) & r=0 & !in -> (r'=3); + [flyw] c=2 & w=6 & (a!=0) & r=0 & !in -> (r'=8); + + // non check points: fly autonomy + // w1 -> r1 | r9 + [flyw1] w=1 & (a!=0) & r=0 & !in -> (r'=1); + [flyw2] w=1 & (a!=0) & r=0 & !in -> (r'=9); + // w3 -> r6 | w4 (any angle point) + [flyw1] w=3 & (a!=0) & r=0 & !in -> (r'=6); + [flyw2] w=3 & (a!=0) & r=0 & !in -> 1/8:(w'=4) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=4) & (a'=8) & (r'=0) & (in'=true); + + // w4 -> w3 | w5 + [flyw1] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + + [flyw2] w=4 & (a!=0) & r=0 & !in -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r1 -> r2 | w1 + [fly1] r=1 -> (r'=2); + [fly2] r=1 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + // r2 -> r1 | w6 + [fly1] r=2 -> (r'=1); + [fly2] r=2 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r3 -> w5 | w6 + [fly1] r=3 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=3 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + // r4 -> r5 | w5 + [fly1] r=4 -> (r'=5); + [fly2] r=4 -> 1/8:(w'=5) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=5) & (a'=8) & (r'=0) & (in'=true); + // r5 -> r4 | w2 + [fly1] r=5 -> (r'=4); + [fly2] r=5 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + // r6 -> w2 | w3 + [fly1] r=6 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=6 -> 1/8:(w'=3) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=3) & (a'=8) & (r'=0) & (in'=true); + // r7 -> w2 | r8 + [fly1] r=7 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=7 -> (r'=8); + // r8 -> w6 | r7 + [fly1] r=8 -> 1/8:(w'=6) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=6) & (a'=8) & (r'=0) & (in'=true); + [fly2] r=8 -> (r'=7); + // r9 -> w1 | w2 + [fly1] r=9 -> 1/8:(w'=1) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=1) & (a'=8) & (r'=0) & (in'=true); + + [fly2] r=9 -> 1/8:(w'=2) & (a'=1) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=2) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=3) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=4) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=5) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=6) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=7) & (r'=0) & (in'=true) + + 1/8:(w'=2) & (a'=8) & (r'=0) & (in'=true); + +endmodule + +module flight + + [wait] !roz -> 0.99: true + 0.01: (stop'=true); + [wait] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw] roz -> 0.9: true + 0.1: (stop'=true); + + [flyw1] !roz -> 0.99: true + 0.01: (stop'=true); + [flyw2] roz -> 0.9: true + 0.1: (stop'=true); + + [fly1] !roz -> 0.99: true + 0.01: (stop'=true); + [fly1] roz -> 0.9: true + 0.1: (stop'=true); + + [fly2] !roz -> 0.99: true + 0.01: (stop'=true); + [fly2] roz -> 0.9: true + 0.1: (stop'=true); + +endmodule + + +// rewards "time" // flight time +// [wait] true: 10; +// [fly] true: 60; +// endrewards +// +// rewards "ROZ" // ROZ occupancy +// [fly] roz : 1; +// endrewards \ No newline at end of file diff --git a/models/mdp/sketches/uav/roz/sketch.props b/models/mdp/sketches/uav/roz/sketch.props index 8f96513d6..ad2078aa1 100644 --- a/models/mdp/sketches/uav/roz/sketch.props +++ b/models/mdp/sketches/uav/roz/sketch.props @@ -1 +1 @@ -P>=0.9 [ F w1&w2&w6 ] \ No newline at end of file +P>=0.75 [ F w1&w2&w6 ] \ No newline at end of file diff --git a/models/mdp/sketches/uav/roz/sketch.templ b/models/mdp/sketches/uav/roz/sketch.templ index 9f9899b92..7ccbd7e78 100644 --- a/models/mdp/sketches/uav/roz/sketch.templ +++ b/models/mdp/sketches/uav/roz/sketch.templ @@ -13,8 +13,8 @@ global stop : bool init false; // done visiting all waypoints formula roz = (r=roz_r_1) | (w=3&a=1) | (w=3&a=2) | (w=5&a=2); // restricted operating zones hole int COUNTER in {1..20}; -hole double fd in {0.1,0.3,0.5,0.7,0.9}; -hole double p in {0.1,0.2,0.3,0.4,0.5}; +hole double fd in {0.1..0.9:0.2}; +hole double p in {0.1..0.5:0.1}; hole int roz_r_1 in {1..9};