Updated user and ref manuals (also added hyperlinks)

TODO.md

@@ -1,5 +1,6 @@
 COMPILER
 
+- LHS = LVAL
 - support for synchronous actions (allow `examples/full/single/pgcd:sim` for ex.)
 - allow shared signals with multiple writers in VHDL
 - allow arrays as parameters (ex: `fsm model fir <c: int array[3],...)`)
@@ -20,3 +21,4 @@ DIST
 - use Dune `install` stanza to install documentation, etcs and examples
 
 DOC
+- LHS = LVAL

docs/ref_manual/rfsm_rm.tex

@@ -20,7 +20,8 @@
 \usepackage{fixltx2e}
 \usepackage[multiple]{footmisc}
 \usepackage{grammar-defns}  %% Generated by Obelisk
-\usepackage{url}
+%\usepackage{url}
+\usepackage{hyperref}
 \usepackage{bcprules}
 
 \newsavebox{\FVerbBox}

docs/ref_manual/variants.tex

@@ -4,8 +4,8 @@ \chapter{ Building language variants}
 Following the approach described in~\cite{Leroy00} for example, the RFSM compiler is implemented in
 a \emph{modular} way. The language is split into a \emph{host} language, describing the general
 structure and behavior of FSMs (states, transitions, \ldots) and a \emph{guest}
-language\footnote{``Base'' in the terminology of \cite{Leroy00}.} describing the syntax and
-semantics of \emph{expressions} used in transition guards and semantics. 
+language\footnote{``Base language'' in the terminology of \cite{Leroy00}.} describing the syntax and
+semantics of \emph{expressions} used in transition guards and actions. 
 Technically, this ``separation of concern'' is realized by providing the host language in the form
 of a \emph{functor} taking as argument the module implementing the guest language.
 
@@ -75,7 +75,7 @@ \section{Implementing the \texttt{Guest} module}
 \end{itemize}
 
 Listings~\ref{lst:mini-types}, \ref{lst:mini-syntax},\ref{lst:mini-value} and \ref{lst:mini-eval}
-respectively show the contents of of the \texttt{Types},
+respectively show the contents of the \texttt{Types},
 \texttt{Syntax}, \texttt{Value} and \texttt{Eval} modules for the \texttt{mini} language.
 The definition of non essential fonctions has been omitted\footnote{See the corresponding source files in
   \texttt{src/guests/others/mini/lib} for a complete listing.}.
@@ -145,7 +145,7 @@ \section{Implementing the \texttt{Guest} module}
 let pp_lhs fmt l =  ...
 \end{lstlisting}
 
