You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

287 lines
12 KiB

  1. mdp
  2. // parameters
  3. const int n_resources = 3;
  4. const int n_tasks = 2;
  5. const int n_sensors = 3;
  6. // sensor resources
  7. const int resource1=1;
  8. const int resource2=2;
  9. const int resource3=3;
  10. // network configuration
  11. const int e12=1;
  12. const int e13=1;
  13. const int e21=e12;
  14. const int e23=1;
  15. const int e31=e13;
  16. const int e32=e23;
  17. module controller // schedules the algorithm
  18. // algorithm status
  19. status : [0..6];
  20. // task resource indicator variables
  21. t1_r1 : [0..1];
  22. t1_r2 : [0..1];
  23. t1_r3 : [0..1];
  24. t2_r1 : [0..1];
  25. t2_r2 : [0..1];
  26. t2_r3 : [0..1];
  27. // schedule placeholders
  28. turn1 : [0..n_sensors];
  29. turn2 : [0..n_sensors];
  30. turn3 : [0..n_sensors];
  31. // selecting schedule uniformly at random
  32. [] status=0 -> 1/6 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (status'=1)
  33. + 1/6 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (status'=1)
  34. + 1/6 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (status'=1)
  35. + 1/6 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (status'=1)
  36. + 1/6 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (status'=1)
  37. + 1/6 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (status'=1);
  38. // initialising non-empty tasks uniformly at random
  39. [] status=1 -> 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  40. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  41. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  42. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  43. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  44. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  45. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  46. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  47. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  48. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  49. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  50. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  51. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  52. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  53. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  54. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  55. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  56. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  57. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  58. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  59. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  60. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  61. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  62. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  63. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  64. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  65. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  66. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  67. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  68. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  69. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  70. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  71. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  72. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  73. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  74. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  75. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  76. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  77. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  78. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  79. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  80. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  81. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  82. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  83. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  84. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  85. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  86. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  87. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2);
  88. // executing the schedule
  89. // 1st round
  90. [str1] status=2 & turn1=1 -> (status'=2);
  91. [fin1] status=2 & turn1=1 -> (status'=3);
  92. [str2] status=2 & turn1=2 -> (status'=2);
  93. [fin2] status=2 & turn1=2 -> (status'=3);
  94. [str3] status=2 & turn1=3 -> (status'=2);
  95. [fin3] status=2 & turn1=3 -> (status'=3);
  96. // 2nd round
  97. [str1] status=3 & turn2=1 -> (status'=3);
  98. [fin1] status=3 & turn2=1 -> (status'=4);
  99. [str2] status=3 & turn2=2 -> (status'=3);
  100. [fin2] status=3 & turn2=2 -> (status'=4);
  101. [str3] status=3 & turn2=3 -> (status'=3);
  102. [fin3] status=3 & turn2=3 -> (status'=4);
  103. // 3rd round
  104. [str1] status=4 & turn3=1 -> (status'=4);
  105. [fin1] status=4 & turn3=1 -> (status'=5);
  106. [str2] status=4 & turn3=2 -> (status'=4);
  107. [fin2] status=4 & turn3=2 -> (status'=5);
  108. [str3] status=4 & turn3=3 -> (status'=4);
  109. [fin3] status=4 & turn3=3 -> (status'=5);
  110. [] status=5 -> (status'=6);
  111. [] status=6 -> true;
  112. endmodule
  113. module sensor1
  114. state1 : [0..1];
  115. // team membership indicators
  116. m1_t1 : [0..1];
  117. m1_t2 : [0..1];
  118. // starting turn, selecting order of tasks
  119. [str1] state1=0 -> (state1'=1);
  120. // if there is no team and has required skill - initiating the team
  121. [] state1=1 & !committed & team_size_t1=0 & has_resource_t1 -> (m1_t1'=1);
  122. [] state1=1 & !committed & team_size_t2=0 & has_resource_t2 -> (m1_t2'=1);
  123. // if team already exists and one of the neighbours is in it - joining the team
  124. [] state1=1 & !committed & team_size_t1>0 & can_join_t1 & has_resource_t1 & !resource_filled_t1 -> (m1_t1'=1);
  125. [] state1=1 & !committed & team_size_t2>0 & can_join_t2 & has_resource_t2 & !resource_filled_t2 -> (m1_t2'=1);
  126. [fin1] state1>0 -> (state1'=0);
  127. endmodule
  128. module sensor2 = sensor1
  129. [
  130. state1=state2,
  131. str1=str2,
  132. fin1=fin2,
  133. m1_t1=m2_t1,
  134. m1_t2=m2_t2,
  135. m2_t1=m1_t1,
  136. m2_t2=m1_t2,
  137. resource1=resource2,
  138. resource2=resource1,
  139. e12=e21,
  140. e13=e23,
  141. e14=e24,
  142. e15=e25,
  143. e21=e12,
  144. e23=e13,
  145. e24=e14,
  146. e25=e15
  147. ]
  148. endmodule
  149. module sensor3 = sensor1
  150. [
  151. state1=state3,
  152. str1=str3,
  153. fin1=fin3,
  154. m1_t1=m3_t1,
  155. m1_t2=m3_t2,
  156. m3_t1=m1_t1,
  157. m3_t2=m1_t2,
  158. resource1=resource3,
  159. resource3=resource1,
  160. e12=e32,
  161. e13=e31,
  162. e14=e34,
  163. e15=e35,
  164. e31=e13,
  165. e32=e12,
  166. e34=e14,
  167. e35=e15
  168. ]
  169. endmodule
  170. // agent is committed to some team
  171. formula committed = (m1_t1+m1_t2) > 0;
  172. // formulae to compute team sizes
  173. formula team_size_t1 = m1_t1+m2_t1+m3_t1;
  174. formula team_size_t2 = m1_t2+m2_t2+m3_t2;
  175. // formulae to check whether the agent can join the team
  176. formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
  177. formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
  178. // formulae to check whether agent has the resource required by the task
  179. formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
  180. formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
  181. // formulae to check whether the resource of an agent has been already filled in the team
  182. formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
  183. formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
  184. // formula to compute team initiation probability (assuming each agent has at least one connection)
  185. formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
  186. // labels and formulae for property specification
  187. formula finished = (status=5);
  188. label "end" = (status=6);
  189. formula task1_completed = finished
  190. & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)))
  191. & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)))
  192. & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)));
  193. formula task2_completed = finished
  194. & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)))
  195. & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)))
  196. & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)));
  197. formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1);
  198. formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1);
  199. formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2);
  200. formula agent1_joins_successful_team_of_3 = (task1_completed & m1_t1=1 & team_size_t1=3) | (task2_completed & m1_t2=1 & team_size_t2=3);
  201. formula agent2_joins_successful_team = (task1_completed & m2_t1=1) | (task2_completed & m2_t2=1);
  202. formula agent2_joins_successful_team_of_1 = (task1_completed & m2_t1=1 & team_size_t1=1) | (task2_completed & m2_t2=1 & team_size_t2=1);
  203. formula agent2_joins_successful_team_of_2 = (task1_completed & m2_t1=1 & team_size_t1=2) | (task2_completed & m2_t2=1 & team_size_t2=2);
  204. formula agent2_joins_successful_team_of_3 = (task1_completed & m2_t1=1 & team_size_t1=3) | (task2_completed & m2_t2=1 & team_size_t2=3);
  205. formula agent3_joins_successful_team = (task1_completed & m3_t1=1) | (task2_completed & m3_t2=1);
  206. formula agent3_joins_successful_team_of_1 = (task1_completed & m3_t1=1 & team_size_t1=1) | (task2_completed & m3_t2=1 & team_size_t2=1);
  207. formula agent3_joins_successful_team_of_2 = (task1_completed & m3_t1=1 & team_size_t1=2) | (task2_completed & m3_t2=1 & team_size_t2=2);
  208. formula agent3_joins_successful_team_of_3 = (task1_completed & m3_t1=1 & team_size_t1=3) | (task2_completed & m3_t2=1 & team_size_t2=3);
  209. // rewards
  210. rewards "w_1_total"
  211. [] agent1_joins_successful_team : 1;
  212. [] agent2_joins_successful_team : 1;
  213. [] agent3_joins_successful_team : 1;
  214. endrewards
  215. rewards "w_2_total"
  216. [] task1_completed : 1;
  217. [] task2_completed : 1;
  218. endrewards