RSL specifications within L^ATEX files

RSL specifications can also be written directly within a L^ATEX document. This is convenient if you e.g. want to include fractions of a specification within the ordinary text of an article or a report.

RSL formulae within a L^ATEX file should be written between \RSLatex and \endRSLatex, e.g.:

\documentclass{article}
\usepackage{rslenv}
\begin{document}
\RSLatex
  scheme COUNTER =
    class
      variable counter : Nat := 0
      value increase : Unit -> write counter Nat
      axiom increase() is counter := counter + 1 ; counter
    end
\endRSLatex
\end{document}

By pressing key F2 from within emacs, the RSL formulae in ascii-format are converted into L^ATEX-format:

\documentclass{article}
\usepackage{rslenv}
\begin{document}
%\RSLatex
%  scheme COUNTER =
%    class
%      variable counter : Nat := 0
%      value increase : Unit -> write counter Nat
%      axiom increase() is counter := counter + 1 ; counter
%    end
%\endRSLatex
\bp
\>\kw{scheme} COUNTER {\EQ}\\
\>\>\kw{class}\\
\>\>\>\kw{variable} counter : \kw{Nat} :{\EQ} 0\\
\>\>\>\kw{value} increase : \kw{Unit} {\RIGHTARROW} \kw{write} counter \kw{Nat}\\
\>\>\>\kw{axiom} increase() {\IS} counter :{\EQ} counter {\PLUS} 1 ; counter\\
\>\>\kw{end}
\ep
\end{document}

The file can now be converted to PostScript format as described in section 5.2.

By pressing the key F3, the L^ATEX-formatted formulae are converted back to the original ascii-format.

Notice that you may need to change some of the spacing in your ascii formulae to make it appear nicely in the final PostScript file -- indentation has to be done by inserting blank spaces.