ATACORA
The ATS (Abstract Transition System) working grammar :
/*------------------------------------------------------------------*/
/* Basic Form of ATS (Abstract Transition Systems) */
/* An ATS is a transition system equipped with data
The data is not specific
but 'abstract' so as to capture various description
The transitions are described as guarded statement
The expected interest : to use ATS as a common description
Guarded statements avoid the exhaustive description
(c) J. C. Attiogbé, LINA, Mars 2004, NatIF Project
Updates
December 2004 :
January 2005 :
/*-----------------------------------------------------------------*/
/*------------ Shape of a basic ATS (without composition) */
<ATS> ::= <DataPart> <Transitions>
<DataPart> ::= DATAPART <TypeDef> <VariableDef>
/* Generic Data Language */
<TypeDef>::= TYPES <TheTypes>
/*sets may be used as support for types
existing/predefined types; user defined types
*/
<TheTypes> ::=
<!UsusalTypes>
| <Sets>
| <Relations>
| <Functions>
...
<VariableDef> ::= <GlobalVars> <LocalVars>
/* variables are typed
GlobalVars and LocalVars have the same description
*/
<GlobalVars> ::=
GLOBAL_VARS /*! keyword !*/
<VarDecl_List>
<VarDecl> ::=
[<VarQualifier>] <Variable> : <TheTypes>
<VarDecl_List> ::= <VarDecl> ( "," <VarDecl> )*
<VarQualifier> ::= in /* input only */
| out /* ouput only */
| io /* both input and output */
| ...
<LocalVars> ::=
LOCAL_VARS /*! keyword !*/
<VarDecl_List>
<Variable> ::= /* alphanumeric as usually */
...
GLOBAL_PROPERTIES /*! keyword !*/
<Predicate>
LOCAL_PROPERTIES /*! keyword !*/
<Predicate>
LIVENESS /*! keyword !*/
<Predicate>
SAFETY /*! keyword !*/
<Predicate>
INITIALISATION
<StatementKeyWord> "{" <Statement_List> "}")*
<Transitions> ::= <ATSBehaviourKeyword>
/*List of non deterministic named guarded transitions */
(<TransitionName> "="
<LocalCtxKeyword> <LocalContext>
<TBehaviourKeyword>
[] <Guard><Constraints> --<Label>--> <StatementKeyWord> "{" <Statement_List> "}")*
<ATSBehaviourKeyword> ::= BEHAVIOUR
<TransitionName> ::= /* ID */
<LocalCtxKeyword> ::= LOCALCONTEXT
<LocalContext> ::= <VarDecl_List> <Predicate>
/* variable decl. + predicate(localV, globalV) */
<BehaviourKeyword> ::= TRANSITION
<Guard> ::=
/* Predicate expressed in the data language */
<Predicate>
<Constraints> ::=
<Predicate>
| <SpecificConstraint>
| <ImportedConstraint> <Formalism>
<SpecificConstraint> ::=
at <delai> ... /* timing constraint */
every <delai> ... /* scheduling */
...
<ImportedConstraint> /* Constraints imported from a given formalism */
<Label> ::= /* ID */
... /* just a label ??*/
/*------------------------- MODULES ---------------------*/
<Identifier> "=" <ATS> /* named ATS */
/* Renaming ---------------------------*/
<ATS> ::= Rename <ATS> <ID_Substitution>
<ID_Substitution> ::= (<Renaming>)*
<Renaming> ::= <Identifier> "/" <Identifier>
/* Hidding -----------------------------
hide some variable from the ATS */
<ATS> ::= HideVar <ATS> <VarList>
/* the hidden variables become local */
/* Extension---------------------------
extends an existing ATS */
<ATS> ::= Extends <ATS> <ATS>
/* the second one complements the firts */
/* parallel composition operators -----*/
/* 1 : asynchronous parallel composition
with possibly shared (global) variables
*/
<ATS> := <ATS> "]|[" <ATS> /* binary */
| "]|[" <Boundary> <ATS> /* n-ary */
/* 2 : synchronous parallel composition
with possibly shared (global) variables
*/
<ATS> = <ATS> "[|]" <ATS>
| "]|[" <Boundary> <ATS>
<Boundary> ::= /!* like i= 1..n or "x \in setdef "/
...
/*----------------- MISC --------------------------------*/
<delai> ::= ... /* pour gestion du temps */
<Predicate> ::= ... /* First Order Logic */
<Expression> ::= ... /* As usuallly BUT DataPart-Dependent */
<Statement> ::= <Assignment>
<Statement_List> := <Statement> [(Statement)]*
<StatementKeyWord> ::= nondeterminitic
| atomic
| ...
<Assignment> ::= <Variable> ":=" <Expression>
...
/*-------------------------------------------------------*/
'Concrete' form of guarded statement
Transition_name =
LOCALCONTEXT
VarDecl
GUARD
Predicate
CONSTRAINTS
Predicate
THEN [label = actionname]
Statements
END
/*-------------------------------------------------------*/
'Concrete' form of ATS
ATS
Nom
DATAPART
TYPES
...
GLOBALVARS
...
LOCALVARS
...
GLOBAL_PROPERTIES
...
LOCAL_PROPERTIES
...
LIVENESS
...
SAFETY
...
INITIALISATION
...
BEHAVIOUR
t1 =
LOCALCONTEXT ...
TRANSITION ...
GUARD ... --label--> Stat
t2 =
LOCALCONTEXT ...
TRANSITION ...
GUARD ... --label--> Stat
...
STA
/*--------------------------------------------------*/
Atacora Home Page
Christian Attiogbé