\documentclass{article}

\usepackage[lmargin=2cm,rmargin=2cm,tmargin=3cm,bmargin=3cm,landscape]{geometry}%
\usepackage{circus}
\usepackage{czt}
%\AddToShipoutPicture{\AtTextLowerLeft{\framebox(\LenToUnit{\textwidth},\LenToUnit{\textheight}){}}}
\renewcommand{\circblockbegin}{\left(\begin{array}{l}}
\renewcommand{\circblockend}{\end{array}\right)}
\newcommand{\ppuniverse}{\universe}
\newcommand{\real}{\mathbb{R}}

\begin{document}
\setlength{\zedindent}{0pt}
\begin{zsection}
  \SECTION Stateflow2Circus \parents StateflowAbstractSyntax, CircusFormalSyntax
\end{zsection}
%
\begin{axdef}
chartname, chartid: WF\_CHART \inj NAME\\
%begin statename
statename: WF\_STATE \inj NAME\\
%end statename
stateid: WF\_STATE \inj NAME\\
junctionname, junctionid: WF\_JUNCTION \inj NAME\\
transitionname, transitionid: WF\_TRANSITION \inj NAME\\
dataname: WF\_DATA \inj NAME\\
eventname: WF\_EVENT \inj NAME\\
eventcountername: WF\_EVENT \inj NAME\\
datachannelname: WF\_DATA \inj NAME\\
outputeventchannelname: WF\_EVENT \inj NAME\\
processname, processstatename: WF\_CHART \inj NAME\\
DuringActionName: WF\_STATE \inj NAME\\
EntryActionName: WF\_STATE \inj NAME\\
ExitActionName: WF\_STATE \inj NAME\\
ConditionActionName: WF\_TRANSITION \inj NAME\\
TransitionActionName: WF\_TRANSITION \inj NAME\\
ConditionName: WF\_TRANSITION \inj NAME\\
TriggerName: WF\_TRANSITION \inj NAME\\
namesets:\seq(\power NAME)
\where
namesets = \langle \ran chartname, \ran chartid, \ran statename, \ran stateid,\\
\t1\ran junctionname, \ran junctionid, \ran transitionname, \ran transitionid,\\
\t1\ran dataname, \ran eventname, \ran datachannelname, \ran processname,\\
\t1\ran processstatename, \ran DuringActionName, \ran EntryActionName,\\
\t1\ran ExitActionName, \ran ConditionActionName, \ran TransitionActionName,\\
\t1\ran ConditionName, \ran TriggerName,\ran eventcountername\rangle\\
\disjoint namesets
\end{axdef}
%
\begin{axdef}
getdatabyname: WF\_CHART \cross DNAME \pfun Data\\
geteventbyname: WF\_CHART \cross ENAME \pfun Event\\
gettransitionbyid: WF\_CHART \cross TID \pfun Transition\\
getstatebyid: WF\_CHART \cross SID \pfun State\\
getchartbyid: WF\_CHART \cross CID \pfun WF\_CHART\\
getjunctionbyid: WF\_CHART \cross JID \pfun Junction
\end{axdef}

\begin{axdef}
STATESTATUS: NAME\\
\end{axdef}

\begin{axdef}
EXECUTEDURINGACTION, DURINGACTIONS: N
\end{axdef}

\begin{axdef}
EXECUTEENTRYACTION, X, ENTRYACTIONS: N
\end{axdef}

\begin{axdef}
EXECUTEEXITACTION, EXITACTIONS: N
\end{axdef}

\begin{axdef}
EXECUTECONDITIONACTION, CONDITIONACTIONS, O: N
\end{axdef}

\begin{axdef}
EXECUTETRANSITIONACTION, TRANSITIONACTIONS: N
\end{axdef}

\begin{axdef}
EVALUATECONDITION, CONDITIONSACTION: N
\end{axdef}
\begin{axdef}
CHECKTRIGGERCHANNEL, TRIGGERSACTION, RESULTCHANNEL: N
\end{axdef}

\begin{axdef}
GETSTATE, GETTRANSITION, GETJUNCTION, GETCHART, GETEVENTS:NAME\\
STATUSACTION, HISTORYACTION, STATEHISTORY: NAME\\
EVENTSCHANNEL, STATECHANNEL, JUNCTIONCHANNEL:NAME\\
CHARTCHANNEL, TRANSITIONCHANNEL:NAME\\
STATUSCHANNEL, HISTORYCHANNEL: NAME
\end{axdef}
\begin{axdef}
ACTIVATIONACTION,ACTIVATECHANNEL,ACTIVATESCHEMA:NAME\\
DEACTIVATIONACTION,DEACTIVATECHANNEL,DEACTIVATESCHEMA:NAME\\
CHARTACTIONS,INTERFACEACTIONS,INPUTSACTION,OUTPUTSACTION:NAME\\
READINPUTSCHANNEL,WRITEOUTPUTSCHANNEL,ACTIONVARIABLE:NAME
\end{axdef}
\begin{axdef}
STATE, STATEID, TRANSITION, TRANSITIONID, JUNCTION, JUNCTIONID: NAME\\
EVENT, UNIVERSE, REAL,SFBOOL: NAME\\
IDENTIFIER, DEFAULT, INNER, OUTER, PARENT, TRANS: NAME\\
LEFT, RIGHT, SUBSTATES, DECOMPOSITION, TYPE, HISTORY: NAME\\
CLUSTER, SET,CHART, AND, OR: NAME\\
SOURCE, DESTINATION, NEXT, SNODE, JNODE: NAME\\
NULLSTATE, NULLTRANSITION, NULLJUNCTION, NULLEVENT:NAME\\
NULLTRANSITIONID, NULLSTATEID : NAME
\end{axdef}

\begin{axdef}
SimulationData, InitSimulationData: NAME\\
SimulationInstance, InitSimulationInstance, InitState: NAME\\
\end{axdef}

\begin{axdef}
STATES, TRANSITIONS, JUNCTIONS, STATEFLOWCHART: N
\end{axdef}
\begin{axdef}
BROADCAST,CHECK,ORIGIN,DEST,ALLACTIONS: NAME\\
ENDLOCALEXECUTION,ENDACTION: NAME\\
I,J,E,S,B: NAME
\end{axdef}

\begin{gendef}[X]
set2seq: \power X \fun \seq X
\where
\forall s: \power X @ \ran (set2seq(s)) = s
\end{gendef}

\begin{axdef}
binarysfop: \power (EXPR \cross EXPR \inj EXPR)
\where
binarysfop = \{or, and, bor, band, bxor, neq, eq, leq, geq, lt, gt, lshift, rshift, sum, sub,\\
\t1 modulus, mult, division\}
\end{axdef}

\begin{axdef}
unarysfop: \power (EXPR \inj EXPR)
\where
unarysfop = \{not, bnot, neg\}
\end{axdef}

\begin{axdef}
binaryop: binarysfop \pfun (Expression \cross Expression \fun Expression)\\
unaryop: unarysfop \pfun (Expression \fun Expression)
\end{axdef}

\begin{axdef}
translate_{VectorDomain}: (\nat \cross \seq \nat) \fun Expression
\where
\forall n:\nat; s:\seq\nat @ translate_{VectorDomain}(n,s) =\\
\circblockbegin
\IF~~~s = \langle\rangle\\
\THEN~~~functionapplication(app(UPTO,\langle numberliteral(0), numberliteral(n-1)\rangle))\\
\ELSE~~~product(\\
\t2 functionapplication(app(UPTO,\langle numberliteral(0), numberliteral(n-1)\rangle)),\\
\t2 translate_{VectorDomain}(head~s,tail~s)\\
\t1)
\circblockend
\end{axdef}

\begin{axdef}
translate_{Type}: DATATYPE \fun Expression
\where
translate_{Type}(scalar(INT32)) = reference(ref(INTEGER)) \\
translate_{Type}(scalar(INT16)) = reference(ref(INTEGER)) \\
translate_{Type}(scalar(INT8)) = reference(ref(INTEGER)) \\
translate_{Type}(scalar(UINT32)) = reference(ref(NATURAL))\\
translate_{Type}(scalar(UINT16)) = reference(ref(NATURAL))\\
translate_{Type}(scalar(UINT8)) = reference(ref(NATURAL)) \\
translate_{Type}(scalar(DOUBLE)) = reference(ref(REAL)) \\
translate_{Type}(scalar(SINGLE)) = reference(ref(REAL)) \\
translate_{Type}(scalar(BOOLEAN)) = reference(ref(SFBOOL)) \\
\forall s:(\seq_1 \nat); t: SCALAR @\\\t1
translate_{Type}(vector(t,s)) = functionapplication(app(FUN, \langle\\
\t2 translate_{VectorDomain}(head~s,tail~s),\\
\t2 translate_{Type}(scalar(t))\\
\t1 \rangle))
\end{axdef}


