modelverse/models/reachabilitygraph_print.mvc

include "primitives.alh"
include "modelling.alh"
include "object_operations.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
                            String place
                            dict_values = create_node()
                            all_values = allAssociationDestinations(model, name, "ReachabilityGraph/Contains")
                            while (read_nr_out(all_values) > 0):
                                place = set_pop(all_values)
                                dict_add(dict_values, read_attribute(model, place, "name"), read_attribute(model, place, "tokens"))
                            log((cast_v2s(read_attribute(model, name, "name")) + ": ") + 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):
                            log((((cast_v2s(read_attribute(model, mapping["0"], "name")) + " --[") + cast_v2s(read_attribute(model, name, "name"))) + "]--> ") + cast_v2s(read_attribute(model, mapping["1"], "name")))
                            return!
                        $
                }
            }
        }
    }

    Initial (schedule, print_states) {}
    OnSuccess (print_states, print_transitions) {}
    OnFailure (print_states, failure) {}
    OnSuccess (print_transitions, success) {}
    OnFailure (print_transitions, success) {}
}