Dear Missi,
(This could be interesting for all, so I Cc to the list)
On Wednesday 17 March 2004 11:47, you wrote:
> > Dear Missi,
> >
> > On Wednesday 17 March 2004 10:36, you wrote:
> > > Hi.
> > >
> > > Is there only one parallel operator in CSPJassda ?
> > > Does it correspond to the parallel operator || in CSP
> > > (synchronization on all actions) or the other parallel=20
> > > operator ||| in CSP (strict interleaving) ?
> >
> > Yes, only one parallel operator with synchronisation on all common
> > events (intersection of the alphabets).
>
> Do you plan to implement the parallel operator that corresponds to the
> strict interleaving ? Or can we use the parallel operator || to
> describe that ?
Short answer: no and no ;-)
We could implement an interleaving operator, but I'm not sure if this would=
be=20
a good idea. I would not like the semantics for this very much:
1.)
P --e--> P' , \notexists Q' : Q --e--> Q'
___________________________________________
P ||| Q --e--> P' ||| Q =20
2.)
Q --e--> Q' , \notexists P' : P --e--> P'
___________________________________________
P ||| Q --e--> P ||| Q' =20
3.)
P --e--> P' , Q' : Q --e--> Q'
___________________________________________
P ||| Q --e--> P' ||| Q [] P ||| Q'=20
This "expansion" of the state space (or better: the "state size") in the th=
ird=20
rule of the operational semantics could be somewhat dangerous (especially f=
or=20
runtime checking). But we already have a similar construction for the=20
skipping so perhaps this is not a real problem.
> [...]
> write something like that:
> eventset a1{...}
> eventset a2{...} // a1 and a2 correspond to the same eventset in fact
> eventset b{...}
> eventset c{...}
> R =3D a1.begin -> a1.end -> b.begin -> b.end -> R [] SKIP
> S =3D a2.begin -> a2.end -> c.begin -> c.end -> S [] SKIP
> M =3D R || S ; STOP
>
No, this would not work. The names of the event sets are not relevant for=20
alphabet calculation.
But are you sure, that a1 and a2 should be the same event sets? Or should i=
t=20
read as:
R(c) =3D c.a.begin -> c.a.end -> SKIP
P(b) =3D b.begin -> b.end -> SKIP
M =3D ||c:[instance] @ R(c) ; ( P(b) || P(c) ) ; STOP
In any case this seems to be a complicated process. Can you give me an idea=
of=20
what kind of software should behave accordingly to this specification?
> >The alphabet is calculated such that it
> > includes the minimum number of required events.
> >
> > (using simplified syntax:)
> >
> > P =3D a -> P [] SKIP
> > Q =3D b -> Q [] SKIP
> >
> > In case of:
> > 1.) M =3D a -> (P || Q ) ; b -> STOP
> > alphabet(P) =3D a
> > alphabet(Q) =3D b
> > 2.) M =3D a -> (P || Q ) ; Q
> > alphabet(P) =3D a
> > alphabet(Q) =3D a+b
> > (with + meaning event set union)
>
> I am a bit lost here. Why do the alphabets of P and Q depend on the
> way other processes (in that case, M) refer to them ?
>
This is because process references must have the same static alphabet in an=
y=20
context (only parameters may have different bindings and thus could result =
in=20
different dynamic alphabets). Since we "guess" the alphabet of a process fr=
om=20
its context we choose the minimum set of events.
We could require explicit alphabets. This would sometimes be more easy to=
=20
understand, but I think it is also inconvenient.
So the rules are:
a -> P requires alphabet(a -> P) =3D alphabet(P) and a \subset alphabet=
(P)
P [] Q requires alphabet(P [] Q) =3D alphabet(P) =3D alphabet(Q)=20
P || Q requires alphabet(P || Q) =3D alphabet(P) \union alphabet(Q)=20
P ; Q requires alphabet(P ; Q) =3D alphabet(P) =3D alphabet(Q)=20
In the first case it is not required that alphabet(Q) includes b whereas in=
=20
the second case the last rule requires it.
BTW: I'm unsure about the second rule. This is the way it is implemented, b=
ut=20
perhaps the second "=3D" should be replaced by a \union. Only in case of=20
process references this would make a difference. Has anyone an opinion on=20
that?
> > So with the new version of Jassda I provided a patch-script. Have
> > you tried to get your example running with Jassda, again? Have you=20
> > been successful?
>
> Yes, I have used the patch and my example works now :)
That is good news! :o)
> Well, my example is just a very simple java class, I have not used
> jassda on more interesting examples yet.
>
If you have more interesting examples sometime and you would like to share=
=20
them we would be happy if we could include them in a Jassda release.
Best regards,
Michael
=2D-=20
Michael M=F6ller University of Oldenburg, Faculty II,
Dept. of Computing Science, D-26111 Oldenburg, Germany
phone:+49 441 798-3483 fax:+49 441 798-2965
mailto:Mic...@in...
|