\begin{axdef}
translate_{Expr}:  WF\_EXPR \fun Expression\\
translate_{Exprs}: WF\_CHART \cross \seq EXPR \pfun \seq Expression\\
\where
\forall op: \dom unaryop; e: EXPR; c: WF\_CHART | (c,op(e)) \in WF\_EXPR @\\\t1
translate_{Expr}(c,op(e)) = unaryop(op)(translate_{Expr}(c,e))\\

\forall op: \dom binaryop; e_1, e_2: EXPR; c: WF\_CHART | (c,op(e_1,e_2)) \in WF\_EXPR @\\\t1
translate_{Expr}(c,op(e_1,e_2)) = binaryop(op)(translate_{Expr}(c,e_1),translate_{Expr}(c,e_2))\\

\forall n: DNAME; es: \seq EXPR; c: WF\_CHART | (c,name(n,es)) \in WF\_EXPR @\\
translate_{Expr}(c,name(n,es)) =  \\
\circblockbegin
\IF~\# es = 0\\
\THEN~reference(ref(dataname(c,getdatabyname(c,n))))\\
\ELSE~functionapplication(app(dataname(c,getdatabyname(c,n)),translate_{Exprs}(c,es)))
\circblockend\\

\forall n: NAME; es: \seq EXPR; c: WF\_CHART | (c,fun(n,es)) \in WF\_EXPR @\\
translate_{Expr}(c,fun(n,es)) = functionapplication(app(n,translate_{Exprs}(c,es)))\\

\forall v: \arithmos; c: WF\_CHART | (c,value(v)) \in WF\_EXPR @\\
\t1 translate_{Expr}(c,value(v)) = numberliteral(v)\\

\forall s: \seq_1\arithmos; c: WF\_CHART | (c,array(s)) \in WF\_EXPR @\\
\t1 translate_{Expr}(c,array(s)) =\\
\t2 \LET pairs == \{i:0\upto \#s -1 @\\
\t3 functionapplication(app(MAPSTO,\langle numberliteral(i), numberliteral(s(i+1)) \rangle)) \}\\
\t2 @ setextension(set2seq(pairs))\\

\forall s: \seq_1\seq_1\arithmos; c: WF\_CHART | (c,matrix(s)) \in WF\_EXPR@\\
\t1 translate_{Expr}(c,matrix(s)) = \\\t2
\LET pairs == \{i:0\upto \#s -1 ; j: 0\upto \#s(1) - 1 @\\
\t3 functionapplication(app(MAPSTO,\langle\\
\t4 tupleextension(\langle numberliteral(i),numberliteral(j)\rangle),\\
\t4 numberliteral(s(i+1)(j+1)) \rangle))\}\\
\t2 @ setextension(set2seq(pairs))\\

\forall n: SNAME; s: State; c: WF\_CHART | s.name = n \land (c,s) \in WF\_STATE @\\
\t1 translate_{Expr}(c,in(n)) =\\
\t2 functionapplication(app(STATESTATUS,\langle reference(ref(stateid(c,s))) \rangle))\\

\forall c: WF\_CHART @ translate_{Exprs} (c,\langle \rangle) = \langle \rangle\\
\forall es: \seq EXPR; c: WF\_CHART | \# es > 0 \land (\forall e: \ran es @ (c,e) \in WF\_EXPR) @\\\t1
translate_{Exprs}(c,es) = \langle translate_{Expr}(c,head~es) \rangle \cat translate_{Exprs}(c,tail~es)
\end{axdef}

\begin{axdef}
translate_{InitExpr}: WF\_DATA \fun Expression
\where
\forall d: Data; c: WF\_CHART | (c,d) \in WF\_DATA @ translate_{InitExpr}(c,d) =\\
\circblockbegin
\IF d.type \in \ran scalar\\
\THEN~~translate_{Expr}(c,d.initial)\\
\ELSE~~\circblockbegin
\IF d.initial \in \ran value\\
\THEN~~\LET decl == declpart(\langle variable(\langle decl(X) \rangle, \\
\t1 translate_{VectorDomain}(head~((vector\inv)(d.type)).2,tail~((vector\inv)(d.type)).2)) \rangle)\\
\t1 @ functionconstruction(schematext(\langle decl\rangle,\langle\rangle),translate_{Expr}(c,d.initial))\\
\ELSE~~translate_{Expr}(c,d.initial)
\circblockend
\circblockend
\end{axdef}

\begin{axdef}
translate_{Var}: Action \fun Action
\where
\forall a: Action @ translate_{Var}(a) = \LET\\\t1
decl == declpart(\langle variable(\langle decl(B)\rangle,reference(ref(BOOL))) \rangle)
@\\
\t2 commandaction(variableblock(decl,a))
\end{axdef}

\begin{axdef}
translate_{Interrupt}: Action \fun Action
\where
\forall a: Action @ translate_{Interrupt}(a) = \\
\t1 \LET pred == relationapplication(rel(EQUAL,\langle reference(ref(B)), reference(ref(T))\rangle)) @\\
\t2 \LET conditions == gactions(\langle (pred,cspaction(skip)),(negation(pred),a)\rangle) @\\
\t3 commandaction(ifcommand(conditions))
\end{axdef}

\begin{axdef}
translate_{Check}: Action
\where
translate_{Check} = \\
\t1\LET pars == \langle reference(ref(B)) \rangle\\
@ cspaction(paractioninstantiation(paraction(namedaction(CHECK)),pars))
\end{axdef}

\begin{axdef}
translate_{Broadcast}: ENAME \cross (SID \cup CID) \cross WF\_CHART \fun Action
\where
\forall n: ENAME; d: (SID\cup CID); c: WF\_CHART @ translate_{Broadcast}(n,d,c) = \\ \circblockbegin
\LET dest == \circblockbegin \IF~d \in CID\\
\THEN~chartid(c)\\
\ELSE~stateid(c,getstatebyid(c,d)) \circblockend @\\
\LET pars == \langle reference(ref(eventname(c,geteventbyname(c,n)))),reference(ref(dest))\rangle\\	 @ cspaction(paractioninstantiation(paraction(namedaction(BROADCAST)),pars))\\
\circblockend
\end{axdef}

\begin{axdef}
translate_{Act}: WF\_ACTION\fun Action
\where
\forall n: DNAME; es: \seq EXPR; e: EXPR; c: WF\_CHART | (c,assign(n,es,e)) \in WF\_ACTION @\\
translate_{Act}(c,assign(n,es,e)) = \\
\circblockbegin
\IF~\# es = 0\\
\THEN~commandaction(assignment(\langle (dataname(c,getdatabyname(c,n)),translate_{Expr}(c,e)) \rangle))\\
\ELSE\\\circblockbegin
\IF~\# es = 1\\
\THEN~commandaction(assignment(\langle\\
\t1 (dataname(c,getdatabyname(c,n)), functionapplication(app(OVERRIDE,\langle\\
\t2 reference(ref(dataname(c,getdatabyname(c,n)))),setextension(\langle\\
\t3 tupleextension(\langle translate_{Expr}(c,head~es), translate_{Expr}(c,e)\rangle)\\
\t2 \rangle)\\
\t1 \rangle)))\\
\rangle))\\
\ELSE~commandaction(assignment(\langle\\
\t1 (dataname(c,getdatabyname(c,n)), functionapplication(app(OVERRIDE,\langle\\
\t2 reference(ref(dataname(c,getdatabyname(c,n)))), setextension(\langle\\
\t3 tupleextension(\langle tupleextension(translate_{Exprs}(c,es)), translate_{Expr}(c,e)\rangle)\\
\t2 \rangle)\\
\t1 \rangle)))\\
\rangle))
\circblockend\circblockend\\

\forall n: ENAME; d: (SID\cup CID); c: WF\_CHART | (c,bcast(n,d)) \in WF\_ACTION @\\
translate_{Act}(c,bcast(n,d)) = \\
\circblockbegin
\IF~ (geteventbyname(c,n)).scope = OUTPUTEVENT\\
\THEN~commandaction(\\
\t1 assignment(\langle\\
\t2(eventcountername(c,geteventbyname(c,n)),\\
\t2 functionapplication(app(PLUS,\\
\t3 \langle reference(ref(eventcountername(c,geteventbyname(c,n)))),numberliteral(1) \rangle)))\\
\t1 \rangle)\\
)\\
\ELSE cspaction(actionsequentialcomposition(translate_{Broadcast}(n,d,c),translate_{Check}))
\circblockend\\

\forall e: EXPR; c: WF\_CHART | (c,expr(e)) \in WF\_ACTION @\\ translate_{Act}(c,expr(e)) = cspaction(skip)
\end{axdef}

