Changeset 2233 for src/LIN/joint_LTL_LIN_semantics_paolo.ma

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:

• src/LIN/joint_LTL_LIN_semantics_paolo.ma (modified) (1 diff)

src/LIN/joint_LTL_LIN_semantics_paolo.ma

@@ -63 +63 @@
   (* read_result        ≝ *) (λ_.λ_.λ_.
   λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
-  (* eval_ext_seq       ≝ *) (λ_.λ_.eval_ltl_lin_seq)
+  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
   (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
-  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st).
+  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
+  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).