source: src/LTL/semantics.ma @ 1451

Last change on this file since 1451 was 1451, checked in by sacerdot, 8 years ago
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File size: 267 bytes
Line 
1include "LIN/joint_LTL_LIN_semantics.ma".
2include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition ltl_fullexec : fullexec io_out io_in ≝
5 ltl_lin_fullexec … graph_succ_p (graph_fetch_statement … (ltl_lin_sem_params …))
6  (graph_pointer_of_label …).
Note: See TracBrowser for help on using the repository browser.