# colored models; questions about Symmetric Nets and PNML

## 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 www-galilee.univ-paris13.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 instance---the code below is taken from one of the models in SimpleLoadBal-pnml---what is the successor of C-clients_no-2 ?

<successor>

<subterm>

<variable refvariable="V-l1-clients_no"/>

</subterm>

</successor>

<namedsort id="T-clients_no" name="clients_no">

<finiteenumeration>

<feconstant id="C-clients_no-0" name="0"/>

<feconstant id="C-clients_no-1" name="1"/>

<feconstant id="C-clients_no-2" name="2"/>

</finiteenumeration>

</namedsort>

<variabledecl id="V-l1-clients_no" name="l1">

<usersort declaration="T-clients_no"/>

</variabledecl>

Many colored models seems to be "1-safe" (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 www-galilee.univ-paris13.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 instance---the code below is taken from one of the models in SimpleLoadBal-pnml---what is the successor of C-clients_no-2 ?

<successor>

<subterm>

<variable refvariable="V-l1-clients_no"/>

</subterm>

</successor>

<namedsort id="T-clients_no" name="clients_no">

<finiteenumeration>

<feconstant id="C-clients_no-0" name="0"/>

<feconstant id="C-clients_no-1" name="1"/>

<feconstant id="C-clients_no-2" name="2"/>

</finiteenumeration>

</namedsort>

<variabledecl id="V-l1-clients_no" name="l1">

<usersort declaration="T-clients_no"/>

</variabledecl>

Many colored models seems to be "1-safe" (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 : 2017-03-29

## 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 : 2016-11-26

## 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 : 2017-03-29

## 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 : 2016-11-26

## 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:

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:

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 : 8

Join date : 2017-01-04

## 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 COL-02 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 COL-02 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 : 4

Join date : 2016-11-30

## 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 : 2017-03-29

## 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 : 2016-11-26

## 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 : 2017-03-29

## 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 Well-formed 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. CPN-AMI 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 Well-formed 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. CPN-AMI 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 : 2017-04-06

## 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 : 2016-11-26

## 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 : 8

Join date : 2017-01-04

## 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 T-clients_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 T-clients_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 : 2016-11-26

## 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:

SimpleLoadBal-COL-02

916 marking(s), 2918 transitions(s)

SimpleLoadBal-PT-02

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:

SimpleLoadBal-COL-02

916 marking(s), 2918 transitions(s)

SimpleLoadBal-PT-02

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 : 2017-03-29

## 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 : 2016-11-26

## 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 : 2016-11-26

## Re: colored models; questions about Symmetric Nets and PNML

For SimpleLoadBal-COL-02 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 : 2017-03-29

## 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 : 2016-11-26

Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission

Page

**1**of**1****Permissions in this forum:**

**cannot**reply to topics in this forum