BNF Symmetric Nets

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 transition guards attribute,
  • The arc valuation attribute,
  • The place marking attribute.

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

Wikipedia also offers some useful basic definitions.

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 CosyVerif implementation of Symmetric Nets :

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

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

[/code]

Declaration of Color Classes (Basic Color Types)

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

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

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

Declaration of Color Domains (Composition of Color Classes)

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

::= is ;
::= |

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

[/code]

Declaration of variables

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

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

Grammar for Arc Valuations

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

::= |
+ |

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

::= |
. |
++ |
|
.all
::= |
[/code]

Grammar for Transition Guards

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

::= |

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

Grammar for Place Marking

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

::= |
*
[/code]