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>