\begin{axdef}
actions\_have\_broadcast: \power (WF\_CHART\cross \seq ACTION)
\where
\forall c: WF\_CHART; as: \seq ACTION @ (c,as) \in actions\_have\_broadcast \iff\\\t1
\exists a: \ran as @ (a \in \ran bcast \land (geteventbyname(c,((bcast\inv)(a)).1)).scope = LOCALEVENT)
\end{axdef}

\begin{axdef}
daction\_has\_broadcast: \power (WF\_CHART\cross DACTION)
\where
\forall c: WF\_CHART; a: DACTION @ (c,a) \in daction\_has\_broadcast \iff\\\t1
(a \in \ran action \land (c,((action\inv) a)) \in actions\_have\_broadcast) \lor (a \in \ran on \land (c,(((on\inv) a).2)) \in actions\_have\_broadcast)
\end{axdef}

\begin{axdef}
dactions\_have\_broadcast: \power (WF\_CHART\cross \seq DACTION)
\where
\forall c: WF\_CHART; as: \seq DACTION @ (c,as) \in dactions\_have\_broadcast \iff\\\t1
\exists a: \ran as @ ((c,a) \in daction\_has\_broadcast)
\end{axdef}

\begin{axdef}
translate_{Acts}: WF\_CHART \cross \seq ACTION \pfun Action
\where
\forall as: \seq ACTION; c: WF\_CHART | \# as = 0 @ translate_{Acts}(c,as) = cspaction(skip)\\
\forall as: \seq ACTION; c: WF\_CHART | \# as \geq 1 \land (\forall a: \ran as @ (c,a) \in WF\_ACTION) @ translate_{Acts}(c,as) = \\
\t1 \circblockbegin
\IF ((head~as) \in \ran bcast) \land ((geteventbyname(c,((bcast\inv)(head~as)).1)).scope = LOCALEVENT)\\
\THEN~~cspaction(actionsequentialcomposition(translate_{Act}(c,head~as), translate_{Interrupt}(translate_{Acts}(c,tail~as))))\\
\ELSE~~cspaction(actionsequentialcomposition(translate_{Act}(c,head~as), translate_{Acts}(c,tail~as)))\\
\circblockend
\end{axdef}

\begin{axdef}
translate_{ONAct}: WF\_ONACTION \fun Action
\where
\forall n: ENAME; as: \seq ACTION; c: WF\_CHART | (c,(n,as)) \in WF\_ONACTION @ translate_{ONAct}(c,(n,as)) =\\
\t1 commandaction(ifcommand(gactions(\langle\\
\t1 (relationapplication(rel(EQUAL,\langle reference(ref(E)),reference(ref(eventname(c,geteventbyname(c,n)))) \rangle)), translate_{Acts}(c,as)),\\
\t1 (negation(relationapplication(rel(EQUAL,\langle reference(ref(E)),reference(ref(eventname(c,geteventbyname(c,n)))) \rangle))), cspaction(skip))\\
\rangle)))
\end{axdef}

\begin{axdef}
translate_{DAct}: WF\_DACTION \fun Action
\where
\forall as: \seq ACTION; c: WF\_CHART | \forall a: \ran as @ (c,a) \in WF\_ACTION @ translate_{DAct}(c,action(as)) = translate_{Acts}(c,as)\\
\forall a: ONACTION; c: WF\_CHART | (c,a) \in WF\_ONACTION @ translate_{DAct}(c,on(a)) = translate_{ONAct}(c,a)
\end{axdef}

\begin{axdef}
translate_{DActs}: WF\_CHART \cross \seq DACTION \pfun Action
\where
\forall as: \seq DACTION; c: WF\_CHART | \# as = 0 @ translate_{DActs}(c,as) = cspaction(skip)\\
\forall as: \seq DACTION; c: WF\_CHART | \# as \geq 1  \land (\forall a: \ran as @ (c,a) \in WF\_DACTION) @ translate_{DActs}(c,as) =\\
\t1 \circblockbegin
\IF (c,head~as) \in daction\_has\_broadcast\\
\THEN cspaction(actionsequentialcomposition(translate_{DAct}(c,head~as), translate_{Interrupt}(translate_{DActs}(c,tail~as))))\\
\ELSE cspaction(actionsequentialcomposition(translate_{DAct}(c,head~as), translate_{DActs}(c,tail~as)))\\
\circblockend
\end{axdef}

\begin{axdef}
tv: Expression \fun Predicate
\where
\forall e: Expression @ tv(e) = negation(relationapplication(rel(EQUAL, \langle e, numberliteral(0) \rangle)))
\end{axdef}

\begin{axdef}
translate_{Pred}: WF\_EXPR \fun Predicate
\where
\forall e: EXPR; c: WF\_CHART | (c,e) \in WF\_EXPR @ translate_{Pred}(c,e) = tv(translate_{Expr}(c,e))
\end{axdef}

\begin{axdef}
translate_{Trigger}: WF\_TRIGGER \fun Predicate
\where
\forall n: ENAME; c: WF\_CHART | (c,e(n)) \in WF\_TRIGGER @ translate_{Trigger}(c,e(n)) = \\
\t1 relationapplication(rel(EQUAL,\langle reference(ref(E)),reference(ref(eventname(c,geteventbyname(c,n)))) \rangle))\\
\forall texp: TEXPR; c: WF\_CHART | (c,t(texp)) \in WF\_TRIGGER @ translate_{Trigger}(c,t(texp)) = \\
\t1 translate_{Pred}(c,texp)
\end{axdef}

\begin{axdef}
translate_{Triggers}: WF\_CHART \cross \seq_1 TRIGGER \pfun Predicate
\where
\forall ts: \seq_1 TRIGGER; c: WF\_CHART | \# ts = 1 \land (c,head~ts) \in WF\_TRIGGER @\\
\t1 translate_{Triggers}(c,ts) = translate_{Trigger}(c,head~ts)\\
\forall ts: \seq_1 TRIGGER; c: WF\_CHART | \# ts > 1 \land \forall t: \ran ts @ (c,t) \in WF\_TRIGGER @\\
\t1 translate_{Triggers}(c,ts) = disjunction(translate_{Trigger}(c,head~ts),translate_{Triggers}(c,tail~ts))
\end{axdef}

\begin{axdef}
StateIdentifierDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART  @ StateIdentifierDeclaration(c) = \LET\\\t1
snames == set2seq(\{s: \ran c.states @ decl(stateid(c,s))\});\\\t1
cname == \langle decl(chartid(c)) \rangle;\\\t1
exprs == set2seq(\{s: \ran c.states @ reference(ref(stateid(c,s)))\})\cat \langle reference(ref(chartid(c))) \rangle;\\\t1
type == reference(ref(STATEID)) @ \LET\\\t2
decl == declpart(\langle variable(snames \cat cname, type)\rangle);\\\t2
pred == relationapplication(rel(EQUAL, \langle reference(ref(STATEID)),setextension(exprs)\rangle)) @\\\t3
axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
state\_identifier: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall s: State; c: WF\_CHART | (c,s) \in WF\_STATE @ state\_identifier(c,s) =\\
\t1 (decl(IDENTIFIER),reference(ref(stateid(c,s))))
\end{axdef}

\begin{axdef}
state\_default: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_default(c,s) = \\
\circblockbegin
\IF~\# s.default = 0\\
\THEN~(decl(DEFAULT),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(DEFAULT),\\\t2 reference(ref(transitionid(c,gettransitionbyid(c,head~(s.default))))))
\circblockend
\end{axdef}

\begin{axdef}
state\_inner: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_inner(c,s) = \\
\circblockbegin
\IF~\# s.inner = 0\\
\THEN~(decl(INNER),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(INNER),\\\t2 reference(ref(transitionid(c,gettransitionbyid(c,head~(s.inner))))))
\circblockend
\end{axdef}

\begin{axdef}
state\_outer: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_outer(c,s) = \\
\circblockbegin
\IF~\# s.outer = 0\\
\THEN~(decl(OUTER),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(OUTER),\\\t2 reference(ref(transitionid(c,gettransitionbyid(c,head~(s.outer))))))
\circblockend
\end{axdef}

\begin{axdef}
state\_parent: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_parent(c,s) = \\
\t1 \IF~s.parent \in \dom c.states\\
\t1 \THEN~(decl(PARENT), reference(ref(stateid(c,getstatebyid(c,s.parent)))))\\
\t1 \ELSE~(decl(PARENT), reference(ref(chartid(c))))
\end{axdef}

\begin{axdef}
state\_left: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_left(c,s) = \\
\circblockbegin
\IF~\# s.left = 0\\
\THEN~(decl(LEFT), reference(ref(NULLSTATEID)))\\
\ELSE~(decl(LEFT), reference(ref(stateid(c,getstatebyid(c,head(s.left))))))
\circblockend
\end{axdef}

