include "LIN/joint_LTL_LIN_semantics.ma".
include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)

definition ltl_fullexec : fullexec io_out io_in ≝
 ltl_lin_fullexec … graph_succ_p (graph_fetch_statement … (ltl_lin_sem_params …))
  (graph_pointer_of_label …).