AUTOC format

AUTOC format

General structure.

<autoc> ::= <type_definition>*
<channel_declarations>*
<process_decl>+
<system_decl>
[<explicit_decl>]
<pragma>*

Declarations.

<type_definition> ::= type <ident> = enum { <ident> (,<ident>)* } ;
<channel_declarations> ::= channel <channel_decl> (,<channel_decl>)* ;
<channel_decl> ::= <ident>( [<type> (,<type>)*] )

The declaration part possibly defines enumerated types. Labels should be different among different types, and different from variable names.

The declaration of a channel consists in a channel name, followed by the type of its parameters when the channel carries communication parameters. The non-terminal "type" is the same as for NBAC.

Processes.

<process_decl> ::= processs <ident> <process_body>
<process_body> ::= { [<sync_decl>] [<var_decl>] <init_decl> <location>+ }
<sync_decl> ::= sync <ident> (,<ident>)* ;
<var_decl> ::= var <ident> (,<ident>)* : <type> ;)+
<init_decl> ::= init <expression> ;

The syntax of expressions is the same as for NBAC.

Locations & (hybrid) transitions.

<location> ::= loc <ident> [<continuous>] <transition>*
<continuous> ::= continuous <dexpr> ;
<transition> ::= [<integer>:] when <expression> [<synchronisation>] goto <ident> [<assignements>] ;
<synchronization> ::= sync <ident> ( [<ident> (,<ident>)*] )
<assignements> ::= assign { <assign> (;<assign>)* [;] }
<assign> ::= <ident> := <expression>

Composition.

<system_decl> ::= system <ident> (,<ident>)* ;
<explicit_decl> ::= explicit <ident> (,<ident>)* ;
<pragma> ::= #pragma <ident> " ([^"]) * "
Bertrand Jeannet, February 10, 2011

AUTOC format