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:

::= 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
::= ..

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.

::=
[]
[]

Declaration of Color Classes (Basic Color Types)

::= class
::= |

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

::=
::= | []
::= |
,

Declaration of Equivalence in Color Classes

::= equivalence
::= |

::= in : ;
::= |
,
::= is
::= | Integer

Declaration of Color Domains (Composition of Color Classes)

::= domain
::= |

::= is ;
::= |

::=
::= |

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

::= bag (

Declaration of variables

::= var
::= |

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

Grammar for Arc Valuations

::= |

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

::= |
. |
++ |
-- |
.all
::= |
::= {}
::= |
() |
|
|
~
::= union | inter | diff

Grammar for Transition Guards

::= true | false | [ ]
::= not |
() |
and |
or |
|
unique () |
card () |
in |

::= |

::= = | <> | < | > | <= | >=
::= included | strictincluded

Grammar for Place Marking

::= |

::= |
*