|
@@ -0,0 +1,69 @@
|
|
|
+include "primitives.alh"
|
|
|
+include "modelling.alh"
|
|
|
+
|
|
|
+ReachabilityGraph_RAM reachabilitygraph_print {
|
|
|
+ Composite schedule {
|
|
|
+ {Contains} Success success {}
|
|
|
+ {Contains} Failure failure {}
|
|
|
+ {Contains} ForAll print_states {
|
|
|
+ LHS {
|
|
|
+ Pre_ReachabilityGraph/State {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_ReachabilityGraph/State {
|
|
|
+ label = "0"
|
|
|
+ action = $
|
|
|
+ Void function action(model : Element, name : String, mapping : Element):
|
|
|
+ Element dict_values
|
|
|
+ Element all_values
|
|
|
+ dict_values = create_node()
|
|
|
+ all_values = allAssociationDestinations(model, name, "Contains")
|
|
|
+ while (read_nr_out(all_values) > 0):
|
|
|
+ String place
|
|
|
+ place = set_pop(all_values)
|
|
|
+ dict_add(dict_values, read_attribute(model, place, "name"), read_attribute(model, place, "tokens"))
|
|
|
+ output((cast_v2s(mapping["0"]) + ": ") + dict_to_string(dict_values))
|
|
|
+ return!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll print_transitions {
|
|
|
+ LHS {
|
|
|
+ Pre_ReachabilityGraph/State pre_s1 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Pre_ReachabilityGraph/State pre_s2 {
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Pre_ReachabilityGraph/Transition (pre_s1, pre_s2){
|
|
|
+ label = "2"
|
|
|
+ }
|
|
|
+ }
|
|
|
+ RHS {
|
|
|
+ Post_ReachabilityGraph/State post_s1 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_ReachabilityGraph/State post_s2 {
|
|
|
+ label = "1"
|
|
|
+ }
|
|
|
+ Post_ReachabilityGraph/Transition (post_s1, post_s2) {
|
|
|
+ label = "2"
|
|
|
+ action = $
|
|
|
+ Void function action(model : Element, name : String, mapping : Element):
|
|
|
+ output((((cast_v2s(mapping["0"]) + " --[") + cast_v2s(read_attribute(model, name, "name"))) + "]--> ") + cast_v2s(mapping["1"]))
|
|
|
+ return!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ OnSuccess (print_states, print_transitions) {}
|
|
|
+ OnFailure (print_states, failure) {}
|
|
|
+ OnSuccess (print_transitions, success) {}
|
|
|
+ OnFailure (print_transitions, success) {}
|
|
|
+}
|