modelverse/integration/code/pm_pn_reachability.mvc

Start start {}
Finish finish {}
Exec initializePN {
    name = "test/initialize_PN"
}
Exec refinePN {
    name = "test/refine_PN"
}
Exec reachability {
    name = "test/reachability"
}
Exec reachability_print{
    name = "test/reachability_print"
}

Data pn {
    name = "pn"
    type = "test/PetriNet"
}
Data reachability_graph {
    name = "reachability"
    type = "test/ReachabilityGraph"
}

Next (start, initializePN) {}
Next (initializePN, refinePN) {}
Next (refinePN, reachability) {}
Next (reachability, reachability_print) {}
Next (reachability_print, finish) {}

Produces (initializePN, pn) {
    name = "PetriNet"
}
Consumes (refinePN, pn) {
    name = "PetriNet"
}
Produces (refinePN, pn) {
    name = "PetriNet"
}
Consumes (reachability, pn) {
    name = "PetriNet"
}
Produces (reachability, reachability_graph) {
    name = "ReachabilityGraph"
}
Consumes (reachability_print, reachability_graph) {
    name = "ReachabilityGraph"
}