-The module \texttt{Syntax} use the modules \texttt{Location}, \texttt{Annot}  and \texttt{Ident}
+The module \texttt{Syntax} uses the modules \texttt{Location}, \texttt{Annot}  and \texttt{Ident}
 provided by the \texttt{Rfsm} host library. These modules provide types and functions to handle
 source code locations, syntax annotations and identifiers respectively. The type
 \verb|('a,Types.typ) Annot.t| is associated to syntax nodes of type
@@ -193,7 +193,7 @@ \section{Implementing the \texttt{Guest} module}
 let pp fmt (v: t) =  ...
 \end{lstlisting}
 
-The module \verb|Guest.Value| define the values, associated to guest-level expressions by the
+The module \verb|Guest.Value| defines the values, associated to guest-level expressions by the
 dynamic semantics. The value \verb|Val_unknown| is used to represent undefined or unitialized
 value. The functions \verb|vcd_type| and \verb|vcd_value| provide the interface to the VCD backend,
 generating simulation traces~: they should return a VCD compatible representation  (defined in the
@@ -234,12 +234,12 @@ \section{Implementing the \texttt{Guest} module}
 
 The module \verb|Guest.Eval| defines the guest-level dynamic semantics, \emph{i.e.} the definition
 of the dynamic environment \texttt{env}, used to bind identifiers to values and of the 
-functions \verb|eval_expr| and \verb|exal_bool| used to evaluate guest-level expressions. The
+functions \verb|eval_expr| and \verb|eval_bool| used to evaluate guest-level expressions. The
 presence of a distinct, \verb|eval_bool| function is required because the boolean type and
 expressions are not part of the host-level syntax. The definition of the \texttt{env} type here uses
-that provided by the host library but any definition matching the corresponding signature would do.
+that provided by the RFSM host library but any definition matching the corresponding signature would do.
 
-\section{Implementing the \texttt{Guest} parser}
+\section{Implementing the guest language parser}
 
 The parser for the guest language defines the concrete syntax for guest-level type expressions,
 expressions and LHS. It is written in a separate \texttt{.mly} file which will be combined with the
@@ -282,16 +282,16 @@ \section{Implementing the \texttt{Guest} parser}
 
 \end{lstlisting}
 
-\section{Implementing the \texttt{Guest} lexer}
+\section{Implementing the guest language lexer}
 
 The \texttt{ocamllex} tool, used for defining the lexer, does not support multi-file definitions.
 The lexer for the guest-specific part of the target language is therefore supplied in the form of
 code fragments to be inserted in the host lexer definition file\footnote{Technically, this insertion is
-  performed using the \texttt{cppo} tool.}. These fragments are listed in two separate files,
-present in the \texttt{bin} subdirectory of the guest directory~:
+  performed using the \texttt{cppo} tool.}. These fragments are listed in two separate files, which
+must be supplied in the \texttt{bin} subdirectory of the guest directory~:
 \begin{itemize}
-\item the file \texttt{guest_km} contains the lexer definition of the guest-specific keywords,
-\item the file \texttt{guest_rules} contains the guest-specific rules.
+\item the file \texttt{guest_kw.mll} contains the lexer definition of the guest-specific keywords,
+\item the file \texttt{guest_rules.mll} contains the guest-specific rules.
 \end{itemize}
 
 In the case of the \texttt{mini} language defined here, the latter is empty and the former only

docs/user_manual/ex1-systemc.tex

@@ -1,4 +1,4 @@
-\chapter*{Appendix A1 - Example of generated SystemC code}  
+\chapter*{Appendix A2 - Example of generated SystemC code}  
 \label{cha:ex1-systemc}
 
 This is the code generated from program given in Listing~\ref{lst:rfsm-gensig} by the SystemC

docs/user_manual/introduction.tex

@@ -5,15 +5,16 @@ \chapter{Introduction}
 
 \medskip
 RFSM is a domain specific language aimed at describing, drawing and simulating \emph{reactive finite state
-  machines}. Reactive FSMs are a FSMs for which transitions can only take place at the occurence of
-events.
+  machines}. Reactive FSMs are FSMs for which transitions can only take place at the occurence of
+\emph{events}.
 
 \medskip
-RFSM has been developed mainly for pedagogical purposes, in order to initiate students to
+RFSM has been developed mainly for pedagogical purposes, in order to initiate students into
 model-based design. It is currently used in courses dedicated to embedded system design both on
 software and hardware platforms (microcontrolers and FPGA resp.). But RFSM can also be used to
-generate code (C, SystemC or VHDL) from high-level models to be integrated to existing applications.
+generate code (C, SystemC or VHDL) from high-level models, to be integrated to existing applications.
 
+\medskip
 More precisely, RFSM can be used to
 \begin{itemize}
 \item describe FSM-based models and testbenches,

docs/user_manual/language.tex

@@ -8,18 +8,18 @@ \chapter{The RFSM language}
 \section{Programs}
 \label{sec:programs}
 
-A RSFM program contains declarations of six kinds~: 
+A RSFM program is made of successive sections, containing, respectively 
 \begin{itemize}
-\item \textbf{types}
-\item \textbf{constants}
-\item \textbf{functions}
-\item \textbf{FSM models}
-\item \textbf{global objects}
-\item \textbf{FSM instanciations}
+\item type declarations,
+\item constant declarations,
+\item function declarations,
+\item FSM model definitions,
+\item global object definitions,
+\item FSM instanciations.
 \end{itemize}
 
