PhilosophersDyn this time

Hello again, ...

... this time to discuss a different known model, PhilosophersDyn.

(Sorry, I am not allowed to post links yet. My account is not old enough).

The graphical description of the colored net given in the PDF file states that the condition for transition Initialize if [p != q], that I interpret as p is different from q. Nonetheless, file philo_dyn-3.pnml contains the following code (line 110) :

<structure>
<equality>
<subterm>
<variable refvariable="varp"/>
</subterm>
<subterm>
<variable refvariable="varq"/>
</subterm>
</equality>
</structure>

This is quite surprising. Indeed, since there are only one copy of each philosopher "color" in place Outside in the initial marking, the condition [p == q] would entails that either:
(1) the initial marking is dead because I cannot subtract p and q (two copies of p) from Philosopher.All, see arc48 in the PNML file.
(2) the transition can fire (because A - p - p is the same than A - p !) and therefore there is a reachable state with two copies of p in place Think; meaning that the net is not 1-safe. But the results tell otherwise !

I have two questions then:

(1) Should I believe the PNML file or the graphical description (I am afraid my tools can only parse the first one) ?

(2) What is the semantics of subtract(S1, S2). Is it multiset difference ? What is the meaning of subtract({2'p + q}, {1'p + 2'q + 1'r}) ? I guess it could be either 1'p or some kind of error.

Stay tune for my analysis of DotAndBoxes coming soon.

Silvano

By looking at the P/T net file philo_dyn-3-unfolded.pnml I can confirm that the condition used for transition Initialize is p != q.

Anyway, I would like to find a source describing the meaning of the <subtract> operation. Can someone paste the paragraphs corresponding to this element from the ISO standard ?

Silvano

I had a quick look on the standard (sorry, we cannot make available his part publicly, unless we accidentally meet at the Petri net conference ;-).

Applied to a multiset, subtract is a multiset subtraction. Is that clearer for you?

Dear Silvano,

Thanks a lot for submitting the errors in the models.
1) It is indeed p!= q so this will be corrected in the PNML and propagated this year.
2) I confirm what Admin has said. The standard states: Subtract: Multiset x Multiset -> Multiset.

Best regards,
Lom

Hi

Yes, thank you Silvano for finding the bugs in the pnml COL version. I should retroactively get points for previous years where my getting different results for PT and COL was counted against me on that model.

The main issue here is that both colored and PT nets are produced in truth from a third artifact (a CPN AMI model I believe).
So in this instance, the CAMI2PNML for COL produced garbage obviously.

Concerning the S -p -q ; apart that it's pretty ugly, the semantics of multiset bindings for colors is this : the arc inscription to place p must resolve to a Bag(C(p)), where C(p) is the color domain of p. Any binding where the resulting multiset would have negative entries is simply a bad binding (not feasible) remove it from unfolded net.

For me these formal definitions of bindings for colors are found in Chiola/Dutheillet/Francheschini/Haddad '91 or '92, paper on "Well-formed nets" and from Claude Dutheillet's Thesis.

best regards

yann

Yann,

thanks for the pointer (again!). I really appreciate the reference.

OK, so for information purpose only, I found:

[1] On well-formed coloured nets and their symbolic reachability graph. G Chiola, C Dutheillet, G Franceschinis, S Haddad - High-level Petri nets, 1991 - Springer

[2] A symbolic reachability graph for coloured petri nets. G. Chiola. https://doi.org/10.1016/S0304-3975(96)00010-2

[3] Symetries dans les reseaux colores : definition, analyse et application a l'evaluation de performance
par CLAUDE DUTHEILLET LAMONTHEZIE. http: www.theses.fr/1991PA066105

[1] is only on the Springer website, [2] can be found on the LSV website: http: www.lsv.fr/Publis/PAPERS/PDF/CDFH-tcs97.pdf

Hi,

The journal paper CDFH'97 is fine, you do get defs of multiset difference in section 2, there are precautions taken so that we don't get negative (we ask that a >= b).

Claude's thesis is in French, I forgot that fact. I don't know if there are electronic versions, I have a paper one, but that does'nt help you much. In any case besides there being more examples in there, the definitions coincide.

The PhD thesis is not available in electronic form, and she has no personal homepage. But the other references are enough at this point.

French is OK ;-)

YannTM wrote:
Yes, thank you Silvano for finding the bugs in the pnml COL version. I should retroactively get points for previous years where my getting different results for PT and COL was counted against me on that model.

In fact, it was strange because last year, it was OK for the number of states but not for the number of transitions if another tool would have computed the colored version, it would have been easier to detect the problem.

YannTM wrote:
The main issue here is that both colored and PT nets are produced in truth from a third artifact (a CPN AMI model I believe).
So in this instance, the CAMI2PNML for COL produced garbage obviously.

No, this model was produce by Alban when he was in Geneva. It is derived from some higher level vision I guess... but you are right, there were probably translations that mixed up.

Another question about PhiloDyn.

As defined, the Join transition in the colored net allows a new philosopher to join the Neighborhood when there are already more than two philosophers present. If I understand it right, the new Philosopher enters without its Fork, which seems counter intuitive since the number of forks will never be greater than 2. I would have expected an arc from Join to Forks with a decoration of the form 1'<l> + 1'<r> + '1<p> instead of 1'<l> + 1'<r>.

Also, the Leave transition can lead to a situation where there is only one philosopher in the Neighborhood; just take l = r, which should be a deadlock. I guess these deadlocks are interesting for the ReachabilityDeadlock competition. But again, not necessarily desired by the authors.

The PNML file for the COL and PT case are coherent with respect to this behavior, so there is nothing to change for the contest. Nonetheless, I was wondering if this was really the behavior intended by the authors.

We did not had time to look very closely at the possible symmetries of the models (we plan to do it for the next contests though). I think that this may have an impact (e.g. reduce the number of symmetries) since a philosopher entering with a Join is different from the two philosophers who entered during initialization.

Silvano

PS: I haven't found discussions about this in the previous forum, so I posted this for information only. Once again, the models are correct; just different from what a modeler will expect. Sorry if this is already well-known by the previous competitors.