|
| explicit_state_tid (const pda_state &s, const size_n &n) |
|
| explicit_state_tid (const id_thread &id, const ctx_bound &k, const pda_state &s, const size_n &n) |
|
| explicit_state_tid (const id_thread &id, const pda_state &s, const stack_vec &W) |
|
| explicit_state_tid (const id_thread &id, const ctx_bound &k, const pda_state &s, const stack_vec &W) |
|
| explicit_state_tid (const explicit_state_tid &c) |
|
ctx_bound | get_context_k () const |
|
void | set_context_k (const ctx_bound &k) |
|
id_thread | get_thread_id () const |
|
| explicit_state (const pda_state &s, const size_n &n) |
|
| explicit_state (const pda_state &s, const stack_vec &W) |
|
| explicit_state (const explicit_state &c) |
|
| ~explicit_state () |
|
pda_state | get_state () const |
|
const stack_vec & | get_stacks () const |
|
visible_state | top () |
|
visible_state | top () const |
|
Explicit state – with thread id and contexts – of a CPDS is of the form (id,k,s|w1,...,wn). It is an element of Q x (L*)^n, where n represents a number of threads