LaTeX listings of PRISM models

617 views
Skip to first unread message

wouter...@gmail.com

unread,
Mar 12, 2009, 6:40:35 AM3/12/09
to PRISM model checker
Hello,

I am also trying to get a nice latex formatted PRISM model. I managed
to do that by following your instructions about the shell script on
this forum.

However, if I copy-past the generated content into my PRISM chapter,
an error is reported about the last closing curly bracket. Should I
just remove it? I already included the commands in prism.tex.

Moreover, the latex model is not very neat: just normal font instead
of
(for example) sans serif or courier, no color coding and lines are way
to long (but the latter is something I can change in the original
model, so no problem)...

Is there yet another way to retrieve nice PRISM code listings for
latex? Or how can I improve this output?

Thnx in advance for your time.

Wouter


On 1 jul 2008, 17:20, Dave Parker <david.par...@comlab.ox.ac.uk>
wrote:
Hi Peter,

I haven't tried embedding PRISM code directly in this fashion, but
there
is a (hidden) PRISM-to-latexconverter in PRISM you could have a look
at. If you're on Linux/Mac, use this script:

-----------
#!/bin/sh
PRISM_MAINCLASS="parser.PrismSyntaxHighlighterlatex"
export PRISM_MAINCLASS
prism "$@"
-----------

Make sure that prism is in your path and then do "prism2latex
mycode.pm
> mycode.tex". You'll also need the macros in prism.tex which is in the
etc directory of the PRISM distribution.

Let me know if you have any problems.

Dave.

Dave Parker

unread,
Mar 12, 2009, 9:12:25 AM3/12/09
to prismmod...@googlegroups.com
Hi Wouter,

> However, if I copy-past the generated content into my PRISM chapter,
> an error is reported about the last closing curly bracket. Should I
> just remove it? I already included the commands in prism.tex.

I have not encountered this problem before. Perhaps it is a bug which
occurs on the model you are using. If you email me your file, I can look
into it.

> Moreover, the latex model is not very neat: just normal font instead
> of
> (for example) sans serif or courier, no color coding and lines are way
> to long (but the latter is something I can change in the original
> model, so no problem)...
>
> Is there yet another way to retrieve nice PRISM code listings for
> latex? Or how can I improve this output?

The generated formatting for Latex is not as neat as for HTML. I think
there have been a few small improvements so it might be worth checking
you are running the latest version of PRISM (i.e. the development
version) but this will not fix all of your problems.

The Latex generation code in PRISM is quite simple, so if you know Java,
you are welcome to try and improve it. I can point you towards the
relevant file. It depends how much code you have as to whether it is
worth your while.

I don't know of any other options, apart from coding it by hand, I'm afraid.

Cheers,

Dave.

wouter...@gmail.com

unread,
Apr 5, 2009, 8:59:26 AM4/5/09
to PRISM model checker
Hello,

I did it the following way, using the latex listings package. It is
much more flexible than the way described here.
Please, post improvements, if any!



%% PRISM CODE LISTING *********************************************

\definecolor{prismgreen}{rgb}{0, 0.6, 0}

\lstdefinelanguage{Prism}{ % syntax highlight via font
basicstyle=\color{red}\tiny\ttfamily, % small true type font (like
courier)
keywords=
{bool,C,ceil,const,ctmc,double,dtmc,endinit,endmodule,endrewards,

endsystem,F,false,floor,formula,G,global,I,init,int,label,max,mdp,min,

module,nondeterministic,P,Pmin,Pmax,prob,probabilistic,R,rate,rewards,
Rmin,Rmax,S,stochastic,system,true,U,X},
keywordstyle={\bfseries\color{black}},
numberstyle=\tiny\color{black},
comment=[l] {//}, morecomment=[s]{/*}{*/}, % single and multi-line
commentstyle= \color{prismgreen}, % dark green
tabsize=4, % tab treatment (going to be fixed in Prism)
captionpos=b, % put captions at the bottom
escapechar=@ % write LaTeX comments escaped by @ symbol
}

%define command \prism with one argument for inline printing of \prism
code
\newcommand{\prism}[1]{\lstinline[language=Prism,basicstyle=\small
\ttfamily]|#1|}

%% END PRISM CODE LISTING
*********************************************

Now use for instance this to create a listing of a PRISM model, where
the model is contained in file "modelv704.nm":

\lstinputlisting[float=ht!, language={Prism}, numbers=left,
frame=shadowbox,
rulesepcolor=\color{black}, rulecolor=\color{black}, breaklines=true,
breakatwhitespace=true, firstnumber=1, firstline=1, lastline=25,
caption={PRISM
Model V2},label={lst_prism_v2_prt1_app}]{models/modelv704.nm}
Reply all
Reply to author
Forward
0 new messages