\begin{axdef}
state\_right: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_right(c,s) = \\
\circblockbegin
\IF~\# s.right = 0\\
\THEN~(decl(RIGHT), reference(ref(NULLSTATEID)))\\
\ELSE~(decl(RIGHT), reference(ref(stateid(c,getstatebyid(c,head(s.right))))))
\circblockend
\end{axdef}

\begin{axdef}
state\_substates: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_substates(c,s) = \\
\t1 (decl(SUBSTATES), sequence(\{i: \dom s.substates @ i \mapsto reference(ref(stateid(c,getstatebyid(c,(s.substates)(i)))))\}))
\end{axdef}

\begin{axdef}
state\_decomposition: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_decomposition(c,s) = \\
\t1 \IF~s.decomp = SEQ\\
\t1 \THEN~(decl(DECOMPOSITION), reference(ref(CLUSTER)))\\
\t1 \ELSE~(decl(DECOMPOSITION), reference(ref(SET)))
\end{axdef}

\begin{axdef}
state\_type: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_type(c,s) = \\
\t1 \IF~s.type = PAR\\
\t1 \THEN~(decl(TYPE), reference(ref(AND)))\\
\t1 \ELSE~(decl(TYPE), reference(ref(OR)))
\end{axdef}

\newcommand{\hashistory}{~\textrm{has\_history}~}

\begin{axdef}
state\_history: WF\_STATE \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ state\_history(c,s) = \\
\t1 \IF~s.history = \true\\
\t1 \THEN~(decl(HISTORY),reference(ref(T)))\\
\t1 \ELSE~(decl(HISTORY),reference(ref(F)))
\end{axdef}

\begin{axdef}
StateDeclaration: WF\_STATE \fun Paragraph
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ StateDeclaration(c,s) =
\LET\\
\t1 name == \langle decl(statename(c,s)) \rangle;\\
\t1 type == reference(ref(STATE));\\
\t1 binding == bindingextension(\langle\\
\t2 state\_identifier(c,s),\\
\t2 state\_default(c,s),\\
\t2 state\_inner(c,s),\\
\t2 state\_outer(c,s),\\
\t2 state\_parent(c,s),\\
\t2 state\_left(c,s),\\
\t2 state\_right(c,s),\\
\t2 state\_substates(c,s),\\
\t2 state\_decomposition(c,s),\\
\t2 state\_type(c,s),\\
\t2 state\_history(c,s)\\
\t1 \rangle) @ \LET\\
\t2 decl == declpart(\langle variable(name,type) \rangle);\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(statename(c,s))),binding \rangle))
 @ \\
\t3 axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
StateSetDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ StateSetDeclaration(c) = \LET\\
\t1 names == \circblockbegin set2seq(\{s: \ran c.states @ reference(ref(statename(c,s)))\}\cup\\
\{reference(ref(NULLSTATE)),reference(ref(chartname(c)))\}) \circblockend @ \LET\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(STATE)),setextension(names)\rangle)) @\\
\t3 axiomaticdescription(schematext(\langle \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
chart\_identifier: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_identifier(c) =\\
\t1 (decl(IDENTIFIER),reference(ref(chartid(c))))
\end{axdef}

\begin{axdef}
chart\_default: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_default(c) = \\
\circblockbegin
\IF~\# c.default = 0\\
\THEN~(decl(DEFAULT),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(DEFAULT),\\\t2 reference(ref(transitionid(c,gettransitionbyid(c,head~(c.default))))))
\circblockend
\end{axdef}

\begin{axdef}
chart\_inner: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_inner(c) = \\
\t1 (decl(INNER),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\end{axdef}

\begin{axdef}
chart\_outer: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_outer(c) = \\
\t1 (decl(OUTER),\\\t2 reference(ref(NULLTRANSITIONID)))\\
\end{axdef}

\begin{axdef}
chart\_parent: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_parent(c) = \\
(decl(PARENT), reference(ref(NULLSTATEID)))
\end{axdef}

\begin{axdef}
chart\_left: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_left(c) = \\
\t1 (decl(LEFT), reference(ref(NULLSTATEID)))
\end{axdef}

\begin{axdef}
chart\_right: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_right(c) = \\
\t1 (decl(RIGHT), reference(ref(NULLSTATEID)))
\end{axdef}

\begin{axdef}
chart\_substates: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_substates(c) = \\
\t1 (decl(SUBSTATES),\\
\t1 sequence(\{i: \dom c.substates @ i \mapsto reference(ref(stateid(c,getstatebyid(c,(c.substates)(i)))))\}))
\end{axdef}

\begin{axdef}
chart\_decomposition: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_decomposition(c) = \\
\t1 \IF~c.decomp = SEQ\\
\t1 \THEN~(decl(DECOMPOSITION), reference(ref(CLUSTER)))\\
\t1 \ELSE~(decl(DECOMPOSITION), reference(ref(SET)))
\end{axdef}

\begin{axdef}
chart\_type: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_type(c) = \\
\t1 (decl(TYPE), reference(ref(CHART)))\\
\end{axdef}

\begin{axdef}
chart\_history: WF\_CHART \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART @ chart\_history(c) = \\
\t1 (decl(HISTORY),reference(ref(F)))
\end{axdef}

\begin{axdef}
ChartAsStateDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ ChartAsStateDeclaration(c) =
\LET\\
\t1 name == \langle decl(chartname(c)) \rangle;\\
\t1 type == reference(ref(STATE));\\
\t1 binding == bindingextension(\langle\\
\t2 chart\_identifier(c),\\
\t2 chart\_default(c),\\
\t2 chart\_inner(c),\\
\t2 chart\_outer(c),\\
\t2 chart\_parent(c),\\
\t2 chart\_left(c),\\
\t2 chart\_right(c),\\
\t2 chart\_substates(c),\\
\t2 chart\_decomposition(c),\\
\t2 chart\_type(c),\\
\t2 chart\_history(c)\\
\t1 \rangle) @ \LET\\
\t2 decl == declpart(\langle variable(name,type) \rangle);\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(chartname(c))),binding \rangle))
 @ \\
\t3 axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
TransitionIdentifierDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ TransitionIdentifierDeclaration(c) = \LET\\\t1
tnames == set2seq(\{t: \ran c.transitions @ decl(transitionid(c,t))\});\\\t1
exprs == set2seq(\{t: \ran c.transitions @ reference(ref(transitionid(c,t)))\});\\\t1
type == reference(ref(TRANSITIONID)) @ \LET\\\t2
decl == declpart(\langle variable(tnames, type)\rangle);\\\t2
pred == relationapplication(rel(EQUAL, \langle reference(ref(TRANSITIONID)),setextension(exprs)\rangle)) @\\\t3
axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
transition\_identifier : WF\_TRANSITION \fun  (DeclName \cross Expression)
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ transition\_identifier(c,t) = \\
(decl(IDENTIFIER),(reference(ref(transitionid(c,t)))))
\end{axdef}

\begin{axdef}
transition\_source : WF\_TRANSITION \fun  (DeclName \cross Expression)
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ transition\_source(c,t) = \\
\t1 \IF~\# t.source = 0\\
\t1 \THEN~(decl(SOURCE),(reference(ref(NULLTRANSITIONID))))\\
\t1 \ELSE~\IF~head~t.source \in \dom c.states \\
\t2 \THEN~(decl(SOURCE),\\\t3 application(reference(ref(SNODE)),\\\t4 reference(ref(stateid(c,getstatebyid(c,head~t.source))))))\\
\t2 \ELSE~(decl(SOURCE),\\\t3 application(reference(ref(JNODE)),\\\t4 reference(ref(junctionid(c,getjunctionbyid(c,head~t.source))))))
\end{axdef}

\begin{axdef}
transition\_destination : WF\_TRANSITION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ transition\_destination(c,t) = \\
\IF~t.destination \in \dom c.states\\
\t2 \THEN~(decl(DESTINATION),\\\t3 application(reference(ref(SNODE)),\\\t4 reference(ref(stateid(c,getstatebyid(c,t.destination))))))\\
\t2 \ELSE~(decl(DESTINATION),\\\t3 application(reference(ref(JNODE)),\\\t4 reference(ref(junctionid(c,getjunctionbyid(c,t.destination))))))
\end{axdef}

\begin{axdef}
transition\_next : WF\_TRANSITION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ transition\_next(c,t) = \\
\circblockbegin
\IF~\# t.next = 0\\
\THEN~(decl(NEXT),reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(NEXT),reference(ref(transitionid(c,gettransitionbyid(c,head~t.next)))))
\circblockend
\end{axdef}

\begin{axdef}
transition\_parent: WF\_TRANSITION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ transition\_parent(c,t) = \\
\t1 \IF~t.parent \in \dom c.states\\
\t1 \THEN~(decl(PARENT), reference(ref(stateid(c,getstatebyid(c,t.parent)))))\\
\t1 \ELSE~(decl(PARENT), reference(ref(chartid(c))))
\end{axdef}

\begin{axdef}
TransitionDeclaration: WF\_TRANSITION \fun Paragraph
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ TransitionDeclaration(c,t) =
\LET\\
\t1 name == \langle decl(transitionname(c,t)) \rangle;\\
\t1 type == reference(ref(TRANSITION));\\
\t1 binding == bindingextension(\langle\\
\t2 transition\_identifier(c,t),\\
\t2 transition\_source(c,t),\\
\t2 transition\_destination(c,t),\\
\t2 transition\_next(c,t),\\
\t2 transition\_parent(c,t)
\t1 \rangle) @ \LET\\
\t2 decl == declpart(\langle variable(name,type) \rangle);\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(transitionname(c,t))),binding \rangle))
 @ \\
\t3 axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
TransitionSetDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ TransitionSetDeclaration(c) = \LET\\
\t1 names ==  set2seq(\{t: \ran c.transitions @ reference(ref(transitionname(c,t)))\}\cup\{reference(ref(NULLTRANSITION))\}) @ \LET\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(TRANSITION)),setextension(names)\rangle)) @\\
\t3 axiomaticdescription(schematext(\langle \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
JunctionIdentifierDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART  @ JunctionIdentifierDeclaration(c) = \LET\\\t1
jnames == set2seq(\{j: \ran c.junctions @ decl(junctionid(c,j))\});\\\t1
exprs == set2seq(\{j: \ran c.junctions @ reference(ref(junctionid(c,j)))\});\\\t1
type == reference(ref(JUNCTIONID)) @ \LET\\\t2
decl == declpart(\langle variable(jnames, type)\rangle);\\\t2
pred == relationapplication(rel(EQUAL, \langle reference(ref(JUNCTIONID)),setextension(exprs)\rangle)) @\\\t3
axiomaticdescription(schematext(\langle decl \rangle, \langle \rangle))
\end{axdef}

\begin{axdef}
junction\_identifier : WF\_JUNCTION \fun  (DeclName \cross Expression)
\where
\forall c: WF\_CHART; j: Junction | (c,j) \in WF\_JUNCTION @ junction\_identifier(c,j) = \\
(decl(IDENTIFIER),(reference(ref(junctionid(c,j)))))
\end{axdef}

\begin{axdef}
junction\_transition: WF\_JUNCTION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; j: Junction | (c,j) \in WF\_JUNCTION @ junction\_transition(c,j) = \\
\circblockbegin
\IF~\# j.transition = 0\\
\THEN~(decl(TRANS),reference(ref(NULLTRANSITIONID)))\\
\ELSE~(decl(TRANS),reference(ref(transitionid(c,gettransitionbyid(c,head~j.transition)))))
\circblockend
\end{axdef}

\begin{axdef}
junction\_parent: WF\_JUNCTION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; j: Junction | (c,j) \in WF\_JUNCTION @ junction\_parent(c,j) = \\
\t1 \IF~j.parent \in \dom c.states \\
\t1 \THEN~(decl(PARENT), reference(ref(stateid(c,getstatebyid(c,j.parent)))))\\
\t1 \ELSE~(decl(PARENT), reference(ref(chartid(c))))
\end{axdef}

\begin{axdef}
junction\_history: WF\_JUNCTION \fun (DeclName \cross Expression)
\where
\forall c: WF\_CHART; j: Junction | (c,j) \in WF\_JUNCTION @ junction\_history(c,j) = \\
\t1 \IF~j.history = \true\\
\t1 \THEN~(decl(HISTORY),reference(ref(T)))\\
\t1 \ELSE~(decl(HISTORY),reference(ref(F)))
\end{axdef}

\begin{axdef}
JunctionDeclaration: WF\_JUNCTION \fun Paragraph
\where
\forall c: WF\_CHART; j: Junction | (c,j) \in WF\_JUNCTION @ JunctionDeclaration(c,j) =
\LET\\
\t1 name == \langle decl(junctionname(c,j)) \rangle;\\
\t1 type == reference(ref(JUNCTION));\\
\t1 binding == bindingextension(\langle\\
\t2 junction\_identifier(c,j),\\
\t2 junction\_transition(c,j),\\
\t2 junction\_parent(c,j),\\
\t2 junction\_history(c,j)
\t1 \rangle) @ \LET\\
\t2 decl == declpart(\langle variable(name,type) \rangle);\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(junctionname(c,j))),binding \rangle))
 @ \\
\t3 axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
JunctionSetDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ JunctionSetDeclaration(c) = \LET\\
\t1 names ==  set2seq(\{j: \ran c.junctions @ reference(ref(junctionname(c,j)))\}\cup\{reference(ref(NULLJUNCTION))\}) @ \LET\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(JUNCTION)),setextension(names)\rangle)) @\\
\t3 axiomaticdescription(schematext(\langle \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
EventsDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ EventsDeclaration(c) = \LET\\
\t1 names == set2seq(\{e: \ran c.events | e.scope \neq OUTPUTEVENT @ decl(eventname(c,e))\}\cup\{decl(NULLEVENT)\});\\
\t1 exprs ==  set2seq(\{e: \ran c.events | e.scope \neq OUTPUTEVENT @ reference(ref(eventname(c,e)))\}\cup\{reference(ref(NULLEVENT))\});\\
\t1 type == reference(ref(EVENT)) @ \LET\\
\t2 decl == declpart(\langle variable(names,type) \rangle);\\
\t2 pred == relationapplication(rel(EQUAL, \langle reference(ref(EVENT)),setextension(exprs)\rangle)) @\\
\t3 axiomaticdescription(schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
ChartDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ ChartDeclaration(c) =
\LET\\
\t1 states == set2seq(\{s: \ran c.states @\\\t2 tupleextension(\langle reference(ref(stateid(c,s))), reference(ref(statename(c,s))) \rangle) \});\\
\t1 chart == \langle tupleextension(\langle reference(ref(chartid(c))), reference(ref(chartname(c))) \rangle) \rangle;\\
\t1 transitions == set2seq(\{t: \ran c.transitions @\\\t2 tupleextension(\langle reference(ref(transitionid(c,t))), reference(ref(transitionname(c,t)))\rangle)\});\\
\t1 junctions == set2seq(\{j: \ran c.junctions @\\\t2 tupleextension(\langle reference(ref(junctionid(c,j))), reference(ref(junctionname(c,j))) \rangle)\}) @ \LET\\
\t3 decl == declpart(\langle expression(reference(ref(STATEFLOWCHART))) \rangle);\\
\t3 pred == newline(relationapplication(rel(EQUAL, \langle reference(ref(IDENTIFIER)), reference(ref(chartid(c))) \rangle)),\\
\t4 newline(relationapplication(rel(EQUAL, \langle reference(ref(STATES)),setextension(states\cat chart)\rangle)),\\
\t4 newline(relationapplication(rel(EQUAL, \langle reference(ref(TRANSITIONS)),setextension(transitions)\rangle)), \\
\t4 relationapplication(rel(EQUAL, \langle reference(ref(JUNCTIONS)),setextension(junctions)\rangle)))))
@\\
\t5 schemadefinition(processstatename(c),schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
DataDeclaration: WF\_DATA \fun Declaration
\where
\forall c: WF\_CHART; d: Data | (c,d) \in WF\_DATA @ DataDeclaration(c,d) = \\
\t1 variable(\langle decl(dataname(c,d))\rangle, translate_{Type}(d.type))
\end{axdef}

\begin{axdef}
OutputEventDeclaration: WF\_EVENT \fun Declaration
\where
\forall c: WF\_CHART; e: Event | (c,e) \in WF\_EVENT @ OutputEventDeclaration(c,e) = \\
\t1 variable(\langle decl(eventcountername(c,e))\rangle, reference(ref(NATURAL)))
\end{axdef}

\begin{axdef}
SimulationInstanceDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ SimulationInstanceDeclaration(c) = \LET\\
\t1 variables   == squash\{i: \dom c.data @ i \mapsto DataDeclaration(c,c.data(i))\};\\
\t1 outputevents == squash \{i: \dom c.events | (c.events(i)).scope = OUTPUTEVENT @\\
\t3 i \mapsto OutputEventDeclaration(c,c.events(i))\}@ \LET\\
\t2 decl == declpart(variables \cat outputevents) @\\
\t3 schemadefinition(SimulationInstance,schematext(\langle decl \rangle, \langle \rangle))
\end{axdef}

\begin{axdef}
newline\_conjunction: \seq_1 Predicate \fun Predicate
\where
\forall ps: \seq Predicate | \# ps = 1 @ newline\_conjunction(ps) = ps(1)\\
\forall ps: \seq Predicate | \# ps > 1 @ newline\_conjunction(ps) = newline(head~ps,newline\_conjunction(tail~ps))
\end{axdef}

\begin{axdef}
InitSimulationInstanceDeclaration: WF\_CHART \fun Paragraph
\where
\forall c: WF\_CHART @ InitSimulationInstanceDeclaration(c) = \LET\\
\t1 datainit == \{i: \dom c.data @\\\t2
	 i \mapsto relationapplication(rel(EQUAL, \langle reference(ref(dataname(c,c.data(i)))),translate_{InitExpr}(c,c.data(i))\rangle))\};\\
\t1 eventinit == \{i: \dom c.events | (c.events(i)).scope = OUTPUTEVENT @\\\t2
	 i \mapsto relationapplication(rel(EQUAL, \langle reference(ref(eventcountername(c,c.events(i)))),numberliteral(0)\rangle))\}\\\t1
 @ \LET decl == declpart(\langle expression(reference(ref(SimulationInstance))) \rangle);\\
\t2 pred == newline\_conjunction(datainit\cat eventinit)@\\
\t3 schemadefinition(InitSimulationInstance,schematext(\langle decl \rangle, \langle pred \rangle))
\end{axdef}

\begin{axdef}
InitStateDeclaration: Paragraph
\where
InitStateDeclaration = horizontaldefinition(decl(InitState),\\\t1
schemaconjunction(reference(ref(InitSimulationInstance)),reference(ref(InitSimulationData)))\\
)
\end{axdef}

\begin{axdef}
EntryActionDeclaration: WF\_STATE \fun PPar
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ EntryActionDeclaration(c,s) = \LET\\
\t1 name == EntryActionName(c,s);\\
\t1 comm == communication(EXECUTEENTRYACTION, \langle simpleparameter(reference(ref(stateid(c,s)))) \rangle) @\\
\circblockbegin \IF~\# s.entry > 0\\
\THEN~\circblockbegin
\IF~(c,s.entry) \in actions\_have\_broadcast\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Var}(translate_{Acts}(c,s.entry))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Acts}(c,s.entry)))))\\
\circblockend\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
externalchoiceextension: \seq N \fun Action
\where
\forall as: \seq N | \# as = 0 @ externalchoiceextension(as) = cspaction(skip)\\
\forall as: \seq N | \# as = 1 @ externalchoiceextension(as) = namedaction(head~as)\\
\forall as: \seq N | \# as > 1 @ externalchoiceextension(as) = \\
\t1 cspaction(actionexternalchoice(namedaction(head~as),externalchoiceextension(tail~as)))
\end{axdef}

