\documentclass[11pt,a4paper]{article}
\usepackage{color}
\usepackage[utf8]{inputenc}
\usepackage[ruled,linesnumbered]{algorithm2e}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage[english]{babel}
\usepackage{url}
\usepackage{supertabular}
\usepackage{multirow}
\usepackage{booktabs}
\usepackage{ae,aecompl,aeguill}   % meilleur rendu que T1 fontenc
\usepackage{subfigure}

% dimensions de page (reglages probablement non optimaux...)
\evensidemargin=0cm
\oddsidemargin=0cm
\topmargin=-1.5cm
\textheight=25cm
\leftmargin=0cm
\textwidth=19cm
\sloppy
\flushbottom
\parindent 1em
\hoffset -0.5in
\oddsidemargin  0pt
\evensidemargin 0pt
\marginparsep   10pt
\RequirePackage{geometry}
\geometry{reset,
  papersize={210mm,297mm},
  text={180mm,260mm},
  headheight=50pt,
  headsep=10pt,
  hoffset=0cm,
  voffset=0cm,
}

\graphicspath{{fig/}}
\newcommand{\TODO}[1] {\par\textcolor{red}{TODO : #1}\par}
\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}

\begin{document}
% entête
\thispagestyle{empty}

\title{Experiments with the Huffman Decoder/Encoder\\
(VIS bench)
}
\date{\today}
\author{Cécile Braunstein}
\maketitle

\section{Original platform from VIS}
\subsection{Model architecture}
\begin{figure}[h]
\centering
\includegraphics[]{ArchGeneral}
\caption{\label{fig:huff_original_arch} Architecture of Huffman original}
\end{figure}
\begin{figure}[h]
\centering
\subfigure[Encoder automaton]{
\includegraphics[]{encoder_aut}
\label{fig:huff_original_encod}
}
\subfigure[Decoder automaton]{
\includegraphics[]{decoder_aut}
\label{fig:huff_original_decod}
}
\end{figure}
The Huffman circuit describes the implementation of static (English) Huffman
encoder/decoder.
\begin{itemize}
\item Encoder: Read a character and return the encoding form bit by bit
\item Decoder: Explore the encoding tree and return the character when it
reaches a leaf.
\end{itemize}


\subsection{Robustness Analysis}
The robustness analysis has been performed for usut and msmt faults only. The
set of safe states for robustness 4 is the reach set of states.
\begin{table}[htbp]
\input{./experiments/huff_original_res_small}
\caption{Robustness of the Huffman circuit from the VIS
bench\label{table:orig_vis}}
\end{table}
The table \ref{table:orig_vis} shows the robustness analysis of the original
circuit in VIS bench.
There exists $eds$ from where the circuits will never recover.
After analyzing these path (by producing counterexample),
we were able to avoid them path by modifying the encoder automaton. The case
were {\tt shiftreg} equals 0 is not taken into account on this automaton.
This can be solved by replacing the guard transition from SHIFT to INIT.

From this point, we will considered only this modified version of the Huffman
circuit.
\begin{table}[htbp]
\input{experiments/huff_my_orig}
\caption{Robustness of the corrected Huffman circuit  from the VIS
bench\label{table:orig_cor}}
\end{table}

\begin{table}[htbp]

\input{experiments/huff_grade2}
\caption{Register grading of the corrected Huffman circuit from the VIS
bench\label{table:grade_cor}}
\end{table}

This circuit is not completely robust due to the desynchronization between the
encoder and the decoder machine. The fault may have change the code of
character in the encoder while the decoder where decoding it.
The original circuit does not have a mechanism to prevent such
desynchronization such as handshake protocol.

\section{Huffman decoder/encoder synchronization}
We synchronized the behavior of the decoder and the encoder device.
The decoder starts only when the encoder said so. The encoder may restarts the
decoder even when the decoding part is not over.

This mechanism ensure the robustness level 4 with the set of reachable states
considered as safe states. Nevertheless this does not ensure the
synchronization with the golden behavior.
The non-robustness 3 comes from  the fact that the environment does not have
constraints. Moreover, it comes also from the lack of synchronization between the
environment and the model under test.

\begin{figure}[htbp]
\centering
\subfigure[Encoder automaton]{
\includegraphics[scale=1]{encoder_synchro}
\label{fig:huff_synchro_encod}
}
\subfigure[Decoder automaton]{
\includegraphics[scale=1]{decoder_synchro}
\label{fig:huff_synchro_decod}
}
\end{figure}
\begin{table}[htbp]
\input{experiments/huff_synchro}
\caption{Robustness Huffman circuit with internal
synchronization\label{table:rob_synchro}}
\end{table}

\begin{table}[htbp]

\input{experiments/huff_grade_synchro}
\caption{Register grading Huffman circuit with internal
synchronization\label{table:grade_synchro}}
\end{table}

\section{Huffman with a constraint environment}
\subsection{Environment: a given text}
We build an environment synchronized with the encoder. The environment send
the letter A and E alternatively when it received the acknowledgment from the
encoder saying that the character code is sent.

\begin{figure}[htbp]
\centering
\subfigure[Environment]{
\includegraphics[scale=1]{environment}
\label{fig:environment}
}
\subfigure[New Encoder]{
\includegraphics[scale=1]{encoder_with_env}
\label{fig:encod_with_env}
}
\end{figure}

We perform a robustness analysis with a new rob3~:\\
The faulty and the golden have got the same inputs from the environment. The
environment only reacts to the outputs from the faulty circuits.

The set of safe states are the ones where the golden and the faulty states are
observably equivalent.

\input{experiments/huff_with_env}

Self stabilized after 10 steps, there is not healthy states before.
Just checking the \verb+AX:9 AG (golendOut == faultyOut) +
\verb+and  AX:10 AG (golendOut == faultyOut)+

\subsection{Synchronized with the decoder}
Our goal is to model the basis functionnalities that an environment should at
least have.
In this experiments any character may be encode. The environment is waiting
that the encoder is ready to take a letter (\verb+ack = 1+) and send a letter in a non
deterministic time (free input \verb+i_val+).
This modeling implies that we need to add
fairness constraints to avoid the infinite path where the environment never
asks for a new encoding.
\begin{figure}[htbp]
\centering
\includegraphics[scale=1]{env_start}
\label{fig:environment_nd}
\caption{Less constraint environment}

\end{figure}
\begin{table}[htbp]

\input{experiments/huff_basic_env}
\caption{Robustness with any text environment\label{table:basic_env}}
\end{table}


\subsection{Separate study for decoder and encoder}
The encoder is completely robust (rob3 and rob4) under the fairness constraint
that the environment should ask for a new computation from time to time.

The decoder has got the same characteristic. It is robust iff his environment
always need a new computation.
The encoder verifies this property \verb+(AG(AF(start = 1)))+, hence the
composition of the decoder and encoder is 100\% robust.
\end{document}