reachability.alc 6.3 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187
  1. include "primitives.alh"
  2. include "modelling.alh"
  3. include "object_operations.alh"
  4. Element function reachability_graph(params : Element, output_mms : Element):
  5. Element result
  6. Element model
  7. Element workset
  8. Element out_model
  9. Element in_model
  10. Element transition_vectors_produce
  11. Element transition_vectors_consume
  12. Element all_transitions
  13. Element all_transitions_original
  14. Element tv
  15. Element links
  16. Element mappings
  17. Element reachable_states
  18. Element keys
  19. String transition
  20. String new_transition
  21. String state
  22. String name
  23. String link
  24. String place
  25. String key
  26. Integer link_weight
  27. Integer initial
  28. Integer state_id
  29. Integer next_id
  30. Boolean possible
  31. Element all_places
  32. Element dict_repr
  33. Element new_dict_repr
  34. Element work_unit
  35. Element cache
  36. cache = create_node()
  37. result = create_node()
  38. out_model = instantiate_model(output_mms["ReachabilityGraph"])
  39. in_model = params["pn"]
  40. // Create a dictionary representation for each transition
  41. transition_vectors_produce = create_node()
  42. transition_vectors_consume = create_node()
  43. all_transitions = allInstances(in_model, "Transition")
  44. while (read_nr_out(all_transitions) > 0):
  45. transition = set_pop(all_transitions)
  46. tv = create_node()
  47. links = allIncomingAssociationInstances(in_model, transition, "P2T")
  48. while (read_nr_out(links) > 0):
  49. link = set_pop(links)
  50. name = reverseKeyLookup(in_model["model"], read_edge_src(in_model["model"][link]))
  51. link_weight = read_attribute(in_model, link, "weight")
  52. dict_add_fast(tv, name, link_weight)
  53. dict_add_fast(transition_vectors_consume, transition, tv)
  54. tv = create_node()
  55. links = allOutgoingAssociationInstances(in_model, transition, "T2P")
  56. while (read_nr_out(links) > 0):
  57. link = set_pop(links)
  58. name = reverseKeyLookup(in_model["model"], read_edge_dst(in_model["model"][link]))
  59. link_weight = read_attribute(in_model, link, "weight")
  60. dict_add_fast(tv, name, link_weight)
  61. dict_add_fast(transition_vectors_produce, transition, tv)
  62. workset = create_node()
  63. all_places = allInstances(in_model, "Place")
  64. dict_repr = create_node()
  65. while (read_nr_out(all_places) > 0):
  66. place = set_pop(all_places)
  67. dict_add_fast(dict_repr, place, read_attribute(in_model, place, "tokens"))
  68. all_transitions_original = allInstances(in_model, "Transition")
  69. mappings = create_node()
  70. state_id = 0
  71. next_id = 1
  72. reachable_states = create_node()
  73. dict_add_fast(reachable_states, state_id, dict_repr)
  74. dict_add_fast(mappings, state_id, create_node())
  75. set_add(workset, state_id)
  76. // And add in the model itself
  77. state = instantiate_node(out_model, "State", cast_i2s(state_id))
  78. instantiate_attribute(out_model, state, "name", cast_i2s(state_id))
  79. keys = dict_keys(dict_repr)
  80. while (read_nr_out(keys) > 0):
  81. key = set_pop(keys)
  82. place = instantiate_node(out_model, "Place", "")
  83. instantiate_attribute(out_model, place, "name", read_attribute(in_model, key, "name"))
  84. instantiate_attribute(out_model, place, "tokens", dict_repr[key])
  85. instantiate_link(out_model, "Contains", "", state, place)
  86. while (read_nr_out(workset) > 0):
  87. state_id = set_pop(workset)
  88. dict_repr = reachable_states[state_id]
  89. // Compute how the PN behaves with this specific state
  90. // For this, we fetch all transitions and check if they are enabled
  91. all_transitions = set_copy(all_transitions_original)
  92. while (read_nr_out(all_transitions) > 0):
  93. transition = set_pop(all_transitions)
  94. keys = dict_keys(transition_vectors_consume[transition])
  95. possible = True
  96. while (read_nr_out(keys) > 0):
  97. key = set_pop(keys)
  98. // Compare the values in the state with those consumed by the transition
  99. if (integer_lt(dict_repr[key], transition_vectors_consume[transition][key])):
  100. // Impossible transition, so discard this one
  101. possible = False
  102. break!
  103. if (possible):
  104. new_dict_repr = dict_copy(dict_repr)
  105. // Transition can execute, so compute and add the new state based on the consume/produce vectors
  106. keys = dict_keys(transition_vectors_consume[transition])
  107. while (read_nr_out(keys) > 0):
  108. key = set_pop(keys)
  109. dict_overwrite(new_dict_repr, key, integer_subtraction(new_dict_repr[key], transition_vectors_consume[transition][key]))
  110. keys = dict_keys(transition_vectors_produce[transition])
  111. while (read_nr_out(keys) > 0):
  112. key = set_pop(keys)
  113. dict_overwrite(new_dict_repr, key, integer_addition(new_dict_repr[key], transition_vectors_produce[transition][key]))
  114. // Check if this state already has an associated ID
  115. Integer other_state_id
  116. Integer target_id
  117. keys = dict_keys(reachable_states)
  118. target_id = -1
  119. while (read_nr_out(keys) > 0):
  120. other_state_id = set_pop(keys)
  121. if (dict_eq(reachable_states[other_state_id], new_dict_repr)):
  122. target_id = other_state_id
  123. break!
  124. if (target_id == -1):
  125. // New state
  126. target_id = next_id
  127. next_id = next_id + 1
  128. // Add to all data structures
  129. dict_add_fast(reachable_states, target_id, new_dict_repr)
  130. dict_add_fast(mappings, target_id, create_node())
  131. set_add(workset, target_id)
  132. // And add in the model itself
  133. state = instantiate_node(out_model, "State", cast_i2s(target_id))
  134. instantiate_attribute(out_model, state, "name", cast_i2s(target_id))
  135. keys = dict_keys(new_dict_repr)
  136. Element sub
  137. String name
  138. while (read_nr_out(keys) > 0):
  139. key = set_pop(keys)
  140. name = read_attribute(in_model, key, "name")
  141. if (bool_not(dict_in(cache, name))):
  142. dict_add_fast(cache, name, create_node())
  143. sub = cache[name]
  144. if (bool_not(dict_in(sub, new_dict_repr[key]))):
  145. place = instantiate_node(out_model, "Place", "")
  146. instantiate_attribute(out_model, place, "name", name)
  147. instantiate_attribute(out_model, place, "tokens", new_dict_repr[key])
  148. dict_add_fast(sub, new_dict_repr[key], place)
  149. else:
  150. place = sub[new_dict_repr[key]]
  151. instantiate_link(out_model, "Contains", "", state, place)
  152. // Anyway, we have found a transition, which we should store
  153. dict_add_fast(mappings[state_id], transition, target_id)
  154. // And also store it in the model itself
  155. new_transition = instantiate_link(out_model, "Transition", "", cast_i2s(state_id), cast_i2s(target_id))
  156. instantiate_attribute(out_model, new_transition, "name", read_attribute(in_model, transition, "name"))
  157. dict_add_fast(result, "ReachabilityGraph", out_model)
  158. return result!