\begin{axdef}
EntryActionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ EntryActionsDeclaration(c) = \LET\\
\t1 actions == \{s: \ran c.states @ EntryActionName(c,s) \} @\\
\t2 actionparagraph(ENTRYACTIONS, paraction(externalchoiceextension(set2seq(actions))))
\end{axdef}


\begin{axdef}
DuringActionDeclaration: WF\_STATE \fun PPar
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ DuringActionDeclaration(c,s) = \LET\\
\t1 name == DuringActionName(c,s);\\
\t1 comm == communication(EXECUTEDURINGACTION, \langle simpleparameter(reference(ref(stateid(c,s)))), inputparameter(E) \rangle) @\\
\circblockbegin \IF~\# s.during > 0\\
\THEN~
\circblockbegin
\IF~(c,s.during) \in dactions\_have\_broadcast\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Var}(translate_{DActs}(c,s.during))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{DActs}(c,s.during)))))
\circblockend\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
DuringActionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ DuringActionsDeclaration(c) = \LET\\
\t1 actions == \{s: \ran c.states @ DuringActionName(c,s) \} @\\
\t3 actionparagraph(DURINGACTIONS, paraction(externalchoiceextension(set2seq(actions))))
\end{axdef}

\begin{axdef}
ExitActionDeclaration: WF\_STATE \fun PPar
\where
\forall c: WF\_CHART; s: State | (c,s) \in WF\_STATE @ ExitActionDeclaration(c,s) = \LET\\
\t1 name == ExitActionName(c,s);\\
\t1 comm == communication(EXECUTEEXITACTION, \langle simpleparameter(reference(ref(stateid(c,s)))) \rangle) @\\
\circblockbegin \IF~\# s.exit > 0\\
\THEN~\circblockbegin
\IF~(c,s.exit) \in actions\_have\_broadcast\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Var}(translate_{Acts}(c,s.exit))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Acts}(c,s.exit)))))\\
\circblockend\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
ExitActionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ ExitActionsDeclaration(c) = \LET\\
\t2 actions == \{s: \ran c.states @ ExitActionName(c,s) \} @\\
\t3 actionparagraph(EXITACTIONS, paraction(externalchoiceextension(set2seq(actions))))
\end{axdef}

\begin{axdef}
ConditionActionDeclaration: WF\_TRANSITION \fun PPar
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ ConditionActionDeclaration(c,t) = \LET\\
\t1 name == ConditionActionName(c,t);\\
\t1 comm == communication(EXECUTECONDITIONACTION, \langle simpleparameter(reference(ref(transitionid(c,t)))) \rangle) @\\
\circblockbegin \IF~\# t.condact > 0\\
\THEN~\circblockbegin
\IF~(c,t.condact) \in actions\_have\_broadcast\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Var}(translate_{Acts}(c,t.condact))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Acts}(c,t.condact)))))\\
\circblockend\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
ConditionActionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ ConditionActionsDeclaration(c) = \LET\\
\t2 actions == \{t: \ran c.transitions @ ConditionActionName(c,t) \} @\\
\t3 actionparagraph(CONDITIONACTIONS, paraction(externalchoiceextension(set2seq(actions))))
\end{axdef}

\begin{axdef}
TransitionActionDeclaration: WF\_TRANSITION \fun PPar
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ TransitionActionDeclaration(c,t) = \LET\\
\t1 name == TransitionActionName(c,t);\\
\t1 comm == communication(EXECUTETRANSITIONACTION, \langle simpleparameter(reference(ref(transitionid(c,t)))) \rangle) @\\
\circblockbegin \IF~\# t.transact > 0\\
\THEN~\circblockbegin
\IF~(c,t.transact) \in actions\_have\_broadcast\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Var}(translate_{Acts}(c,t.transact))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, translate_{Acts}(c,t.transact)))))\\
\circblockend\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
TransitionActionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ TransitionActionsDeclaration(c) = \LET\\
\t2 actions == \{t: \ran c.transitions @ TransitionActionName(c,t) \} @\\
\t3 actionparagraph(TRANSITIONACTIONS, paraction(externalchoiceextension(set2seq(actions))))
\end{axdef}

\begin{axdef}
ConditionDeclaration: WF\_TRANSITION \fun PPar
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ ConditionDeclaration(c,t) = \LET\\
\t1 name == ConditionName(c,t);\\
\t1 truecomm == communication(EVALUATECONDITION,\\\t1 \langle simpleparameter(reference(ref(transitionid(c,t)))), outputparameter(reference(ref(T))) \rangle);\\
\t1 falsecomm == communication(EVALUATECONDITION,\\\t1 \langle simpleparameter(reference(ref(transitionid(c,t)))), outputparameter(reference(ref(F))) \rangle) @\\
\t2 \circblockbegin \IF~\# t.condition > 0\\
\THEN~actionparagraph(name, paraction(commandaction(ifcommand(gactions(\langle\\
\t3 (translate_{Pred}(c,head~t.condition),cspaction(prefixedaction(truecomm, cspaction(skip)))),\\
\t3 (negation(translate_{Pred}(c,head~t.condition)),cspaction(prefixedaction(falsecomm, cspaction(skip))))\\
\t2 \rangle)))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(truecomm, cspaction(skip)))))
\circblockend
\end{axdef}

\begin{axdef}
ConditionsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ ConditionsDeclaration(c) = \LET\\
\t2 conditions == \{t: \ran c.transitions @ ConditionName(c,t) \} @\\
\t3 actionparagraph(CONDITIONSACTION, paraction(externalchoiceextension(set2seq(conditions))))
\end{axdef}

