What the State is, and Where it comes from, when Generating Reachability Graphs

Question

For Timed Automata, I found Figure 1 below. For Coloured Petri Nets I found Figure 2. Both are for "Reachability Graph Construction".

However, they don't describe where they got the states from (Figure 3), for generating the reachability graph. They assume you have "states" to generate a reachability graph, but I'm not sure what these states are. In the timed automata case, I'm not sure the automata "states" are what they are describing, it seems like by "state" they mean the program state after the automata runs (or on each step). Likewise for Petri nets, the state isn't the place or the transition, but the program state. At least that's what I'm getting.

Given that, my question is how to construct the program state, so that I can then construct the reachability graph. In addition, I'm wondering what the states actually are composed of. What the state is (boolean predicates, temporal logic expressions, data, etc.).

Some more detail. From here (on Petri nets):

A marking $M'$ is reachable from a marking $M$ if $M[s\rangle M'$ for some $s \in T^*$... The reachability set Reach(N) of N is the set of all markings that are reachable from the initial marking. [The markings have to do with the data associated to a place (a Petri net node)]... A Petri net $N = (P, T, F, M_0)$ induces several standard structures on which first-order logics may be interpreted... To specify properties of structures ... obtained from a Petri net $N$, we introduce a first-order logic FO with atomic predicates $x \to y$, $x \overset{*}{\to} y$, $x \overset{+}{\to} y$ and $init(x)$. [Then they go into the model checking part].

That just demonstrates how the Reachability Graph Construction is left out. That is, what it is composed of (in some detail), and how to construct it.

---

Figure 1 $\downarrow$

Figure 2 $\downarrow$

Figure 3 $\downarrow$