BNF Symmetric Nets – CosyVerif

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 :

“Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications”, C. Girault and R. Valk (editors), Springer Verlag, 2003,

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:

<Integer> ::= any sequence of numeric character
<PositiveInteger> ::= any sequence of numeric character which value > 0
 <NaturalInteger> ::= any sequence of numeric character which value ? 0
     <Identifier>  ::= any sequence of character starting with a non numeric character
       <Interval> ::= <Integer> .. <Integer>

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.

<Declaration> ::= <ClassSection>
                    [<DomainDeclaration>]
                    <VariableSection>

Declaration of Color Classes (Basic Color Types)

<ClassSection>  ::= class <ListClassDeclarations>
<ListClassDeclarations> ::= <ClassDeclaration> |
                               <ListClassDeclarations> <ClassDeclarations>
     <ClassDeclaration>  ::= <ListClassNames> is [circular] <ClassDescription>;
       <ListClassNames>  ::= <ClassIdentifier> |
                               <ListClassNames> <ClassIdentifier>
       <ClassIdentifier> ::= <Identifier>
     <ClassDescription> ::= <interval> | [<ListElements>]
         <ListElements> ::= <Identifier> |
                              <ListElements>, <Identifier>

Declaration of Color Domains (Composition of Color Classes)

<DomainSection> ::= domain <ListDomainDeclarations>
<ListDomainDeclarations>  ::= <DomainDeclaration> |
                              <ListDomainDeclarations> <DomainDeclaration>
      <DomainDeclaration> ::= <ListDomainNames> is <ProductDefinition>;
        <ListDomainNames> ::= <DomainIdentifier> |
                              <ListDomainNames> <DomainIdentifier>
        <DomainIdentifier> ::= <Identifier>
       <ProductDefinition> ::= <ComponentList>
          <ComponentList> ::= <Component> |
                              <ComponentList>, <Component>
              <Component> ::= <ClassIdentifier> |
                              <DomainIdentifier>

Declaration of variables

<VariableSection> ::= var <ListVariableDeclarations>
<ListVariableDeclarations> ::= <VariableDeclaration> |
                               <ListVariableDeclarations> <VariableDeclaration>
     <VariableDeclaration> ::= <ListVariableNames> in <Component>;
       <ListVariableNames> ::= <VariableIdentifier> |
                               <ListVariableNames>, <VariableIdentifier>
       <VariableIdentifier> ::= <Identifier>

Grammar for Arc Valuations

<ArcLabel> ::= <ListElementaryExpr> |
                           <PositiveInteger>
  <ListElementaryExpr> ::= <ElementaryExpression> |
                           <ElementaryExpression> + <ElementaryExpression> |
                           <ElementaryExpression> - <ElementaryExpression>
<ElementaryExpression> ::= <ElementaryProduct> |
                           <PositiveInteger> * <ElementaryProduct>
   <ElementaryProduct> ::= <ListProdElements>
    <ListProdElements> ::= <ListProdElements> |
                           <ListProdElements>, <ProdElement>
         <ProdElement> ::= <ElementaryExpression> |
                           <VarClassElement>
     <VarClassElement> ::= <VariableIdentifier> |
                           <ClassIdentifier>.<LitteralValue> |
                           <VariableIdentifier>++<PositiveInteger> |
                           <VariableIdentifier>--<PositiveInteger> |
                           <ClassIdentifier>.all
       <LitteralValue> ::= <Integer> | <Identifier>

Grammar for Transition Guards

<TransitionGuard> ::= true | false | [ <Guard> ]
            <Guard> ::= not <Guard> |
                        (<Guard>) |
                        <Guard> and <Guard> |
                        <Guard> or <Guard> |
                        <GuardOperand> <RelOperation> <GuardOperand>
     <GuardOperand> ::= <VarClassElement> |
                        <SimpleBagOperators>
     <RelOperation> ::= = | <> | < | > | <= | >=
<InclusionOperator> ::= included | strictincluded

Grammar for Place Marking

<InitialMarking> ::= <Marking> |
                     <InitialMarking> <Marking>
       <Marking> ::= <ElementaryProduct> |
                     <PositiveInteger> * <ElementaryProduct>