\begin{axdef}
TriggerDeclaration: WF\_TRANSITION \fun PPar
\where
\forall c: WF\_CHART; t: Transition | (c,t) \in WF\_TRANSITION @ TriggerDeclaration(c,t) = \LET\\
\t1 name == TriggerName(c,t);\\
\t1 comm == communication(CHECKTRIGGERCHANNEL, \langle\\
\t2 simpleparameter(reference(ref(transitionid(c,t)))),\\
\t2 inputparameter(E)\\
\rangle);
\t1 trueguard == translate_{Triggers}(c,t.trigger);
\t1 truecomm == communication(RESULTCHANNEL,\langle\\
\t2 simpleparameter(reference(ref(transitionid(c,t)))),\\
\t2 simpleparameter(reference(ref(E))),\\
\t2 outputparameter(reference(ref(T)))\\
\t1 \rangle);
\t1 falsecomm == communication(RESULTCHANNEL,\langle\\
\t2 simpleparameter(reference(ref(transitionid(c,t)))),\\
\t2 simpleparameter(reference(ref(E))),\\
\t2 outputparameter(reference(ref(F)))\\
\t1 \rangle) @\\
\t2 \circblockbegin
\IF~\# t.trigger > 0\\
\THEN~actionparagraph(name, paraction(cspaction(prefixedaction(comm,\\
\t3 commandaction(ifcommand(gactions(\langle\\
\t4 (trueguard,cspaction(prefixedaction(truecomm, cspaction(skip)))),\\
\t4 (negation(trueguard),cspaction(prefixedaction(falsecomm, cspaction(skip))))\\
\t3 \rangle)))))))\\
\ELSE~actionparagraph(name, paraction(cspaction(prefixedaction(comm, cspaction(prefixedaction(truecomm, cspaction(skip)))))))
\circblockend
\end{axdef}

\begin{axdef}
TriggersDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ TriggersDeclaration(c) = \LET\\
\t1 triggers == \{t: \ran c.transitions @ TriggerName(c,t) \} @\\
\t3 actionparagraph(TRIGGERSACTION, paraction(externalchoiceextension(set2seq(triggers))))
\end{axdef}

Next, we define the paragraphs of the specification that are independent from the diagram; these are defined as
constants of type $PPar$.

