"book-pflow-xyz/chapters/appendix-d-glossary.md" . . "The graph of all markings reachable from the initial marking through sequences of transition firings. Each node is a marking, each edge is a transition firing. The reachability graph may be infinite for unbounded nets."@en . . "Reachability graph"@en .