PhilosophersDyn this time

View previous topic View next topic Go down

PhilosophersDyn this time

Post by dalzilio on Mon 3 Apr - 0:05


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


dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by dalzilio on Mon 3 Apr - 10:40


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

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by Admin on Wed 5 Apr - 20:36

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?

Admin
Admin

Posts : 24
Join date : 2016-11-26

View user profile http://mc-contest.forumactif.com

Back to top Go down

Re: PhilosophersDyn this time

Post by lhillah on Thu 6 Apr - 10:47

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

lhillah

Posts : 8
Join date : 2017-01-04

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by YannTM on Thu 6 Apr - 13:06

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

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

YannTM

Posts : 7
Join date : 2017-04-06

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by dalzilio on Thu 6 Apr - 14:31


Yann,

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

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by dalzilio on Thu 6 Apr - 15:02

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

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by YannTM on Thu 6 Apr - 17:51

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.

YannTM

Posts : 7
Join date : 2017-04-06

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by dalzilio on Thu 6 Apr - 17:56


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 ;-)

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by Admin on Sat 8 Apr - 19:32

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

In fact, it was strange because last year, it was OK for the number of states but not for the number of transitions Basketball 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.

Admin
Admin

Posts : 24
Join date : 2016-11-26

View user profile http://mc-contest.forumactif.com

Back to top Go down

Re: PhilosophersDyn this time

Post by dalzilio on Wed 19 Apr - 19:46


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.

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: PhilosophersDyn this time

Post by Sponsored content


Sponsored content


Back to top Go down

View previous topic View next topic Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum