\documentclass{article}

\usepackage[margin=30mm,a4paper,landscape]{geometry}
\usepackage{circus}

\newcommand{\opt}{~\textrm{opt}~}
\newcommand{\unique}{~\textrm{unique}~}

%\AddToShipoutPicture{\AtTextLowerLeft{\framebox(\LenToUnit{\textwidth},\LenToUnit{\textheight}){}}}

\begin{document}

\begin{zsection}
  \SECTION StateflowAbstractSyntax \parents basic\_toolkit
\end{zsection}

A frequent type used in Stateflow charts is the type name: charts, states, data,
events and functions have names. We define the sets of name and subsets that
correspond to each of the types that have associated names.
The set of names of charts, states, data, events and functions are disjoint sets of names.

\begin{axdef}
CNAME, SNAME, DNAME, ENAME, FNAME: \power NAME
\where
\disjoint \langle CNAME, SNAME, DNAME, ENAME, FNAME \rangle
\end{axdef}

We define the sets of identifiers of each of the elements of Stateflow in the same way
we defined the sets of names. We must also include set of identifiers of junctions and
transitions which have no name.

\begin{axdef}
CID, SID, JID, TID, EID, DID, FID: \power \nat
\where
\disjoint \langle CID, SID, JID, TID, EID, DID, FID \rangle
\end{axdef}

One of the most basic elements of the Stateflow notation are expressions.
Expressions are elements of the notations that have an associated value,
for example, the number $1$ has value 1, the expression $1+1$ has value 2, etc.

An expression can be a variable name, a value, a function application, an
operator applied to one or more expressions, or a temporal expression. For a
description of the operators see Appendix \ref{app:X}.

%begin teste
\begin{zed}
EXPR ::= name\ldata DNAME\cross \seq EXPR\rdata |\\
	 value\ldata \arithmos\rdata |\\
     array\ldata \seq_1 \arithmos\rdata |\\
     matrix\ldata \seq_1\seq_1\arithmos\rdata |\\
     fun\ldata NAME\cross \seq EXPR\rdata|\\
	 not\ldata EXPR\rdata |\\
	 and\ldata EXPR\cross EXPR\rdata |\\
	 or\ldata EXPR\cross EXPR\rdata |\\
	 bnot\ldata EXPR\rdata |\\
	 band\ldata EXPR\cross EXPR\rdata |\\
	 bor\ldata EXPR\cross EXPR\rdata |\\
	 bxor\ldata EXPR\cross EXPR\rdata |\\
	 neg\ldata EXPR\rdata |\\
	 sum\ldata EXPR\cross EXPR\rdata |\\
	 sub\ldata EXPR\cross EXPR\rdata |\\
	 mult\ldata EXPR\cross EXPR\rdata |\\
	 division\ldata EXPR\cross EXPR\rdata |\\
	 modulus\ldata EXPR\cross EXPR\rdata |\\
	 lshift\ldata EXPR\cross EXPR\rdata |\\
	 rshift\ldata EXPR\cross EXPR\rdata |\\
	 gt\ldata EXPR\cross EXPR\rdata |\\
	 lt\ldata EXPR\cross EXPR\rdata |\\
	 geq\ldata EXPR\cross EXPR\rdata |\\
	 leq\ldata EXPR\cross EXPR\rdata |\\
	 eq\ldata EXPR\cross EXPR\rdata |\\
	 neq\ldata EXPR\cross EXPR\rdata |\\
	 in\ldata SNAME\rdata |\\
	 after\ldata EXPR\cross ENAME\rdata |\\
	 before\ldata EXPR\cross ENAME\rdata |\\
	 at\ldata EXPR\cross ENAME\rdata |\\
	 every\ldata EXPR\cross ENAME\rdata |\\
	 tempCount\ldata ENAME\rdata\\
\end{zed}
%end teste

The set of temporal expressions is the range of the constructors of those expressions.

\begin{zed}
TEXPR == \ran after \cup \ran before \cup \ran at \cup \ran every \cup \ran tempCount
\end{zed}

In general, expressions don't alter the state of the system, except for a particular
type of function expressions. When the function being applied is a graphical function,
it can change data value.

Actions, on the other hand, in general, alter the state of the system and do not have
an associated value. An expression can be used as an action, in which case the state may
or may not be modified. Other types of action are the broadcasting of an event, the
assignment of an expression to a variable and the sequential composition of two actions.

\begin{zed}
ACTION ::= bcast\ldata ENAME\cross (SID\cup CID)\rdata |\\
	   expr\ldata EXPR\rdata |\\
	   assign\ldata DNAME \cross \seq EXPR \cross EXPR\rdata |\\
	   massign \ldata \seq DNAME \cross EXPR\rdata
\end{zed}

A derived type of action is an on action, which associated an action to an event name.

\begin{zed}
ONACTION == ENAME \cross \seq ACTION
\end{zed}

A state contains an identifier, a name, a reference to its parent, information
about its type and decomposition, entry, during and exit actions, and a list of bound
variables and events.

While the decomposition of a state refers to the organisation of its sub-states, the
type of a state refers to the way it is organised with respect to its siblings. The
terms used to represent type are the same as for decomposition, but their meanings
are different.

\begin{zed}
DECOMP ::= SEQ | PAR
\end{zed}

\begin{zed}
STYPE == DECOMP
\end{zed}

The parent of a state can be either a state or a chart, the set of possible identifiers
of a parent is $CID \cup SID$. Some of the information contained in a state are optional,
e.g., entry and exit actions.

Unlike entry and exit action, a during action can be either a regular action or
an on action. We define the type of during actions as follows. The component $during$
is a sequence of during actions.

\begin{zed}
DACTION ::= action\ldata \seq ACTION \rdata | on\ldata ONACTION \rdata
\end{zed}

\begin{schema}{State}
identifier: SID\\
name: SNAME\\
parent: CID\cup SID\\
decomp: DECOMP\\
type: STYPE\\
entry, exit: \seq ACTION\\
during: \seq DACTION\\
binding: \seq (ENAME \cup DNAME)\\
history: \boolean\\
default, inner, outer: \opt TID\\
left, right: \opt SID\\
substates: \seq SID
\end{schema}

A junction has an identifier, a reference to its parent and the first outgoing transition, and information about whether or not it is a history junction.

\begin{schema}{Junction}
identifier: JID\\
parent: CID \cup SID\\
transition: \opt TID\\
history: \boolean
\end{schema}

A transition has a sequence of triggers, a condition, a condition action and a transition actions.
A trigger is either an event or a temporal expression.

\begin{zed}
TRIGGER ::= e\ldata ENAME\rdata | t\ldata TEXPR\rdata
\end{zed}

\begin{schema}{Transition}
identifier: TID\\
parent: CID \cup SID\\
source: \opt (SID \cup JID)\\
destination: SID \cup JID\\
trigger: \seq TRIGGER\\
condition: \opt EXPR\\
condact: \seq ACTION\\
transact: \seq ACTION\\
next: \opt TID
\end{schema}

An event has trigger type and scope; the trigger type can be rising edge, falling edge, either edge or function call, and the
event scope can be local, input or output.

\begin{zed}
EVENTTRIGGER ::= RISINGEDGE | FALLINGEDGE | EITHEREDGE | FUNCTIONCALL\\
EVENTSCOPE ::= LOCALEVENT | INPUTEVENT | OUTPUTEVENT
\end{zed}

The representation of an event consists of an identifier and a name, a reference to its parent, and information about its scope and trigger type.

\begin{schema}{Event}
identifier: EID\\
name: ENAME\\
parent: CID \cup SID\\
scope: EVENTSCOPE\\
trigger: EVENTTRIGGER\\
\end{schema}

Data has a larger choice of scopes; they can be local, input, output, constant, parameter and data store memory. The type of the data is restricted
to scalar types and multi-dimentional vectors of scalar types.

\begin{zed}
DATASCOPE ::= LOCALDATA | INPUTDATA | OUTPUTDATA | CONSTANTDATA | PARAMETERDATA | DATASTOREMEMORYDATA\\
SCALAR ::= BOOLEAN | DOUBLE | SINGLE | INT32 | INT16 | INT8 | UINT32 | UINT16 | UINT8\\
DATATYPE ::= scalar\ldata SCALAR\rdata | vector \ldata SCALAR \cross \seq \nat\rdata
\end{zed}

A piece of data consists of an identifier and a name, a reference to its parent, and information about its scope and type.

\begin{schema}{Data}
identifier: DID\\
name: DNAME\\
parent: CID \cup SID\\
scope: DATASCOPE\\
type: DATATYPE\\
initial: EXPR
\end{schema}

A Simulink function consists an identifier and a name, a sequence of names of input variables and a sequence of names of output variables, a reference to
its parent and the name of the Simulink block that defines the function.

\begin{schema}{SimulinkFunction}
identifier: FID\\
name: FNAME\\
inputs, outputs: \seq DNAME\\
parent: CID \cup SID\\
block: NAME
\end{schema}

A graphical function is similar to a Simulink function, but the Simulink block name component is substituted by
the identifier of a chart; the chart to which the function refers is obtained from the flow chart that defines
the function.

\begin{schema}{GraphicalFunction}
identifier: FID\\
name: FNAME\\
inputs, outputs: \seq DNAME\\
parent: CID \cup SID\\
chart: CID
\end{schema}

The top element of a Stateflow model is a chart; it contains an identifier, a name,
a sequence of state identifiers, its decomposition and partial functions from identifier
to the elements contained in the chart.

\begin{schema}{Chart}
identifier: CID\\
name: CNAME\\
default: \opt TID\\
substates: \seq SID\\
decomp: DECOMP\\
states: SID \ffun State\\
junctions: JID \ffun Junction\\
transitions: TID \ffun Transition\\
events: EID \ffun Event\\
data: DID \ffun Data\\
sfunctions: FID \ffun SimulinkFunction\\
gfunctions: FID \ffun GraphicalFunction
\end{schema}


We define well-formedness conditions for the elements of the language with respect to a diagram with the objective of defining the set
of well-formed diagrams. The following functions are used to extract information about names of states, data, events, Simulink functions and graphical
functions from a diagram.

\begin{axdef}
snames: Chart \fun \power SNAME\\
dnames: Chart \fun \power DNAME\\
enames: Chart \fun \power ENAME\\
sfnames: Chart \fun \power FNAME\\
gfnames: Chart \fun \power FNAME
\where
\forall c: Chart @ snames(c) = \{s: \ran c.states @ s.name\}\\
\forall c: Chart @ dnames(c) = \{data: \ran c.data @ data.name\}\\
\forall c: Chart @ enames(c) = \{e: \ran c.events @ e.name\}\\
\forall c: Chart @ sfnames(c) = \{f: \ran c.sfunctions @ f.name\}\\
\forall c: Chart @ gfnames(c) = \{f: \ran c.gfunctions @ f.name\}
\end{axdef}

The next three sets define the sets of unary expression constructors, binary expression constructors and binary temporal expression constructors; they are used
in order to simplify the well-formedness conditions over expressions.

\begin{axdef}
unary: \power (EXPR \fun EXPR)\\
binary: \power (EXPR \cross EXPR \fun EXPR)\\
tempbinary: \power (EXPR \cross ENAME \fun EXPR)
\where
unary = \{not,bnot,neg\}\\
binary = \{and,or,band,bor,bxor,sum,sub,mult,division,modulus,lshift,rshift,gt,lt,geq,leq,eq,neq\}\\
tempbinary = \{after, before, at, every\}
\end{axdef}

A well-formed expression is defined inductively over the the constructors of expressions;
a name expression is well-formed with respect to a diagram if, and only if, its name
component corresponds to a piece of data in the diagram and the expressions in the
index sequence are well-formed with respect to the diagram. A well-formedness condition
always depends on a diagram; for that reason, when stating the condition, we will
omit the phrase "with respect to a diagram".

A value expression is always well-formed, since we are abstracting from the actual
representation of data types, we cannot assert a value well-formedness. A function
application expression is well-formed if, and only if, the name corresponds to a
function definition and the sequence of expressions that defines the parameters consists
of well-formed expressions. The application of a unary operator to an expression is
well-formed if, and only if, the expression is well-formed; the application of a
binary operator to two expressions is well-formed if, and only if, both expressions
are well-formed. The application of a binary temporal operator to an expression and
an event name is well-formed if, and only if, the expression is well-formed and the
name corresponds to an event. A $tempCount$ expression is well formed if the name
that forms that expression corresponds to an event.

\begin{axdef}
WF\_EXPR: Chart \rel EXPR
\where
\forall c: Chart; n: DNAME; s: \seq EXPR @ (c,name(n,s)) \in WF\_EXPR \iff n \in dnames(c) \land (\forall e: \ran s @ (c,e) \in WF\_EXPR)\\
\forall c: Chart; n: NAME; s: \seq EXPR @ (c,fun(n,s)) \in WF\_EXPR \iff n \in sfnames(c) \cup gfnames(c) \land (\forall e: \ran s @ (c,e) \in WF\_EXPR)\\
\forall c: Chart; a: \arithmos @ (c,value(a)) \in WF\_EXPR\\
\forall c: Chart; s: \seq_1 \arithmos | \#s > 1 @ (c,array(s)) \in WF\_EXPR\\
\forall c: Chart; s: \seq_1 \seq_1 \arithmos | \# s > 1 @ (c,matrix(s)) \in WF\_EXPR \iff \exists n: \nat @ \forall row: \ran~s @ \# row = n\\
\forall c: Chart; e: EXPR; op: unary @ (c,op(e)) \in WF\_EXPR \iff (c,e) \in WF\_EXPR\\
\forall c: Chart; e_1,e_2: EXPR; op: binary @ (c,op(e_1,e_2)) \in WF\_EXPR \iff (c,e_1) \in WF\_EXPR \land (c,e_2) \in WF\_EXPR\\
\forall c: Chart; s: SNAME @ (c,in(s)) \in WF\_EXPR \iff s \in snames(c)\\
\forall c: Chart; e: EXPR; n: ENAME; op: tempbinary @ (c,op(e,n)) \in WF\_EXPR \iff (c,e) \in WF\_EXPR \land n \in enames(c)\\
\forall c: Chart; n: ENAME @ (c,tempCount(n)) \in WF\_EXPR \iff n \in enames(c)
\end{axdef}

Like in the case of expressions, we define the well-formedness of actions inductively.
A broadcast action is well-formed if, and only if, the name corresponds to an event.
An action formed by an expression is well-formed if, and only if, the expression
is well-formec. An assignment is well-formed if, and only if, the name corresponds
to a piece of data, the expressions that form the sequence of indexes are well-formed
and the expression being assigned is well-formed.

\begin{axdef}
WF\_ACTION: Chart \rel ACTION
\where
\forall c: Chart; e: Event;  d:(SID\cup CID) @ (c,bcast(e.name,d)) \in WF\_ACTION \iff\\\t1
(e.scope \neq INPUTEVENT \land e \in \ran c.events \land\\\t2
(d \in (\dom c.states) \lor d = c.identifier))\\
\forall c: Chart; e: EXPR @ (c,expr(e)) \in WF\_ACTION \iff (c,e) \in WF\_EXPR\\
\forall c: Chart; n: DNAME; s: \seq EXPR; e: EXPR @ (c,assign(n,s,e)) \in WF\_ACTION \iff \\
\t1 n \in dnames(c) \land (\forall e: \ran s @ (c,e) \in WF\_EXPR) \land (c,e) \in WF\_EXPR
\end{axdef}

An on action is well-formed if, and only if, the name corresponds to an event and
the action is well-formec.

\begin{axdef}
WF\_ONACTION: Chart \rel ONACTION
\where
\forall c: Chart; n: ENAME; as: \seq ACTION @ (c,(n,as)) \in WF\_ONACTION \iff
(n \in enames(c) \land
(\exists_1 e: \ran c.events | e.name = n @ e.scope \neq OUTPUTEVENT) \land
(\forall a: \ran as @ (c,a) \in WF\_ACTION))
\end{axdef}

The well-formedness of during actions is defined inductively; a during action formed
by an action is well-formed if, and only if, the action is well-formed, and a during
action formed by an on action is well-formed if, and only if, the on action is well-formec.

\begin{axdef}
WF\_DACTION: Chart \rel DACTION
\where
\forall c: Chart; as: \seq ACTION @ (c,action(as)) \in WF\_DACTION \iff \forall a: \ran as @ (c,a) \in WF\_ACTION\\
\forall c: Chart; a: ONACTION @ (c,on(a)) \in WF\_DACTION \iff (c,a) \in WF\_ONACTION
\end{axdef}

A binding is well-formed if, and only if, the names in the sequence of binding correspond to either an event or a piece of data.

\begin{axdef}
WF\_BINDING: Chart \rel \seq (ENAME \cup DNAME)
\where
\forall c: Chart; s: \seq (ENAME \cup DNAME) @ (c,s) \in WF\_BINDING \iff \forall n: \ran s @ n \in enames(c) \cup dnames(c)
\end{axdef}

A state is well-formed if, and only if, it belong to the diagram, its parent is either
the chart or to a state in the diagram, if the state is parallel its parent has parallel
decomposition, if the state is sequential its parent has sequential decomposition,
the entry and exit actions are well-formed, the sequence of during actions is formed
by well-formed during actions, the binding is well-formed, the references to its
default, inner and outer transitions correspond to transitions in the diagram, and
the references to its left and right sibling correspond to states in the diagram.


\begin{axdef}
WF\_STATE: Chart \rel State
\where
\forall c: Chart; s: State @ (c,s) \in WF\_STATE \iff\\
\t1 s \in \ran c.states \land\\
\t1 s.parent \in \dom c.states \cup \{c.identifier\} \land\\
\t1 s.parent \in \dom c.states \implies (s.type = PAR\iff (c.states~s.parent).decomp = PAR) \land\\
\t1 s.parent \notin \dom c.states \implies (s.type = PAR \iff c.decomp = PAR) \land\\
\t1 s.parent \in \dom c.states \implies (s.type = SEQ \iff (c.states~s.parent).decomp = SEQ) \land\\
\t1 s.parent \notin \dom c.states \implies (s.type = SEQ \iff c.decomp = SEQ) \land\\
\t1 \forall a: \ran s.entry @ (c,a) \in WF\_ACTION \land\\
\t1 \forall a: \ran s.exit @ (c,a) \in WF\_ACTION \land\\
\t1 \forall a: \ran s.during @ (c,a) \in WF\_DACTION \land\\
\t1 (c,s.binding) \in WF\_BINDING \land\\
\t1 s.history = \true \implies s.decomp = SEQ \land\\
\t1 \ran s.default \subseteq \dom c.transitions \land\\
\t1 \ran s.inner \subseteq \dom c.transitions \land\\
\t1 \ran s.outer \subseteq \dom c.transitions \land\\
\t1 \ran s.left \subseteq \dom c.states \land\\
\t1 \ran s.right \subseteq \dom c.states \land\\
\t1 \ran s.substates \subseteq \dom c.states
\end{axdef}

A junction is well-formed if, and only if, it belongs to the diagram, the reference
to its parent correspond to the chart or to a state in the diagram, the reference to
its transition corresponds to a transition in the diagram, if its parent is the chart
or its parent is a state with parallel decomposition then it is not a history junction.

\begin{axdef}
WF\_JUNCTION: Chart \rel Junction
\where
\forall c: Chart; j: Junction @ (c,j) \in WF\_JUNCTION \iff\\
\t1 j \in \ran c.junctions \land\\
\t1 j.parent \in \dom c.states \cup \{c.identifier\} \land\\
\t1 \ran j.transition \subseteq \dom c.transitions \land\\
\t1 j.parent = c.identifier \implies j.history = \false \land\\
\t1 j.parent \in \dom c.states \implies (c.states~j.parent).decomp = PAR \implies j.history = \false
\end{axdef}

The well-formedness of trigger is defined inductively; if a trigger is a temporal expression, it
is well-formed if the temporal expression is well-formed. If the trigger is an event name, it
is well formed if the event is a input or local event of the chart.

\begin{axdef}
WF\_TRIGGER: Chart \rel TRIGGER
\where
\forall c: Chart; n: ENAME @ (c,e(n)) \in WF\_TRIGGER \iff\\
\t1 \exists event: \ran c.events @ event.name = n \land event.scope \neq OUTPUTEVENT\\
\forall c: Chart; texp: TEXPR @ (c,t(texp)) \in WF\_TRIGGER \iff\\
\t1 (c,texp) \in WF\_EXPR
\end{axdef}

A transition is well formed if, and only if, it belongs to the diagram, the reference
to its source (if one exists) corresponds to either a state or junction in the diagram,
the reference to its destination corresponds to either a state or junction in the
diagram, the reference to its parent corresponds to the chart or to a state in the diagram,
and its condition, condition action and transition action are well-formec.

\begin{axdef}
WF\_TRANSITION: Chart \rel Transition
\where
\forall c: Chart; t: Transition @ (c,t) \in WF\_TRANSITION \iff\\
\t1 t \in \ran c.transitions \land\\
\t1 \ran t.source \subseteq (\dom c.states \cup \dom c.junctions)\land\\
\t1 t.destination \in (\dom c.states \cup \dom c.junctions)\land\\
\t1 t.parent \in \dom c.states \cup \{c.identifier\} \land\\
\t1 \# t.condition > 0 \implies (c,t.condition~1) \in WF\_EXPR \land\\
\t1 \forall a: \ran t.condact @ (c,a) \in WF\_ACTION \land\\
\t1 \forall a: \ran t.transact @ (c,a) \in WF\_ACTION
\end{axdef}

A piece of data is well-formed if, and only if, it belongs to the diagram and the
reference to its parent corresponds to the chart or to a state in the diagram.

\begin{axdef}
WF\_DATA: Chart \rel Data
\where
\forall c: Chart; data: Data @ (c,data) \in WF\_DATA \iff\\
\t1 data \in \ran c.data \land\\
\t1 data.parent \in \dom c.states \cup \{c.identifier\}
\end{axdef}

An event is well-formed if, and only if, it belongs to the diagram and the reference
to its parent corresponds to the chart or to a state in the diagram.

\begin{axdef}
WF\_EVENT: Chart \rel Event
\where
\forall c: Chart; e: Event @ (c,e) \in WF\_EVENT \iff\\
\t1 e \in \ran c.events \land\\
\t1 e.parent \in \dom c.states \cup \{c.identifier\}
\end{axdef}

A Simulink function is well formed if, an only if, it belongs to the diagram, its
inputs and outputs correspond to pieces of data in the diagram, and the reference
to its parent corresponds to the chart or to a state in the diagram.

\begin{axdef}
WF\_SFUNCTION: Chart \rel SimulinkFunction
\where
\forall c: Chart; f: SimulinkFunction @ (c,f) \in WF\_SFUNCTION \iff\\
\t1 f \in \ran c.sfunctions \land\\
\t1 \ran f.inputs \subseteq sfnames(c) \land\\
\t1 \ran f.outputs \subseteq sfnames(c) \land\\
\t1 f.parent \in \dom c.states \cup \{c.identifier\}\\
\end{axdef}

The well-formedness condition for graphical function is the same as the one for Simulink
function with the extra restriction that the reference to its default transition
corresponds to a transition in the diagram.

\begin{axdef}
WF\_GFUNCTION: Chart \rel GraphicalFunction
\where
\forall c: Chart; f: GraphicalFunction @ (c,f) \in WF\_GFUNCTION \iff\\
\t1 f \in \ran c.gfunctions \land\\
\t1 \ran f.inputs \subseteq gfnames(c) \land\\
\t1 \ran f.outputs \subseteq gfnames(c) \land\\
\t1 f.parent \in \dom c.states \cup \{c.identifier\} \land\\
\t1 f.chart \in \dom c.transitions\\
\end{axdef}

A chart is well-formed if, and only if, the references to its sub-states correspond
to states in the diagram.

\begin{axdef}
WF\_CHART: \power Chart
\where
\forall c: Chart @ c \in WF\_CHART \iff\\
\t1 \ran c.substates \subseteq \dom c.states \land\\
\t1 \forall s: \ran c.states @ (c,s) \in WF\_STATE \land\\
\t1 \forall j: \ran c.junctions @ (c,j) \in WF\_JUNCTION \land\\
\t1 \forall t: \ran c.transitions @ (c,t) \in WF\_TRANSITION \land\\
\t1 \forall data: \ran c.data @ (c,data) \in WF\_DATA \land\\
\t1 \forall e: \ran c.events @ (c,e) \in WF\_EVENT \land\\
\t1 \forall f: \ran c.gfunctions @ (c,f) \in WF\_GFUNCTION \land\\
\t1 \forall f: \ran c.sfunctions @ (c,f) \in WF\_SFUNCTION
\end{axdef}

\end{document}