-These declarations may appear in any order in a given program but an object used in a given section must
-have been declared before. 
+Each section is optional\footnote{Though, obviously, a program with no model definition, and hence
+  no FSM instanciation, is of little interest.} but their must appear in the order given above.
 
 \section{FSM models}
 \label{sec:fsm-models}
@@ -230,18 +230,19 @@ \subsubsection*{Semantic issues}
 the action \verb|y:=x*2|. 
 
 This interpretation is the most intuitive one and naturally fits with software-based
-implementations. There's actually another interpretation in which actions are not performed sequentially but
-\emph{synchronously}. In this case, all the expressions appearing on the right-hand-side of
-assignations are fisrt evaluated \emph{in parallel} and then, and only then, all the assignations
-are performed. Because the values of the variables occuring in the RHS expressions are those 
-\emph{before} the transition, the order in which the actions are performed does not matter in this
-case. In the example above, the values assigned to \texttt{x} and \texttt{y} will be 2 and 2
-  respectively. This interpretation more naturally fits to \emph{hardware-based} implementations,
-in which variables are implemented as \emph{signals} all updated synchronously at each clock cycle. 
-Switching to a synchronous interpretation is possible by invoking the \texttt{rfsmc} compiler with the
-\texttt{-synchronous_actions} option. \textbf{Caveat}. This option is
-available when using the simulator and the VHDL backend but is
-currently not supported when using the C and SystemC backends.
+implementations.
+% There's actually another interpretation in which actions are not performed sequentially but
+% \emph{synchronously}. In this case, all the expressions appearing on the right-hand-side of
+% assignations are fisrt evaluated \emph{in parallel} and then, and only then, all the assignations
+% are performed. Because the values of the variables occuring in the RHS expressions are those 
+% \emph{before} the transition, the order in which the actions are performed does not matter in this
+% case. In the example above, the values assigned to \texttt{x} and \texttt{y} will be 2 and 2
+%   respectively. This interpretation more naturally fits to \emph{hardware-based} implementations,
+% in which variables are implemented as \emph{signals} all updated synchronously at each clock cycle. 
+% Switching to a synchronous interpretation is possible by invoking the \texttt{rfsmc} compiler with the
+% \verb|-synchronous_actions| option. \textbf{Caveat}. This option is
+% available when using the simulator and the VHDL backend but is
+% currently not supported when using the C and SystemC backends.
 
 \medskip
 \textbf{Non-determinism and priorities}. 
@@ -293,7 +294,7 @@ \subsubsection*{Semantic issues}
 sense, cheating, since the \texttt{StartStop} event is supposed to modelize user interaction which
 occur, by essence, at impredictible dates.
 
-The above problem can be solved by assigning a \emph{priority} to transitions. In the current
+The above problem can be solved by assigning \emph{priorities} to transitions. In the current
 implementation, this is achieved by tagging some transitions as ``high priority''
 transitions\footnote{Future versions may evolve towards a more sophisticated mechanism allowing
   numeric priorities.}.  When several transitions are enabled, if one is tagged as ``high priority''
@@ -338,8 +339,9 @@ \subsection{Initial transition}
 \framebox{\lstinline[language=Rfsm]{| -> init_state}}
 \end{center}
 
-\medskip
-\textbf{Note}. Output values can be set by either attaching them to states or by updating them on
+\subsection{Output values}
+
+Output values can be set by either attaching them to states or by updating them on
 transitions. For a given output \texttt{o}, attaching a value \texttt{v} to a state \texttt{S}, by writing
 
 \begin{center}
@@ -365,6 +367,7 @@ \section{Inputs and outputs}
 
 Interface to the external world are represented by \verb|input| and \verb|output| objects.
 
+\medskip
 \step For outputs the declaration simply gives a name and a type~:
 
 \begin{center}
@@ -435,6 +438,7 @@ \section{Shared objects}
 occurs when the system model involves several FSM instances and when the input of a given instance
 is provided by the output of another one.
 
+\medskip
 \step For shared objects the declaration simply gives a name and a type~:
 
 \begin{center}
@@ -456,17 +460,19 @@ \section{Shared objects}
 \subsection*{Semantic issues}
 
 \medskip
-Shared objects are typically used to perform some kind synchronisation between FSMs. The precise semantics
-of this synchronisation depends on the shared object. It is described formally in Appendix D.
+Shared objects are typically used to perform some kind synchronisation between FSMs. The precise semantic
+of this synchronisation depends on the shared object. We here describe it informally. A formal
+account is given the reference manual. 
 
 \subsubsection*{Synchronisation using a shared event}
 \label{sec:synchr-using-shar}
 
 Synchronisation using a shared event is both instantaneous and ephemeral.
 
+\medskip
 \textbf{Instantaneous} means that an event emitted by a FSM when taking a
 transition can trigger a reaction of another FSM at the same logical instant, the two reactions -- that of
-emitting FSM and that of the ``receiving'' FSM -- being simultaneous. 
+the ``emitting'' FSM and that of the ``receiving'' FSM -- being simultaneous. 
 This is illustrated in Fig.~\ref{fig:sync-ev1}. Here, each occurence of event \texttt{H} when
 \texttt{a1} is in state \texttt{A} triggers the simultaneous transition of \texttt{a2} from state
 \texttt{A} to state \texttt{B}.
@@ -588,7 +594,7 @@ \subsubsection*{Synchronisation using a shared event}
 backends.  The support of shared events in the SystemC backend, for example, is fragile and has not
 yet fully tested\footnote{It relies on the insertion of zero-time \texttt{wait} instructions.}. It
 is completely lacking in the VHDL backend (VHDL implementation of FSMs can only be triggered by a
-single, ``external'' \texttt{clock} signal).  Finally, the \emph{event} mechanism provided by most
+single, external, \texttt{clock} signal).  Finally, the \emph{event} mechanism provided by most
 of real-time operating systems (as abstracted by \verb|notify_ev()| and \verb|wait_ev()|
 pseudo-primitives used in the code generated by the C backend) may not obey the semantics provided
 here (most of OS-supported events are \emph{memorized} when they are not awaited for when emitted in
@@ -609,7 +615,7 @@ \subsubsection*{Synchronisation using shared variables}
 \begin{figure}[h]
   \centering
 \begin{tabular}[c]{cc}
-  \begin{minipage}[b]{0.3\linewidth}
+  \begin{minipage}[b]{0.4\linewidth}
   \begin{lstlisting}[language=Rfsm]
 fsm model A1(
   in h: event,
@@ -635,10 +641,10 @@ \subsubsection*{Synchronisation using shared variables}
 }
   \end{lstlisting}
   \end{minipage} &
-  \begin{minipage}[b]{0.7\linewidth}
+  \begin{minipage}[b]{0.6\linewidth}
 \begin{lstlisting}[language=Rfsm]
-input H : event = sporadic(10, 20, 30, 40)
-shared V : bool
+input H: event = sporadic(10,20,30,40)
+shared V: bool
 
 fsm a1 = A1(H,V)
 fsm a2 = A2(H,V)
@@ -652,18 +658,18 @@ \subsubsection*{Synchronisation using shared variables}
 \end{figure}
 
 \bigskip Because shared variables are, by definition, memorized, they can used to implement
-\emph{defered synchronisation}, \emph{i.e.} the situation where a FSM emits an event which be used
+\emph{defered synchronisation}, \emph{i.e.} the situation where a FSM emits an event which will be used
 \emph{later} by another FSM (shared events cannot be used in this case since, as described above,
 non-awaited events are not memorized and hence lost). This is illustrated in
 Fig.~\ref{fig:sync-sv2}. Here, \texttt{a1} set variable \texttt{v} to 1 when going from state
-\texttt{S1} to \texttt{S2} but \texttt{a2} only detect this when going from state \texttt{S2} to
+\texttt{S1} to \texttt{S2} but \texttt{a2} only detects this when going from state \texttt{S2} to
 \texttt{S3}, reseting the variable to 0 \emph{en passant}. In effect, \texttt{a1} has emitted a
 event which has been memorized and caught latter by \texttt{a2}.
 
 \begin{figure}[h]
   \centering
 \begin{tabular}[c]{cc}
-  \begin{minipage}[b]{0.3\linewidth}
+  \begin{minipage}[b]{0.4\linewidth}
   \begin{lstlisting}[language=Rfsm]
 fsm model A1(
   in h: event,
@@ -685,17 +691,18 @@ \subsubsection*{Synchronisation using shared variables}
   states: S1, S2, S3;
   trans:
   | S1 -> S2 on h
-  | S2 -> S3 on h when v=1 with v:=0
+  | S2 -> S3 on h when v=1
+                  with v:=0
   | S3 -> S1 on h;
   itrans:
   | -> S1 ;
 }
   \end{lstlisting}
   \end{minipage} &
-  \begin{minipage}[b]{0.7\linewidth}
+  \begin{minipage}[b]{0.6\linewidth}
 \begin{lstlisting}[language=Rfsm]
-input H : event = sporadic(10, 20, 30)
-shared v : bool
+input H: event = sporadic(10,20,30)
+shared v: bool
 
 fsm a1 = A1(H,v)
 fsm a2 = A2(H,v)
@@ -785,10 +792,10 @@ \section{FSM instances}
 For example, the last line of the program given in Listing~\ref{lst:rfsm-gensig}
 
 \begin{center}
-\example{\lstinline[language=Rfsm]'fsm g = gensig<4>(H,E,S)'}
+\example{\lstinline[language=Rfsm]'fsm g = gensig<3>(H,E,S)'}
 \end{center}
 
-creates an instance of model \verb|gensig| for which \verb|n=4| and whose inputs (resp. output) are
+creates an instance of model \verb|gensig| for which \verb|n=3| and whose inputs (resp. output) are
 connected to the global inputs (resp. output) \texttt{H} and \texttt{E} (resp. \texttt{S}).
 
 \medskip
@@ -817,9 +824,9 @@ \section{Constants}
 \noindent
 where
 \begin{itemize}
-\item \lstinline[language=Rfsm]|<type>| is the type of the defined constant (currently limited to
+\item \emph{type} is the type of the defined constant (currently limited to
   \verb|int|, \verb|bool|, \verb|char|, \verb|float| and arrays of such types,
-\item \lstinline[language=Rfsm]|<value>| is the value of the constant.
+\item \emph{value} is the value of the constant.
 \end{itemize}
 
 Global constants have a global scope and hence can be used in any FSM model or instance.
@@ -903,7 +910,7 @@ \section{Types and type declarations}
 \step Objects of type \texttt{bool} can have only two values : \texttt{0} (false) and \texttt{1} (true).
 
 \step Values of type \texttt{char} are
-denoted using single quotes. For example, for a variable \verb|c| having type \verb|char| :
+denoted using single quotes. For example, for a variable \verb|c| having type \verb|char|~:
 \begin{center}
   \example{\lstinline[language=Rfsm]|c := 'A'|}
 \end{center}
@@ -946,7 +953,7 @@ \section{Types and type declarations}
 syntax \verb|n[i]|, where \verb|n| is an integer is equivalent to \verb|n[i:i]|. The \emph{cast}
 operator (\verb|::|) can be used to combine integers with different sizes (for example, if \verb|n|
 has type \verb|int<16>| and \verb|m| has type \verb|int<8>|, writing \verb|n:=n+m| is not allowed
-and mus be written, instead, \verb|n:=n+m::int<16>|. Note that the
+and must be written, instead, \verb|n:=n+m::int<16>|. Note that the
 logical ``or'' operator is denoted ``\verb+||+'' because the single ``\verb+|+'' is already used in
 the syntax.
 
@@ -979,6 +986,7 @@ \section{Types and type declarations}
 \textbf{User defined types} are either \emph{type abbreviations}, \emph{enumerations} or
 \emph{records}.
 
+\medskip
 \step Type abbreviations are introduced with the following declaration
 \begin{center}
   \framebox{\lstinline[language=Rfsm]{type typename = type_expression}}