Anemone 1.0.0 documentation

The Multi-Bach language

«  The Multi-Bach language and its temporal logic   ::   Contents

The Multi-Bach language

This page provides the BNF definitions of the Multi-Bach features.

1. MultiBach primitives

Multi-Bach primitives obey to the following syntax:

1
Simple Prim ::=  Basic Prim  |  Proc Prim  |  Rule Prim   |  Scene Prim
Basic Prim  ::=  tell(stInfo)     |  ask(stInfo)     |  get(stInfo)      |  nask(stInfo)

Proc Prim   ::=  tellp(procCall)  |  askp(procCall)  |  getp(procCall)   |  naskp(procCall)

Rule Prim   ::=  tellr(rName)     |  askr(rName)     |  getr(rName)      |  naskr(rName)

Scene Prim  ::=  draw_scene(idLC) |  place_at(idLC, idLC, stInfo, stInfo)|  move_to(idLC, idLC, stInfo, stInfo, stInfo)|
                 hide(idLC, idLC) |  show(idLC, idLC)   |  layer(idLC, idLC, idLC) | att(stInfo, idLC, idLC, stInfo)

where:

stInfo     ::=  idAC | idAC "(" stInfoArgs ")"
stInfoArgs ::=  stInfo | stInfo "," stInfoArgs
procCall   ::=  idUC   | procCall "(" stInfoArgs ")"
rName      ::=  rName  | "-->" | rName
idLC       ::=  (ExprLC ).r
idUC       ::=  (ExprUC).r
idAC       ::=  (ExprAC).r

ExprLC     ::=  " [a-z][0-9a-zA-Z_]* "
ExprUC     ::=  " [A-Z][0-9a-zA-Z_]* "
ExprAC     ::=  " [0-9a-zA-Z_]+ "

2. AnimBach’s agents

2.1. Composite agent

The code of a composite agent:

1
Agent ::= choiceComposedAgent
choiceComposedAgent ::= paraComposedAgent | paraComposedAgent OpChoice choiceComposedAgent

paraComposedAgent   ::= seqComposedAgent  | seqComposedAgent OpPara paraComposedAgent

seqComposedAgent    ::= simpleAgent  | simpleAgent OpSeq  seqComposedAgent
OpChoice  ::= "+"
OpPara    ::= "||"
OpSeq     ::= ";"

2.2. Simple agent

The code of a simple agent:

1
simpleAgent ::=  Prim  |  ProcedureCall  |  ParenthesizedAgent  |  CondAgent  |  SumAgent
ProcedureCall      ::=  idUC | idUC "(" stInfoArgs ")"

ParenthesizedAgent ::=  "(" Agent ")"

CondAgent          ::=  ifThenElseAgent | ifThenAgent

SumAgent           ::= "sum" idLC "in" idLC ":" Agent

where:

ifThenAgent       ::=  abCond "->"  Agent
ifThenElseAgent   ::=  abCond "->"  Agent  "<>"  Agent
abCond            ::=  orCond
orCond            ::=  andCond | andCond op_or orCond
andCond           ::=  simpleCond | simpleCond op_and andCond
simpleCond        ::=  primitiveCond | negCond | parenthesizedCond
primitiveCond     ::=  stInfo relop  stInfo
negCond           ::=  op_neg  abCond
parenthesizedCond ::=  "(" abCond ")"

op_or    ::= "|"
op_and   ::= "&"
op_neg   ::= "!"
relop    ::= op_equal | op_sless | op_leq | op_sge | op_geq

op_equal ::=  "="
op_sless ::=  "<"
op_leq   ::=  "<="
op_sge   ::=  ">"
op_geq   ::=  ">="

3. AnimBach’s procedure

ProcDecls     ::= "proc" |  (ProcedureDecl)*

ProcedureDecl ::= ProcedureName "=" ProcedureBody | "."

ProcedureName ::= idUC | idUC "(" LargsDefProc ")"

LargsDefProc  ::= ArgDefProc | ArgDefProc "," LargsDefProc

ArgDefProc    ::= idLC ":" idUC

ProcedureBody ::= Agent

4. Temporal formulae

1
Ab_ltl_form   ::= Ab_store_form | Ab_store_form "Until" Ab_ltl_form | "Next" Ab_ltl_form | "Reach" Ab_store_form

where:

Ab_store_form   ::= OrStoreForm

OrStoreForm     ::= AndStoreForm | AndStoreForm op_or OrStoreForm

AndStoreForm    ::= SimpleStoreForm | SimpleStoreForm op_and  AndStoreForm

SimpleStoreForm ::= TrueStoreForm | FalseStoreForm | PrimitiveStoreForm | NegStoreForm | ParenthesizedStoreForm

TrueStoreForm          ::= "true"
FalseStoreForm         ::= "false"
PrimitiveStoreForm     ::= Ab_sf_exp relop Ab_sf_exp
NegStoreForm           ::= op_neg Ab_store_form
ParenthesizedStoreForm ::= "(" Ab_store_form ")"

Ab_sf_exp              ::= idInt
idInt                  ::= (ExprInt).r
ExprInt                ::= "[0-9]+"

5. Anemone’s core program

1
 Aabprgm  ::= Aboptset | Aboptmap | Abopteqn | Aboptscene | Aboptproc | Aboptrule

where:

Aboptset    ::= Aboptset "(" SetSpec ")"
Aboptmap    ::= Aboptmap "(" MapSpec ")"
Abopteqn    ::= Abopteqn "(" EqnSpec ")"
Aboptscene  ::= Aboptscene "(" SceneSpec ")"
Aboptproc   ::= Aboptproc "(" ProcDecls ")"
Aboptrule   ::= Aboptrule "(" RuleDecls ")"

5.1. Set specifications

1
SetSpec ::= SetKeyword | SetDecls
SetKeyword ::= "set" | "eset"
SetDecls   ::= SetDecls  idUC  "="  "{"  idACList  "}"  "."
idACList   ::= idAC  |   idAC  ","  idACList

5.2. Map specifications

1
2
MapSpec   ::= "map"
EqnSpec   ::= "eqn"  EqnDecls
EqnDecls  ::= EqnDecls  eqnDecl
eqnDecl   ::= stInfo   "="   stInfo   "."

5.3. Scene description

1
SceneSpec ::=  "scene" | SceneSpec | SceneDef

where:

SceneDef       ::=  idLC      "="  "{"  SizeScene   | LayersScene | ImgsScene | ListWidgetDesc  "}"  "."
SizeScene      ::= "size"     "="  "("  idInt  ","    idInt  ")"  "."
LayersScene    ::= "layers"   "="  "{"  idLC | idLC  "," LayersScene "}"   "."

ImgsScene      ::= ImgsScene imgDef
imgDef         ::= idLC  "="  "loadImage(" idPathFile ")"  "."
idPathFile     ::= (ExprIdPath).r
ExprIdPath     ::= " [.0-9a-zA-Z_/\"]+ "

ListWidgetDesc   ::=  ListWidgetDesc  widgetDesc
widgetDesc       ::= "widget"  idLC  "="  "{"  wdAttributes  wdDisplays  wdInits   "}"

wdAttributes     ::=  wdAttributes "(" realWdAttributes ")"
realWdAttributes ::= "attributes"  "="  "{" realWdAttributes "(" idLC  "in"  idUC "." ")"  "}"

wdDisplays       ::= "display"  "="   "{"  wdDisplays "(" abCond  "->"  idLC  "." | idLC ")"  "}"

wdInits          ::=  wdInits "(" realWdInits ")"
realWdInits      ::= "init"  "="  "{"  realWdInits idLC "=" idLC  "."  "}"

5.3. Rule description

1
RuleDecls ::= "rule" | RuleDecls RuleDef

where:

RuleDef       ::=   idLC  "= "  optVarsInFor  preCRule  "-->"  postCRule  "."

optVarsInFor  ::= optVarsInFor "(" lVarsInFor ")"
lVarsInFor    ::= lVarsInFor     | "for"  lVarsInFor( idLC  "in"  idUC, ",")  ":"

preCRule      ::= lSiStPnElm
postCRule     ::= lSiStPnElm
lSiStPnElm    ::= signedStPnInfo | signedStPnInfo ","  lSiStPnElm

signedStPnInfo ::= signSIElm  stPnInfo
signSIElm      ::=  "+"   |  "-"
stPnInfo       ::= stInfo | ProcedureCall

«  The Multi-Bach language and its temporal logic   ::   Contents