\documentclass[12pt]{article} \usepackage[spanish]{babel} \usepackage[latin1]{inputenc} \usepackage{stmaryrd} \usepackage[usenames,dvipsnames]{color} \usepackage{amssymb} \usepackage{amsxtra} \usepackage{amsmath} \usepackage{amstext} \usepackage{amsthm} \usepackage{amsbsy} \usepackage{latexsym} \usepackage{mathrsfs} \usepackage{eucal} \usepackage{alltt} \usepackage{listings} \theoremstyle{definition} \newtheorem{definition}{Definici\'on}[section] \newtheorem{proposition}{Proposici\'on}[section] \newtheorem{lemma}{Lema}[section] \newtheorem{theorem}{Teorema}[section] \newtheorem{corollary}{Corolario}[section] \newtheorem{example}{Ejemplo}[section] \newtheorem{observation}{Observaci\'on}[section] \newtheorem{problem}{Problema}[section] \newtheorem{question}{Pregunta}[section] \newtheorem{pml}{Código Promela}[section] \def\proof{\noindent{\textbf{Demostraci\'on}}\\} \def\endproof{\hfill{\ensuremath\square}} \def\refname{Referencias} \def\abstractname{Resumen} \title{Código Promela \\ en \LaTeX \\ Métodos Formales \\ Otoño 2012 \\ Sección 101} \author{José de Jesús Lavalle Martínez} \begin{document} \maketitle \begin{abstract} Este documento sirve para aprender a escribir código Promela en \LaTeX. \end{abstract} En general siempre hay al menos tres maneras de presentar en \LaTeX\, código de lenguajes de programación, la primera es usar el ambiente \verb+verbatim+, la segunda usando el ambiente \verb+alltt+, para la tercera se debe usar el ambiente \verb+lstlisting+. \section{verbatim} En la primera manera se escribe el código entre \verb+\begin{verbatim}+ y \verb+\end{verbatim}+, note que en este ambiente \LaTeX\ no interpreta los comandos, no se necesita incluir algún paquete, así obtendrá: \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+verbatim+. \begin{verbatim} /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("%d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{verbatim} \end{pml} \section{alltt} En la segunda manera se escribe el código entre \verb+\begin{alltt}+ y \verb+\end{alltt}+, note que en este ambiente \LaTeX\ sí interpreta los comandos, necesita poner en el preámbulo \verb+\usepackage{alltt}+, para obtener: \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \texttt{alltt}. \begin{alltt} /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n ", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{alltt} \end{pml} \section{lstlisting} La tercera forma es escribiendo el código entre \verb+\begin{lstlisting}+ y \verb+\end{lstlisting}+ con opción \verb+[language=Promela]+, en este ambiente tampoco se interpretan los comandos, lo único que hace el paquete es formatear el código de acuerdo al lenguaje seleccionado y poner en negras las palabras reservadas del lenguaje, ponga en el preámbulo \verb+\usepackage{listings}+. \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+. \begin{lstlisting}[language=Promela] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("\% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} Observe que las líneas largas se salen del margen derecho de la hoja. Ponga el código entre \verb+\begin{lstlisting}+ y \verb+\end{lstlisting}+ con opción \verb+[language=Promela,numbers=left,breaklines=true]+ si quiere que el paquete \verb+listings+ numere las líneas de código y parta automáticamente las líneas muy grandes, obtendrá: \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas y ruptura automática de líneas largas. \begin{lstlisting}[language=Promela, numbers=left, breaklines=true] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} Si además quiere encerrar el código en una caja sombreada agregue la opción \verb+frame=shadowbox+. \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas y caja sombreada. \begin{lstlisting}[language=Promela, numbers=left, breaklines=true,frame=shadowbox] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} Como puede observar en la línea 27 se imprimen mal los carácteres de formato, para solucionarlo utilizamos la opción \verb+escapeinside=`'+ para que lo que encerremos entre estos dos carácteres sea interpretado por \LaTeX, es decir \verb+"`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'"+. \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas y carácteres interpretados por \LaTeX. \begin{lstlisting}[language=Promela, numbers=left, breaklines=true,escapeinside=`'] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} Lo malo es que al habilitar a \LaTeX\, para que interprete el código, el paquete \verb+listings+ pierde el control, si ahora ponemos el código en una caja el paquete se equivoca al pintarla, obtenemos: \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas, carácteres especiales interpretados por \LaTeX\, y caja sombreada. \begin{lstlisting}[language=Promela, numbers=left, breaklines=true,escapeinside=`',frame=shadowbox] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} Como no se puede tener todo, debemos tomar una decisión, es decir, si queremos la caja deshabilitamos la ruputura automática de líneas, nosotros partimos las líneas, para obtener: \begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura manual de líneas largas, carácteres especiales interpretados por \LaTeX\, y caja sombreada. \begin{lstlisting}[language=Promela, numbers=left, breaklines=false,escapeinside=`',frame=shadowbox] /* Copyright 2007 by Moti Ben-Ari under the GNU GPL; see readme.txt */ active proctype P() { int dividend = 15, divisor = 4; int quotient = 0, remainder = 0; int n = dividend; assert (dividend >= 0 && divisor > 0); do :: n != 0 -> assert(dividend == quotient * divisor + remainder + n); assert(0 <= remainder && remainder < divisor); if :: remainder + 1 == divisor -> quotient++; remainder = 0 :: else -> remainder++ fi; n-- :: else -> break od; printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", dividend, divisor, quotient, remainder); assert (dividend == quotient * divisor + remainder); assert (0 <= remainder && remainder < divisor); } \end{lstlisting} \end{pml} \end{document}