colored models; questions about Symmetric Nets and PNML
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1 • Share •
colored models; questions about Symmetric Nets and PNML
Hello,
I have some questions about the semantics of symmetric nets.
I have found some helpful information on the slides accessible at wwwgalilee.univparis13.fr/actualite.php?id_info=381 but I have not found any comprehensive definition of the corresponding PNML encoding (outside of the XML schemas). The best documentation seems to be sitting behind a Swiss paywall and I do not plan to grok the PNML schema and OCL definitions yet ! Any help and pointers would be greatly appreciated.
I have already found Marcie's andl tool and am looking into it right now.
I have been able to translate colored Petri nets into standard P/T nets with good results (meaning that I find the correct number of reachable states), except for two models: SimpleLoadBal and DotAndBoxes. I think that the problem is with computing the successor of the last element in a finite enumeration: f1  f2  ...  fn. What is the expected behavior ? Is it possible to compute the successor of fn or is it an error ?
For instancethe code below is taken from one of the models in SimpleLoadBalpnmlwhat is the successor of Cclients_no2 ?
<successor>
<subterm>
<variable refvariable="Vl1clients_no"/>
</subterm>
</successor>
<namedsort id="Tclients_no" name="clients_no">
<finiteenumeration>
<feconstant id="Cclients_no0" name="0"/>
<feconstant id="Cclients_no1" name="1"/>
<feconstant id="Cclients_no2" name="2"/>
</finiteenumeration>
</namedsort>
<variabledecl id="Vl1clients_no" name="l1">
<usersort declaration="Tclients_no"/>
</variabledecl>
Many colored models seems to be "1safe" (with at most one token of a given color in each place). Is there a way to declare this constraint with PNML ?
Finally, one last remark, the model for DotAndBoxes is also the only PNML file with an element of type <numberof> that contains only one subterm (the usual <numberconstant value="1"> element is missing). Is this supposed to declare a token with multiplicity one ?
<numberof>
<subterm>
<tuple>
<subterm>
<useroperator declaration="Player1"/>
</subterm>
<subterm>
<useroperator declaration="Bool1"/>
</subterm>
</tuple>
</subterm>
</numberof>
Sincerely
Silvano
I have some questions about the semantics of symmetric nets.
I have found some helpful information on the slides accessible at wwwgalilee.univparis13.fr/actualite.php?id_info=381 but I have not found any comprehensive definition of the corresponding PNML encoding (outside of the XML schemas). The best documentation seems to be sitting behind a Swiss paywall and I do not plan to grok the PNML schema and OCL definitions yet ! Any help and pointers would be greatly appreciated.
I have already found Marcie's andl tool and am looking into it right now.
I have been able to translate colored Petri nets into standard P/T nets with good results (meaning that I find the correct number of reachable states), except for two models: SimpleLoadBal and DotAndBoxes. I think that the problem is with computing the successor of the last element in a finite enumeration: f1  f2  ...  fn. What is the expected behavior ? Is it possible to compute the successor of fn or is it an error ?
For instancethe code below is taken from one of the models in SimpleLoadBalpnmlwhat is the successor of Cclients_no2 ?
<successor>
<subterm>
<variable refvariable="Vl1clients_no"/>
</subterm>
</successor>
<namedsort id="Tclients_no" name="clients_no">
<finiteenumeration>
<feconstant id="Cclients_no0" name="0"/>
<feconstant id="Cclients_no1" name="1"/>
<feconstant id="Cclients_no2" name="2"/>
</finiteenumeration>
</namedsort>
<variabledecl id="Vl1clients_no" name="l1">
<usersort declaration="Tclients_no"/>
</variabledecl>
Many colored models seems to be "1safe" (with at most one token of a given color in each place). Is there a way to declare this constraint with PNML ?
Finally, one last remark, the model for DotAndBoxes is also the only PNML file with an element of type <numberof> that contains only one subterm (the usual <numberconstant value="1"> element is missing). Is this supposed to declare a token with multiplicity one ?
<numberof>
<subterm>
<tuple>
<subterm>
<useroperator declaration="Player1"/>
</subterm>
<subterm>
<useroperator declaration="Bool1"/>
</subterm>
</tuple>
</subterm>
</numberof>
Sincerely
Silvano
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
Dear Silvano,
Have you been there?
http://www.pnml.org
There are numerous resources for the problems you are mentioning. Maybe Lom could also help (he is the best specialist in PNML ;).
Fabrice
Have you been there?
http://www.pnml.org
There are numerous resources for the problems you are mentioning. Maybe Lom could also help (he is the best specialist in PNML ;).
Fabrice
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
Yes, I have read the docs on the PNML website first before posting here. I have only found information about the syntax (the schemas), but nothing about the semantics.
The schematron file SNetconstraints.sch allows a finite enumeration constant inside a successor, but what is the expected meaning ?
Assume we have a finite enumeration f0, ..., fn. If the successor of fn is equal to f0 then what is the point of having a separate sort for cyclic enumeration.
My initial guess was that a "pattern" of the form (x, y++1) will never match the value (fn, f0) (in some sense the unification should fail), but it looks like this is not the expected behavior.
So what is left then !
The schematron file SNetconstraints.sch allows a finite enumeration constant inside a successor, but what is the expected meaning ?
Assume we have a finite enumeration f0, ..., fn. If the successor of fn is equal to f0 then what is the point of having a separate sort for cyclic enumeration.
My initial guess was that a "pattern" of the form (x, y++1) will never match the value (fn, f0) (in some sense the unification should fail), but it looks like this is not the expected behavior.
So what is left then !
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
OK, in fact, as far as I remember, there was a huge and long discussion about his topic with the two being possible. If you want to do unfolding with the capabilities of ++and , you need to think the type is circular otherwise, you have troubles in the management of bounds.
In the MCC, this is he semantics to understand... Lom, please correct me if I made a mistake.
In the MCC, this is he semantics to understand... Lom, please correct me if I made a mistake.
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
Dear Silvano,
Indeed the use of the successor function requires the enumeration be cyclic. The standard states that as an OCL constraint on the abstract type CyclicEnumOperator from which Successor and Predecessor are derived: context CyclicEnumOperator: self.input>size() = 1 and self.input.oclIsTypeOf(CyclicEnumeration) and selft.output.oclIsTypeOf(CyclicEnumeration).
It was not captured in the PNML schema. It must not have been captured in the Schematron constraints either (which are not complete wrt. to all the constraints that should be captured) but contributions will be welcome.
Thanks very much for bringing up these bugs in the models. Indeed, in SimpleLoadBal the successor must not be used on a variable which references a constant from a finite enumeration. In DotAndBoxes, the usual <numberconstant> is missing. It is required by the standard: context NumberOf inv: self.input>size() = 2 and self.input>forAll{c , d  c.oclIsTypeOf(Integer::Natural) and d.oclIsKindOf(Terms::Sort)} and self.output.oclIsKindOf(Terms:MultisetSort). I will patch these 2 models and their corresponding instances.
Best regards,
Lom
Indeed the use of the successor function requires the enumeration be cyclic. The standard states that as an OCL constraint on the abstract type CyclicEnumOperator from which Successor and Predecessor are derived: context CyclicEnumOperator: self.input>size() = 1 and self.input.oclIsTypeOf(CyclicEnumeration) and selft.output.oclIsTypeOf(CyclicEnumeration).
It was not captured in the PNML schema. It must not have been captured in the Schematron constraints either (which are not complete wrt. to all the constraints that should be captured) but contributions will be welcome.
Thanks very much for bringing up these bugs in the models. Indeed, in SimpleLoadBal the successor must not be used on a variable which references a constant from a finite enumeration. In DotAndBoxes, the usual <numberconstant> is missing. It is required by the standard: context NumberOf inv: self.input>size() = 2 and self.input>forAll{c , d  c.oclIsTypeOf(Integer::Natural) and d.oclIsKindOf(Terms::Sort)} and self.output.oclIsKindOf(Terms:MultisetSort). I will patch these 2 models and their corresponding instances.
Best regards,
Lom
lhillah Posts : 9
Join date : 20170104
Re: colored models; questions about Symmetric Nets and PNML
Dear Fabrice, Lom, Silvano,
Dear All,
I think that the SimpleLoadBal model does not use a circular semantics, at least for what concerns the provided unfolding from COL instances to PT instances. It seems that the semantics is the following: if a transition instance is not possible, due to an "overflow/underflow" of the successor/predecessor function on the colored tokens, than the transition instance is dropped.
For instance, if I use this semantics on the COL02 instance, I obtain 32 places and 45 transitions from the unfolding, exactly like the provided unfolded PT model.
If instead I treat the colors as circular enumerations, I obtain 32 places and 65 transitions from the unfolding.
For this specific model, this does not seem to change the state space.
However, it looks like the provided unfolding uses this overflow/underflow semantics. (or maybe my unfolding is wrong )
Regards.
Elvio
Dear All,
I think that the SimpleLoadBal model does not use a circular semantics, at least for what concerns the provided unfolding from COL instances to PT instances. It seems that the semantics is the following: if a transition instance is not possible, due to an "overflow/underflow" of the successor/predecessor function on the colored tokens, than the transition instance is dropped.
For instance, if I use this semantics on the COL02 instance, I obtain 32 places and 45 transitions from the unfolding, exactly like the provided unfolded PT model.
If instead I treat the colors as circular enumerations, I obtain 32 places and 65 transitions from the unfolding.
For this specific model, this does not seem to change the state space.
However, it looks like the provided unfolding uses this overflow/underflow semantics. (or maybe my unfolding is wrong )
Regards.
Elvio
amparore Posts : 6
Join date : 20161130
Re: colored models; questions about Symmetric Nets and PNML
Dear all,
I will also be in favor of using the overflow/underflow semantics. (This is what I was doing initially.)
Could you please confirm if this is what will be used during the competition and post a new version of the PNML file if you plan to do some changes ?
To help with the discussion, I have posted a new message with a way to reproduce my current results.
Silvano
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
I had a discussion with Lom and apparently he agrees on the fact that the semantic is not the one I was thinking of. The update on the PNML will be done and pushed in a new archive as soon as possible. Anyway, you may prepare your VMs and check for them. I usually update the INPUT directory with formulas and surprise models after the qualification phase ;).
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
Sorry but the answer is not clear enough for me.
Could you told us, yes or no, if: ((3) and (2) are exclusive)
(1) we should expect to find models containing successor(x) in an "edge pattern" where x is a variable of type Finite Enumeration.
(2) if yes to (1), then the computed reachability graph of the model should not have a transition for the case where x stands for the last value in a finite enumeration.
(3) if yes to (1), then the computed reachability graph of the model should have a transition for the case where x stands for the last value in a finite enumeration and x++1 stands for the first value in this enumeration.
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
Just as feedback,
My own translation does rely on the standard being correct, I just assume Cyclic if I meet successor => I always add a modulo to the increment.
I've seen models that add a guard specifying x != Max if they want to suppress the circular behavior.
Successor, in the Wellformed net definitions at least, is only applicable to CircularTypes, and is not to be confused with arithmetic +, in the sense that circularTypes do not admit an order relation, just this successor relation.
This is important to get the "symmetry" properties, i.e. the elements of the domain admit a rotation as symmetry.
In more loose models, e.g. CPNAMI colored nets, you could mix successor and guards such as x < y, in which case I would interpret as non circular domain, but I'm unsure w=how to treat overflow if other guard elements don't explicitly forbid them
My own translation does rely on the standard being correct, I just assume Cyclic if I meet successor => I always add a modulo to the increment.
I've seen models that add a guard specifying x != Max if they want to suppress the circular behavior.
Successor, in the Wellformed net definitions at least, is only applicable to CircularTypes, and is not to be confused with arithmetic +, in the sense that circularTypes do not admit an order relation, just this successor relation.
This is important to get the "symmetry" properties, i.e. the elements of the domain admit a rotation as symmetry.
In more loose models, e.g. CPNAMI colored nets, you could mix successor and guards such as x < y, in which case I would interpret as non circular domain, but I'm unsure w=how to treat overflow if other guard elements don't explicitly forbid them
YannTM Posts : 7
Join date : 20170406
Re: colored models; questions about Symmetric Nets and PNML
So far, the use of successor/predecessor functions means that the color domain is circular. If not, there is probably a mistake. As far as I understand (but you should check with Lom), the standards allows successor on non cyclic types (I remember big discussions on this issue), at least for the current version (to be replaced by a revision we are working on).
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
Dear All,
As stated in the constraint reported earlier, and in Yann's and Admin's comments, you should assume cyclicenumeration when you meet the successor/predecessor functions. The model Silvano has reported is now corrected for the 2017 edition.
Best regards,
Lom
As stated in the constraint reported earlier, and in Yann's and Admin's comments, you should assume cyclicenumeration when you meet the successor/predecessor functions. The model Silvano has reported is now corrected for the 2017 edition.
Best regards,
Lom
lhillah Posts : 9
Join date : 20170104
Re: colored models; questions about Symmetric Nets and PNML
I will propagate the archive with the three models updated with the three patches from Lom as soon as possible (I am traveling this week).
1) Correct finitenum into cyclicenum for sort Tclients_no in SimpleLoadBal
2) Add missing <numberconstant> subterm in incomplete <numberof> elements on DotAndBoxes
3) fixed condition on transition Initialize in PhiloDyn (ineq instead of eq)
1) Correct finitenum into cyclicenum for sort Tclients_no in SimpleLoadBal
2) Add missing <numberconstant> subterm in incomplete <numberof> elements on DotAndBoxes
3) fixed condition on transition Initialize in PhiloDyn (ineq instead of eq)
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
Just a remark.
Now that model SimpleLoadBal uses a cylicenum, I think that equiv_pt should be set to FALSE.
For instance, from the files in the 2017 VM I obtain:
SimpleLoadBalCOL02
916 marking(s), 2918 transitions(s)
SimpleLoadBalPT02
832 marking(s), 2650 transitions(s)
Now that model SimpleLoadBal uses a cylicenum, I think that equiv_pt should be set to FALSE.
For instance, from the files in the 2017 VM I obtain:
SimpleLoadBalCOL02
916 marking(s), 2918 transitions(s)
SimpleLoadBalPT02
832 marking(s), 2650 transitions(s)
Last edited by dalzilio on Wed 19 Apr  12:23; edited 1 time in total
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
Hello Silvano,
This is in fact to be checked first. Both colored and P/T versions were provided by Samy Evangelista who confirmed it was supposed to be cyclic. But if his tool was using the actual definition, maybe, P/T instances should be regenerated too.
We will check this with Lom and come back to you.
This is in fact to be checked first. Both colored and P/T versions were provided by Samy Evangelista who confirmed it was supposed to be cyclic. But if his tool was using the actual definition, maybe, P/T instances should be regenerated too.
We will check this with Lom and come back to you.
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
We have started to check with the author. But last year, both outputs from P/T and colored where correct and I bet that at least ITS has a cyclic interpretation (the outputs were then confirmed by Marcie). So this should be double checked at least with Yann, and probably with Christian.
Best regards.
Fabrice
Best regards.
Fabrice
Admin Admin
 Posts : 25
Join date : 20161126
Re: colored models; questions about Symmetric Nets and PNML
For SimpleLoadBalCOL02 I find the same numbers of states and transitions than the PT version when I use the overflow semantics. I think this was also observed by Elvio (@amparore).
The numbers that I give (916 marking(s), 2918 transitions(s)) are with the cyclicenum semantics. So this is normal if the PT version have not been updated since last year.
I just wanted to point out the fact that, currently, the file equiv_pt tells us TRUE.
dalzilio Posts : 31
Join date : 20170329
Re: colored models; questions about Symmetric Nets and PNML
In fact it should be. This is not a problem because, if necessary, I can disconnect the two models from my analysis scripts if we cannot solve the problem on time.
Admin Admin
 Posts : 25
Join date : 20161126
Similar topics
» Game Insight answer questions
» DarkStar Developer Jeff Williams On Board to Answer Any Questions
» Playmates TMNT Classics
» Lost in Space ~ The Pod
» Questions about the game
» DarkStar Developer Jeff Williams On Board to Answer Any Questions
» Playmates TMNT Classics
» Lost in Space ~ The Pod
» Questions about the game
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