\begin{axdef}
GetStateDeclaration: PPar
\where
GetStateDeclaration = \LET\\
\t1 comm == communication(STATECHANNEL,\langle\\
\t2 guardedinputparameter(X,relationapplication(rel(IN,\langle\\
\t3 reference(ref(X)), functionapplication(app(DOM,\langle reference(ref(STATES)) \rangle))\\
\t2 \rangle))),\\
\t2 outputparameter(functionapplication(app(STATES,\langle reference(ref(X)) \rangle)))\\
\t1 \rangle) @ actionparagraph(GETSTATE, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
GetJunctionDeclaration: PPar
\where
GetJunctionDeclaration = \LET\\
\t1 comm == communication(JUNCTIONCHANNE    L,\langle\\
\t2 guardedinputparameter(X,relationapplication(rel(IN,\langle\\
\t3 reference(ref(X)), functionapplication(app(DOM,\langle reference(ref(JUNCTIONS)) \rangle))\\
\t2 \rangle))),\\
\t2 outputparameter(functionapplication(app(JUNCTIONS,\langle reference(ref(X)) \rangle)))\\
\t1 \rangle) @ actionparagraph(GETJUNCTION, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
GetTransitionDeclaration: PPar
\where
GetTransitionDeclaration = \LET\\
\t1 comm == communication(TRANSITIONCHANNEL,\langle\\
\t2 guardedinputparameter(X,relationapplication(rel(IN,\langle\\
\t3 reference(ref(X)), functionapplication(app(DOM,\langle reference(ref(TRANSITIONS)) \rangle))\\
\t2 \rangle))),\\
\t2 outputparameter(functionapplication(app(TRANSITIONS,\langle reference(ref(X)) \rangle)))\\
\t1 \rangle) @ actionparagraph(GETTRANSITION, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
GetEventsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @
GetEventsDeclaration(c) = \LET\\
\t1 seqevents == squash(\{e: \ran (c.events) | e.scope = INPUTEVENT @ e.identifier \mapsto reference(ref(eventname(c,e)))\}) @
\LET\\
comm == communication(EVENTSCHANNEL,\langle
outputparameter(sequence(\\\t1
	\IF~seqevents = \langle\rangle \THEN~~\langle reference(ref(NULLEVENT)) \rangle \ELSE~~seqevents))\rangle)\\
@ actionparagraph(GETEVENTS, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}


\begin{axdef}
GetChartDeclaration: PPar
\where
GetChartDeclaration = \LET\\
\t1 comm == communication(CHARTCHANNEL,\langle\\
\t2 outputparameter(functionapplication(app(STATES,\langle reference(ref(IDENTIFIER)) \rangle)))\\
\t1 \rangle) @ actionparagraph(GETCHART, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
StatusDeclaration: PPar
\where
StatusDeclaration = \LET\\
\t1 comm == communication(STATUSCHANNEL,\langle\\
\t2 guardedinputparameter(X,relationapplication(rel(IN,\langle\\
\t3 reference(ref(X)), functionapplication(app(DOM,\langle reference(ref(STATESTATUS)) \rangle))\\
\t2 \rangle))),\\
\t2 outputparameter(functionapplication(app(STATESTATUS,\langle reference(ref(X)) \rangle)))\\
\t1 \rangle) @ actionparagraph(STATUSACTION, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
HistoryDeclaration: PPar
\where
HistoryDeclaration = \LET\\
\t1 comm == communication(HISTORYCHANNEL,\langle\\
\t2 guardedinputparameter(X,relationapplication(rel(IN,\langle\\
\t3 reference(ref(X)), functionapplication(app(DOM,\langle reference(ref(STATEHISTORY)) \rangle))\\
\t2 \rangle))),\\
\t2 outputparameter(functionapplication(app(STATEHISTORY,\langle reference(ref(X)) \rangle)))\\
\t1 \rangle) @ actionparagraph(HISTORYACTION, paraction(cspaction(prefixedaction(comm,cspaction(skip)))))
\end{axdef}

\begin{axdef}
ActivationDeclaration: PPar
\where
ActivationDeclaration = \LET\\
\t1 comm == communication(ACTIVATECHANNEL,\langle\\
\t2 inputparameter(X) \rangle);\\
\t1 activate == schemaaction(reference(ref(ACTIVATESCHEMA))) @\\
\t2 actionparagraph(ACTIVATIONACTION,paraction(cspaction(prefixedaction(comm,activate))))
\end{axdef}

\begin{axdef}
DeactivationDeclaration: PPar
\where
DeactivationDeclaration = \LET\\
\t1 comm == communication(DEACTIVATECHANNEL,\langle\\
\t2 inputparameter(X) \rangle);\\
\t1 deactivate == schemaaction(reference(ref(DEACTIVATESCHEMA))) @\\
\t2 actionparagraph(DEACTIVATIONACTION,paraction(cspaction(prefixedaction(comm,deactivate))))
\end{axdef}


\begin{axdef}	
ChartActionsDeclaration: PPar
\where
ChartActionsDeclaration = \LET\\
\t1 actions == \langle ENTRYACTIONS, DURINGACTIONS, EXITACTIONS, CONDITIONACTIONS, TRANSITIONACTIONS \rangle @ \LET\\
\t1 a1 == externalchoiceextension(actions);\\
\t1 a2 == cspaction(prefixedaction(communication(ENDACTION,\langle\rangle),cspaction(skip))) @\\
\t2 actionparagraph(CHARTACTIONS,paraction(cspaction(actionsequentialcomposition(a1,a2))))
\end{axdef}

\begin{axdef}
InterfaceActionsDeclaration: PPar
\where
InterfaceActionsDeclaration = \LET\\
\t1 actions == \langle GETCHART, GETSTATE, GETJUNCTION, GETTRANSITION, STATUSACTION, HISTORYACTION,\\
\t2 ACTIVATIONACTION, DEACTIVATIONACTION \rangle @\\
\t3 actionparagraph(INTERFACEACTIONS,paraction(externalchoiceextension(actions)))
\end{axdef}

\begin{axdef}
interleaveextension: \seq (Action \cross \seq N) \fun Action
\where
\forall as: \seq (Action \cross \seq N) | \# as = 0 @ interleaveextension(as) = cspaction(skip)\\
\forall as: \seq (Action \cross \seq N) | \# as = 1 @ interleaveextension(as) = (head~as).1\\
\forall as: \seq (Action \cross \seq N) | \# as > 1 @ interleaveextension(as) = \\
\t1 cspaction(actioninterleave((head~as).1,ns((head~as).2),ns(\dcat\{i:\dom~(tail~as) @ i \mapsto ((tail~as)i).2\}),interleaveextension(tail~as)))
\end{axdef}

\begin{axdef}
InputsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ InputsDeclaration(c) = \LET\\
\t1 channels == \{d: \ran c.data | d.scope = INPUTDATA @ (datachannelname(c,d),dataname(c,d))\} @ \LET\\
\t2 commassign == \{cv: channels @ (communication(cv.1,\langle inputparameter(X) \rangle),assignment(\langle (cv.2,reference(ref(X))) \rangle),\langle cv.2\rangle) \} @ \LET\\
\t3 actions == \{ca: commassign @ (cspaction(prefixedaction(ca.1,commandaction(ca.2))),ca.3)\} @ \\
\t4 actionparagraph(INPUTSACTION,paraction(cspaction(prefixedaction(communication(READINPUTSCHANNEL,\langle\rangle),\\
\t5 interleaveextension(set2seq(actions))))))
\end{axdef}

\begin{axdef}
WriteOutputEvent: WF\_CHART \cross Event \fun Action
\where
\forall c: WF\_CHART; e: Event | e.scope = OUTPUTEVENT @\\
WriteOutputEvent(c,e) = \LET pred == relationapplication(rel(GT,\langle reference(ref(eventcountername(c,e))),numberliteral(0)\rangle));\\\t1
pair == (eventcountername(c,e),functionapplication(app(MINUS,\langle reference(ref(eventcountername(c,e))),numberliteral(1)\rangle)));\\\t1
commtrue == communication(outputeventchannelname(c,e),\langle outputparameter(reference(ref(T)))\rangle);\\\t1
commfalse == communication(outputeventchannelname(c,e),\langle outputparameter(reference(ref(F)))\rangle) @ \LET\\\t2
a1 == cspaction(prefixedaction(commtrue,commandaction(assignment(\langle pair\rangle))));\\
a2 == cspaction(prefixedaction(commfalse,cspaction(skip))) @\\\t3
commandaction(ifcommand(gactions(\langle (pred,a1),(negation(pred),a2)\rangle)))
\end{axdef}

\begin{axdef}
OutputsDeclaration: WF\_CHART \fun PPar
\where
\forall c: WF\_CHART @ OutputsDeclaration(c) = \LET\\
\t1 channels == \{d: \ran c.data | d.scope = OUTPUTDATA @ (datachannelname(c,d),dataname(c,d))\} @ \LET\\
\t2 comm == \{cv: channels @ (communication(cv.1,\langle outputparameter(reference(ref(cv.2))) \rangle),\langle cv.2\rangle) \} @ \LET\\
\t3 actions == \{c: comm @ (cspaction(prefixedaction(c.1,cspaction(skip))),c.2)\} \cup\\\t4
	\{e: \ran c.events | e.scope = OUTPUTEVENT @ (WriteOutputEvent(c,e),\langle eventcountername(c,e)\rangle)\} @\\
\t4 actionparagraph(OUTPUTSACTION,paraction(cspaction(prefixedaction(communication(WRITEOUTPUTSCHANNEL,\langle\rangle),\\
\t5 interleaveextension(set2seq(actions))))))
\end{axdef}

\begin{axdef}
AllActionsDeclaration: PPar
\where
AllActionsDeclaration = \LET\\
\t1 actions == \langle CONDITIONSACTION, TRIGGERSACTION, INPUTSACTION, OUTPUTSACTION, CHARTACTIONS,\\\t2 INTERFACEACTIONS \rangle @\\
\t1 actionparagraph(ALLACTIONS,paraction(externalchoiceextension(actions)))
\end{axdef}

\begin{axdef}
MainActionDeclaration: Action
\where
MainActionDeclaration = \LET\\
\t1 first == schemaaction(reference(ref(InitState)))
@\\
\t1 cspaction(actionsequentialcomposition(first,cspaction(recursiveaction(X,\\\t2
	cspaction(actionsequentialcomposition(namedaction(ALLACTIONS),namedaction(X)))))))
\end{axdef}

\begin{axdef}
ProcessStateDeclaration: WF\_CHART \fun ProcessState
\where
\forall c: WF\_CHART @ ProcessStateDeclaration(c) =\\\t1
stateDecl(decl(processstatename(c)),schemaconjunction(reference(ref(SimulationInstance)),reference(ref(SimulationData))))
\end{axdef}

\begin{axdef}
BroadcastDeclaration: PPar\\
CheckDeclaration: PPar\\
\end{axdef}

\begin{axdef}
ProcessDeclaration: WF\_CHART \fun ProcDecl
\where
\forall c: WF\_CHART @ ProcessDeclaration(c) = \LET\\
\t1 stateparagraphs == \langle zparagraph(ChartDeclaration(c)), zparagraph(SimulationInstanceDeclaration(c)),\\
\t2 zparagraph(InitSimulationInstanceDeclaration(c)), zparagraph(InitStateDeclaration) \rangle;\\
\t1 state == ProcessStateDeclaration(c);\\
\t1 entryactions == set2seq(\{s: \ran c.states @ EntryActionDeclaration(c,s)\}\cup\{EntryActionsDeclaration(c)\});\\
\t1 duringactions == set2seq(\{s: \ran c.states @ DuringActionDeclaration(c,s)\}\cup\{DuringActionsDeclaration(c)\});\\
\t1 exitactions == set2seq(\{s: \ran c.states @ ExitActionDeclaration(c,s)\}\cup\{ExitActionsDeclaration(c)\});\\
\t1 conditionactions == set2seq(\{t: \ran c.transitions @ ConditionActionDeclaration(c,t)\}\cup\{ConditionActionsDeclaration(c)\});\\
\t1 transitionactions == set2seq(\{t: \ran c.transitions @ TransitionActionDeclaration(c,t)\}\cup\{TransitionActionsDeclaration(c)\});\\
\t1 conditions == set2seq(\{t: \ran c.transitions @ ConditionDeclaration(c,t)\} \cup \{ConditionsDeclaration(c)\});\\
\t1 triggers == set2seq(\{t: \ran c.transitions @ TriggerDeclaration(c,t)\} \cup \{TriggersDeclaration(c)\});\\
\t1 getters == \langle GetStateDeclaration, GetJunctionDeclaration, GetTransitionDeclaration, GetChartDeclaration, GetEventsDeclaration(c) \rangle;\\
\t1 broadcast == \langle BroadcastDeclaration, CheckDeclaration \rangle;\\
\t1 others == \langle StatusDeclaration, HistoryDeclaration, ActivationDeclaration, DeactivationDeclaration \rangle;\\
\t1 collections == \langle ChartActionsDeclaration, InterfaceActionsDeclaration, InputsDeclaration(c), OutputsDeclaration(c), AllActionsDeclaration \rangle @\\
\t1 \LET actions == entryactions\cat duringactions \cat exitactions \cat conditionactions \cat transitionactions \cat conditions \cat triggers \cat\\\t2
 getters \cat broadcast \cat others \cat collections @\\
\t3 simpleprocessdeclaration(processname(c),processdefinition(proc(stateparagraphs, state, actions, MainActionDeclaration)))
\end{axdef}

\begin{axdef}
ChannelsDeclaration: WF\_CHART \fun CircusPar
\where
\forall c: WF\_CHART @ ChannelsDeclaration(c) = \LET\\
\t1 datachannelsdecl == set2seq(\{d: \ran c.data | d.scope = INPUTDATA \lor d.scope = OUTPUTDATA @\\\t2
typedsimplecdecl(\langle datachannelname(c,d)\rangle,translate_{Type}(d.type))\});\\
\t1 eventchannels == \{e: \ran c.events | e.scope = OUTPUTEVENT @ outputeventchannelname(c,e)\}  @\\
\t2 channeldeclaration(cdecl(datachannelsdecl\cat\langle typedsimplecdecl(set2seq(eventchannels),reference(ref(BOOL)))\rangle))
\end{axdef}

\begin{axdef}
translate: WF\_CHART \fun Program
\where
\forall c: WF\_CHART @ translate(c) = \LET\\
identifiers == \langle zparagraphdeclaration(StateIdentifierDeclaration(c)),\\
\t1 zparagraphdeclaration(JunctionIdentifierDeclaration(c)),\\
\t1 zparagraphdeclaration(TransitionIdentifierDeclaration(c)) \rangle;\\
chart == \langle zparagraphdeclaration(ChartAsStateDeclaration(c)) \rangle;\\
states == set2seq(\{s: \ran c.states @ zparagraphdeclaration(StateDeclaration(c,s))\})\cat\\\t1
 \langle zparagraphdeclaration(StateSetDeclaration(c))\rangle;\\
junctions == set2seq(\{j: \ran c.junctions @ zparagraphdeclaration(JunctionDeclaration(c,j))\})\cat\\\t1
 \langle zparagraphdeclaration(JunctionSetDeclaration(c))\rangle;\\
transitions == set2seq(\{t: \ran c.transitions @ zparagraphdeclaration(TransitionDeclaration(c,t))\})\cat\\\t1
 \langle zparagraphdeclaration(TransitionSetDeclaration(c))\rangle;\\
events == \langle zparagraphdeclaration(EventsDeclaration(c)) \rangle;\\
channels == \langle ChannelsDeclaration(c) \rangle;\\
proc == \langle processdeclaration(ProcessDeclaration(c)) \rangle @\\
program(identifiers \cat chart \cat states \cat junctions \cat transitions \cat events \cat channels \cat proc)
\end{axdef}

\end{document}
