Thank you for helping me understand with your explanation.

Your event semantics has two invariant.

 1. for all e, t : occurrence of [e] at time [t] is one or zero.
 2. if primitive [e] is occurred in time [t], update cycle runs in time [t].

Do you have any experience to proof a theorem against event combination term
by using above axiom and event combinators semantics? I'm interested in this
kind of reasoning.

(2012/04/19 19:31), Daniel Bünzli wrote:
Right. But you still have to maintain some kind of mapping between the 
primitive event and the leaves they may influence to know which ones to update 
when the corresponding primitive event occurs. Do you store that in the 
primitive event itself or do you use a global data structure ?

Primitive events has list of leaves.


Best Regards,
 Ogasawara

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Reply via email to