For questions regarding the syntax, please contact Maximilien Colange, Fabrice Kordon, or Yann Thierry-Mieg.

The presentation of the syntax is divided in four parts:

• The declaration attribute,
• The arc valuation attribute,
• The transition guards attribute,
• The place marking attribute.

A precise (and formal) definition can be found here for Symmetric Nets with bags:

• “Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains”, S. Haddad, F. Kordon, L. Petrucci, J-F. Pradat-Peyre, and N. Trèves. 28th American Control Conference (ACC), pages 5018-5025, Omnipress IEEE Catalog, June 2009 – also available here

Grammar: Basic Elements

The grammar is presented as a Backus-Naur form.

First of all, let us define some elements of the grammar:

[code language=”bnf”]
::= any sequence of numeric character
::= any sequence of numeric character which value > 0
::= any sequence of numeric character which value ≥ 0
::= any sequence of character starting with a non numeric character
::= ..
[/code]

Keywords are presented like this; they are case insensitive.

Grammar for the Declaration Attribute

This attribute allows one to declare color types. There are several possibilities in the implementation of Symmetric Nets with Bags :

• Basic types (integer ranges or enumerations),
• cartesian product of these types,
• bags of these types.

Please note that bag-types can be part of cartesian products. There is also the possibility to define explicit equivalence classes.

[code language=”bnf”]
::=
[]
[]

[/code]

Declaration of Color Classes (Basic Color Types)

[code language=”bnf”]
::= class
::= |

::= is [circular] ;
::= |

::=
::= | []
::= |
,
[/code]

Declaration of Equivalence in Color Classes

[code language=”bnf”]
::= equivalence
::= |

::= in : ;
::= |
,
::= is
::= | Integer
[/code]

Declaration of Color Domains (Composition of Color Classes)

[code language=”bnf”]
::= domain
::= |

::= is ;
::= |

::=
::= |

::=
::= |
,
::= |

::= bag (
[/code]

Declaration of variables

[code language=”bnf”]
::= var
::= |

::= in [unique] ;
::= |
,
::=
[/code]

Grammar for Arc Valuations

[code language=”bnf”]
::= |

::= |
+ |
–
::= |
*
::= |
ord () |
ord (.)
::=
::= |
,
::= |
|
|

::= |
. |
++ |
— |
.all
::= |
::= {}
::= |
() |
|
|
~
::= union | inter | diff
[/code]

Grammar for Transition Guards

[code language=”bnf”]
::= true | false | [ ]
::= not |
() |
and |
or |
|
unique () |
card () |
in |

::= |

::= = | <> | < | > | <= | >=
::= included | strictincluded
[/code]

Grammar for Place Marking

[code language=”bnf”]
::= |

::= |
*
[/code]