Ignore:
Timestamp:
Jul 23, 2012, 4:51:51 PM (7 years ago)
Author:
tranquil
Message:
  • completed update of ERTL semantics
  • some minor changes in joint semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics_paolo.ma

    r2217 r2233  
    6363  (* read_result        ≝ *) (λ_.λ_.λ_.
    6464  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    65   (* eval_ext_seq       ≝ *) (λ_.λ_.eval_ltl_lin_seq)
     65  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
    6666  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    6767  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    68   (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st).
     68  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     69  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
Note: See TracChangeset for help on using the changeset viewer.