From efda2744a011175620407dd7b410c0ec4d5c478f Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Tue, 12 Dec 2023 00:39:18 +0100 Subject: [PATCH] Added rover model --- models/mdp/sketches/rover/rover-small/README | 1 + .../sketches/rover/rover-small/sketch.props | 1 + .../sketches/rover/rover-small/sketch.templ | 113 ++++++++++++++++++ models/mdp/sketches/rover/rover/README | 1 + models/mdp/sketches/rover/rover/sketch.props | 1 + models/mdp/sketches/rover/rover/sketch.templ | 112 +++++++++++++++++ 6 files changed, 229 insertions(+) create mode 100755 models/mdp/sketches/rover/rover-small/README create mode 100755 models/mdp/sketches/rover/rover-small/sketch.props create mode 100755 models/mdp/sketches/rover/rover-small/sketch.templ create mode 100755 models/mdp/sketches/rover/rover/README create mode 100755 models/mdp/sketches/rover/rover/sketch.props create mode 100755 models/mdp/sketches/rover/rover/sketch.templ diff --git a/models/mdp/sketches/rover/rover-small/README b/models/mdp/sketches/rover/rover-small/README new file mode 100755 index 000000000..4fff1ba9a --- /dev/null +++ b/models/mdp/sketches/rover/rover-small/README @@ -0,0 +1 @@ +from paper 'Multi-cost Bounded Reachability in MDP' by Hartmanns et al. TACAS'18 diff --git a/models/mdp/sketches/rover/rover-small/sketch.props b/models/mdp/sketches/rover/rover-small/sketch.props new file mode 100755 index 000000000..8e528602a --- /dev/null +++ b/models/mdp/sketches/rover/rover-small/sketch.props @@ -0,0 +1 @@ +P>=0.75 [F "goal"] diff --git a/models/mdp/sketches/rover/rover-small/sketch.templ b/models/mdp/sketches/rover/rover-small/sketch.templ new file mode 100755 index 000000000..a28b156a5 --- /dev/null +++ b/models/mdp/sketches/rover/rover-small/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 {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 = 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/README b/models/mdp/sketches/rover/rover/README new file mode 100755 index 000000000..4fff1ba9a --- /dev/null +++ b/models/mdp/sketches/rover/rover/README @@ -0,0 +1 @@ +from paper 'Multi-cost Bounded Reachability in MDP' by Hartmanns et al. TACAS'18 diff --git a/models/mdp/sketches/rover/rover/sketch.props b/models/mdp/sketches/rover/rover/sketch.props new file mode 100755 index 000000000..8e528602a --- /dev/null +++ b/models/mdp/sketches/rover/rover/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/sketch.templ new file mode 100755 index 000000000..190ef1d93 --- /dev/null +++ b/models/mdp/sketches/rover/rover/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; +