The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hello,

On 21 sept. 2011, at 03:32, 左樱 wrote:

  We are defined a relationship "simulation" over two traces and try  to prove the transitive property of it. But we meet some problems when proving the sim_tl case. So I wonder whether I give the proper definition on "simulation".

I have trouble relating what you're saying here and the coq file.

We define a simulation relation over two traces trace1 and trace2 inductively as follow:

(1) Let c c’ ∈ cnd, e e’ ∈ event,  (ge c e)  (ge c’ e’)∈grdevt(GuardEvent), 
simulation   (ge c e)  (ge c’ e’) if bImp c c’ and e = e’

This seems to correspond to the sim_hd case (except you don't talk about the tail of the trace in the definition above).

(2)There is a strictly increasing function λ:dom(trace1) -> dom(trace2)
Such that:
Let i,j ∈ grdevt(GuardEvent),
a. Forall  i∈ trace1 , exists j∈ trace2 , simulation i  (λj)
b. forall j= (ge c e) ∈ trace1 ,if not (j ∈image(trace2)) , exists  k=(ge c’ e’)∈grdevt and j strictly follows k in trace1 and c = c’.

(The domain of a function f is denoted dom(f) and its image image(f) = { f(x) | x ∈ dom(f)}.)

This seems related to the sim_add case, but I see a big difference with the coq file: there is a negated condition in the definition above which is not in sim_add.

What is the definition of simulation you're trying to formalize?

Alan