be_ptr trace_exec_get_initial_state( BeFsm_ptr be_fsm )
be_ptr trace_exec_get_transition_relation( BeFsm_ptr be_fsm )