sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
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.
3927 Commits
2 Branches
0 Tags
187 MiB
Tree: 73db040583
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '73db040583'
${ noResults }
tempest/examples/multiobjective/mdp/team/team3obj_5.nm

532 lines
27 KiB
Raw Normal View History

added examples from ATVA'12 paper Former-commit-id: a8dd5d09a568c33a471fb3e536d7b7194bb81764
9 years ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
fixed model files for team benchmark Former-commit-id: e253457611e8523aaa070cca499e375c75890f88
9 years ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
added examples from ATVA'12 paper Former-commit-id: a8dd5d09a568c33a471fb3e536d7b7194bb81764
9 years ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
fixed prism model code (formula used before definition) Former-commit-id: d610960b0e0b85fe132af22ad98be2c2f2cf139d
9 years ago
​
​
​
​
​
​
​
​
​
added examples from ATVA'12 paper Former-commit-id: a8dd5d09a568c33a471fb3e536d7b7194bb81764
9 years ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
  1. mdp
  3. // parameters
  4. const int n_resources = 3;
  5. const int n_tasks = 2;
  6. const int n_sensors = 5;
  9. // sensor resources
  10. const int resource1=1;
  11. const int resource2=2;
  12. const int resource3=3;
  13. const int resource4=1;
  14. const int resource5=2;
  16. // network configuration
  17. const int e12=1;
  18. const int e13=1;
  19. const int e14=1;
  20. const int e15=1;
  22. const int e21=e12;
  23. const int e23=1;
  24. const int e24=1;
  25. const int e25=1;
  27. const int e31=e13;
  28. const int e32=e23;
  29. const int e34=1;
  30. const int e35=1;
  32. const int e41=e14;
  33. const int e42=e24;
  34. const int e43=e34;
  35. const int e45=1;
  37. const int e51=e15;
  38. const int e52=e25;
  39. const int e53=e35;
  40. const int e54=e45;
  43. // agent is committed to some team
  44. formula committed = (m1_t1+m1_t2) > 0;
  46. // formulae to compute team sizes
  47. formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1+m5_t1;
  48. formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2+m5_t2;
  50. // formulae to check whether the agent can join the team
  51. formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 + e15*m5_t1 > 0;
  52. formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 + e15*m5_t2 > 0;
  54. // formulae to check whether agent has the resource required by the task
  55. formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
  56. formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
  58. // formulae to check whether the resource of an agent has been already filled in the team
  59. formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4) | (m5_t1=1 & resource1=resource5);
  60. formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4) | (m5_t2=1 & resource1=resource5);
  62. // formula to compute team initiation probability (assuming each agent has at least one connection)
  63. formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))+e15*(1-((m5_t1+m5_t2)=0?0:1))) / (e12+e13+e14+e15);
  66. module controller // schedules the algorithm
  68. // algorithm status
  69. status : [0..8];
  71. // task resource indicator variables
  72. t1_r1 : [0..1];
  73. t1_r2 : [0..1];
  74. t1_r3 : [0..1];
  76. t2_r1 : [0..1];
  77. t2_r2 : [0..1];
  78. t2_r3 : [0..1];
  80. // schedule placeholders
  81. turn1 : [0..n_sensors];
  82. turn2 : [0..n_sensors];
  83. turn3 : [0..n_sensors];
  84. turn4 : [0..n_sensors];
  85. turn5 : [0..n_sensors];
  87. // selecting schedule uniformly at random
  88. [] status=0 -> 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (turn4'=4) & (turn5'=5) & (status'=1)
  89. + 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (turn4'=5) & (turn5'=4) & (status'=1)
  90. + 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=4) & (turn4'=3) & (turn5'=5) & (status'=1)
  91. + 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=4) & (turn4'=5) & (turn5'=3) & (status'=1)
  92. + 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=5) & (turn4'=3) & (turn5'=4) & (status'=1)
  93. + 1/120 : (turn1'=1) & (turn2'=2) & (turn3'=5) & (turn4'=4) & (turn5'=3) & (status'=1)
  94. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (turn4'=4) & (turn5'=5) & (status'=1)
  95. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (turn4'=5) & (turn5'=4) & (status'=1)
  96. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=4) & (turn4'=2) & (turn5'=5) & (status'=1)
  97. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=4) & (turn4'=5) & (turn5'=2) & (status'=1)
  98. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=5) & (turn4'=2) & (turn5'=4) & (status'=1)
  99. + 1/120 : (turn1'=1) & (turn2'=3) & (turn3'=5) & (turn4'=4) & (turn5'=2) & (status'=1)
  100. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=2) & (turn4'=3) & (turn5'=5) & (status'=1)
  101. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=2) & (turn4'=5) & (turn5'=3) & (status'=1)
  102. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=3) & (turn4'=2) & (turn5'=5) & (status'=1)
  103. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=3) & (turn4'=5) & (turn5'=2) & (status'=1)
  104. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=5) & (turn4'=2) & (turn5'=3) & (status'=1)
  105. + 1/120 : (turn1'=1) & (turn2'=4) & (turn3'=5) & (turn4'=3) & (turn5'=2) & (status'=1)
  106. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=2) & (turn4'=3) & (turn5'=4) & (status'=1)
  107. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=2) & (turn4'=4) & (turn5'=3) & (status'=1)
  108. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=3) & (turn4'=2) & (turn5'=4) & (status'=1)
  109. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=3) & (turn4'=4) & (turn5'=2) & (status'=1)
  110. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=4) & (turn4'=2) & (turn5'=3) & (status'=1)
  111. + 1/120 : (turn1'=1) & (turn2'=5) & (turn3'=4) & (turn4'=3) & (turn5'=2) & (status'=1)
  112. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (turn4'=4) & (turn5'=5) & (status'=1)
  113. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (turn4'=5) & (turn5'=4) & (status'=1)
  114. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=4) & (turn4'=3) & (turn5'=5) & (status'=1)
  115. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=4) & (turn4'=5) & (turn5'=3) & (status'=1)
  116. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=5) & (turn4'=3) & (turn5'=4) & (status'=1)
  117. + 1/120 : (turn1'=2) & (turn2'=1) & (turn3'=5) & (turn4'=4) & (turn5'=3) & (status'=1)
  118. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (turn4'=4) & (turn5'=5) & (status'=1)
  119. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (turn4'=5) & (turn5'=4) & (status'=1)
  120. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=4) & (turn4'=1) & (turn5'=5) & (status'=1)
  121. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=4) & (turn4'=5) & (turn5'=1) & (status'=1)
  122. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=5) & (turn4'=1) & (turn5'=4) & (status'=1)
  123. + 1/120 : (turn1'=2) & (turn2'=3) & (turn3'=5) & (turn4'=4) & (turn5'=1) & (status'=1)
  124. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=1) & (turn4'=3) & (turn5'=5) & (status'=1)
  125. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=1) & (turn4'=5) & (turn5'=3) & (status'=1)
  126. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=3) & (turn4'=1) & (turn5'=5) & (status'=1)
  127. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=3) & (turn4'=5) & (turn5'=1) & (status'=1)
  128. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=5) & (turn4'=1) & (turn5'=3) & (status'=1)
  129. + 1/120 : (turn1'=2) & (turn2'=4) & (turn3'=5) & (turn4'=3) & (turn5'=1) & (status'=1)
  130. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=1) & (turn4'=3) & (turn5'=4) & (status'=1)
  131. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=1) & (turn4'=4) & (turn5'=3) & (status'=1)
  132. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=3) & (turn4'=1) & (turn5'=4) & (status'=1)
  133. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=3) & (turn4'=4) & (turn5'=1) & (status'=1)
  134. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=4) & (turn4'=1) & (turn5'=3) & (status'=1)
  135. + 1/120 : (turn1'=2) & (turn2'=5) & (turn3'=4) & (turn4'=3) & (turn5'=1) & (status'=1)
  136. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (turn4'=4) & (turn5'=5) & (status'=1)
  137. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (turn4'=5) & (turn5'=4) & (status'=1)
  138. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=4) & (turn4'=2) & (turn5'=5) & (status'=1)
  139. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=4) & (turn4'=5) & (turn5'=2) & (status'=1)
  140. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=5) & (turn4'=2) & (turn5'=4) & (status'=1)
  141. + 1/120 : (turn1'=3) & (turn2'=1) & (turn3'=5) & (turn4'=4) & (turn5'=2) & (status'=1)
  142. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (turn4'=4) & (turn5'=5) & (status'=1)
  143. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (turn4'=5) & (turn5'=4) & (status'=1)
  144. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=4) & (turn4'=1) & (turn5'=5) & (status'=1)
  145. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=4) & (turn4'=5) & (turn5'=1) & (status'=1)
  146. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=5) & (turn4'=1) & (turn5'=4) & (status'=1)
  147. + 1/120 : (turn1'=3) & (turn2'=2) & (turn3'=5) & (turn4'=4) & (turn5'=1) & (status'=1)
  148. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=1) & (turn4'=2) & (turn5'=5) & (status'=1)
  149. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=1) & (turn4'=5) & (turn5'=2) & (status'=1)
  150. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=2) & (turn4'=1) & (turn5'=5) & (status'=1)
  151. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=2) & (turn4'=5) & (turn5'=1) & (status'=1)
  152. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=5) & (turn4'=1) & (turn5'=2) & (status'=1)
  153. + 1/120 : (turn1'=3) & (turn2'=4) & (turn3'=5) & (turn4'=2) & (turn5'=1) & (status'=1)
  154. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=1) & (turn4'=2) & (turn5'=4) & (status'=1)
  155. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=1) & (turn4'=4) & (turn5'=2) & (status'=1)
  156. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=2) & (turn4'=1) & (turn5'=4) & (status'=1)
  157. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=2) & (turn4'=4) & (turn5'=1) & (status'=1)
  158. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=4) & (turn4'=1) & (turn5'=2) & (status'=1)
  159. + 1/120 : (turn1'=3) & (turn2'=5) & (turn3'=4) & (turn4'=2) & (turn5'=1) & (status'=1)
  160. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=2) & (turn4'=3) & (turn5'=5) & (status'=1)
  161. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=2) & (turn4'=5) & (turn5'=3) & (status'=1)
  162. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=3) & (turn4'=2) & (turn5'=5) & (status'=1)
  163. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=3) & (turn4'=5) & (turn5'=2) & (status'=1)
  164. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=5) & (turn4'=2) & (turn5'=3) & (status'=1)
  165. + 1/120 : (turn1'=4) & (turn2'=1) & (turn3'=5) & (turn4'=3) & (turn5'=2) & (status'=1)
  166. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=1) & (turn4'=3) & (turn5'=5) & (status'=1)
  167. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=1) & (turn4'=5) & (turn5'=3) & (status'=1)
  168. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=3) & (turn4'=1) & (turn5'=5) & (status'=1)
  169. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=3) & (turn4'=5) & (turn5'=1) & (status'=1)
  170. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=5) & (turn4'=1) & (turn5'=3) & (status'=1)
  171. + 1/120 : (turn1'=4) & (turn2'=2) & (turn3'=5) & (turn4'=3) & (turn5'=1) & (status'=1)
  172. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=1) & (turn4'=2) & (turn5'=5) & (status'=1)
  173. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=1) & (turn4'=5) & (turn5'=2) & (status'=1)
  174. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=2) & (turn4'=1) & (turn5'=5) & (status'=1)
  175. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=2) & (turn4'=5) & (turn5'=1) & (status'=1)
  176. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=5) & (turn4'=1) & (turn5'=2) & (status'=1)
  177. + 1/120 : (turn1'=4) & (turn2'=3) & (turn3'=5) & (turn4'=2) & (turn5'=1) & (status'=1)
  178. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=1) & (turn4'=2) & (turn5'=3) & (status'=1)
  179. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=1) & (turn4'=3) & (turn5'=2) & (status'=1)
  180. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=2) & (turn4'=1) & (turn5'=3) & (status'=1)
  181. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=2) & (turn4'=3) & (turn5'=1) & (status'=1)
  182. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=3) & (turn4'=1) & (turn5'=2) & (status'=1)
  183. + 1/120 : (turn1'=4) & (turn2'=5) & (turn3'=3) & (turn4'=2) & (turn5'=1) & (status'=1)
  184. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=2) & (turn4'=3) & (turn5'=4) & (status'=1)
  185. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=2) & (turn4'=4) & (turn5'=3) & (status'=1)
  186. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=3) & (turn4'=2) & (turn5'=4) & (status'=1)
  187. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=3) & (turn4'=4) & (turn5'=2) & (status'=1)
  188. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=4) & (turn4'=2) & (turn5'=3) & (status'=1)
  189. + 1/120 : (turn1'=5) & (turn2'=1) & (turn3'=4) & (turn4'=3) & (turn5'=2) & (status'=1)
  190. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=1) & (turn4'=3) & (turn5'=4) & (status'=1)
  191. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=1) & (turn4'=4) & (turn5'=3) & (status'=1)
  192. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=3) & (turn4'=1) & (turn5'=4) & (status'=1)
  193. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=3) & (turn4'=4) & (turn5'=1) & (status'=1)
  194. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=4) & (turn4'=1) & (turn5'=3) & (status'=1)
  195. + 1/120 : (turn1'=5) & (turn2'=2) & (turn3'=4) & (turn4'=3) & (turn5'=1) & (status'=1)
  196. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=1) & (turn4'=2) & (turn5'=4) & (status'=1)
  197. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=1) & (turn4'=4) & (turn5'=2) & (status'=1)
  198. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=2) & (turn4'=1) & (turn5'=4) & (status'=1)
  199. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=2) & (turn4'=4) & (turn5'=1) & (status'=1)
  200. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=4) & (turn4'=1) & (turn5'=2) & (status'=1)
  201. + 1/120 : (turn1'=5) & (turn2'=3) & (turn3'=4) & (turn4'=2) & (turn5'=1) & (status'=1)
  202. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=1) & (turn4'=2) & (turn5'=3) & (status'=1)
  203. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=1) & (turn4'=3) & (turn5'=2) & (status'=1)
  204. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=2) & (turn4'=1) & (turn5'=3) & (status'=1)
  205. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=2) & (turn4'=3) & (turn5'=1) & (status'=1)
  206. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=3) & (turn4'=1) & (turn5'=2) & (status'=1)
  207. + 1/120 : (turn1'=5) & (turn2'=4) & (turn3'=3) & (turn4'=2) & (turn5'=1) & (status'=1);
  210. // initialising non-empty tasks uniformly at random
  211. [] status=1 -> 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  212. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  213. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  214. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  215. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  216. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  217. + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  218. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  219. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  220. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  221. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  222. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  223. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  224. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  225. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  226. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  227. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  228. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  229. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  230. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  231. + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  232. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  233. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  234. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  235. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  236. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  237. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  238. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  239. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  240. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  241. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  242. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  243. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  244. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  245. + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  246. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  247. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  248. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  249. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  250. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  251. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  252. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  253. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  254. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  255. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
  256. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
  257. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
  258. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
  259. + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2);
  261. // executing the schedule
  263. // 1st round
  264. [str1] status=2 & turn1=1 -> (status'=2);
  265. [fin1] status=2 & turn1=1 -> (status'=3);
  266. [str2] status=2 & turn1=2 -> (status'=2);
  267. [fin2] status=2 & turn1=2 -> (status'=3);
  268. [str3] status=2 & turn1=3 -> (status'=2);
  269. [fin3] status=2 & turn1=3 -> (status'=3);
  270. [str4] status=2 & turn1=4 -> (status'=2);
  271. [fin4] status=2 & turn1=4 -> (status'=3);
  272. [str5] status=2 & turn1=5 -> (status'=2);
  273. [fin5] status=2 & turn1=5 -> (status'=3);
  275. // 2nd round
  276. [str1] status=3 & turn2=1 -> (status'=3);
  277. [fin1] status=3 & turn2=1 -> (status'=4);
  278. [str2] status=3 & turn2=2 -> (status'=3);
  279. [fin2] status=3 & turn2=2 -> (status'=4);
  280. [str3] status=3 & turn2=3 -> (status'=3);
  281. [fin3] status=3 & turn2=3 -> (status'=4);
  282. [str4] status=3 & turn2=4 -> (status'=3);
  283. [fin4] status=3 & turn2=4 -> (status'=4);
  284. [str5] status=3 & turn2=5 -> (status'=3);
  285. [fin5] status=3 & turn2=5 -> (status'=4);
  287. // 3rd round
  288. [str1] status=4 & turn3=1 -> (status'=4);
  289. [fin1] status=4 & turn3=1 -> (status'=5);
  290. [str2] status=4 & turn3=2 -> (status'=4);
  291. [fin2] status=4 & turn3=2 -> (status'=5);
  292. [str3] status=4 & turn3=3 -> (status'=4);
  293. [fin3] status=4 & turn3=3 -> (status'=5);
  294. [str4] status=4 & turn3=4 -> (status'=4);
  295. [fin4] status=4 & turn3=4 -> (status'=5);
  296. [str5] status=4 & turn3=5 -> (status'=4);
  297. [fin5] status=4 & turn3=5 -> (status'=5);
  299. // 4th round
  300. [str1] status=5 & turn4=1 -> (status'=5);
  301. [fin1] status=5 & turn4=1 -> (status'=6);
  302. [str2] status=5 & turn4=2 -> (status'=5);
  303. [fin2] status=5 & turn4=2 -> (status'=6);
  304. [str3] status=5 & turn4=3 -> (status'=5);
  305. [fin3] status=5 & turn4=3 -> (status'=6);
  306. [str4] status=5 & turn4=4 -> (status'=5);
  307. [fin4] status=5 & turn4=4 -> (status'=6);
  308. [str5] status=5 & turn4=5 -> (status'=5);
  309. [fin5] status=5 & turn4=5 -> (status'=6);
  311. // 5th round
  312. [str1] status=6 & turn5=1 -> (status'=6);
  313. [fin1] status=6 & turn5=1 -> (status'=7);
  314. [str2] status=6 & turn5=2 -> (status'=6);
  315. [fin2] status=6 & turn5=2 -> (status'=7);
  316. [str3] status=6 & turn5=3 -> (status'=6);
  317. [fin3] status=6 & turn5=3 -> (status'=7);
  318. [str4] status=6 & turn5=4 -> (status'=6);
  319. [fin4] status=6 & turn5=4 -> (status'=7);
  320. [str5] status=6 & turn5=5 -> (status'=6);
  321. [fin5] status=6 & turn5=5 -> (status'=7);
  323. [] status=7 -> (status'=8);
  325. [] status=8 -> (status'=8);
  327. endmodule
  329. module sensor1
  331. state1 : [0..1];
  333. // team membership indicators
  334. m1_t1 : [0..1];
  335. m1_t2 : [0..1];
  337. // starting turn, selecting order of tasks
  338. [str1] state1=0 -> (state1'=1);
  340. // if there is no team and has required skill - initiating the team
  341. [] state1=1 & !committed & team_size_t1=0 & has_resource_t1 -> (m1_t1'=1);
  342. [] state1=1 & !committed & team_size_t2=0 & has_resource_t2 -> (m1_t2'=1);
  344. // if team already exists and one of the neighbours is in it - joining the team
  345. [] state1=1 & !committed & team_size_t1>0 & can_join_t1 & has_resource_t1 & !resource_filled_t1 -> (m1_t1'=1);
  346. [] state1=1 & !committed & team_size_t2>0 & can_join_t2 & has_resource_t2 & !resource_filled_t2 -> (m1_t2'=1);
  348. [fin1] state1>0 -> (state1'=0);
  350. endmodule
  352. module sensor2 = sensor1
  353. [
  354. state1=state2,
  356. str1=str2,
  357. fin1=fin2,
  359. m1_t1=m2_t1,
  360. m1_t2=m2_t2,
  362. m2_t1=m1_t1,
  363. m2_t2=m1_t2,
  365. resource1=resource2,
  366. resource2=resource1,
  368. e12=e21,
  369. e13=e23,
  370. e14=e24,
  371. e15=e25,
  373. e21=e12,
  374. e23=e13,
  375. e24=e14,
  376. e25=e15
  377. ]
  378. endmodule
  380. module sensor3 = sensor1
  381. [
  382. state1=state3,
  384. str1=str3,
  385. fin1=fin3,
  387. m1_t1=m3_t1,
  388. m1_t2=m3_t2,
  389. m3_t1=m1_t1,
  390. m3_t2=m1_t2,
  392. resource1=resource3,
  393. resource3=resource1,
  395. e12=e32,
  396. e13=e31,
  397. e14=e34,
  398. e15=e35,
  400. e31=e13,
  401. e32=e12,
  402. e34=e14,
  403. e35=e15
  404. ]
  405. endmodule
  407. module sensor4 = sensor1
  408. [
  409. state1=state4,
  411. str1=str4,
  412. fin1=fin4,
  414. m1_t1=m4_t1,
  415. m1_t2=m4_t2,
  417. m4_t1=m1_t1,
  418. m4_t2=m1_t2,
  420. resource1=resource4,
  421. resource4=resource1,
  423. e12=e42,
  424. e13=e43,
  425. e14=e41,
  426. e15=e45,
  428. e41=e14,
  429. e42=e12,
  430. e43=e13,
  431. e45=e15
  432. ]
  433. endmodule
  435. module sensor5 = sensor1
  436. [
  437. state1=state5,
  439. str1=str5,
  440. fin1=fin5,
  442. m1_t1=m5_t1,
  443. m1_t2=m5_t2,
  445. m5_t1=m1_t1,
  446. m5_t2=m1_t2,
  448. resource1=resource5,
  449. resource5=resource1,
  451. e12=e52,
  452. e13=e53,
  453. e14=e54,
  454. e15=e51,
  456. e51=e15,
  457. e52=e12,
  458. e53=e13,
  459. e54=e14
  460. ]
  461. endmodule
  463. // formulae for scheduling
  464. formula s1_sched = (turn1=1 | turn2=1 | turn3=1 | turn4=1 | turn5=1);
  465. formula s2_sched = (turn1=2 | turn2=2 | turn3=2 | turn4=2 | turn5=2);
  466. formula s3_sched = (turn1=3 | turn2=3 | turn3=3 | turn4=3 | turn5=3);
  467. formula s4_sched = (turn1=4 | turn2=4 | turn3=4 | turn4=4 | turn5=4);
  468. formula s5_sched = (turn1=5 | turn2=5 | turn3=5 | turn4=5 | turn5=5);
  469. formula all_not_sched = !(s1_sched | s2_sched | s3_sched | s4_sched | s5_sched);
  470. formula all_sched = (s1_sched & s2_sched & s3_sched & s4_sched & s5_sched);
  475. // labels and formulae for property specification
  476. formula finished = (status=7);
  477. label "end" = (status=8);
  480. formula task1_completed = finished
  481. & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)|(m5_t1=1&resource5=1)))
  482. & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)|(m5_t1=1&resource5=2)))
  483. & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)|(m5_t1=1&resource5=3)));
  485. formula task2_completed = finished
  486. & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)|(m5_t2=1&resource5=1)))
  487. & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)|(m5_t2=1&resource5=2)))
  488. & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)|(m5_t2=1&resource5=3)));
  490. formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1);
  491. 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);
  492. 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);
  493. 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);
  495. formula agent2_joins_successful_team = (task1_completed & m2_t1=1) | (task2_completed & m2_t2=1);
  496. 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);
  497. 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);
  498. 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);
  500. formula agent3_joins_successful_team = (task1_completed & m3_t1=1) | (task2_completed & m3_t2=1);
  501. 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);
  502. 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);
  503. 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);
  505. formula agent4_joins_successful_team = (task1_completed & m4_t1=1) | (task2_completed & m4_t2=1);
  506. formula agent4_joins_successful_team_of_1 = (task1_completed & m4_t1=1 & team_size_t1=1) | (task2_completed & m4_t2=1 & team_size_t2=1);
  507. formula agent4_joins_successful_team_of_2 = (task1_completed & m4_t1=1 & team_size_t1=2) | (task2_completed & m4_t2=1 & team_size_t2=2);
  508. formula agent4_joins_successful_team_of_3 = (task1_completed & m4_t1=1 & team_size_t1=3) | (task2_completed & m4_t2=1 & team_size_t2=3);
  510. formula agent5_joins_successful_team = (task1_completed & m5_t1=1) | (task2_completed & m5_t2=1);
  511. formula agent5_joins_successful_team_of_1 = (task1_completed & m5_t1=1 & team_size_t1=1) | (task2_completed & m5_t2=1 & team_size_t2=1);
  512. formula agent5_joins_successful_team_of_2 = (task1_completed & m5_t1=1 & team_size_t1=2) | (task2_completed & m5_t2=1 & team_size_t2=2);
  513. formula agent5_joins_successful_team_of_3 = (task1_completed & m5_t1=1 & team_size_t1=3) | (task2_completed & m5_t2=1 & team_size_t2=3);
  515. // rewards
  516. rewards "w_1_total"
  517. [] agent1_joins_successful_team : 1;
  518. [] agent2_joins_successful_team : 1;
  519. [] agent3_joins_successful_team : 1;
  520. [] agent4_joins_successful_team : 1;
  521. [] agent5_joins_successful_team : 1;
  522. endrewards
  524. rewards "w_2_total"
  525. [] task1_completed : 1;
  526. [] task2_completed : 1;
  527. endrewards