RE: [abc] found small mistake in the semantics

Hi.

Thanks for spotting that! You were right, I was sort of "resetting to
false" too often. What needs to be done is actually, to accumulate the
positive updates when processing an event. I am doing this now in an
accumulating parameter (\gamma_a). This parameter is reset to
(true,false,...) only once before processing the event. This should fix
the problem IMHO. Do you agree? (updated version attached)

Eric

P.S. I had another look at the OOPSLA paper and I think I should be able
to provide a proof along the lines of your section 4.6 where you prove
that for any extension "e" of a trace "t" to "te", we are doing the
correct thing. Also I will try to get my notation closer to the one you
had there.

> -----Original Message-----
> From: Julian Tibble [mailto:julian.tibble@worcester.oxford.ac.uk]
> Sent: Sunday, October 08, 2006 11:19 AM
> To: Eric Bodden
> Subject: RE: [abc] found small mistake in the semantics
>
> Hi Eric,
>
> Thanks for your response, think I'm understanding things a little
> better now.
>
> My confusion stems from the fact that there is no difference in the
way
> the positive bindings are combined and the way that the negative
> bindings are combined except for the use of \gamma_0 - the initial
> configuration. I don't understand why that is correct.
>
> Suppose conf = {
> 1 -> true
> 2 -> x=a
> 3 -> x=a
> 4 -> false
> }
>
> And event e = { (A, {x->a}) }
>
> For the positive edges:
> 1 to 2 labelled B
> 2 to 3 labelled A
> 3 to 4 labelled A
>
> Is it correct that the positive update is the following?
>
> let conf2 = delta(conf, (A, {x->a}), (2, A, 3)) in let conf3 =
> delta(conf2, (A, {x->a}), (3, A, 4)) in
> conf3
>
> Which can be simplified to:
>
> let conf2 = pos(conf, {x->a}, 2, 3) in
> let conf3 = pos(conf2, {x->a}, 3, 4) in
> conf3
>
> And if so, doesn't the use of \gamma_0 in the equation after equation
> 14 mean that conf3 maps everything to false apart from the initial
> state and state 4? If so, that's not correct is it?
>
> Thanks for your patience,
> Julian