PhilosophersDyn this time
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1 • Share •
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_dyn3.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 1safe. 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 : 20170329
Re: PhilosophersDyn this time
By looking at the P/T net file philo_dyn3unfolded.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 : 20170329
Re: PhilosophersDyn this time
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?
Applied to a multiset, subtract is a multiset subtraction. Is that clearer for you?
Admin Admin
 Posts : 25
Join date : 20161126
Re: PhilosophersDyn this time
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
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 : 9
Join date : 20170104
Re: PhilosophersDyn this time
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 "Wellformed nets" and from Claude Dutheillet's Thesis.
best regards
yann
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 "Wellformed nets" and from Claude Dutheillet's Thesis.
best regards
yann
YannTM Posts : 7
Join date : 20170406
Re: PhilosophersDyn this time
Yann,
thanks for the pointer (again!). I really appreciate the reference.
dalzilio Posts : 31
Join date : 20170329
Re: PhilosophersDyn this time
OK, so for information purpose only, I found:
[1] On wellformed coloured nets and their symbolic reachability graph. G Chiola, C Dutheillet, G Franceschinis, S Haddad  Highlevel Petri nets, 1991  Springer
[2] A symbolic reachability graph for coloured petri nets. G. Chiola. https://doi.org/10.1016/S03043975(96)000102
[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/CDFHtcs97.pdf
[1] On wellformed coloured nets and their symbolic reachability graph. G Chiola, C Dutheillet, G Franceschinis, S Haddad  Highlevel Petri nets, 1991  Springer
[2] A symbolic reachability graph for coloured petri nets. G. Chiola. https://doi.org/10.1016/S03043975(96)000102
[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/CDFHtcs97.pdf
dalzilio Posts : 31
Join date : 20170329
Re: PhilosophersDyn this time
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 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 : 20170406
Re: PhilosophersDyn this time
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 : 20170329
Re: PhilosophersDyn this time
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.
Admin Admin
 Posts : 25
Join date : 20161126
Re: PhilosophersDyn this time
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 wellknown by the previous competitors.
dalzilio Posts : 31
Join date : 20170329
Similar topics
» Bracken Tor to Explore The Time Of Tooth and Claw
» Houdini 1.5 at long Time Control: 100 games.
» Fantage: NIGHT TIME AGAIN!!
» Long time no Fantage Recolor, huh?
» Stockfish 01022015 64bit 4CPU Gauntlet [Long Time Control]
» Houdini 1.5 at long Time Control: 100 games.
» Fantage: NIGHT TIME AGAIN!!
» Long time no Fantage Recolor, huh?
» Stockfish 01022015 64bit 4CPU Gauntlet [Long Time Control]
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum

