FW: [abc] found small mistake in the semantics

Sorry, sent this just to Eric by mistake.
For those of you following the semantics discussion...

-----Original Message-----
From: Julian Tibble [mailto:julian.tibble@worcester.oxford.ac.uk]
Sent: 08 October 2006 16:19
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
Received on Sun Oct 08 16:24:41 2006