Timed-Altarica-To-Fiacre-Translator/doc/Rapport post-doc/app.tex

\section{Interpretation of AltaRica in Fiacre}
\lstset{  keywordstyle=\bfseries,
  % keywordstyle={[2]\itshape},
  keywordstyle=\color{bluekeywords},
  basewidth=0.94ex,
  showstringspaces=false,
  emptylines=1,
  aboveskip=4pt,belowskip=4pt,
  mathescape=true, 
  texcl=true, 
  escapechar=@,
  numberblanklines=false}
 \newcommand{\sem}[1]{\llbracket{#1}\rrbracket}

This appendix can be safely ignored and is not necessary to understand
the approach described in the report. Its main purpose is to give a
precise definition of the encoding from AltaRica to Fiacre that is
only roughly described in Sect.~\ref{sec:sect3}.

We give a more precise definition of our encoding from AltaRica
Dataflow to Fiacre. We base our definition on a simplified grammar for
AltaRica Dataflow, using the Cecilia OCAS syntax, and a ``semantics
function'' (denoted $\sem{\,}$) to translate an AltaRica expression
into Fiacre. The encoding uses an environment, $\sigma$, to map event
identifiers (\code{evt}) to their timing constraints (defined in the
\code{extern} heading). We omit this environment when it is obvious
from the context.

We describe the grammar of the AltaRica language using a variant of
Extended Bachus Naur Form (EBNF). The EBNF describes a set of
production rules of the form ``\code{symb ::= expr}'', meaning that
the nonterminal symbol \code{symb} represents anything that can be
generated by the EBNF expression \code{expr}. An expression
\code{expr} may be one of the following: a terminal symbol or keyword,
between quotes (e.g., \code{'event'}); a nonterminal symbol; an
optional expression, written ``\code{[ expr0 ]}''; a choice between
two expressions, written ``\code{expr1} $\,\mid\,$ \code{expr2}''; the
iterative concatenation of one or more expressions, with successive
occurrences being separated by a given symbol \code{s}, written
``\code{(expr s)*}''.


\subsection*{Types}
\label{sec:types}

AltaRica base types include ``Boolean'' and Integers. We do not
consider floating point number in our translation; even though real
numbers are useful to declare probabilities, floating point variables
do not fit well with an enumerative model-checking approach. The
language also provides enumeration types, called \emph{domains}, that
defines sets of symbolic constants that can be used with state
variables.

\begin{lstlisting}[language=BNF]
Type   ::= 'Boolean' | 'Integer' | Ident
Domain ::= 'domain' Ident '{' (Ident ',')* '}'
\end{lstlisting}

Fiacre supports a boolean type \code{bool}, with the same primitive
operators than AltaRica, equality (\code{=}) and inequality
(\code{<>}), and a ternary conditional operator. The numeric types of
Fiacre include the type \code{int} of all integers and the the type
\code{nat} of non negative integers. As we stated in
Sect.~\ref{sec:sect3}, domains can be directly encoded using union
types in Fiacre.

\begin{lstlisting}[language=BNF]
[[Boolean]] = bool       [[Integer]] = int       [[Ident]] = Ident
[[domain IType {I1 , ..., In}]] = type IType is union I1 | ... | In end ;
\end{lstlisting}

The fact that we can directly reuse the same type identifier in the
two languages means that we can directly reuse AltaRica type
declarations in Fiacre. Indeed, a type declaration of the form
\code{V1 : T1, ..., Vn : Tn} is encoded in Fiacre  as follows:
%
\lstinline[language=BNF]{V1 : [[T1]], ..., Vn : [[Tn]]}

Note that a limitation of Fiacre type declarations is that all type
constructors must be different, therefore we assume that the constants
used in different domains are always distinct. (This restriction
could be lifted by renaming constants using some information from the
type checker, but this has no effects on the expressiveness of our
approach.)

\subsection*{Instructions}
\label{sec:instructions}

Instructions are used to described the actions (postcondition) of
transitions and assertions. There are fundamentally four instructions:
skip, assignments, if-then instructions and composition. All the
possible instructions in AltaRica can be rewritten using only these
four fundamental instructions. A notable example of instruction
missing in this short list is the switch statement (that can be
encoded using nested conditionals). Fiacre provides an equivalent
\code{case}-statement that can be used to do traditional
pattern-matching.

\begin{lstlisting}[language=BNF]
Instr ::= 'skip' | V ':=' Expr | 'if' Expr 'then' Instr | '{' (Instr)* '}
\end{lstlisting}

Expressions, \code{Expr}, are built using the variables, constants and
the usual arithmetic operators. The syntax of expressions is exactly
the same as in Fiacre, so we have
%
\lstinline[language=BNF]{[[Expr]] = Expr}.

The equivalent of instructions in Fiacre is called statement.  The
\code{skip} instruction is a ``neutral element''; it describes the
instruction that does nothing. Fiacre has an equivalent notion with
the statement \code{null}. Assignments and conditionals are also
present in Fiacre, with the same semantics. The main difference is
that we do not enforce any differences between flow and state
variables.

\begin{lstlisting}[language=BNF]
[[skip]]               = null 
[[V := Expr]]          = V := [[Expr]]
[[if Expr then Instr]] = if [[Expr]] then [[Instr]] end
[[{I1 ... In}]]        = [[I1]] ; ... ; [[In]]
\end{lstlisting}

The interpretation of AltaRica instructions is straightforward. The
main discrepancy is with composition. For most practical purposes,
composition in AltaRica can be encoded using sequential
composition. In the case where different statements in a composition
update the same variable, it could be necessary to introduce temporary
variables, but this can be already enforced in the original AltaRica
instruction. For example, the composition \code{\{(X := Y) (Y :=
  X)\}}, that can be used to swap the values of two variables in
AltaRica, should be replaced by the instruction \code{\{(TEMP := X) (X
  := Y) (Y := TEMP)\}}.

\subsection*{Nodes}

An AltaRica model is essentially a collection of node declarations. A
node is made of three parts: declaration of state variables, flow
variables and events; declaration of transitions; and finally
assertions.

\begin{lstlisting}[language=BNF]
Node   ::= 'node' Ident Flow State Event Init Trans Assert [Extern]
Flow   ::= 'flow' (Ident ':' Expr ':' ('in' | 'out') ',')* ';'
State  ::= 'state' (Ident ':' TypIdent ',')* ';'
Event  ::= (Ident ',')* ';'
Init   ::= 'init' Expr ';'
Trans  ::= 'trans' (Expr v- Ident -> Expr ';')* 
Assert ::= 'assert' Expr ';'
\end{lstlisting}

In the following, we assume that we want to encode a node \F{} with
flow variables declaration \code{flow V1 : T1, ..., Vk : Tk;} and
state variables declaration \code{state S1 : I1, ..., Sn : In;}.  Our
encoding makes use of a Fiacre record type, \code{Flows}, defined as
follows.

\begin{lstlisting}[language=BNF,mathescape=true]
type Flows is record V1 : [[T1]], ..., Vk : [[Tk]] end
\end{lstlisting}

The type \code{Flows} is used to define a function computing the
effect of assertions on the flow variables. The behaviour of
assertions is one of the main differences between dialects of
AltaRica. The case of AltaRica Dataflow is the simplest since, by
definition, there should be a fixed order (computable at compile time)
in which to evaluate the assignments defined in the \code{assert}
heading. In this case, if the node declares an assert expressions
\code{assert exp;} then we assume that the Fiacre function
\code{update} is declared as follows, where \code{((exp))} is the
Fiacre expression $\llbracket$\code{exp}$\rrbracket$ in which every
occurrence of flow variables, \code{Vi}, are replaced with a record
field access, \code{f.Vi}.

\begin{lstlisting}[language=BNF,mathescape=true]
function update(S1 : I1, ..., Sn : In, env : Flows) : Flows is
   var f : Flows := env
   begin
      ((exp))
      return f
   end
\end{lstlisting}

Other dialects of AltaRica may require a fixpoint computation, or at
least a recursive evaluation of the \code{assert} expression. This
different semantics could be encoded in Fiacre as well. Indeed Fiacre
functions can be recursively defined. For better performances, it is
also possible to implement the computation of assertions in an
external library and to import it in Fiacre using Foreign Function
Interfaces.

The definition of the node may also contain timing constraints
declared using an \code{extern} clause. A timing constraint is a
(time) interval of the form \code{[a, b]}, \code{]a, b]}, \code{[a,
  b[}, or \code{]a, b[}. An interval of the form \code{[a, ...[} is
used to denote an unbounded interval (that is a $\infty$-bound).

\begin{lstlisting}[language=BNF]
Extern ::= 'extern'  ('law' '(' Ident ')' '=' '"' Time '"' ';')*
Time   ::= Left ',' Right
Left   ::= '[' Int | '[' Int
Right  ::= Int ']' | Int '[' |  '...' '['
\end{lstlisting}

When there is a declaration \code{extern law(evt) = "Time";} in the
definition of the node \F{}, we assume that the environment $\sigma$
is such that $\sigma$(\code{evt}) = \code{Time}. If an event is not
declared in the \code{extern} heading then we can safely assume that it
is associated with the time constraint \code{[0, ...[}.

Equipped with all these additional definitions, it is possible to
encode every transition declared in \F{} into a Fiacre statement. In
particular, each transition of the form
%%
\lstinline[language=Altarica]{g |-evt-> Exp ;}.
%%
in the AltaRica code can be encoded into Fiacre as a sequence of a
conditional (a test on the guard \code{g}); followed by an action
(evaluation of the expression $\llbracket$\code{exp}$\rrbracket$);
finished by the evaluation of assertions. In this example we assume
that the transition \code{evt} is associated with the time interval
$I$, that is $\sigma(\text{\code{env}}) = \text{I}$.
%%
\begin{lstlisting}[language=BNF,mathescape=true]
[[evt]] = #evt; wait $\text{I}$; on(g); [[Exp]]; env := update(S1, ..., Sn, env); loop
\end{lstlisting}

Our encoding makes use of some assumptions that were not introduced
previously. Like in the example of Sect.~\ref{sec:sect3}, we encode a
node as a Fiacre process with a unique state. The statement
\code{loop} is used in Fiacre to declare that the target (the
destination state) of the transition is the same as its source. The
expression \verb+#+\code{evt} is a way to associate a ``tag'' with a
Fiacre transition. Tags give an alternative way to name transitions in
a temporal logic formula (for model-checking) and when we print or
simulate a counterexample. In a nutshell, we use tags as a simple
mechanism for traceability between the AltaRica and Fiacre code.  

With all the definitions introduced in this section, the encoding of
node \F{}, with transitions \code{evt1, ..., evtk}, boils down to a
single Fiacre process. To conclude, we simply need to create a
top-level component that creates an instance of this process and
initializes the state and flow variables. In the following listing, we
assume that \code{Expi} corresponds to the (AltaRica) expression
associated with the state variables \code{Si} in the \code{init}
heading of \F{}. In this code, we use the \code{init} declaration of
Fiacre that allows us to initialize the value of the flow variables in
the initial state.

%,float=hbt,frame=single,captionpos=b,caption=\protect{Code
%skeleton for the interpreation of the Node \F{} in  Fiacre}]
\begin{lstlisting}[language=BNF]
type Flows is record V1 : [[T1]], ..., Vk : [[Tk]] end

function update(S1 : I1, ..., Sn : In, env : Flows) : Flows is
   var f : Flows := env
   begin
      ((exp))
      return f
   end

process F(&S1 : I1, ..., &Sn : In, &env : Flows) is
   states s0

   init 
      env := update(S1, ..., Sn, env);
      to s0
 
   from s0 select
      [[evt1]] [] ... [] [[evtk]]
   end

component Main is
   var env : Flows,
       S1  : I1 := [[Exp1]],
       ...,
       Sn  : In := [[Expn]]

   par F(S1, ..., Sn, env) end
\end{lstlisting}




\section{Method and translation}\label{sec:sectB}

\subsection{Time Petri Nets}
Petri Nets are bi-partite graphs with two classes of nodes: places and transitions.
Time Petri Nets are en extension to classical Petri nets that include time features, % TODO Cite Merlin
namely two real numbers, $a$ and $b$, with $a < b$, that label each transition and indicate the time interval a transition is active, being \emph{de facto} a temporal guard.

	\begin{definition}[Time Petri Nets]\label{def:TPN}
	A time Petri net (TPN) is a tuple  $\langle P, T, B, F, M_0, \tau \rangle $ where:
	\begin{itemize}
		\item $P$ is a finite nonempty set of places $p_i$;
		\item $T$ is a finite nonempty set of transitions $t_i$;
		\item $F$ is the flow relation 
		$ F : P \times T \to P$
		\item $M_0$ is the initial marking function
		$ 	M_0 :P \to \mathbb{N} $
		\item $\tau$ is a mapping called static (firing) interval for transitions
		$ 	\tau : T \to \mathbb{R}^+_0 \times (\mathbb{R}^+_0 \cup \infty) $
	\end{itemize}


%	\item $B$ is the backward incidence function
%$ B:T\times P \to  \mathbb{N}$
%\item $F$ is the forward incidence function
%$ F:T\times P \to P\times T $
%% However, as new markings via a transition t_i are given by 
%% M'(p) = M(p) - B(t_i,p) + F(t_i,p) for all p
% The function F resumes and simplifies this transition, associating to a set of places and enabled transitions (i.e. a state), a set of places and enabled transitions.
% The current marking $M$ of a TPN is obtained from the transitions history $t_1, \ldots t_n$, s.t. $ M = t_n \circ t_1(M_0)$,
% with the new marking $M'$, calculated from a transition $t$ and a marking $M$ is given by
% M' = M - prec(p) + post(p)
	\end{definition}
For reference, the tuple  $\langle P, T, F, M_0\rangle $ identifies a Petri net.

A transition $t \in T$ is \emph{fireable} when all its input places have at least one token; for sake of simplicity, we do not consider here weights on transitions, as the result is similar, with just a change in the marking calculation.
The flow relation then associates to the number of tokens in a place (which we call $w: P \to \mathbb{N}$ a function of the place) and a fireable transition, the tokens in the target place.


\subsubsection{States in a TPN}

The dynamic aspects of Petri net model are denoted by
markings which are assignments of tokens 
to the places of a Petri net. The execution  is then derived  from the number and emplacements of tokens. 

Given the definition above, a state in a TPN is given by the pair $(M,I)$, where 
the marking $ M = \{m = w(p)\,|\, p \in P\}$ can be seen as a vector of markings,
and
% the temporal constraints on each active transition $TC= (\theta_{min}, \theta_{max})$
the firing interval set is $I = \{\tau(t)\:|\:t\in T\}$, which can be seen as a vector of firing intervals for the fireable transitions~\cite{berthomieu1991TPN}.



Over TPN states and transitions between them, it is possible to define an \emph{extended state graph}\cite{yao},
which root corresponds to the state coming from the initial marking and fireable transitions
%
The new markings are computed as usual, by applying $F$ on the marking of the current state, and,
similarly, the new firing interval is computed consequently, for a more detailed description refer to \cite{berthomieu1991TPN}.
Thus, the transition rules permit to compute states and state reachability.

% The reachable states from a state $S = (M,I)$
% are the states $S'$ such that, $\forall t \in I$ (the transitions fireable) at time $\theta$ leading to state $S'$.

\subsection{From AltaRica to Tina}
The underlying mathematical model of the AltaRica language is a Guarded Transition System (GTS), an automaton that generalises Reliability Block Diagrams, Markov chains and Stochastic Petri nets~\cite{rau08}. In GTS, states are represented by value assignment to variables, while the states transitions are triggered by events, that change the variables value. Synchronisation between events (habitually asynchronous) is produced by introducing a new event.

Given that it is always possible to obtain a flattened model from a
composition of interconnected AltaRica nodes, it is then possible to
interpret a (general) AltaRica model by using the GTS model encoding.
Our translation approach relies on Extended Timed Guarded Transition System (ETGTS), an extension of the GTS of AltaRica opportunely enriched to include timed guards.

Expressing durations over event and non-deterministic transitions triggered by temporal guards, fall out of the AltaRica Dataflow expressiveness and thus cannot be captured nor analysed by its associated tool. %which can treat time as a set of delay assignment, i.e. with a fixed delay associated to each transition.
So, we enriching the syntax of AltaRica Dataflow to model temporal guarded transitions by adding a new event law, as defined in Def.~\ref{def:ETGTS}.


\begin{comment}
%%%%start comment
\begin{definition}[ETGTS]\label{def:ETGTS}
  An Extended  Timed Guarded Transition System is a tuple $\langle S, s_0, E, T, \tau \rangle $ where:
  \begin{itemize}
  \item $S$ is a set of states;
    \item $s_0 \in S$ is the initial state;
  \item $E$ is a set of event symbols;
    \item $T$ is  a set of transitions s.t. $T \subseteq S \times E \times S$. 
    \item $\tau$ is the delay relation, $\tau: E \to \mathbb{R}^+ \times (\mathbb{R}^+  \cup \infty)$, assigning a minimal and a maximal delay to the transitions bound to event $e$.
  \end{itemize}
  A transition $t \in T: (s, e, s')$ associates a state $s'$, to a state $s$ by executing the event $e$ in $s$, after a delay in the interval $[\delta_{min}, \delta_{max}]$ given by $\tau(e)$.
      
    A \emph{run}  $\rho$ of a timed Transition System is a sequence of pairs event-time from the initial state $s_0$:
    \begin{align*}
      \rho &= \{ (e_1,\delta_1), \ldots, (e_n,\delta_n)  \} \; 
      \text{s.t. } \forall i \;\delta_i \in \tau(e_i), \text{ and }\\
      &s_0 \xrightarrow{t_1} s_1 \xrightarrow{t_2}\cdots \xrightarrow{t_n} s_n, \text{ with }  \forall i \;t_i = (s_{i-1}, e_i, s_i) \in T
      \end{align*}
\end{definition}


\TODO{TGTS for us, as delta can be used, but not necessary}

\begin{definition}[GTS]\label{def:GTS}
  A GTS is a tuple $\langle V,E,T, A, \nu \rangle $ where:
  \begin{itemize}
  \item $V$ is a set of variables, divided in two sets of variables: the set $S$ of \emph{state variables}, and $F$ of \emph{flow variables} s.t. $V = S \cup F.$
  \item $E$ is a set of event symbols
    \item $T$ is  a set of transitions, s.t. $t \equiv (\gamma, e, \varphi) \in T$ with $e \in E$, $\gamma$ and $\varphi$ are Boolean  expressions built over $V$ called \emph{guard} and \emph{post-condition} resp. A transition $t$ applies in a state $s \in 2^{|V|}$ s.t. $s \models \gamma$, resulting in a state $s' \models \varphi$.
    \item $A$ is the set of \emph{assertions}, i.e.  Boolean expressions built over $V$. Assertions are concatenated to each transition, in order to update flow variables, \TODO{modelling the failure propagation. }
    \item $\nu$ is the initial assignment of variables of $V$.
  \end{itemize}
  \end{definition}

\TODO{1) define the semantics of a transition, i.e. how to pass from a state $\sigma$ to a state $\rho$. 2) define a trace in the timed graph, with events labelled by the firing time, i.e. a plan for Tina}

A GTS is a (possibly infinite) graph $\Gamma = (\Sigma, \Theta)$, where $\Sigma$ is a set of nodes given by all the possible variable assignments in $V$, and $\Theta$ is a set of guarded transitions $(\sigma, e, \rho)$, where $\sigma, \rho \in \Sigma$ and $e \in E$.

blocks and processes, from the GTS to the Petri Net (states, places, tokens).

\begin{definition}[Temporal GTS]\label{TTGTS}
\TODO{Timed GTS already exist, we can use another name to avoid confusion}
A Temporal Guarded Transition System is a tuple $\langle V,E,T, A,\nu, \Delta \rangle$ where
  \begin{itemize}
  \item $\langle V,E,T, A, \nu \rangle $ is a GTS defined as in Def.~\ref{def:GTS}
  \item $\Delta$ is a delay function s.t. $\Delta: E \to \mathbb{R}^+ \times \mathbb{R}^+$, assigning an initial and a final firing time to the transitions bound to event $e$.
  \end{itemize}
\end{definition}


\TODO{Next paragraph is possibly untrue, as TGTS can be modified such to include delay \emph{functions} as we did with Fiacre and Petri Nets. We can say that these delays are instantaneous, when we aim at timed guards}
However, the limitation of the GTS formalism resides in the lack of expressivity wrt the delays in failure propagation.
In timed Guarded Transition Systems -- an extension of GTSs -- a delay function is associated to each event, indicating the date when the event occurs. However,  the propagation of messages, as failures, dealt by assertions, are not included in the (state) transitions that are delayed.

in the case of flow variables, they are updated in AltaRica simultaneously, as they represent the instantaneous propagation of a message in a system. Here, adding delays in such transitions, cannot be directly done within the AltaRica models, so we had to hack it.
We introduced \say{delay buffers}, which, in the AltaRica modelling, have a flow variable as input, a delayed state transition, and an output, which value depends on the state variable, which has been updated only after a delay. See Fig.~\ref{fig:delay-buffer}



The extension to temporal guards on the transitions expressed by the ETGTS falls out of the AltaRica expressiveness, so cannot be captured nor analysed by its associated tool, which can treat time as a set of delay assignment, i.e. with a fixed delay associated to each transition.
% Thus, the aforedefined Extended Temporal GTS is obtained from the AltaRica DataFlow model, by enriching it the syntax for temporal guarded transitions, i.e. by adding delays as defined in Def.~\ref{def:ETGTS} to the transitions in a new event law.
\end{comment}

\subsection{Factored model of ETGTS}
Representing the whole state space can be costly. For this reason, instead of describing the ETGTS as a state space, it is preferable to define a factored version of
the ETGTS, and describing the associated semantics.

AltaRica separates flow variables and state variables.
% State variables are modified by transitions, i.e. explicit changes of system configuration.
%
Delayed transitions affecting state variables are trivially extended to include a temporal interval in the guard matching the non-deterministic delay we plan to add. Flow variables are updated by assertions in AltaRica models, but this distinction between variables  does not appear in the associated  GTS; thus, in order to assign delays assertions, a auxiliary state variables and transitions are used to create a (delayed) state transition.

Let be $V$ a finite set of variable, possible multi-valued, and let be $\sigma$ the function that associates to each variable its finite domain.  
Thus, a variable assignment is here a function $f: V \to \sigma(v)$ for $v \in V$, associating to each $v \in V$ its value $f(v)$.
A state in $S$ is then a  assignment of all variables $v \in V$. As syntactic sugar, we can express the evaluation of an expression $\epsilon$ over $V$
in a state $s$ by considering $s(\epsilon)$.

\begin{definition}[Factored ETGTS]\label{def:factored-ETGTS}
  A GTS is a tuple $\langle V, O, I, \Delta\rangle $ where:
  \begin{itemize}
  \item $V$ is a set of variables, possibly multivalued, divided in two sets of variables: the set $St$ of \emph{state variables}, and $Fl$ of \emph{flow variables} s.t. $V = St \cup Fl.$
  \item $O$ is  a finite set of operators, where each operator consists in
    \begin{itemize}
    \item a Boolean  expressions $\Gamma$ built over $V$ called \emph{guard};
    \item a  \emph{post-condition} instruction,  a partial variable assignments $\P$. Post-conditions where the left members of the assignment are only state variables are referred as \emph{transitions}. Post-conditions where the left members of the assignment are only flow variables are referred as \emph{assertions}. 
      \end{itemize}
  \item $I$ is the initial assignment of variables of $V$.
  \item $\Delta$ is a delay function s.t. $\Delta: O \to \mathbb{R}^+ \times \mathbb{R}^+$, assigning an initial and a final firing time to the operators. We consider that, when not defined, the effects of the operators are instantaneous.

  \end{itemize}
  \end{definition}

We say that an operator $<\Gamma, P>$ is fireable in a state $s$ when the guard holds in $s$, i.e.
the variable assignment in $s$ is such that $s \models \Gamma$.
Assertions are concatenated to each transition, in order to update flow variables.
Thus, applying an operator in a state $s$ leads to a new state $s'$, obtained by applying first $P$ then the assertions to the variables in $s$ . % P(s)

\subsubsection{Semantics of a ETGTS}


The semantics of a Temporal Extended GTS, associated to the above definition  is a Kripke structure $\langle S, S_0, \to \rangle$ defining an oriented graph,  where edges are labelled by the events, and their associated delays.

\begin{definition}[Semantics of ETGTS]\label{def:ETGTS}
  An Extended  Timed Guarded Transition System is a tuple $\langle S, s_0, E, T, \tau \rangle $ where:
  \begin{itemize}
  \item $\mathcal{S} = S \cup \mathbb{R}_0^+$ is a set of states;
  \item $\mathcal{S} _0 = s_0 \cup \{0\} \in S$ is the initial state;
  \item $E$ is a set of event symbols;
  \item $\tau$ is the delay relation, $\tau: E \to \mathbb{R}^+_0 \times \mathbb{R}^+_0$, assigning a minimal and a maximal delay to the transitions bound to event $e$.
  \item $\mathcal{T}$ is  a set of transitions s.t. $\mathcal{T} \subseteq \mathcal{S} \times E \times \mathcal{S}$. For sake of simplicity, we consider two different kinds of transitions that can be associated to an event $e$:
    \begin{itemize}
    \item  transitions $s \xrightarrow{t} s'$, associating to a state $<s,  \theta>$ a new state $<s', \theta>$, whith $t = (s, e, s')$
    \item timed transitions $s \xrightarrow{\theta} s'$, associating to a state $<s,  \theta>$ a new state $<s, \theta + \delta>$, whith $\delta \in \tau(e)$
    \end{itemize}
  \end{itemize}
%  A transition $t \in T: (s, e, s')$ associates a state $s'$, to a state $s$ by executing the event $e$ in $s$, after a delay in the interval $[\delta_{min}, \delta_{max}]$ given by $\tau(e)$,
%  such that $t = (s, e, s')$ and $$
      
    A \emph{firing schedule}  $\rho$ of a timed Transition System is a sequence of pairs event-time from the initial state $s_0$:
    \begin{align*}
      \rho &= \{ (e_1,\delta_1), \ldots, (e_n,\delta_n)  \} \; 
      \text{s.t. } \forall i \;\delta_i \in \tau(e_i), \text{ and }\\
      &s_0 \xrightarrow{t_1} s_1 \xrightarrow{t_2}\cdots \xrightarrow{t_n} s_n, \text{ with }  \forall i \;t_i = (s_{i-1}, e_i, s_i) \in T
      \end{align*}
\end{definition}
\subsubsection{Translation}

The states are of the form of $<s, \theta>$, where $s \in S$ is a total assignment and $s_0$ is the initial assignment of variables in $V$;
$\theta$ is a real positive number.
Thus, transitions associate to pair $<s, \theta>$ other pairs  $<s', \theta'>$. % a transition $t in T$ 


The translation from the ETGTS to an TPN is straightforward.

A state in the  ETGTS represents the marking of the TPN, so
we can associate to each variable assignment in a state of the ETGTS, tokens in a state of the TPN,
with the initial state $\mathcal{S} _0$ defining the initial markup $M_0$.
The set of events $\{e | e \in E\}$ are mapped in the set of transitions $\{t_e \in T| e \in E\}$ in the TPN,
with an arc $(s, e, s')$ corresponding to % $\{p' | v_p \in s \text{ and } F(p, t_e) \neq 0\}$,
the marking $M'$ resulting from the set of markings obtained by applying  the transition $t_e$ to the set all the places with a not null token that activate the transition (i.e. $M$).
Wrt to the timed transitions
the firing interval $I'$ after a transition $t_e$ is obtained from the set of transitions in ETGTS that are fireable at $\theta'$ ( the timing obtained in the ETGTS after applying $e$ in  $<s, \theta>$)
such that $I' = \{\tau(t_e)\: | \: \theta' \in \tau(t_e) \}$.

Such transitions affect state variables only, while flow variables are updated simultaneously only if are kept, possibly adding them a delay.\TODO{ (dessin de la fleur)}

It is easy to see that the translated ETGTS is made of a single place and $n$ transitions, where $n$ corresponds to the number of state transitions in the initial model. We can ask ourselves if there is a more compact alternative to such a ``monolithic'' Petri Net. By enumerating the states in the model, we could create a ``stateful'' Petri net with a place for each reachable state, with the relative transitions. Another alternative for our translated model, would be to use a ``concurrent'' model, using different blocks for the different AltaRica nodes.

In the worst case scenario, the number of transitions of the monolithic Petri net would be equal to the possible variable assignment;
when considering Boolean variables only, the possible truth values assignment to $k$ variables would be $2^k$.
On the other side, if we consider the stateful model, we would end up, in the worst case, with $2^k$ places and the same amount of transitions.
Using the concurrent Petri net, we could obtain $n2k$ places (with $n$ the number of AltaRica nodes) which, in the worst case, would end up with $n2^k$ transitions and states. This worst case analysis yields to the fact that the simple monolithic Petri net is the more compact way to represent the original AltaRica model.


%%%% Comment on how do we create a buffered block to transmit faults
\begin{comment}

% It is easy to see from Def.~\ref{def:ETGTS} and Def.~\ref{def:PN} that any Petri Net can be modelled as a GTS~\cite{rau08}. % Any GTS in Petri Net?



While transitions affecting the state variables updates support a direct expression of the delay in AltaRica (and hence in ETGTS as well), flow variables are updated by assertions, that natively do not support delays. To express a delayed failure affecting an input/output variable (a flow variable) auxiliary state variables and transitions have to be used to model the delay and the failure buffer. Thus, a delay element will depend on three parameters $(k, \delta_1, \delta_2)$, where $\delta_1$ and $\delta_2$ are indicate the minimal and the maximal delay (resp.), and $k$ indicates the maximal buffer for the element.

\TODO{Following example is useless, as it has been explained clearly in the former sentence}
\subsubsection{Example}
Given a failure propagation represented by a flow variable $v$ as input $v_i$ of an element, the assertion $a$ updating these values would be such that $v_i = v$. To introduce a  delay between $d_e$ and $d_e'$, we add to the AltaRica model two auxiliary state variables $w, w'$, and two new events $e$ and $e'$.
The event $e$ is instantaneous s.t. $\Delta(e_d) = (d_e, d_e')$, and the resulting transition assigns $w = v$.
The event $e_d$ is delayed s.t. $\Delta(e_d) = (d_e, d_e')$, and the resulting transition assigns $w' = w$.
The following assignments are added as assertions: $a': w' = w$, $a'': v_i = w'$. The result is delay of a value comprised in the interval $[d_e, d_e']$ between the assignment $w = v$, and the propagation to change the value of $v_i$.

In OCAS, to produce such a model, N delay elements has to be created, with N the size of the buffer. This is automatised in our tool-chain, as the code corresponding to the delay element for $(k, \delta_1, \delta_2)$ is generated in Fiacre from the AltaRica code (where only the delay is indicated, while the buffer size $k$ is calculated from the elements uphill.
% NB: We can say that if the value v is new, THEN we update w. but can be more confusing.

\subsection{From Timed GTS to Timed Petri Nets}
\TODO{1) Get definition of timed Petri Nets, 2) define the translation\\}
We build a state $s_0$, s.t. for each transition $t \in T$ in the TGTS, a transition $t \circ a$ from $s_0$ to $s_0$ is added in the TPN. Eventual delays are maintained.
It is easy to see that such transitions affect state variables only, while flow variables are updated simultaneously only if are kept, possibly adding them a delay. (dessin de la fleur)


For each delayed transition affecting a flow variable, e.g. a delay in the failure propagation in our example, we add a new element working as a buffer delaying the input messages.


Introducing the delay, synchronisation, and new states
1) first in OCAS;
2) AltaRica code generated with timed transitions;
3) Fiacre code, with temporal guards (from the timed transitions expressed before).

Equivalence between the AltaRica models with no stochastic information, i.e. in Fiacre probabilities are abstracted away. Trivial to see that, when guards on transitions are conserved. Then, the time information is not part of the AltaRica models, and has there been artificially introduced for our purpose of taking trace of it during the translation. (taking trace of the transition names, for traceability purpose).


\end{comment}
%%% end comment


\section{Command line}

Sources du projet disponibles sur (C++):

\url{http://git-ingequip.pf.irt-aese.local/diffusion/TALTARICA/}

Benchmarks (utilisés entre autre pour l'article IMBSA 2017):

\url{http://git-ingequip.pf.irt-aese.local/diffusion/TALTARICA/browse/master/altarica\_epoch/benchmarks/models/}


In the IRT repository, we have:

v.1.0-erts18  The version used for ERTS.
 
v.1.1  Current version. Some bugs corrected

Known bugs of v.1.0-erts18 

Error in printing the guards of synchronized transitions: adds and 'and' at the end of the line when there are empty guards)
Duplicated syncronizations events


to compile :
/usr/bin/make KCFLAGS=-ggdb3 -Wdeprecated-declarations epochnogui

to execute:

 ./src/console/epochnogui --ds 0 --ps 0 --file <filename.alt> > <filename.fcr>

%%  LocalWords:  TGTS Fiacre Dataflow OCAS ETGTS
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: