jassda-discuss

[Michael M. <Michael.Moeller@Informatik.Uni-Oldenburg.DE>]

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...