jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

User manual: first version

Browse source
This commit is contained in:
Gwenal Delaval 2012-06-14 23:07:40 +02:00
parent 502c5e446f
commit d36e988fb9
34 changed files with 47458 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

112
manual/Makefile Normal file
View file

@ -0,0 +1,112 @@
# -*- Makefile -*-
# LaTeX Makefile for dvi, ps, and pdf file creation.
# By Jeffrey Humpherys
# Written April 05, 2004
# Revised January 13, 2005
# Revised 2006
# Thanks Bjorn and Boris
LATEX=latex -src-specials
BIBTEX=bibtex
PDFLATEX=pdflatex
DVIPS=dvips -sPAPERSIZE=a4
PS2PDF=ps2pdf -sPAPERSIZE=a4
INTERMEDIATE_FILES=aux,log,bbl,blg,dvi,toc,lof,log,lot,out,cb,nav,snm,vrb
MAIN = $(shell grep -l documentclass ./*.tex)
SOURCES = $(wildcard ./*.tex)
FIGURES = $(wildcard ./figures/*.fig)
ANIMS = $(wildcard ./anim/*.anim)
TEXANIMS = $(patsubst %.anim,%.tex,$(ANIMS))
EPSFIGURES = $(patsubst %.fig,%.eps,$(FIGURES))
PDFFIGURES = $(patsubst %.fig,%.pdf,$(FIGURES))
PSORPDF=pdf
-include config
DVIS = $(patsubst %.tex,%.dvi,$(MAIN))
PDFS = $(patsubst %.tex,%.pdf,$(MAIN))
PSS = $(patsubst %.tex,%.ps,$(MAIN))
ifeq ($(PSORPDF),pdf)
PSORPDFFIGURES=$(PDFFIGURES)
else
PSORPDFFIGURES=$(EPSFIGURES)
endif
ifeq ($(PSORPDF),pdf)
all: pdf
else
all: dvi
endif
dvi: $(DVIS)
pdf: $(PDFS)
ps: $(PSS)
figures: $(PSORPDFFIGURES)
anim: $(TEXANIMS)
%.dvi: %.tex $(SOURCES) $(EPSFIGURES) $(TEXANIMS)
$(LATEX) $*
@while ( grep "Rerun to get cross-references" \
$*.log > /dev/null ); do \
echo '** Re-running LaTeX **'; \
$(LATEX) $*; \
done
ifeq ($(PSORPDF),pdf)
$(PDFS) : $(SOURCES) $(PDFFIGURES) $(TEXANIMS)
$(PDFLATEX) $(patsubst %.pdf,%.tex,$@)
@if ( grep "\\bibdata" $(patsubst %.pdf,%.aux,$@) > /dev/null ); then \
$(BIBTEX) $(patsubst %.pdf,%,$@); \
fi
@while ( grep "Rerun to get cross-references" \
$(patsubst %.pdf,%.log,$@) > /dev/null ); do \
echo '** Re-running LaTeX **'; \
$(PDFLATEX) $(patsubst %.pdf,%.tex,$@); \
done
else
%.pdf : %.ps
$(PS2PDF) $*.ps
endif
%.bbl: %.tex %.aux
$(BIBTEX) $*
%.aux: %.tex
$(LATEX) $*
%.ps : %.dvi
$(DVIPS) $*.dvi -o $*.ps
%.tex : %.anim %.fig
figanim $<
%.eps %.tex: %.fig
fig2dev -L pstex $*.fig > $*.eps
fig2dev -L pstex_t -F -p $* $*.fig > $*.tex
%.tex : %.fig
fig2dev -L $(PSORPDF)tex_t -F -p $* $*.fig > $*.tex
%.pdf %.tex: %.fig
fig2dev -L pdftex $*.fig > $*.pdf
fig2dev -L pdftex_t -F -p $* $*.fig > $*.tex
clean:
rm -f ./*.aux ./*.log ./*.bbl ./*.blg ./*.dvi ./*.toc ./*.lof ./*.log ./*.lot ./*.out ./*.cb ./*.nav ./*.snm ./*.vrb
rm -f ./*.tex~
figclean:
rm -f ./figures/*.{tex,eps,pdf,bak}
animclean:
rm -f ./anim/*.{tex,eps,pdf,bak}
bigclean: figclean animclean clean
rm -f $(PDFS) $(PSS)

3723
manual/figures/mixed-state-df.eps Normal file
View file

File diff suppressed because it is too large Load diff

3723
manual/figures/mixed-state-df.epsi Normal file
View file

File diff suppressed because it is too large Load diff

BIN
manual/figures/mixed-state-df.pdf Normal file
View file

Binary file not shown.

2314
manual/figures/mixed-state-df.ps Normal file
View file

File diff suppressed because it is too large Load diff

147
manual/figures/mixed-state-df.tex Normal file
View file

@ -0,0 +1,147 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-clés)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}[node distance=3cm,auto,initial text=,initial where=left,pos=0.5]
\draw node[state,initial,label={above:$y=\False$}] (A) {A};
\draw node[state,label={below:$y=\True$}] (C) [below of=A] {C};
\draw node[draw,rounded corners,anchor=west] (B)
[right of=A,anchor=north west] {
\begin{varwidth}{\textwidth}
\begin{tikzpicture}
\matrix (m) [matrix of nodes] {
\begin{tikzpicture}
\begin{scope}[node distance=2cm,auto,initial text=,initial
where=left,pos=0.5]
\draw node[state,initial,label={right:$y_1 =\False$}] (Idle) {Idle};
\draw node[state,label={right:$y_1=\True$}] (Active) [below of=Idle]
{Act};
\path[->] (Idle) edge [bend left] node {$c$} (Active)
(Active) edge [bend left] node {$c$} (Idle);
\end{scope}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{scope}[node distance=2cm,auto,initial text=,initial where=left,pos=0.5]
\draw node[state,initial,label={right:$y_2 =\False$}] (Idle) {Idle};
\draw node[state,label={right:$y_2=\True$}] (Active) [below of=Idle]
{Act};
\path[->] (Idle) edge [bend left] node {$d$} (Active) (Active) edge
[bend left] node {$d$} (Idle);
\end{scope}
\end{tikzpicture}
\\[5mm]
\node {$y = y_1\land y_2$};\\
};
\draw [dashed] (m-1-1.north east) -- (m-1-1.south east);
\draw [dashed] (m-1-1.south west) -- (m-1-2.south east);
\end{tikzpicture}
\end{varwidth}
};
\path[->] (A) edge [bend left] node {$c$} (B)
(B.west) edge [bend left] node {$c\land d$} (C)
(C) edge [bend left] node {$d$} (A);
\end{tikzpicture}
\end{document}

1312
manual/figures/node-contract.eps Normal file
View file

File diff suppressed because it is too large Load diff

1312
manual/figures/node-contract.epsi Normal file
View file

File diff suppressed because it is too large Load diff

BIN
manual/figures/node-contract.pdf Normal file
View file

Binary file not shown.

968
manual/figures/node-contract.ps Normal file
View file

@ -0,0 +1,968 @@
%!PS-Adobe-2.0
%%Creator: dvips(k) 5.95a Copyright 2005 Radical Eye Software
%%Title: node-contract.dvi
%%Pages: 1
%%PageOrder: Ascend
%%BoundingBox: 0 0 595 842
%%DocumentFonts: CMMI10 CMR10 CMR7 CMMI7 t1xbtt
%%DocumentPaperSizes: a4
%%EndComments
%DVIPSWebPage: (www.radicaleye.com)
%DVIPSCommandLine: dvips node-contract.dvi -o
%DVIPSParameters: dpi=600
%DVIPSSource: TeX output 2008.12.23:0957
%%BeginProcSet: tex.pro 0 0
%!
/TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
N}B/A{dup}B/TR{translate}N/isls false N/vsize 11 72 mul N/hsize 8.5 72
mul N/landplus90{false}def/@rigin{isls{[0 landplus90{1 -1}{-1 1}ifelse 0
0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{
landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize
mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[
matrix currentmatrix{A A round sub abs 0.00001 lt{round}if}forall round
exch round exch]setmatrix}N/@landscape{/isls true N}B/@manualfeed{
statusdict/manualfeed true put}B/@copies{/#copies X}B/FMat[1 0 0 -1 0 0]
N/FBB[0 0 0 0]N/nn 0 N/IEn 0 N/ctr 0 N/df-tail{/nn 8 dict N nn begin
/FontType 3 N/FontMatrix fntrx N/FontBBox FBB N string/base X array
/BitMaps X/BuildChar{CharBuilder}N/Encoding IEn N end A{/foo setfont}2
array copy cvx N load 0 nn put/ctr 0 N[}B/sf 0 N/df{/sf 1 N/fntrx FMat N
df-tail}B/dfs{div/sf X/fntrx[sf 0 0 sf neg 0 0]N df-tail}B/E{pop nn A
definefont setfont}B/Cw{Cd A length 5 sub get}B/Ch{Cd A length 4 sub get
}B/Cx{128 Cd A length 3 sub get sub}B/Cy{Cd A length 2 sub get 127 sub}
B/Cdx{Cd A length 1 sub get}B/Ci{Cd A type/stringtype ne{ctr get/ctr ctr
1 add N}if}B/CharBuilder{save 3 1 roll S A/base get 2 index get S
/BitMaps get S get/Cd X pop/ctr 0 N Cdx 0 Cx Cy Ch sub Cx Cw add Cy
setcachedevice Cw Ch true[1 0 0 -1 -.1 Cx sub Cy .1 sub]{Ci}imagemask
restore}B/D{/cc X A type/stringtype ne{]}if nn/base get cc ctr put nn
/BitMaps get S ctr S sf 1 ne{A A length 1 sub A 2 index S get sf div put
}if put/ctr ctr 1 add N}B/I{cc 1 add D}B/bop{userdict/bop-hook known{
bop-hook}if/SI save N @rigin 0 0 moveto/V matrix currentmatrix A 1 get A
mul exch 0 get A mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N/eop{
SI restore userdict/eop-hook known{eop-hook}if showpage}N/@start{
userdict/start-hook known{start-hook}if pop/VResolution X/Resolution X
1000 div/DVImag X/IEn 256 array N 2 string 0 1 255{IEn S A 360 add 36 4
index cvrs cvn put}for pop 65781.76 div/vsize X 65781.76 div/hsize X}N
/p{show}N/RMat[1 0 0 -1 0 0]N/BDot 260 string N/Rx 0 N/Ry 0 N/V{}B/RV/v{
/Ry X/Rx X V}B statusdict begin/product where{pop false[(Display)(NeXT)
(LaserWriter 16/600)]{A length product length le{A length product exch 0
exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false}ifelse
end{{gsave TR -.1 .1 TR 1 1 scale Rx Ry false RMat{BDot}imagemask
grestore}}{{gsave TR -.1 .1 TR Rx Ry scale 1 1 false RMat{BDot}
imagemask grestore}}ifelse B/QV{gsave newpath transform round exch round
exch itransform moveto Rx 0 rlineto 0 Ry neg rlineto Rx neg 0 rlineto
fill grestore}B/a{moveto}B/delta 0 N/tail{A/delta X 0 rmoveto}B/M{S p
delta add tail}B/b{S p tail}B/c{-4 M}B/d{-3 M}B/e{-2 M}B/f{-1 M}B/g{0 M}
B/h{1 M}B/i{2 M}B/j{3 M}B/k{4 M}B/w{0 rmoveto}B/l{p -4 w}B/m{p -3 w}B/n{
p -2 w}B/o{p -1 w}B/q{p 1 w}B/r{p 2 w}B/s{p 3 w}B/t{p 4 w}B/x{0 S
rmoveto}B/y{3 2 roll p a}B/bos{/SS save N}B/eos{SS restore}B end
%%EndProcSet
%%BeginProcSet: texps.pro 0 0
%!
TeXDict begin/rf{findfont dup length 1 add dict begin{1 index/FID ne 2
index/UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]FontType 0
ne{/Metrics exch def dict begin Encoding{exch dup type/integertype ne{
pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get
div def}ifelse}forall Metrics/Metrics currentdict end def}{{1 index type
/nametype eq{exit}if exch pop}loop}ifelse[2 index currentdict end
definefont 3 -1 roll makefont/setfont cvx]cvx def}def/ObliqueSlant{dup
sin S cos div neg}B/SlantFont{4 index mul add}def/ExtendFont{3 -1 roll
mul exch}def/ReEncodeFont{CharStrings rcheck{/Encoding false def dup[
exch{dup CharStrings exch known not{pop/.notdef/Encoding true def}if}
forall Encoding{]exch pop}{cleartomark}ifelse}if/Encoding exch def}def
end
%%EndProcSet
%%BeginProcSet: special.pro 0 0
%!
TeXDict begin/SDict 200 dict N SDict begin/@SpecialDefaults{/hs 612 N
/vs 792 N/ho 0 N/vo 0 N/hsc 1 N/vsc 1 N/ang 0 N/CLIP 0 N/rwiSeen false N
/rhiSeen false N/letter{}N/note{}N/a4{}N/legal{}N}B/@scaleunit 100 N
/@hscale{@scaleunit div/hsc X}B/@vscale{@scaleunit div/vsc X}B/@hsize{
/hs X/CLIP 1 N}B/@vsize{/vs X/CLIP 1 N}B/@clip{/CLIP 2 N}B/@hoffset{/ho
X}B/@voffset{/vo X}B/@angle{/ang X}B/@rwi{10 div/rwi X/rwiSeen true N}B
/@rhi{10 div/rhi X/rhiSeen true N}B/@llx{/llx X}B/@lly{/lly X}B/@urx{
/urx X}B/@ury{/ury X}B/magscale true def end/@MacSetUp{userdict/md known
{userdict/md get type/dicttype eq{userdict begin md length 10 add md
maxlength ge{/md md dup length 20 add dict copy def}if end md begin
/letter{}N/note{}N/legal{}N/od{txpose 1 0 mtx defaultmatrix dtransform S
atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{
itransform lineto}}{6 -2 roll transform 6 -2 roll transform 6 -2 roll
transform{itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll
curveto}}{{closepath}}pathforall newpath counttomark array astore/gc xdf
pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack}
if}N/txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1
-1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3
get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip
yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub
neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{
noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop
90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get
neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr
1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr
2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4
-1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S
TR}if}N/cp{pop pop showpage pm restore}N end}if}if}N/normalscale{
Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale
}if 0 setgray}N/psfts{S 65781.76 div N}N/startTexFig{/psf$SavedState
save N userdict maxlength dict begin/magscale true def normalscale
currentpoint TR/psf$ury psfts/psf$urx psfts/psf$lly psfts/psf$llx psfts
/psf$y psfts/psf$x psfts currentpoint/psf$cy X/psf$cx X/psf$sx psf$x
psf$urx psf$llx sub div N/psf$sy psf$y psf$ury psf$lly sub div N psf$sx
psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub
TR/showpage{}N/erasepage{}N/setpagedevice{pop}N/copypage{}N/p 3 def
@MacSetUp}N/doclip{psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll
newpath 4 copy 4 2 roll moveto 6 -1 roll S lineto S lineto S lineto
closepath clip newpath moveto}N/endTexFig{end psf$SavedState restore}N
/@beginspecial{SDict begin/SpecialSave save N gsave normalscale
currentpoint TR @SpecialDefaults count/ocount X/dcount countdictstack N}
N/@setspecial{CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs
neg 0 rlineto closepath clip}if ho vo TR hsc vsc scale ang rotate
rwiSeen{rwi urx llx sub div rhiSeen{rhi ury lly sub div}{dup}ifelse
scale llx neg lly neg TR}{rhiSeen{rhi ury lly sub div dup scale llx neg
lly neg TR}if}ifelse CLIP 2 eq{newpath llx lly moveto urx lly lineto urx
ury lineto llx ury lineto closepath clip}if/showpage{}N/erasepage{}N
/setpagedevice{pop}N/copypage{}N newpath}N/@endspecial{count ocount sub{
pop}repeat countdictstack dcount sub{end}repeat grestore SpecialSave
restore end}N/@defspecial{SDict begin}N/@fedspecial{end}B/li{lineto}B
/rl{rlineto}B/rc{rcurveto}B/np{/SaveX currentpoint/SaveY X N 1
setlinecap newpath}N/st{stroke SaveX SaveY moveto}N/fil{fill SaveX SaveY
moveto}N/ellipse{/endangle X/startangle X/yrad X/xrad X/savematrix
matrix currentmatrix N TR xrad yrad scale 0 0 1 startangle endangle arc
savematrix setmatrix}N end
%%EndProcSet
%%BeginProcSet: color.pro 0 0
%!
TeXDict begin/setcmykcolor where{pop}{/setcmykcolor{dup 10 eq{pop
setrgbcolor}{1 sub 4 1 roll 3{3 index add neg dup 0 lt{pop 0}if 3 1 roll
}repeat setrgbcolor pop}ifelse}B}ifelse/TeXcolorcmyk{setcmykcolor}def
/TeXcolorrgb{setrgbcolor}def/TeXcolorgrey{setgray}def/TeXcolorgray{
setgray}def/TeXcolorhsb{sethsbcolor}def/currentcmykcolor where{pop}{
/currentcmykcolor{currentrgbcolor 10}B}ifelse/DC{exch dup userdict exch
known{pop pop}{X}ifelse}B/GreenYellow{0.15 0 0.69 0 setcmykcolor}DC
/Yellow{0 0 1 0 setcmykcolor}DC/Goldenrod{0 0.10 0.84 0 setcmykcolor}DC
/Dandelion{0 0.29 0.84 0 setcmykcolor}DC/Apricot{0 0.32 0.52 0
setcmykcolor}DC/Peach{0 0.50 0.70 0 setcmykcolor}DC/Melon{0 0.46 0.50 0
setcmykcolor}DC/YellowOrange{0 0.42 1 0 setcmykcolor}DC/Orange{0 0.61
0.87 0 setcmykcolor}DC/BurntOrange{0 0.51 1 0 setcmykcolor}DC
/Bittersweet{0 0.75 1 0.24 setcmykcolor}DC/RedOrange{0 0.77 0.87 0
setcmykcolor}DC/Mahogany{0 0.85 0.87 0.35 setcmykcolor}DC/Maroon{0 0.87
0.68 0.32 setcmykcolor}DC/BrickRed{0 0.89 0.94 0.28 setcmykcolor}DC/Red{
0 1 1 0 setcmykcolor}DC/OrangeRed{0 1 0.50 0 setcmykcolor}DC/RubineRed{
0 1 0.13 0 setcmykcolor}DC/WildStrawberry{0 0.96 0.39 0 setcmykcolor}DC
/Salmon{0 0.53 0.38 0 setcmykcolor}DC/CarnationPink{0 0.63 0 0
setcmykcolor}DC/Magenta{0 1 0 0 setcmykcolor}DC/VioletRed{0 0.81 0 0
setcmykcolor}DC/Rhodamine{0 0.82 0 0 setcmykcolor}DC/Mulberry{0.34 0.90
0 0.02 setcmykcolor}DC/RedViolet{0.07 0.90 0 0.34 setcmykcolor}DC
/Fuchsia{0.47 0.91 0 0.08 setcmykcolor}DC/Lavender{0 0.48 0 0
setcmykcolor}DC/Thistle{0.12 0.59 0 0 setcmykcolor}DC/Orchid{0.32 0.64 0
0 setcmykcolor}DC/DarkOrchid{0.40 0.80 0.20 0 setcmykcolor}DC/Purple{
0.45 0.86 0 0 setcmykcolor}DC/Plum{0.50 1 0 0 setcmykcolor}DC/Violet{
0.79 0.88 0 0 setcmykcolor}DC/RoyalPurple{0.75 0.90 0 0 setcmykcolor}DC
/BlueViolet{0.86 0.91 0 0.04 setcmykcolor}DC/Periwinkle{0.57 0.55 0 0
setcmykcolor}DC/CadetBlue{0.62 0.57 0.23 0 setcmykcolor}DC
/CornflowerBlue{0.65 0.13 0 0 setcmykcolor}DC/MidnightBlue{0.98 0.13 0
0.43 setcmykcolor}DC/NavyBlue{0.94 0.54 0 0 setcmykcolor}DC/RoyalBlue{1
0.50 0 0 setcmykcolor}DC/Blue{1 1 0 0 setcmykcolor}DC/Cerulean{0.94 0.11
0 0 setcmykcolor}DC/Cyan{1 0 0 0 setcmykcolor}DC/ProcessBlue{0.96 0 0 0
setcmykcolor}DC/SkyBlue{0.62 0 0.12 0 setcmykcolor}DC/Turquoise{0.85 0
0.20 0 setcmykcolor}DC/TealBlue{0.86 0 0.34 0.02 setcmykcolor}DC
/Aquamarine{0.82 0 0.30 0 setcmykcolor}DC/BlueGreen{0.85 0 0.33 0
setcmykcolor}DC/Emerald{1 0 0.50 0 setcmykcolor}DC/JungleGreen{0.99 0
0.52 0 setcmykcolor}DC/SeaGreen{0.69 0 0.50 0 setcmykcolor}DC/Green{1 0
1 0 setcmykcolor}DC/ForestGreen{0.91 0 0.88 0.12 setcmykcolor}DC
/PineGreen{0.92 0 0.59 0.25 setcmykcolor}DC/LimeGreen{0.50 0 1 0
setcmykcolor}DC/YellowGreen{0.44 0 0.74 0 setcmykcolor}DC/SpringGreen{
0.26 0 0.76 0 setcmykcolor}DC/OliveGreen{0.64 0 0.95 0.40 setcmykcolor}
DC/RawSienna{0 0.72 1 0.45 setcmykcolor}DC/Sepia{0 0.83 1 0.70
setcmykcolor}DC/Brown{0 0.81 1 0.60 setcmykcolor}DC/Tan{0.14 0.42 0.56 0
setcmykcolor}DC/Gray{0 0 0 0.50 setcmykcolor}DC/Black{0 0 0 1
setcmykcolor}DC/White{0 0 0 0 setcmykcolor}DC end
%%EndProcSet
TeXDict begin @defspecial
/DvipsToPDF { 72.27 mul Resolution div } def /PDFToDvips { 72.27 div
Resolution mul } def /HyperBorder { 1 PDFToDvips } def /H.V {pdf@hoff
pdf@voff null} def /H.B {/Rect[pdf@llx pdf@lly pdf@urx pdf@ury]} def
/H.S { currentpoint HyperBorder add /pdf@lly exch def dup DvipsToPDF
/pdf@hoff exch def HyperBorder sub /pdf@llx exch def } def /H.L { 2
sub dup /HyperBasePt exch def PDFToDvips /HyperBaseDvips exch def currentpoint
HyperBaseDvips sub /pdf@ury exch def /pdf@urx exch def } def /H.A {
H.L currentpoint exch pop vsize 72 sub exch DvipsToPDF HyperBasePt
sub sub /pdf@voff exch def } def /H.R { currentpoint HyperBorder sub
/pdf@ury exch def HyperBorder add /pdf@urx exch def currentpoint exch
pop vsize 72 sub exch DvipsToPDF sub /pdf@voff exch def } def systemdict
/pdfmark known not {userdict /pdfmark systemdict /cleartomark get put}
if
/pgfH{/pgfheight exch def 0.75 setlinewidth [] 0 setdash /pgfshade
{pgfA} def /pgfdir { dup 0 moveto dup 5 index lineto } bind def} bind
def
/pgfV{/pgfheight exch def 0.75 setlinewidth [] 0 setdash /pgfshade
{pgfA} def /pgfdir { dup 0 exch moveto dup 5 index exch lineto } bind
def} bind def
/pgfA{ /pgfdiff 8 index round cvi 8 index round cvi sub 2 mul 1 add
def 2 index 6 index sub pgfdiff div 2 index 6 index sub pgfdiff div
2 index 6 index sub pgfdiff div pgfheight 9 index 9 index 9 index 14
index pgfdiff { 3 index 3 index 3 index setrgbcolor pgfdir stroke 4
-1 roll 7 index add 4 -1 roll 6 index add 4 -1 roll 5 index add 4 -1
roll .5 sub } repeat mark 15 1 roll cleartomark exch pop }bind def
/pgfR1{ newpath dup dup dup 0 360 arc clip newpath dup /pgfendx exch
def /pgfendy exch def 0.875 setlinewidth [] 0 setdash /pgfshade {pgfR}
def /pgfstartx exch def /pgfstarty exch def /pgfdiffx pgfendx pgfstartx
sub def /pgfdiffy pgfendy pgfstarty sub def dup /pgfdomb exch def }bind
def
/pgfR2{ newpath 0.5 add pgfcircx pgfcircy 3 2 roll 0 360 arc setrgbcolor
fill pop}bind def
/pgfR{ /pgfdiff 8 index round cvi 8 index round cvi sub 4 mul 1 add
def /pgfcircx pgfstartx 9 index pgfdiffx pgfdomb div mul add def /pgfcircy
pgfstarty 9 index pgfdiffy pgfdomb div mul add def /pgfcircxe pgfstartx
8 index pgfdiffx pgfdomb div mul add def /pgfcircye pgfstarty 8 index
pgfdiffy pgfdomb div mul add def /pgfxstep pgfcircxe pgfcircx sub pgfdiff
div def /pgfystep pgfcircye pgfcircy sub pgfdiff div def 2 index 6
index sub pgfdiff div 2 index 6 index sub pgfdiff div 2 index 6 index
sub pgfdiff div 8 index 8 index 8 index 13 index pgfdiff { 3 index
3 index 3 index setrgbcolor pgfcircx pgfcircy 2 index 0 360 arc closepath
stroke 4 -1 roll 6 index add 4 -1 roll 5 index add 4 -1 roll 4 index
add 4 -1 roll .25 sub /pgfcircx pgfcircx pgfxstep add def /pgfcircy
pgfcircy pgfystep add def } repeat mark 14 1 roll cleartomark exch
pop }bind def
/pgfsc{}bind def/pgffc{}bind def/pgfstr{stroke}bind def/pgffill{fill}bind
def/pgfeofill{eofill}bind def/pgfe{a dup 0 rlineto exch 0 exch rlineto
neg 0 rlineto closepath}bind def/pgfw{setlinewidth}bind def/pgfs{save
pgfpd 72 Resolution div 72 VResolution div neg scale magscale{1 DVImag
div dup scale}if pgfx neg pgfy neg translate pgffoa .setopacityalpha}bind
def/pgfr{pgfsd restore}bind def userdict begin/pgfo{pgfsd /pgfx currentpoint
/pgfy exch def def @beginspecial}bind def /pgfc{newpath @endspecial
pgfpd}bind def /pgfsd{globaldict /pgfdelta /delta where {pop delta}
{0} ifelse put}bind def/pgfpd{/delta globaldict /pgfdelta get def}bind
def /.setopacityalpha where {pop} {/.setopacityalpha{pop}def} ifelse
/.pgfsetfillopacityalpha{/pgffoa exch def /pgffill{gsave pgffoa .setopacityalpha
fill 1 .setopacityalpha newpath fill grestore}bind def /pgfeofill{gsave
pgffoa .setopacityalpha eofill 1 .setopacityalpha newpath eofill grestore}bind
def}bind def /.pgfsetstrokeopacityalpha{/pgfsoa exch def /pgfstr{gsave
pgfsoa .setopacityalpha stroke grestore}bind def}bind def /pgffoa 1
def /pgfsoa 1 def end
/pgf1{gsave exec 1.0 pgfw 2.00002 0.0 moveto -6.00006 4.00005 lineto
-3.00003 0.0 lineto -6.00006 -4.00005 lineto pgffill grestore} bind
def
/pgf2{gsave exec 1.0 pgfw 0.8 pgfw [ ] 0.0 setdash 1 setlinecap 1
setlinejoin -3.00003 4.00005 moveto -2.75002 2.50002 0.0 0.24998 0.75
0.0 curveto 0.0 -0.24998 -2.75002 -2.50002 -3.00003 -4.00005 curveto
pgfstr grestore} bind def
/pgf3{gsave exec 1.0 pgfw [ ] 0.0 setdash 0.0 -5.00005 moveto 0.0
5.00005 lineto pgfstr grestore} bind def
/pgf4{gsave exec 1.0 pgfw [ ] 0.0 setdash -3.00003 -5.00005 moveto
0.0 -5.00005 lineto 0.0 5.00005 lineto -3.00003 5.00005 lineto pgfstr
grestore} bind def
/pgf5{gsave exec 1.0 pgfw [ ] 0.0 setdash -2.00002 -5.00005 moveto
1.0 -3.00003 1.0 3.00003 -2.00002 5.00005 curveto pgfstr grestore}
bind def
/pgf6{gsave exec 1.0 pgfw [ ] 0.0 setdash -4.50003 -5.00005 moveto
0.49998 0.0 lineto -4.50003 5.00005 lineto pgfstr grestore} bind def
/pgf7{gsave exec 1.0 pgfw -2.50002 0.0 translate [ ] 0.0 setdash 3.00003
0.0 moveto 3.00003 1.665 1.665 3.00003 0.0 3.00003 curveto -1.665 3.00003
-3.00003 1.665 -3.00003 0.0 curveto -3.00003 -1.665 -1.665 -3.00003
0.0 -3.00003 curveto 1.665 -3.00003 3.00003 -1.665 3.00003 0.0 curveto
closepath gsave pgffc pgffill grestore gsave pgfsc pgfstr grestore
newpath grestore} bind def
/pgf8{gsave exec 1.0 pgfw [ ] 0.0 setdash 1.0 0.0 moveto -5.00005
3.00003 lineto -11.00012 0.0 lineto -5.00005 -3.00003 lineto closepath
gsave pgffc pgffill grestore gsave pgfsc pgfstr grestore newpath grestore}
bind def
@fedspecial end
%%BeginFont: t1xbtt
%!PS-AdobeFont-1.0: t1xbtt 3.0
%%CreationDate: 12/14/2000 at 12:00 PM
%%VMusage: 1024 27998
20 dict begin
/FontInfo 16 dict dup begin
/version (3.0) readonly def
/FullName (t1xbtt) readonly def
/FamilyName (t1xbtt) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch true def
/UnderlinePosition -100 def
/UnderlineThickness 50 def
/Notice (Version 3.0, GPL) readonly def
/em 1000 def
/ascent 800 def
/descent 200 def
end readonly def
/FontName /t1xbtt def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 97 /a put
dup 101 /e put
dup 103 /g put
dup 104 /h put
dup 105 /i put
dup 109 /m put
dup 110 /n put
dup 114 /r put
dup 115 /s put
dup 116 /t put
dup 117 /u put
dup 119 /w put
readonly def
/PaintType 0 def
/FontType 1 def
/StrokeWidth 0 def
/FontMatrix[0.001 0 0 0.001 0 0]readonly def
/FontBBox{-28 -213 1516 882}readonly def
currentdict end
currentfile eexec
D9D66F633B846AB284BCF8B0411B772DE5CD06DFE1BE899059C588357426D7A0
7B684C079A47D271426064AD18CB9750D8A986D1D67C1B2AEEF8CE785CC19C81
DE96489F740045C5E342F02DA1C9F9F3C167651E646F1A67CF379789E311EF91
511D0F605B045B279357D6FC8537C233E7AEE6A4FDBE73E75A39EB206D20A6F6
1021961B748D419EBEEB028B592124E174CA595C108E12725B9875544955CFFD
02843723FD4914EA94CF5C86363ACA5D85BC6F2DC07E1913DE009E806C3EE8F3
FEC9E1C1A320C2124B06F5E41354C077F75C6EB18C1C637209CD429CF0A07147
4C4B3FB0D260C42F8BB83C7DB6A92ABCBC206C45E91E10AF52EEAB7427C2EEAF
00FE4361755860C83861E922F3F9B396CDDD72DCE20CAFF85B4DFC108C6E8C25
982D9DC24E0F00B2D9BF6BE30CF2CD3892B25A4449FE2E0A7E033EE6142D8652
C1E7A5D3B68F9ECB208F609A8B7C86E8AF1B60AB9C346C38846FFBDC552E7341
291E70E890C82591691295993A650184E182741E01DA169E64B4EBB55702E06F
089049ADFD0C4F35A59C3CB2AD1DD25291A3B2B8BD16BFDB519091D2CAD96662
E2DDD3332CFAA7FEFF2FC0C8E26DF69D38ABA34B49948B32FCC1005488C1662B
1A98BCF63020A275CFCA8611C69B85AFBF6167D6A3BE36D568914C6B2ED8E6DF
63A016E4B176ED42146154259263EE0F606C3ADDEA43343301E12304CDD678E4
F19D9BAD10E071D9F7F959365EE625AC55453D22D02BB2A5A27271C054422504
5A6DCBDC95B52E577A2C78FCA613979E564E716CFB2AFE24EB580E55BD31B793
E40676D096325222891C44E70040CE6085ED76FDD2ECFC22F3D5905A6984D312
333B878F1E0CD594A45EE8834CECFB7841DD42F14DC9532DC0FBC8F5DEE99606
2358125BE880721E4058DF14DF97F32561E05C6C3AB1528FE248DAD3DDD994A8
8A9FDCE9AC14792B354E24728BC4BD73EBB653F5D544D279A780A7C613F54CC2
4D464159AE8D8B94A08A299F2E584989FFD867E03AEEE73227AEB5CED09772C6
77DE2763F4D72E6587AA7280D1E505CC215FFC60D942E9951546544F0F8D2ADC
49CFE5BFA7D0390B252816C74625A20A44ACBE3DB67F661E0251CD15D27DB989
29185ABBDCA4D8762C05DAACA252FFDFD28D79857C4A0FE02347BECCEE2ABBF0
BE0F43AC5BB76593F95307F18AD352330DA02CC2305901A45CDDC07A6321CDBD
4BA0BA7CCD8A4B6786DBD28436D018C9537EBD753A2D3EC984282ED87DDC98FA
6F8D9D098182DC77880F74F8D417CD7A3F3A676D408A68517182256FEA86C772
65746E871C8EDB45DF6C45D3B7AC4D77D586A4676692E9FC77E5ACF41EED6BFF
0D9062DFCE7668550F638866DBC557AD44900C7425CA1EEAAF3AC21ECC91264E
9BE838467239782A9D9C954B5FE2374B31804E4902F58E85065E23BCB2890D36
48B43E06CDEB23D0183AD709472F315E510B7B1BE62A5F62D37FC4D4B4C56E14
EFF98BFAB1C43FE9757C055DBD573B814F934858190B3A3FC739F816B3227B9E
443DF6407B364DEDDCC7C7F6E1044466082F36119E6CD6C6DB1395EBC809F8EE
88A10DB2E3102753E2659A40EFD008364D0B00FCC13638FA5C0EF9ADDF824A97
5635014A93120F4CF2AED045170681789253020FA57734DA5180596ECB8D97F8
3F05145BECCEF61C86244849088F5E3DC34F461F1B4FFF5F2A68F42F02F8A6CF
CDE86343EC97505B5223159A745D23109C808CC12244A2F4AD9225FA6FD43BB3
F3740DD98E2AD199AF9060AA47BE511F284C61B72DEED557BE7CF7E7909365B2
94118B25C4A6730EAD5572FDAABC33E2C1BADDCBCB691E81C28840514DA19F47
DAAA080A3D72AFA4D63B3C3DFC9703517D7BA5F1A2C058513DC5FE4017DDB09D
1C7404FCA0C0D6EB24C2E985EEB76F9319A7E570594BD4F85CB21468169D44C4
EFE745398515EACB1D5248ABD169E0FDB9A55FF38EE513DA0C22D7607EFD5B77
EC6D1D9E8DAC52F2AC1BDD749849CE7BAF54A7FE6DD526852437813E58C26AEA
A8A4EB359754A876A478052189F857190BEE3AB7F0B7103A1D6B4E6F479DA0E6
FA7D7E26E0FE365BDF7655C699F7D05CB53347F4402FC05A97EDEB2DE779AC87
B536F42F7367ECD4995500FB0F8F7BFCBFD8844B1DE4782E48116F4775AC9049
665614914483BE13D6604A0692BBD9E8195EC130D92FA2ACD6CE6EFFA49E1B52
B1151DE5755FB983BC066B18D401924563706AB5BE46DD40BABB52CF9105B208
859B03FCEDCC76509FF3113304F3CFCEE8EADA3787CFE7765513B2CF28DD1A31
D50F41EC10D31A3BB294DCBDC3886C2B9412ADD01A23A8A92D04583D36FB26C0
82B5CCE8BA414106AD5CBBB9E76C14F9A531279C98B02D3BFFD91CFF09641A7E
31942C305A3242E4B73B097E537079880D6F80980EEE1BB4059E8D9454FAF961
786F91DD4CB2DE9C2107B60E8BF0E45FE00933038F1B5C3DA9B4C722977DC831
B9640F03E0C6CC30C23A9EEBC4FD60E7CA0EE7E324A5A180BD5AF54D5142BB9F
06C180C6EC1D7D8A2AB3065A8461EA5C2019F34140C0CAF44D9B6EC6C3F27E47
E6740FB04939DCEE6F4C528DAC39F6193C3039196238C78894D411CE923913BA
0BDE1F79498CE858E8F49E9922E466BD89006E54E2FAB228EA3CCADA20AC814E
123EADFCEF131C50BCE424159AE41505CACEFD51EB881C248171BFB80FCFDC21
214BAB83FC86ABE8E98D03274A115B7221EC18B9724732043C0BBCF0F29E17DC
85AB0A8853561882BA87A9E091DB2837B690CEF53814F08B4EFEC323BD339F2E
FC4D21EE77C082FF180BF8AB18E1EB329CF82D92E79BDB467A5ED196992E14BA
C35C32B29DA38CB576A05BA1C1DF3045AE63444B05C3A81BAFF4EE8BBA5D362E
8D660A8AD7BBDAA2A35EB13F51EB0B07E67BD6189B3A5B04F23396C3A9116433
ECDEE775014CA247F326F91676299DA2A22F81B328C9FB4FD2ED6D62856BDB16
FF0F95926D0559086B1F4A0F6D0985E4529357A93AB1E987A4D52D10ACFC1718
47E18BCA34710C0179F7BD292145
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMMI7
%!PS-AdobeFont-1.1: CMMI7 1.100
%%CreationDate: 1996 Jul 23 07:53:53
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.100) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMMI7) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.04 def
/isFixedPitch false def
end readonly def
/FontName /CMMI7 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 65 /A put
dup 71 /G put
dup 110 /n put
readonly def
/FontBBox{0 -250 1171 750}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA0529731C99A784CCBE85B4993B2EEBDE
3B12D472B7CF54651EF21185116A69AB1096ED4BAD2F646635E019B6417CC77B
532F85D811C70D1429A19A5307EF63EB5C5E02C89FC6C20F6D9D89E7D91FE470
B72BEFDA23F5DF76BE05AF4CE93137A219ED8A04A9D7D6FDF37E6B7FCDE0D90B
986423E5960A5D9FBB4C956556E8DF90CBFAEC476FA36FD9A5C8175C9AF513FE
D919C2DDD26BDC0D99398B9F4D03D77639DF1232A4D6233A9CAF69B151DFD33F
C0962EAC6E3EBFB8AD256A3C654EAAF9A50C51BC6FA90B61B60401C235AFAB7B
B078D20B4B8A6D7F0300CF694E6956FF9C29C84FCC5C9E8890AA56B1BC60E868
DA8488AC4435E6B5CE34EA88E904D5C978514D7E476BF8971D419363125D4811
4D886EDDDCDDA8A6B0FDA5CF0603EA9FA5D4393BEBB26E1AB11C2D74FFA6FEE3
FAFBC6F05B801C1C3276B11080F5023902B56593F3F6B1F37997038F36B9E3AB
76C2E97E1F492D27A8E99F3E947A47166D0D0D063E4E6A9B535DC9F1BED129C5
123775D5D68787A58C93009FD5DA55B19511B95168C83429BD2D878207C39770
012318EA7AA39900C97B9D3859E3D0B04750B8390BF1F1BC29DC22BCAD50ECC6
A3C633D0937A59E859E5185AF9F56704708D5F1C50F78F43DFAC43C4E7DC9413
44CEFE43279AFD3C167C942889A352F2FF806C2FF8B3EB4908D50778AA58CFFC
4D1B14597A06A994ED8414BBE8B26E74D49F6CF54176B7297CDA112A69518050
01337CBA5478EB984CDD22020DAED9CA8311C33FBCC84177F5CE870E709FC608
D28B3A7208EFF72988C136142CE79B4E9C7B3FE588E9824ABC6F04D141E589B3
914A73A42801305439862414F893D5B6C327A7EE2730DEDE6A1597B09C258F05
261BC634F64C9F8477CD51634BA648FC70F659C90DC042C0D6B68CD1DF36D615
24F362B85A58D65A8E6DFD583EF9A79A428F2390A0B5398EEB78F4B5A89D9AD2
A517E0361749554ABD6547072398FFDD863E40501C316F28FDDF8B550FF8D663
9843D0BEA42289F85BD844891DB42EC7C51229D33EE7E83B1290404C799B8E8C
889787CDC7AA8BEF7021B3C18A0A61A68CCEA80153A2C2E1CE6D07654730000C
57F4C7817D2A97E68C34052C48BF17B00076F0F21EABE8B9A4E90FF00CD12C86
CF6614154C57E889AF21AB96E24C8B3F890BC647CA2F9EF6E4E3B999106CE83E
3EE7BF9638B31FFBD14576A43154CC0DD3EB4D64B505C9576ED8B190E55112C6
1C931FF7F8529F41CBAAA4E2DB390BEF7F932ECB404D872321446C64508FF03A
692E3B45539E8C8D263021F6EC63F0AD6BF1B09988AC68F66B934E7B4D37B181
A6B4771B115C4D7989F352191703D1B73978E9821513D84E27F4052B3FABE75D
2B40E20E728F7D70C48AFE50DE550AB4E9172DF68E66793B8DF00354839C274D
DFB204205E42E9BEF65140A9777EE7857E3A85067F127F12BD58008ABDEC10DC
A81BF9F22D56299EF237BCAF0DC6BE6BE476500939A755E36EAF82CAC0DB00F3
485186EE04F0123EF2C7141B815113E2DCD9C630A6C7A2EBF64CAA7B8BE65947
B69687EA97ED303695B498E0029ABC8467DD829E18589086110C2A0B41A1C4CD
E65904BE79EB10DB9C2E79B5A797C013EC41371E2AC4EE89AFE2C3ED2AFFF7AC
DEB4823EFC3EB6BAD695E3B6A97FF0F2CAF82DA3016BB9645D2807D44D684203
791505C8919A6B79405424917E3CD895694B8355C32E03CD3B55C97502377A03
AD897FA1B03DEDB6C05299F55D6B2510B7457B7BB3BED95AE154B5BC64BA7442
F7A0E5E17544892D19A85ABDCC5888E2AD391F08BFD48BCFAF2354BADDC445CE
DAF860891DDF0B77C7E28612DB1B0EC23A86352849A264F6A98FB6DE667383A3
4B4899473BA7F2DC6B55AEE696401ECCA45B4D5975FF17328184FC5CF150AD26
5B4795EAB1D05F57DC73CC2C0B37749B2EE4A95C2CD2E6DE2F3AD0E2ABFA333E
961678DA49F631FE1251BBB3BE90566E32AC57A6A09DF6DFE9AAA9B086922994
AABD758D6ECCFF4FB6368B4D0AC53EDBEBA32086A7718D3CE70257243947B112
1961A66B8CA8553086688D955795F7180992655CBAFDF238D9C72F286CB4EB09
08D4A7DEA198C541E6613A4ED82EB41FAA4B253F2323C4C61A4D1FB114F0F5AE
FDD01DC0C0E081DB9E69552506CBC16A773B8D621434B754C1DDC4DA14C5C2F1
CC3A21941B6BBC159E6F7EC23E279507A5BF71534244A06FA1E7246231B98298
2F3DD23E738DBEC11AEE38651B423CF6A4
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR7
%!PS-AdobeFont-1.1: CMR7 1.0
%%CreationDate: 1991 Aug 20 16:39:21
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR7) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR7 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 49 /one put
readonly def
/FontBBox{-27 -250 1122 750}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA052A014267B7904EB3C0D3BD0B83D891
016CA6CA4B712ADEB258FAAB9A130EE605E61F77FC1B738ABC7C51CD46EF8171
9098D5FEE67660E69A7AB91B58F29A4D79E57022F783EB0FBBB6D4F4EC35014F
D2DECBA99459A4C59DF0C6EBA150284454E707DC2100C15B76B4C19B84363758
469A6C558785B226332152109871A9883487DD7710949204DDCF837E6A8708B8
2BDBF16FBC7512FAA308A093FE5CF5B8CABB9FFC6CC3F1E9AE32F234EB60FE7D
E34995B1ACFF52428EA20C8ED4FD73E3935CEBD40E0EAD70C0887A451E1B1AC8
47AEDE4191CCDB8B61345FD070FD30C4F375D8418DDD454729A251B3F61DAE7C
8882384282FDD6102AE8EEFEDE6447576AFA181F27A48216A9CAD730561469E4
78B286F22328F2AE84EF183DE4119C402771A249AAC1FA5435690A28D1B47486
1060C8000D3FE1BF45133CF847A24B4F8464A63CEA01EC84AA22FD005E74847E
01426B6890951A7DD1F50A5F3285E1F958F11FC7F00EE26FEE7C63998EA1328B
C9841C57C80946D2C2FC81346249A664ECFB08A2CE075036CEA7359FCA1E90C0
F686C3BB27EEFA45D548F7BD074CE60E626A4F83C69FE93A5324133A78362F30
8E8DCC80DD0C49E137CDC9AC08BAE39282E26A7A4D8C159B95F227BDA2A281AF
A9DAEBF31F504380B20812A211CF9FEB112EC29A3FB3BD3E81809FC6293487A7
455EB3B879D2B4BD46942BB1243896264722CB59146C3F65BD59B96A74B12BB2
9A1354AF174932210C6E19FE584B1B14C00E746089CBB17E68845D7B3EA05105
EEE461E3697FCF835CBE6D46C75523478E766832751CF6D96EC338BDAD57D53B
52F5340FAC9FE0456AD13101824234B262AC0CABA43B62EBDA39795BAE6CFE97
563A50AAE1F195888739F2676086A9811E5C9A4A7E0BF34F3E25568930ADF80F
0BDDAC3B634AD4BA6A59720EA4749236CF0F79ABA4716C340F98517F6F06D9AB
7ED8F46FC1868B5F3D3678DF71AA772CF1F7DD222C6BF19D8EF0CFB7A76FC6D1
0AD323C176134907AB375F20CFCD667AB094E2C7CB2179C4283329C9E435E7A4
1E042AD0BAA059B3F862236180B34D3FCED833472577BACD472A4DE3E3F6222F
7A252B780C86447859579C68E52691E144F836C1C62F19A12EFB710343D33262
1F7955FE5C37074CE5F9C7ABF1A241078519A4D7913A0AD861E0E357B50FB730
E757C0D26390E6028FAC61EB0E9414716AC8406A6E35DC70A7C1AA524804FC8E
985CC3604A2BE0A8235CC895B2B33CB7EE85FE4F2CD817BAC3D27ADD295D0A0E
BC0E8D849952BCA7325DC261A785CD2305BC377AC61AC5E5B2CD3164CFF033CB
5436B8000673A4D763ED26273130702447C75A774C7799FB8C3E54A2E34D1710
CF7883A9B05285C7DF30F314455A4428A5369D92C0348D45BF4AEC5E16611D16
1E5EF015900F4DF63A58DC233BEE88417B204DBD110AACD1DE3D750F9C
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR10
%!PS-AdobeFont-1.1: CMR10 1.00B
%%CreationDate: 1992 Feb 19 19:54:52
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00B) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 40 /parenleft put
dup 41 /parenright put
dup 61 /equal put
readonly def
/FontBBox{-251 -250 1009 969}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA052A014267B7904EB3C0D3BD0B83D891
016CA6CA4B712ADEB258FAAB9A130EE605E61F77FC1B738ABC7C51CD46EF8171
9098D5FEE67660E69A7AB91B58F29A4D79E57022F783EB0FBBB6D4F4EC35014F
D2DECBA99459A4C59DF0C6EBA150284454E707DC2100C15B76B4C19B84363758
469A6C558785B226332152109871A9883487DD7710949204DDCF837E6A8708B8
2BDBF16FBC7512FAA308A093FE5CF7158F1163BC1F3352E22A1452E73FECA8A4
87100FB1FFC4C8AF409B2067537220E605DA0852CA49839E1386AF9D7A1A455F
D1F017CE45884D76EF2CB9BC5821FD25365DDEA6E45F332B5F68A44AD8A530F0
92A36FAC8D27F9087AFEEA2096F839A2BC4B937F24E080EF7C0F9374A18D565C
295A05210DB96A23175AC59A9BD0147A310EF49C551A417E0A22703F94FF7B75
409A5D417DA6730A69E310FA6A4229FC7E4F620B0FC4C63C50E99E179EB51E4C
4BC45217722F1E8E40F1E1428E792EAFE05C5A50D38C52114DFCD24D54027CBF
2512DD116F0463DE4052A7AD53B641A27E81E481947884CE35661B49153FA19E
0A2A860C7B61558671303DE6AE06A80E4E450E17067676E6BBB42A9A24ACBC3E
B0CA7B7A3BFEA84FED39CCFB6D545BB2BCC49E5E16976407AB9D94556CD4F008
24EF579B6800B6DC3AAF840B3FC6822872368E3B4274DD06CA36AF8F6346C11B
43C772CC242F3B212C4BD7018D71A1A74C9A94ED0093A5FB6557F4E0751047AF
D72098ECA301B8AE68110F983796E581F106144951DF5B750432A230FDA3B575
5A38B5E7972AABC12306A01A99FCF8189D71B8DBF49550BAEA9CF1B97CBFC7CC
96498ECC938B1A1710B670657DE923A659DB8757147B140A48067328E7E3F9C3
7D1888B284904301450CE0BC15EEEA00E48CCD6388F3FC3C8578EF9A20A0E06E
4F7ADDAF0E7D1E182D115BF1AD931977325AD391E72E2B13CC108E3726C11099
E2000623188AAAC9F3E233EB253BDD8B0A4759A66A113E066238B0086AC1B634
5ABFF90E4B5ED3FA69C22541981B2BFC9710AEF6B50A8BB53431C7B4D380D721
639E005D6B4688EE16BFF48443E7C9E5FB5BC5883E271CB03428955D5B6A6C01
F9D9F44C93F0C94D9D0728D2B98C558E20C6DF38DA980247CC7320494E0ADE56
B2F1936E624CA50F8DD14C4674BD8164D73715D01E4845C4D0F9B44DFF396A3C
73954C42DB561C79655F0ACFB39BDEF99E91B69C462AE7D188A88871FC02E84F
B64D11F20453799F19073DAFCDA6BE29A327CA3A1B7B475033E246866AD6A5C9
CE63E677E66AE9EE18E12C91BF75ED357C599C9A3444E1595FBF981120D00727
B85DCAD9DE4BA1211A167D9AD853DC4CE60691A761FEEC7306D80D36CCA55E80
26D1B1AC2FB42CFA5B30DA798C0A830C69BB2C71F7428375D75CD6C9AA1D742B
8A2BBB915E4CCDB69681C7726D78EF2C675DFCE211C6ED0F44B35EFBA9DAE2DC
765D21E1164E195825B688B71A9296EA8873B321A64BD8B7B3BB06EED710B183
D7B5A4469FC3CC45267DE00F267774DCE23A74A4C6F977C8C0EBD9B312AED9AA
3EB9CE2B8132FE3B8CC114169B93FF4FE2EDB053FA42B50206FAF075F15BE61D
870FB5A524F6DDA969F66479A695CA828FA647E7135007C38E73408787A2BC36
FE411C5D5F976192C0C01CBAC5FB2B6057C83F8897740D4C6C7E349829FE59DD
AAE29A018EFB4B9ECE79BF134721FFEB19581802B6444839CFCF6E0193E1AB10
0CCA4D53B084BA6C124B588B922565ABA2C79876D2FE23C6B3EEDD6589CB5BCF
5B454AECC151734F626650083CC3962090AFA6E10FD7120C46E2642CFA19
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMMI10
%!PS-AdobeFont-1.1: CMMI10 1.100
%%CreationDate: 1996 Jul 23 07:53:57
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.100) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMMI10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.04 def
/isFixedPitch false def
end readonly def
/FontName /CMMI10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 58 /period put
dup 59 /comma put
dup 99 /c put
dup 101 /e put
dup 102 /f put
dup 120 /x put
dup 121 /y put
readonly def
/FontBBox{-32 -250 1048 750}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA0529731C99A784CCBE85B4993B2EEBDE
3B12D472B7CF54651EF21185116A69AB1096ED4BAD2F646635E019B6417CC77B
532F85D811C70D1429A19A5307EF63EB5C5E02C89FC6C20F6D9D89E7D91FE470
B72BEFDA23F5DF76BE05AF4CE93137A219ED8A04A9D7D6FDF37E6B7FCDE0D90B
986423E5960A5D9FBB4C956556E8DF90CBFAEC476FA36FD9A5C8175C9AF513FE
D919C2DDD26BDC0D99398B9F4D03D5993DFC0930297866E1CD0A319B6B1FD958
9E394A533A081C36D456A09920001A3D2199583EB9B84B4DEE08E3D12939E321
990CD249827D9648574955F61BAAA11263A91B6C3D47A5190165B0C25ABF6D3E
6EC187E4B05182126BB0D0323D943170B795255260F9FD25F2248D04F45DFBFB
DEF7FF8B19BFEF637B210018AE02572B389B3F76282BEB29CC301905D388C721
59616893E774413F48DE0B408BC66DCE3FE17CB9F84D205839D58014D6A88823
D9320AE93AF96D97A02C4D5A2BB2B8C7925C4578003959C46E3CE1A2F0EAC4BF
8B9B325E46435BDE60BC54D72BC8ACB5C0A34413AC87045DC7B84646A324B808
6FD8E34217213E131C3B1510415CE45420688ED9C1D27890EC68BD7C1235FAF9
1DAB3A369DD2FC3BE5CF9655C7B7EDA7361D7E05E5831B6B8E2EEC542A7B38EE
03BE4BAC6079D038ACB3C7C916279764547C2D51976BABA94BA9866D79F13909
95AA39B0F03103A07CBDF441B8C5669F729020AF284B7FF52A29C6255FCAACF1
74109050FBA2602E72593FBCBFC26E726EE4AEF97B7632BC4F5F353B5C67FED2
3EA752A4A57B8F7FEFF1D7341D895F0A3A0BE1D8E3391970457A967EFF84F6D8
47750B1145B8CC5BD96EE7AA99DDC9E06939E383BDA41175233D58AD263EBF19
AFC0E2F840512D321166547B306C592B8A01E1FA2564B9A26DAC14256414E4C8
42616728D918C74D13C349F4186EC7B9708B86467425A6FDB3A396562F7EE4D8
40B43621744CF8A23A6E532649B66C2A0002DD04F8F39618E4F572819DD34837
B5A08E643FDCA1505AF6A1FA3DDFD1FA758013CAED8ACDDBBB334D664DFF5B53
956017667C419C4021DA92976C7550A196C257FC2124E6F6653FAEA9ECD781C6
793D55009809849DCD349D18C46B7072E96A292E937463E1671EFEF393030EF2
3127AEE8F957106A8BAE6B4C2B8779DF8696E89827FE9B259B0DFF68CC6E69FC
79E59581CCFF1C6888227C58AB77070D16BCCB082108F0B19C1A212F69FB9D2B
723C0E2FBB76D3D722CD5699473E25CE8E77558614157EF67DD4951837D3D18E
6FC510C2E95C238B8E003EFFB8323FFE35181958AFC060D23E365EF74E5622C7
21582D0142399F46C786E6F008CED61262AD5BD5B42A2D64DA6953D8C93F9A96
280757E58B3F12918386DFADADABEE281D31618FD7A6B09EDEF1811575B45563
17CAFD76ABF50A5456F6FF3FD62DF994C484CC2CB19566C1178334575E9063CD
FB7DB158C2EF492801924F54935B9CE774ECD0D20E4FEC1565D4E346F374D29C
BD70E02027F1B8866A972628313AC0D676A5C7F206176C8AF4024EAD2F7EB361
629CC0D2CB9D31311047B2C1890B583BF0D813E2D3FBBB3D44C74BE0AC4A5FA8
CE5418A3680E839E79A1BC70F876345D74C48B232147B1C5C2B2647A234B8482
E42C1670FA26FA976403CAE76D99C1E06831EE83693A48D56DE133A5E3D2B7EC
5C167A9743DCABAE3547FD845844F3A047449F8C998E431CC47551BB0D643F02
52B5D0EA3D69934FA539A4E475B8BBE6ECC9B5151604ADAEB437ABB0F6EB291D
B27FAA6378E2787375A5B70CDC3A1678BF499813126837ABDD85CD61AB25F4B4
5A1A5BFFE3CAC49C9E5DD5A263AE8B32BD580D7F828497E6F2C74ECC8521F05B
7BD359682C1ABF6C6AFAF0733902FEB5D110F3A8B1691F5DBEFC892890F613F3
7AADA3FBADC497786133BB1D93679984604B233A073663A902BA5445F7308392
0F2A75B20CC9EF85EE5B6AB54C70494DB72687342A97426537E63A4676944679
B647AED9050C89C37CDAB35270A0E949F5081751833AEA86891A0D13B599AD60
0CB97558A3E9DAC4CA75E06FE5B3249C7A4CED1017FA3C4D6E44E8242D49E520
E04C33111CF7B9358A9A4C58BA36CE8824C0B45D02BB3323166CD8A8D6911A47
C11A74CFD83E0ED73FAF69433A5ACB7394131DF79468D7876C5C905773FEB935
367E68F074F3B0BA6F74F160DFC74B6425A78B6F6FD5F5657CC886E1ECA484E1
54F59EAD47F87B77F42C931A9959241511BFF891A879ADDB30C8E8D1F39F0437
CD5A5E240AFBA4711A57A7D0814228DC27506E91F3C62C49CB2EF99B9035E402
8C9C6030305709B834B4F25E519565F3E6075ACBAD9720F059BBDCC6578EE4FE
CA2ED94A9A2BC4BAD69E7FED2DD3E13B0E279D55A2E171077A08B0AA64E999FF
D0CCFB4AE9BDB80576A82B224A900107DB6ED29FE2CCA9560F2098D639CAD174
D0BD53FB5A8374AAE0AAF1936FCE5B9D692DFE2D34F0C600A2F3DBCD2B1E19D2
A42D8F0581234F0174680B6CA105AD267C65F7A7BD60735EF05F215F62D39FF6
2E8193A07014E5F2B5CAB84352C462414EB12A1EBD47D747CBA4B615B58A0560
06448FB3D4F514557A0A8BFDAB9B30559921043300D1383FFF1267BFAAA5B30B
50C4FE6BF9B599D77624E22AC5D7435CCE5DB5DC083E423438BB41C9AC52A609
9D631B0382B2B1E93A7B55EB79E87D51FD3F3E4A89B9351B39323C65309FD03B
BCF9138E544A7A0D88032191D5D03C17A81B0D3C9212F9D5CD1AF9FC7873B2CA
FCD9CE788030E99580FC96A983BCED606971C0C434BF97D6E47650DE14AE49E5
523F3603D3A32F628CA5371EF2786EFD869F9628DBC635A190DD374D5592A2E0
A2D0FD8634D5F4CD508196A708
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
TeXDict begin 39158280 55380996 1000 600 600 (node-contract.dvi)
@start /Fa 136[44 1[44 44 44 44 3[44 44 3[44 44 44 1[44
3[44 97[{}12 83.022 /t1xbtt rf /Fb 145[41 38[52 5[50
65[{}3 58.1154 /CMMI7 rf /Fc 206[33 49[{}1 58.1154 /CMR7
rf /Fd 194[65 19[32 32 40[{}3 83.022 /CMR10 rf /Fe 134[41
47 17[41 39 1[36 39[23 23 58[{}7 83.022 /CMMI10 rf end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 600dpi
TeXDict begin
%%PaperSize: A4
end
%%EndSetup
%%Page: 1 1
TeXDict begin 1 0 bop 0 0 a
SDict begin /product where{pop product(Distiller)search{pop pop pop
version(.)search{exch pop exch pop(3011)eq{gsave newpath 0 0 moveto
closepath clip/Courier findfont 10 scalefont setfont 72 72 moveto(.)show
grestore}if}{pop}ifelse}{pop}ifelse}if end
0 0 a 0 0 a
SDict begin [ /Title () /Subject () /Creator (LaTeX with hyperref package)
/Author () /Producer (dvips + Distiller) /Keywords () /DOCINFO pdfmark
end
0 0 a 0 TeXcolorgray
144 34 a
SDict begin H.S end
144 34 a 0 TeXcolorgray 0 TeXcolorgray 144 34
a
SDict begin H.R end
144 34 a 144 34 a
SDict begin [ /View [/XYZ H.V] /Dest (page.1) cvn H.B /DEST pdfmark
end
144 34 a Black 0 TeXcolorgray 144
242 a
SDict begin [ /Page 1 /View [ /Fit ] /PageMode /UseOutlines /DOCVIEW
pdfmark end
144 242 a 144 242 a
SDict begin [ {Catalog} << >> /PUT pdfmark end
144 242 a 144 242 a
SDict begin H.S end
144 242
a 144 242 a
SDict begin 12 H.A end
144 242 a 144 242 a
SDict begin [ /View [/XYZ H.V] /Dest (Doc-Start) cvn H.B /DEST pdfmark
end
144 242 a 798 313 a
798
313 a 798 313 a
pgfo
save
0 setgray
0.3985 pgfw
save
save
/pgfsc{0 setgray}def
save
/pgfsc{0 setgray}def
16.6039 126.59315 -63.29657 -8.30194 pgfe
gsave pgfsc pgfstr grestore newpath
restore
save
[1.0 0.0 0.0 1.0 -59.97601 -2.49069 ] concat
pgfs
0 setgray
798 313 a Fe(f)9 b Fd(\()p Fe(x)927 325
y Fc(1)964 313 y Fe(;)14 b(:)g(:)g(:)g(;)g(x)1196 325
y Fb(n)1241 313 y Fd(\))24 b(=)e(\()p Fe(y)1457 325 y
Fc(1)1495 313 y Fe(;)14 b(:)g(:)g(:)f(;)h(y)1720 325
y Fb(n)1765 313 y Fd(\))798 313 y
pgfr
restore
restore
save
/pgfsc{0 setgray}def
save
restore
save
/pgfsc{0 setgray}def
74.42967 147.14554 -63.29657 -82.73163 pgfe
-63.29657 -21.82733 moveto
83.84895 -21.82733 lineto
-63.29657 -38.82974 moveto
83.84895 -38.82974 lineto
gsave pgfsc pgfstr grestore newpath
restore
save
[1.0 0.0 0.0 1.0 -12.63988 -16.81311 ] concat
pgfs
0 setgray
798 313 a Fa(assume)25
b Fe(e)1126 325 y Fb(A)798 313 y
pgfr
restore
save
[1.0 0.0 0.0 1.0 -58.59467 -32.81923 ] concat
pgfs
0 setgray
798 313 a Fa(guarantee)f
Fe(e)1257 325 y Fb(G)1340 313 y Fa(with)i Fd(\()p Fe(c)1610
325 y Fc(1)1648 313 y Fe(;)14 b(:)g(:)g(:)f(;)h(c)1868
325 y Fb(n)1913 313 y Fd(\))798 313 y
pgfr
restore
save
[1.0 0.0 0.0 1.0 -59.77675 -63.27138 ] concat
pgfs
0 setgray
839 216 a Fe(y)880
228 y Fc(1)940 216 y Fd(=)23 b Fe(f)1069 228 y Fc(1)1106
216 y Fd(\()p Fe(x)1185 228 y Fc(1)1223 216 y Fe(;)14
b(:)g(:)g(:)f(;)h(x)1454 228 y Fb(n)1500 216 y Fe(;)g(c)1573
228 y Fc(1)1610 216 y Fe(;)g(:)g(:)g(:)g(;)g(c)1831 228
y Fb(n)1876 216 y Fd(\))839 316 y Fe(:)g(:)g(:)839 416
y(y)880 428 y Fb(n)948 416 y Fd(=)23 b Fe(f)1077 428
y Fb(n)1122 416 y Fd(\()p Fe(x)1201 428 y Fc(1)1239 416
y Fe(;)14 b(:)g(:)g(:)f(;)h(x)1470 428 y Fb(n)1516 416
y Fe(;)g(c)1589 428 y Fc(1)1626 416 y Fe(;)g(:)g(:)g(:)f(;)h(c)1846
428 y Fb(n)1891 416 y Fd(\))798 313 y
pgfr
restore
save
[1.0 0.0 0.0 1.0 -59.77675 -63.27138 ] concat
pgfs
798 313 a
pgfr
restore
restore
restore
newpath
restore
pgfc
0 TeXcolorgray
0 TeXcolorgray eop end
%%Trailer
userdict /end-hook known{end-hook}if
%%EOF

124
manual/figures/node-contract.tex Normal file
View file

@ -0,0 +1,124 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-clés)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}
\begin{contlsnode}{$f(\ton{x}{,}) = (\ton{y}{,})$}
$\Assume e_A$
\nodepart{second}
$\Guarantee e_G \With (\ton{c}{,})$
\nodepart{third}
\begin{varwidth}{\textwidth}
\[
\begin{array}{l}
y_1 = f_1(\ton{x}{,},\ton{c}{,})\\
\ldots\\
y_n = f_n(\ton{x}{,},\ton{c}{,})\\
\end{array}
\]
\end{varwidth}
\end{contlsnode}
\end{tikzpicture}
\end{document}

486
manual/figures/pds-subcomponents.eps Normal file
View file

@ -0,0 +1,486 @@
%!PS-Adobe-2.0 EPSF-2.0
%%Title: figures/pds-subcomponents.fig
%%Creator: fig2dev Version 3.2 Patchlevel 5a
%%CreationDate: Thu Jun 14 23:05:54 2012
%%BoundingBox: 0 0 130 130
%Magnification: 1.0000
%%EndComments
%%BeginProlog
/MyAppDict 100 dict dup begin def
/$F2psDict 200 dict def
$F2psDict begin
$F2psDict /mtrx matrix put
/col-1 {0 setgray} bind def
/col0 {0.000 0.000 0.000 srgb} bind def
/col1 {0.000 0.000 1.000 srgb} bind def
/col2 {0.000 1.000 0.000 srgb} bind def
/col3 {0.000 1.000 1.000 srgb} bind def
/col4 {1.000 0.000 0.000 srgb} bind def
/col5 {1.000 0.000 1.000 srgb} bind def
/col6 {1.000 1.000 0.000 srgb} bind def
/col7 {1.000 1.000 1.000 srgb} bind def
/col8 {0.000 0.000 0.560 srgb} bind def
/col9 {0.000 0.000 0.690 srgb} bind def
/col10 {0.000 0.000 0.820 srgb} bind def
/col11 {0.530 0.810 1.000 srgb} bind def
/col12 {0.000 0.560 0.000 srgb} bind def
/col13 {0.000 0.690 0.000 srgb} bind def
/col14 {0.000 0.820 0.000 srgb} bind def
/col15 {0.000 0.560 0.560 srgb} bind def
/col16 {0.000 0.690 0.690 srgb} bind def
/col17 {0.000 0.820 0.820 srgb} bind def
/col18 {0.560 0.000 0.000 srgb} bind def
/col19 {0.690 0.000 0.000 srgb} bind def
/col20 {0.820 0.000 0.000 srgb} bind def
/col21 {0.560 0.000 0.560 srgb} bind def
/col22 {0.690 0.000 0.690 srgb} bind def
/col23 {0.820 0.000 0.820 srgb} bind def
/col24 {0.500 0.190 0.000 srgb} bind def
/col25 {0.630 0.250 0.000 srgb} bind def
/col26 {0.750 0.380 0.000 srgb} bind def
/col27 {1.000 0.500 0.500 srgb} bind def
/col28 {1.000 0.630 0.630 srgb} bind def
/col29 {1.000 0.750 0.750 srgb} bind def
/col30 {1.000 0.880 0.880 srgb} bind def
/col31 {1.000 0.840 0.000 srgb} bind def
end
% This junk string is used by the show operators
/PATsstr 1 string def
/PATawidthshow { % cx cy cchar rx ry string
% Loop over each character in the string
{ % cx cy cchar rx ry char
% Show the character
dup % cx cy cchar rx ry char char
PATsstr dup 0 4 -1 roll put % cx cy cchar rx ry char (char)
false charpath % cx cy cchar rx ry char
/clip load PATdraw
% Move past the character (charpath modified the
% current point)
currentpoint % cx cy cchar rx ry char x y
newpath
moveto % cx cy cchar rx ry char
% Reposition by cx,cy if the character in the string is cchar
3 index eq { % cx cy cchar rx ry
4 index 4 index rmoveto
} if
% Reposition all characters by rx ry
2 copy rmoveto % cx cy cchar rx ry
} forall
pop pop pop pop pop % -
currentpoint
newpath
moveto
} bind def
/PATcg {
7 dict dup begin
/lw currentlinewidth def
/lc currentlinecap def
/lj currentlinejoin def
/ml currentmiterlimit def
/ds [ currentdash ] def
/cc [ currentrgbcolor ] def
/cm matrix currentmatrix def
end
} bind def
% PATdraw - calculates the boundaries of the object and
% fills it with the current pattern
/PATdraw { % proc
save exch
PATpcalc % proc nw nh px py
5 -1 roll exec % nw nh px py
newpath
PATfill % -
restore
} bind def
% PATfill - performs the tiling for the shape
/PATfill { % nw nh px py PATfill -
PATDict /CurrentPattern get dup begin
setfont
% Set the coordinate system to Pattern Space
PatternGState PATsg
% Set the color for uncolored pattezns
PaintType 2 eq { PATDict /PColor get PATsc } if
% Create the string for showing
3 index string % nw nh px py str
% Loop for each of the pattern sources
0 1 Multi 1 sub { % nw nh px py str source
% Move to the starting location
3 index 3 index % nw nh px py str source px py
moveto % nw nh px py str source
% For multiple sources, set the appropriate color
Multi 1 ne { dup PC exch get PATsc } if
% Set the appropriate string for the source
0 1 7 index 1 sub { 2 index exch 2 index put } for pop
% Loop over the number of vertical cells
3 index % nw nh px py str nh
{ % nw nh px py str
currentpoint % nw nh px py str cx cy
2 index oldshow % nw nh px py str cx cy
YStep add moveto % nw nh px py str
} repeat % nw nh px py str
} for
5 { pop } repeat
end
} bind def
% PATkshow - kshow with the current pattezn
/PATkshow { % proc string
exch bind % string proc
1 index 0 get % string proc char
% Loop over all but the last character in the string
0 1 4 index length 2 sub {
% string proc char idx
% Find the n+1th character in the string
3 index exch 1 add get % string proc char char+1
exch 2 copy % strinq proc char+1 char char+1 char
% Now show the nth character
PATsstr dup 0 4 -1 roll put % string proc chr+1 chr chr+1 (chr)
false charpath % string proc char+1 char char+1
/clip load PATdraw
% Move past the character (charpath modified the current point)
currentpoint newpath moveto
% Execute the user proc (should consume char and char+1)
mark 3 1 roll % string proc char+1 mark char char+1
4 index exec % string proc char+1 mark...
cleartomark % string proc char+1
} for
% Now display the last character
PATsstr dup 0 4 -1 roll put % string proc (char+1)
false charpath % string proc
/clip load PATdraw
neewath
pop pop % -
} bind def
% PATmp - the makepattern equivalent
/PATmp { % patdict patmtx PATmp patinstance
exch dup length 7 add % We will add 6 new entries plus 1 FID
dict copy % Create a new dictionary
begin
% Matrix to install when painting the pattern
TilingType PATtcalc
/PatternGState PATcg def
PatternGState /cm 3 -1 roll put
% Check for multi pattern sources (Level 1 fast color patterns)
currentdict /Multi known not { /Multi 1 def } if
% Font dictionary definitions
/FontType 3 def
% Create a dummy encoding vector
/Encoding 256 array def
3 string 0 1 255 {
Encoding exch dup 3 index cvs cvn put } for pop
/FontMatrix matrix def
/FontBBox BBox def
/BuildChar {
mark 3 1 roll % mark dict char
exch begin
Multi 1 ne {PaintData exch get}{pop} ifelse % mark [paintdata]
PaintType 2 eq Multi 1 ne or
{ XStep 0 FontBBox aload pop setcachedevice }
{ XStep 0 setcharwidth } ifelse
currentdict % mark [paintdata] dict
/PaintProc load % mark [paintdata] dict paintproc
end
gsave
false PATredef exec true PATredef
grestore
cleartomark % -
} bind def
currentdict
end % newdict
/foo exch % /foo newlict
definefont % newfont
} bind def
% PATpcalc - calculates the starting point and width/height
% of the tile fill for the shape
/PATpcalc { % - PATpcalc nw nh px py
PATDict /CurrentPattern get begin
gsave
% Set up the coordinate system to Pattern Space
% and lock down pattern
PatternGState /cm get setmatrix
BBox aload pop pop pop translate
% Determine the bounding box of the shape
pathbbox % llx lly urx ury
grestore
% Determine (nw, nh) the # of cells to paint width and height
PatHeight div ceiling % llx lly urx qh
4 1 roll % qh llx lly urx
PatWidth div ceiling % qh llx lly qw
4 1 roll % qw qh llx lly
PatHeight div floor % qw qh llx ph
4 1 roll % ph qw qh llx
PatWidth div floor % ph qw qh pw
4 1 roll % pw ph qw qh
2 index sub cvi abs % pw ph qs qh-ph
exch 3 index sub cvi abs exch % pw ph nw=qw-pw nh=qh-ph
% Determine the starting point of the pattern fill
%(px, py)
4 2 roll % nw nh pw ph
PatHeight mul % nw nh pw py
exch % nw nh py pw
PatWidth mul exch % nw nh px py
end
} bind def
% Save the original routines so that we can use them later on
/oldfill /fill load def
/oldeofill /eofill load def
/oldstroke /stroke load def
/oldshow /show load def
/oldashow /ashow load def
/oldwidthshow /widthshow load def
/oldawidthshow /awidthshow load def
/oldkshow /kshow load def
% These defs are necessary so that subsequent procs don't bind in
% the originals
/fill { oldfill } bind def
/eofill { oldeofill } bind def
/stroke { oldstroke } bind def
/show { oldshow } bind def
/ashow { oldashow } bind def
/widthshow { oldwidthshow } bind def
/awidthshow { oldawidthshow } bind def
/kshow { oldkshow } bind def
/PATredef {
MyAppDict begin
{
/fill { /clip load PATdraw newpath } bind def
/eofill { /eoclip load PATdraw newpath } bind def
/stroke { PATstroke } bind def
/show { 0 0 null 0 0 6 -1 roll PATawidthshow } bind def
/ashow { 0 0 null 6 3 roll PATawidthshow }
bind def
/widthshow { 0 0 3 -1 roll PATawidthshow }
bind def
/awidthshow { PATawidthshow } bind def
/kshow { PATkshow } bind def
} {
/fill { oldfill } bind def
/eofill { oldeofill } bind def
/stroke { oldstroke } bind def
/show { oldshow } bind def
/ashow { oldashow } bind def
/widthshow { oldwidthshow } bind def
/awidthshow { oldawidthshow } bind def
/kshow { oldkshow } bind def
} ifelse
end
} bind def
false PATredef
% Conditionally define setcmykcolor if not available
/setcmykcolor where { pop } {
/setcmykcolor {
1 sub 4 1 roll
3 {
3 index add neg dup 0 lt { pop 0 } if 3 1 roll
} repeat
setrgbcolor - pop
} bind def
} ifelse
/PATsc { % colorarray
aload length % c1 ... cn length
dup 1 eq { pop setgray } { 3 eq { setrgbcolor } { setcmykcolor
} ifelse } ifelse
} bind def
/PATsg { % dict
begin
lw setlinewidth
lc setlinecap
lj setlinejoin
ml setmiterlimit
ds aload pop setdash
cc aload pop setrgbcolor
cm setmatrix
end
} bind def
/PATDict 3 dict def
/PATsp {
true PATredef
PATDict begin
/CurrentPattern exch def
% If it's an uncolored pattern, save the color
CurrentPattern /PaintType get 2 eq {
/PColor exch def
} if
/CColor [ currentrgbcolor ] def
end
} bind def
% PATstroke - stroke with the current pattern
/PATstroke {
countdictstack
save
mark
{
currentpoint strokepath moveto
PATpcalc % proc nw nh px py
clip newpath PATfill
} stopped {
(*** PATstroke Warning: Path is too complex, stroking
with gray) =
cleartomark
restore
countdictstack exch sub dup 0 gt
{ { end } repeat } { pop } ifelse
gsave 0.5 setgray oldstroke grestore
} { pop restore pop } ifelse
newpath
} bind def
/PATtcalc { % modmtx tilingtype PATtcalc tilematrix
% Note: tiling types 2 and 3 are not supported
gsave
exch concat % tilingtype
matrix currentmatrix exch % cmtx tilingtype
% Tiling type 1 and 3: constant spacing
2 ne {
% Distort the pattern so that it occupies
% an integral number of device pixels
dup 4 get exch dup 5 get exch % tx ty cmtx
XStep 0 dtransform
round exch round exch % tx ty cmtx dx.x dx.y
XStep div exch XStep div exch % tx ty cmtx a b
0 YStep dtransform
round exch round exch % tx ty cmtx a b dy.x dy.y
YStep div exch YStep div exch % tx ty cmtx a b c d
7 -3 roll astore % { a b c d tx ty }
} if
grestore
} bind def
/PATusp {
false PATredef
PATDict begin
CColor PATsc
end
} bind def
% right45
11 dict begin
/PaintType 1 def
/PatternType 1 def
/TilingType 1 def
/BBox [0 0 1 1] def
/XStep 1 def
/YStep 1 def
/PatWidth 1 def
/PatHeight 1 def
/Multi 2 def
/PaintData [
{ clippath } bind
{ 20 20 true [ 20 0 0 -20 0 20 ]
{<0040100080200100400200800401000802001004
0020080040100080200000401000802001004002
0080040100080200100400200800401000802000>}
imagemask } bind
] def
/PaintProc {
pop
exec fill
} def
currentdict
end
/P5 exch def
/cp {closepath} bind def
/ef {eofill} bind def
/gr {grestore} bind def
/gs {gsave} bind def
/sa {save} bind def
/rs {restore} bind def
/l {lineto} bind def
/m {moveto} bind def
/rm {rmoveto} bind def
/n {newpath} bind def
/s {stroke} bind def
/sh {show} bind def
/slc {setlinecap} bind def
/slj {setlinejoin} bind def
/slw {setlinewidth} bind def
/srgb {setrgbcolor} bind def
/rot {rotate} bind def
/sc {scale} bind def
/sd {setdash} bind def
/ff {findfont} bind def
/sf {setfont} bind def
/scf {scalefont} bind def
/sw {stringwidth} bind def
/tr {translate} bind def
/tnt {dup dup currentrgbcolor
4 -2 roll dup 1 exch sub 3 -1 roll mul add
4 -2 roll dup 1 exch sub 3 -1 roll mul add
4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
bind def
/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
4 -2 roll mul srgb} bind def
/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
/$F2psEnd {$F2psEnteredState restore end} def
/pageheader {
save
newpath 0 130 moveto 0 0 lineto 130 0 lineto 130 130 lineto closepath clip newpath
0.8 114.1 translate
1 -1 scale
$F2psBegin
10 setmiterlimit
0 slj 0 slc
0.06299 0.06299 sc
} bind def
/pagefooter {
$F2psEnd
restore
} bind def
%%EndProlog
pageheader
%
% Fig objects follow
%
%
% here starts figure with depth 50
% Polyline
0 slj
0 slc
7.500 slw
n 0 0 m 2025 0 l 2025 1800 l 0 1800 l
cp gs /PC [[1.00 1.00 1.00] [0.00 0.00 0.00]] def
15.00 15.00 sc P5 [16 0 0 -16 0.00 0.00] PATmp PATsp ef gr PATusp gs col0 s gr
% here ends figure;
%
% here starts figure with depth 45
% Polyline
0 slj
0 slc
7.500 slw
n 0 -225 m 225 -225 l 225 0 l 0 0 l
cp gs col-1 s gr
% Polyline
0.000 slw
n 765 720 m 675 810 l 1170 1035 l 1260 945 l 810 765 l
cp gs col7 1.00 shd ef gr
% Polyline
n 135 1485 m 360 1485 l 360 1710 l 135 1710 l
cp gs col7 1.00 shd ef gr
% here ends figure;
%
% here starts figure with depth 40
% Polyline
0 slj
0 slc
7.500 slw
n 225 225 m 675 225 l 675 675 l 225 675 l
cp gs col7 1.00 shd ef gr gs col0 s gr
% Polyline
n 1350 1125 m 1800 1125 l 1800 1575 l 1350 1575 l
cp gs col7 1.00 shd ef gr gs col0 s gr
% Polyline
15.000 slw
[30] 0 sd
n 810 810 m
1215 990 l gs col7 1.00 shd ef gr gs col0 s gr [] 0 sd
% here ends figure;
pagefooter
showpage
%%Trailer
end
%EOF

29
manual/figures/pds-subcomponents.fig Normal file
View file

@ -0,0 +1,29 @@
#FIG 3.2 Produced by xfig version 3.2.5
Landscape
Center
Metric
A4
100.00
Single
-2
1200 2
6 -90 -225 270 0
2 2 0 1 -1 7 45 -1 -1 3.000 0 0 -1 0 0 5
0 -225 225 -225 225 0 0 0 0 -225
4 1 -1 40 -1 0 12 0.0000 6 180 330 90 -45 $S$\001
-6
2 2 0 1 0 7 40 -1 20 0.000 0 0 -1 0 0 5
225 225 675 225 675 675 225 675 225 225
2 2 0 1 0 7 40 -1 20 0.000 0 0 -1 0 0 5
1350 1125 1800 1125 1800 1575 1350 1575 1350 1125
2 3 0 0 -1 7 45 -1 20 1.500 0 0 -1 0 0 6
765 720 675 810 1170 1035 1260 945 810 765 765 720
2 1 1 2 0 7 40 -1 20 2.000 0 0 -1 0 0 2
810 810 1215 990
2 2 0 1 0 7 50 -1 45 0.000 0 0 -1 0 0 5
0 0 2025 0 2025 1800 0 1800 0 0
2 2 0 0 -1 7 45 -1 20 0.000 0 0 -1 0 0 5
135 1485 360 1485 360 1710 135 1710 135 1485
4 1 -1 35 -1 0 12 0.0000 6 210 540 450 540 $S_1$\001
4 1 -1 35 -1 0 12 0.0000 6 210 540 1575 1440 $S_n$\001
4 1 -1 40 -1 0 12 0.0000 6 180 375 225 1665 $S'$\001

BIN
manual/figures/pds-subcomponents.pdf Normal file
View file

Binary file not shown.

16
manual/figures/pds-subcomponents.tex Normal file
View file

@ -0,0 +1,16 @@
\begin{picture}(0,0)%
\includegraphics{figures/pds-subcomponents}%
\end{picture}%
\setlength{\unitlength}{4144sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2{%
\fontsize{#1}{#2pt}%
\selectfont}%
\fi\endgroup%
\begin{picture}(2049,2049)(-11,-973)
\put( 91,884){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}$S$}}}}
\put(226,-826){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}$S'$}}}}
\put(451,299){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}$S_1$}}}}
\put(1576,-601){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}$S_n$}}}}
\end{picture}%

2851
manual/figures/struct-pg-f.eps Normal file
View file

File diff suppressed because it is too large Load diff

2902
manual/figures/struct-pg-f.ps Normal file
View file

File diff suppressed because it is too large Load diff

120
manual/figures/struct-pg-f.tex Normal file
View file

@ -0,0 +1,120 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-cles)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}
\begin{lsnode}{$f(c,d) = y$}
\begin{scope}[node distance=3cm,auto,initial text=,initial where=left,pos=0.5]
\draw node[state,initial,label={above:$y=\False$}] (A) {A};
\draw node[state,label={below left:$y=\True$}] (C) [below of=A] {C};
\draw node[state,label={right:$y=g(c,d)$}] (B) [right of=C] {B};
\path[->] (A) edge [bend left] node {$c$} (B)
(B) edge [bend left] node {$c\land d$} (C)
(C) edge [bend left] node {$d$} (A);
\end{scope}
\end{lsnode}
\end{tikzpicture}
\end{document}

2306
manual/figures/struct-pg-g.eps Normal file
View file

File diff suppressed because it is too large Load diff

2355
manual/figures/struct-pg-g.ps Normal file
View file

File diff suppressed because it is too large Load diff

121
manual/figures/struct-pg-g.tex Normal file
View file

@ -0,0 +1,121 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-cles)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}
% \begin{lsnode}{$g(a,b) = y$}
% \g{a}{b}{y}
% \end{lsnode}
\begin{lsnode}{$g(a,b) = y$}
\matrix (m) [matrix of nodes] {
\node{$y_1 = h(a,c)$};\\
\node{$y_2 = h(b,d)$};\\
\node{$y = y_1\land y_2$};\\
};
\draw [dashed] (m-1-1.south west) -- (m-1-1.south east);
\draw [dashed] (m-2-1.south west) -- (m-2-1.south east);
\end{lsnode}
\end{tikzpicture}
\end{document}

2779
manual/figures/struct-pg-h.eps Normal file
View file

File diff suppressed because it is too large Load diff

2830
manual/figures/struct-pg-h.ps Normal file
View file

File diff suppressed because it is too large Load diff

118
manual/figures/struct-pg-h.tex Normal file
View file

@ -0,0 +1,118 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-cles)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}
\begin{lsnode}{$h(a,b) = y$}
\begin{scope}[node distance=2cm,auto,initial text=,initial where=left]
\draw node[state,initial,label={right:$y=\False$}] (Idle) {Idle};
\draw node[state,label={right:$y=\True$}] (Active) [below of=Idle] {Act};
\path[->] (Idle) edge [bend left] node {$a\land b$} (Active)
(Active) edge [bend left] node {$a$} (Idle);
\end{scope}
\end{lsnode}
\end{tikzpicture}
\end{document}

6291
manual/figures/struct-pg.eps Normal file
View file

File diff suppressed because it is too large Load diff

4091
manual/figures/struct-pg.epsi Normal file
View file

File diff suppressed because it is too large Load diff

BIN
manual/figures/struct-pg.pdf Normal file
View file

Binary file not shown.

4147
manual/figures/struct-pg.ps Normal file
View file

File diff suppressed because it is too large Load diff

173
manual/figures/struct-pg.tex Normal file
View file

@ -0,0 +1,173 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
\usepackage{lmodern}
\usepackage{varwidth}
\usepackage{tikz}
%\usetikzlibrary{arrows}
\usetikzlibrary{automata}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-cles)
\renewcommand{\ttdefault}{txtt}
% Figures tikz
\tikzstyle{hierarchical state} =
[rectangle,
round corners,
draw=black]
\tikzstyle{ls node} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{file} =
[rectangle,
sharp corners,
draw=black]
\tikzstyle{tool} =
[rectangle,
rounded corners,
draw=black]
\newenvironment{lsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,
anchor=north west,
yshift=\pgflinewidth]
\bgroup
\begin{varwidth}{0.9\textwidth}
\centering
\begin{tikzpicture}[%
node distance=8mm,
pin distance=8mm,
label distance=2mm,
inner sep=1mm,
anchor=center,
pos=0.5,
#1]% optional parameter(s)
}{%
\end{tikzpicture}
\end{varwidth}
\egroup;
}
\newenvironment{contlsnode}[2][]{
\node[% title
ls node
% fill=blue!90!black,
] (title) {#2};% title text
\node at (title.south west) [%
ls node,rectangle split, rectangle split parts=3,
anchor=north west,text badly ragged,
yshift=\pgflinewidth]
\bgroup
% \begin{varwidth}{0.9\textwidth}
% \centering
% \begin{tikzpicture}[%
% node distance=8mm,
% pin distance=8mm,
% label distance=-0.5mm,
% inner sep=1mm,
% anchor=center,
% pos=0.5,
% #1]% optional parameter(s)
}{%
% \end{tikzpicture}
% \end{varwidth}
\egroup;
}
\pagestyle{empty}
\begin{document}
\centering
\begin{tikzpicture}
\begin{lsnode}{$h(a,b) = y$}
\begin{scope}[node distance=2cm,auto,initial text=,initial where=left]
\draw node[state,initial,label={right:$y=\False$}] (Idle) {Idle};
\draw node[state,label={right:$y=\True$}] (Active) [below of=Idle] {Act};
\path[->] (Idle) edge [bend left] node {$a\land b$} (Active)
(Active) edge [bend left] node {$a$} (Idle);
\end{scope}
\end{lsnode}
\end{tikzpicture}
\medskip
\newsavebox{\boite}
\begin{lrbox}{\boite}
\begin{varwidth}{\textwidth}
\begin{tikzpicture}
\matrix (m) [matrix of nodes] {
\node{$y_1 = h(a,c)$};\\
\node{$y_2 = h(b,d)$};\\
\node{$y = y_1\land y_2$};\\
};
\draw [dashed] (m-1-1.south west) -- (m-1-1.south east);
\draw [dashed] (m-2-1.south west) -- (m-2-1.south east);
\end{tikzpicture}
\end{varwidth}
\end{lrbox}
% $\Assume \True$
% \nodepart{second}
% $\Enforce (\Not y) \With (c,d)$
% \nodepart{third}
% \usebox{\boite}
\begin{tikzpicture}
% \begin{lsnode}{$g(a,b) = y$}
% \g{a}{b}{y}
% \end{lsnode}
\begin{lsnode}{$g(a,b) = y$}
\matrix (m) [matrix of nodes] {
\node{$y_1 = h(a,c)$};\\
\node{$y_2 = h(b,d)$};\\
\node{$y = y_1\land y_2$};\\
};
\draw [dashed] (m-1-1.south west) -- (m-1-1.south east);
\draw [dashed] (m-2-1.south west) -- (m-2-1.south east);
\end{lsnode}
\end{tikzpicture}
\medskip
\begin{tikzpicture}
\begin{lsnode}{$f(c,d) = y$}
\begin{scope}[node distance=3cm,auto,initial text=,initial where=left,pos=0.5]
\draw node[state,initial,label={above:$y=\False$}] (A) {A};
\draw node[state,label={below left:$y=\True$}] (C) [below of=A] {C};
\draw node[state,label={right:$y=g(c,d)$}] (B) [right of=C] {B};
\path[->] (A) edge [bend left] node {$c$} (B)
(B) edge [bend left] node {$c\land d$} (C)
(C) edge [bend left] node {$d$} (A);
\end{scope}
\end{lsnode}
\end{tikzpicture}
\end{document}

BIN
manual/heptagon-manual.pdf Normal file
View file

Binary file not shown.

827
manual/heptagon-manual.tex Normal file
View file

@ -0,0 +1,827 @@
\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper]{geometry}
%\usepackage[francais]{babel}
%\usepackage{subfigure}
%\usepackage{fancyvrb}
%\usepackage{fancyhdr}
\usepackage[hypertex,ps2pdf]{hyperref}
\usepackage{array}
\usepackage{xcolor}
%\usepackage{comment}
%\usepackage{lmodern}
\usepackage{varwidth}
%\usepackage{tikz}
%\usetikzlibrary{arrows}
%\usetikzlibrary{automata}
%\usetikzlibrary{matrix}
%\usetikzlibrary{shapes}
%\usetikzlibrary{positioning}
\usepackage{macros}
% fontes tt avec gras (mots-clés)
\renewcommand{\ttdefault}{txtt}
\lstset{
language=Heptagon,% numbers=left, numberstyle=\small,
basicstyle=\normalsize\ttfamily,captionpos=b,
frame={tb}, rulesep=1pt, columns=fullflexible,
xleftmargin=1cm, xrightmargin=1cm,
mathescape=true
}
\title{Heptagon/BZR manual}
\author{}
%\date{}
\begin{document}
\maketitle
\section{Introduction and tutorial}
\label{sec:intro}
\subsection{Heptagon: short presentation}
\label{sec:hept-short-pres}
Heptagon is a synchronous dataflow language, with a syntax allowing the
expression of control structures (e.g., switch or mode automata).
A typical Heptagon program will take as input a sequence of values, and will
output a sequence of values. Then, variables (inputs, outputs or locals) as well
as constants are actually variable or constant \emph{streams}. The usual
operators (e.g., arithmetic or Boolean operators) are applied pointwise on these
sequences of values.
For example, the Heptagon program below is composed of one node \texttt{plus},
performing the pointwise sum of its two integer inputs:
\begin{lstlisting}
node plus(x:int,y:int) returns (z:int)
let
z = x + y;
tel
\end{lstlisting}
\texttt{x} and \texttt{y} are the inputs of the node \texttt{plus}; \texttt{z}
is the output. \texttt{x}, \texttt{y} and \texttt{z} are of type \texttt{int},
denoting integer \emph{streams}. \texttt{z} is defined by the equation
\lstinline|z = x + y|.
An execution of the node \texttt{plus} can then be:
\[
\begin{streams}{5}
x & 1 & 2 & 3 & 4 & \ldots\\\hline
y & 1 & 2 & 1 & 2 & \ldots\\\hline
\mathtt{plus}(x,y) & 2 & 4 & 4 & 6 & \ldots\\
\end{streams}
\]
\subsection{Compilation}
\label{sec:compilation}
The Heptagon compiler is named \texttt{heptc}. Its list of options is available by
:
\begin{alltt}
> heptc -help
\end{alltt}
Every options described below are cumulable.
Assuming that the program to compile is in a file named \texttt{example.ept},
then one can compile it by typing :
\begin{alltt}
> heptc example.ept
\end{alltt}
However, such compilation will only perform standard analysis (such as typing,
causality, scheduling) and output intermediate object code, but not any final or
executable code.
The Heptagon compiler can thus generate code in some general languages, in order
to obtain either a standalone executable, or a linkable library. The target
language must then be given by the \texttt{-target} option:
\begin{alltt}
> heptc -target <language> example.ept
\end{alltt}
Where \texttt{<language>} is the name of the target language. For now, available
languages are C (\texttt{c} option) and Java (\texttt{java} option).
\subsection{Generated code}
\label{sec:generated-code}
The generic generated code consists, for each node, of two imperative functions:
\begin{itemize}
\item one ``reset'' function, used to reset the internal memory of the node;
\item one ``step'' function, taking as input the nodes inputs, and whose call
performs one step of the node, updates the memory, and outputs the nodes
outputs.
\end{itemize}
A standard way to execute Heptagon program is to compile the generated files
together with a main program of the following scheme :
\begin{alltt}
call the \textit{reset} function
for each instant
get the \textit{inputs} values
\textit{outputs} \(\leftarrow\) \textit{step(inputs)}
do something with \textit{outputs} values
\end{alltt}
Appendix~\ref{sec:app-generated-code} give specific technical details for each target language.
\subsection{Simulation}
\label{sec:simulation}
A graphical simulator is available: \texttt{hepts}. It allows the user to simulate
one node by providing a graphical window, where simulation steps can be
performed by providing inputs of the simulated node.
This simulator tool interacts with an executable, typically issued of Heptagon
programs compilation, and which await on the standard input the list of the
simulated node's inputs, and prints its outputs on the standard output. Such
executable, for the simulation of the node \texttt{f}, can be obtained by the
\texttt{-s <node>} option:
\begin{alltt}
> heptc -target c -s f example.ept
\end{alltt}
We can then directly compile the generated C program (whose main function stand
in the \texttt{\_main.c} file):
\begin{alltt}
> cd example_c
> gcc -Wall -c example.c
> gcc -Wall -c _main.c
> gcc -o f_sim _main.o example.o # \text{executable creation}
\end{alltt}
This executable \texttt{f\_sim} can then be used with the graphical simulator
\texttt{hepts}, which takes as argument:
\begin{itemize}
\item The name of the module (capitalized name of the program without the
\texttt{.ept} extension),
\item the name of the simulated node,
\item the path to the executable \texttt{f\_sim}.
\end{itemize}
\begin{alltt}
> hepts -mod Example -node f -exec example_c/f_sim
\end{alltt}
\section{Syntax and informal semantics}
\label{sec:synt-infor-sem}
Heptagon programs are synchronous Moore machines, with parallel and hierarchical
composition. The states of such machines define dataflow equations. The
Figure~\ref{fig:mixed-state-dataflow-example} gives an example of such program.
\begin{figure}[htbp]
\centering
\includegraphics{figures/mixed-state-df}
\caption{Mixed state and dataflow example}
\label{fig:mixed-state-dataflow-example}
\end{figure}
\subsection{Nodes}
\label{sec:nodes}
Heptagon programs are structured in \emph{nodes}: a program is a sequence of
nodes. A node is a subprogram with a name $f$, inputs $\ton{x}{,}$, outputs
$\ton[1][p]{y}{,}$, local variables $\ton[1][q]{z}{,}$ and declarations
$D$. $y_i$ and $z_i$ variables are to be defined in $D$, using operations
between values of $x_j$, $y_j$, $z_j$. Figure~\ref{fig:syntax-nodes} gives the
syntax of node definitions, together with a graphical syntax used in this
manuel\footnote{declaration of local variables are mandatory for the compiler in
the textual syntax, however we will sometimes omit it in the graphical syntax
for the sake of brevity}. The declaration of one variable comes with its type
($t_i$, $t'_i$ and $t''_i$ being the type of respectively $x_i$, $y_i$ and
$z_i$).
\begin{figure}[htb]
\centering
% \begin{varwidth}{\linewidth}
\[
\begin{array}{|c|c}
\cline{1-1}
f(x_1:t_1,\ldots,x_n:t_n) = y_1:t'_1,\ldots,y_p:t'_p & \\\hline
\multicolumn{2}{|c|}{}\\
\multicolumn{2}{|c|}{D}\\
\multicolumn{2}{|c|}{}\\\hline
\end{array}
\]
% \end{varwidth}\hspace{1cm}
% \begin{varwidth}{\linewidth}
\begin{lstlisting}
node f(x$_1$:t$_1$;$\ldots$;x$_n$:t$_n$) returns (y$_1$:t$'_1$,$\ldots$,y$_p$:t$'_p$)
var z$_1$:t$''_1$,$\ldots$,z$_q$:t$''_q$;
let
D
tel
\end{lstlisting}
% \end{varwidth}
\caption{Graphical and textual syntax of node definition}
\label{fig:syntax-nodes}
\end{figure}
The program of the Figure~\ref{fig:mixed-state-dataflow-example} can thus be
structured as the semantically equivalent program of the
Figure~\ref{fig:struct-prog-example}. The Figure~\ref{fig:textual-syntax} gives
the textual syntax of this program.
\begin{figure}[htbp]
\centering
\includegraphics{figures/struct-pg}
\caption{Structured program example}
\label{fig:struct-prog-example}
\end{figure}
\begin{figure}[htbp]
\centering
\begin{lstlisting}
node h(a:bool) returns (y:bool)
let
automaton
state Idle
do y = false
until a then Active
state Active
do y = true
until a then Idle
end
tel
node g (a,b:bool) returns (y:bool)
var y1,y2 : bool;
let
y = y1 & y2;
y1 = h(a);
y2 = h(b);
tel
node f (c,d:bool) returns (y:bool)
let
automaton
state A
do y = false
until c then B
state B
do y = g(c,d)
until c & d then C
state C
do y = true
until d then A
end
tel
\end{lstlisting}
\caption{Textual syntax}
\label{fig:textual-syntax}
\end{figure}
Heptagon allows to distinguish, by mean of clocks and control structures (switch,
automata), for declarations and expressions, the discrete instants of
activation, when the declarations and expressions are computed and progress
toward further states, and other instants when neither computation nor
progression are performed.
\subsection{Expressions}
\label{sec:expressions}
\subsubsection{Values and combinatorial operations}
\label{sec:variables-constants}
Heptagon is a dataflow language, i.e., every value, variable or constant, is
actually a stream of value. The usual operators (e.g., arithmetic or Boolean
operators) are applied pointwise on these sequences of values, as combinatorial
operations (as opposed to \emph{sequential} operations, taking into account the
current \emph{state} of the program: see delays in Section~\ref{sec:delays}).
Thus, \texttt{x} denotes the stream $x_1.x_2.\ldots$, and \lstinline|x + y| is
the stream defined by $($\lstinline|x + y|$)_i=x_i+y_i$.
\[
\begin{streams}{5}
\mathtt{x} & x_1 & x_2 & x_3 & x_4 & \ldots\\\hline
\mathtt{y} & y_1 & y_2 & y_3 & y_4 & \ldots\\\hline
\mathtt{x + y} & x_1+y_1 & x_2+y_2 & x_3+y_3 & x_4+y_4 & \ldots\\
\end{streams}
\]
\subsubsection{Delays}
\label{sec:delays}
Delays are the way to introduce some state in a Heptagon program.
\begin{itemize}
\item \lstinline|pre x| gives the value of \texttt{x} at the preceding
instant. The value at the first instant is undefined.
\item \lstinline|x -> y| takes the value of \texttt{x} at the first instant,
and then the value of \texttt{y};
\item \lstinline|x fby y| is equivalent to \lstinline|x -> pre y|.
\end{itemize}
\[
\begin{streams}{3}
\text{\lstinline|x|} & x_1 & x_2 & x_3 \\
\hline
\text{\lstinline|y|} & y_1 & y_2 & y_3 \\
\hline
\text{\lstinline|pre x|} & \perp & x_1 & x_2 \\
\hline
\text{\lstinline|x -> y|} & x_1 & y_2 & y_3 \\
\hline
\text{\lstinline|x fby y|} & x_1 & y_1 & y_2 \\
\end{streams}
\]
\subsection{Declarations}
\label{sec:declarations}
A declaration $D$ can be either :
\begin{itemize}
\item an equation $x = e$, defining variable $x$ by the expression $e$ at each
activation instants ;
\item a node application $(\tonp{y}{,}) = f(\ton{e}{,})$, defining variables
$\tonp{y}{,}$ by application of the node $f$ with values $\ton{e}{,}$ at each
activation instants ;
\item parallel declarations of $D_1$ and $D_2$, noted graphically $D_1\vdots
D_2$ and textually $D_1\Pv D_2$. Variables defined in $D_1$ and $D_2$ must be
exclusive. The activation of this parallel declaration activate both $D_1$ and
$D_2$, which are both computed and both progress ;
\item a switch control structure ;
\item an automaton.
\end{itemize}
\subsubsection{Switch control structures}
\label{sec:switch-contr-struct}
The \texttt{switch} control structure allows to controls which equations are
evaluated:
\begin{lstlisting}
type modes = Up | Down
node two(m:modes;v:int) returns (o:int)
var last x:int = 0;
let
o = x;
switch m
| Up do x = last x + v
| Down do x = last x - v
end
tel
\end{lstlisting}
The \texttt{last} keyword defines a memory which is shared by the different
modes. Thus, \lstinline|last x| is the value of the variable \texttt{x} in the
previous instant, whichever was the activated mode.
\subsubsection{Automata}
\label{sec:automata}
An automaton is a set of states (one of which being the initial one), and
transitions between these states, triggered by Boolean expressions. A
declaration is associated to each state. The set of variables defined by the
automaton is the union, not necessarily disjoint (variables can have different
definitions in different states, and can be partially defined : in this case,
when the variable is not defined in an active state, the previous value of this
variable is taken.
At each automaton activation instant, one and only one state of this automaton
is active (the initial one at the first activation instant). The declaration
associated to this active state is itself activated and progress in this
activation instant.
\paragraph{Example}
\label{sec:example}
The following example gives the node \texttt{updown}. This node is defined by an
automaton composed of two states:
\begin{itemize}
\item the state \texttt{Up} gives to \texttt{x} its previous value augmented of 1
\item the state \texttt{Down} gives to \texttt{x} its previous value diminued of 1
\end{itemize}
This automaton comprises two transitions:
\begin{itemize}
\item it goes from \texttt{Up} (the initial state) to \texttt{Down} when
\texttt{x} becomes greater or equal than 10;
\item it goes from \texttt{Down} to \texttt{Up} when \texttt{x} becomes less or
equal 0.
\end{itemize}
\begin{lstlisting}
node updown() returns (y:int)
var last x:int = 0;
let
y = x;
automaton
state Up
do x = last x + 1
until x >= 10 then Down
state Down
do x = last x - 1
until x <= 0 then Up
end
tel
\end{lstlisting}
\[
\begin{streams}{14}
\text{current state} & Up & Up & Up & Up & Up & Up & Up & Up & Up & Up & Down & Down & Down & \ldots\\\hline
\mathtt{y} & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 9 & 8 & 7 & \ldots\\\hline
\end{streams}
\]
Expressions on outgoing transitions of this active state are
evaluated, so as to compute the next active state : these are weak
transitions. Transitions are evaluated in declaration order, in the textual
syntax. If no transition can be triggered, then the current state is the next
active state.
\section{BZR: Contracts for controller synthesis}
\label{sec:extens-with-contr}
Contracts are an extension of the Heptagon language, so as to allow to perform
discrete controller synthesis on Heptagon programs. The extended language is
named BZR.
We associate to each node a \emph{contract}, which is a program associated with
two outputs :
\begin{itemize}
\item an output $e_A$ representing the environment model ;
\item an invariance objective $e_G$ ;
\item a set $\set{\ton{c}{,}}$ of controllable variables used for ensuring this objective.
\end{itemize}
This contract means that the node will be controlled, i.e., that values will be
given to $\ton{c}{,}$ such that, given any input trace yielding $e_A$, the
output trace will yield the true value for $e_G$.
\begin{center}
\includegraphics{figures/node-contract}
\end{center}
In the textual syntax, the contracts are noted :
\begin{lstlisting}
node f(x$_1$:t$_1$;$\ldots$;x$_n$:t$_n$) returns (y$_1$:t$'_1$;$\ldots$;y$_p$:t$'_p$)
contract
var $\ldots$
let
$\ldots$
tel
assume $e_A$
enforce $e_G$
with (c$_1$:t$''_1$;$\ldots$;c$_q$:t$''_n$)
var $\ldots$
let
y$_1$ = f$_1$($\ton{\mathtt{x}}{,},\ton[1][q]{\mathtt{c}}{,}$);
$\vdots$
y$_p$ = f$_p$($\ton{\mathtt{x}}{,},\ton[1][q]{\mathtt{c}}{,}$);
tel
\end{lstlisting}
\section{BZR Running Example: Multi-task System}
\label{sec:multi-task-system}
\subsection{Delayable Tasks}
\label{sec:delayable-tasks}
We consider a multi-task system composed of $n$ delayable
tasks. Figure~\ref{fig:del-task} shows a delayable task. A delayable task takes
three inputs \texttt{r}, \texttt{c} and \texttt{e}: \texttt{r} is the task
launch request from the environment, \texttt{e} is the end request, and
\texttt{c} is meant to be a controllable input controlling whether, on request,
the task is actually launched (and therefore goes in the active state), or
delayed (and then forced by the controller to go in the waiting state by stating
the false value to \texttt{c}). This node outputs a unique boolean \texttt{act}
which is true when the task is in the active state.
\begin{figure}[htb]
\begin{lstlisting}
node delayable(r,c,e:bool) returns (act:bool)
let
automaton
state Idle
do act = false
until r & c then Active
| a & not c then Wait
state Wait
do act = false
until c then Active
state Active
do act = true
until e then Idle
end
tel
\end{lstlisting}
\caption{Delayable task}
\label{fig:del-task}
\end{figure}
The Figure~\ref{fig:n-del-task} shows then a node \texttt{ntasks} where $n$
delayable tasks have been put in parallel. The tasks are inlined so as to be
able to perform DSC on this node, taking into account the tasks' states. Until
now, the only interest of modularity is, from the programmer's point of view, to
be able to give once the delayable task code.
\begin{figure}[htb]
\begin{lstlisting}
node ntasks($\ton{\mathtt{r}}{,},\ton{\mathtt{e}}{,}$:bool)
returns ($\ton{\mathtt{a}}{,}$:bool)
contract
let
ca$_{1}$ = a$_{1}$ & (a$_{2}$ or $\ldots$ or a$_{n}$);
$\vdots$
ca$_{n-1}$ = a$_{n-1}$ & a$_{n}$;
tel
enforce not (ca$_{1}$ or \ldots or ca$_{n-1}$)
with ($\ton{\mathtt{c}}{,}$:bool)
let
a$_{1}$ = inlined delayable(r$_{1}$,c$_{1}$,e$_{1}$);
$\vdots$
a$_{n}$ = inlined delayable(r$_{n}$,c$_{n}$,e$_{n}$);
tel
\end{lstlisting}
\caption{\texttt{ntasks} node: $n$ delayable tasks in parallel}
\label{fig:n-del-task}
\end{figure}
This \texttt{ntasks} node is provided with a contract, stating that its
composing tasks are exclusive, i.e., that there are no two tasks in the active
state at the same instant. This contract is enforced with the help of the
controllable inputs $c_i$.
\subsection{Contract composition}
\label{sec:contract-composition}
We want know to reuse the \texttt{ntasks} node, in order to build modularly a
system composed of $2n$ tasks. The Figure~\ref{fig:2n-del-task} shows the
parallel composition of two \texttt{ntasks} nodes. We associate to this
composition a new contract, which role is to enforce the exclusivity of the $2n$
tasks.
\begin{figure}[htb]
\begin{lstlisting}
node main($\ton[1][2n]{\mathtt{r}}{,},\ton[1][2n]{\mathtt{e}}{,}$:bool)
returns ($\ton[1][2n]{\mathtt{a}}{,}$:bool)
contract
let
ca$_{1}$ = a$_{1}$ & (a$_{2}$ or $\ldots$ or a$_{2n}$);
$\vdots$
ca$_{2n-1}$ = a$_{2n-1}$ & a$_{2n}$;
tel
enforce not (ca$_{1}$ or $\ldots$ or ca$_{2n-1}$)
let
($\ton{\mathtt{a}}{,}$) = ntasks($\ton{\mathtt{r}}{,}$,$\ton{\mathtt{e}}{,}$);
($\ton[n+1][2n]{\mathtt{a}}{,}$) = ntasks($\ton[n+1][2n]{\mathtt{r}}{,}$,$\ton[n+1][2n]{\mathtt{e}}{,}$);
tel
\end{lstlisting}
\caption{Composition of two \texttt{ntasks} nodes}
\label{fig:2n-del-task}
\end{figure}
It is easy to see that the contract of \texttt{ntasks} is not precise enough to
be able to compose several of these nodes. Therefore, we need to refine this
contract by adding some way to externally control the activity of the tasks.
\subsection{Contract refinement}
\label{sec:contract-refinement}
We first add an input \texttt{c}, meant to be controllable. The refined contract
will enforce that:
\begin{enumerate}
\item the tasks are exclusive,
\item one task is active only at instants when the input \texttt{c} is
true. This property, appearing in the contract, allow a node instantiating
\texttt{ntasks} to forbid any activity of the $n$ tasks instantiated.
\end{enumerate}
The Figure~\ref{fig:n-del-task-2} contains this new \texttt{ntasks} node.
\begin{figure}[htb]
\begin{lstlisting}
node ntasks(c,$\ton{\mathtt{r}}{,}$,$\ton{\mathtt{e}}{,}$:bool) returns ($\ton{\mathtt{a}}{,}$:bool)
contract
let
ca$_{1}$ = a$_{1}$ & (a$_{2}$ or $\ldots$ or a$_{n}$);$\ldots$
ca$_{n-1}$ = a$_{n-1}$ & a$_{n}$;
one = a$_{1}$ or $\ldots$ or a$_{n}$;
tel
enforce not (ca$_{1}$ or $\ldots$ or ca$_{n-1}$) & (c or not one)
with ($\ton{\mathtt{c}}{,}$:bool)
let
a$_{1}$ = inlined delayable(r$_{1}$,c$_{1}$,e$_{1}$);
$\vdots$
a$_{n}$ = inlined delayable(r$_{n}$,c$_{n}$,e$_{n}$);
tel
\end{lstlisting}
\caption{First contract refinement for the \texttt{ntasks} node}
\label{fig:n-del-task-2}
\end{figure}
However, the controllability introduced here is know too strong. The synthesis
will succeed, but the computed controller, without knowing how \texttt{c} will
be instantiated, will actually block every tasks in their idle state. Indeed, if
the controller allows one task to go in its active state, the input \texttt{c}
can become false at the next instant, violating the property to enforce.
Thus, we propose to add an assumption to this contract: the input \texttt{c}
will not become false if a task was active an instant before. This new contract
is visible in Figure~\ref{fig:n-del-tasks-3}.
\begin{figure}[htb]
\centering
\begin{lstlisting}
node ntasks(c,$\ton{\mathtt{r}}{,}$,$\ton{\mathtt{e}}{,}$:bool) returns ($\ton{\mathtt{a}}{,}$:bool)
contract
let
ca$_{1}$ = a$_{1}$ & (a$_{2}$ or $\ldots$ or a$_{n}$);$\ldots$
ca$_{n-1}$ = a$_{n-1}$ & a$_{n}$;
one = a$_{1}$ or $\ldots$ or a$_{n}$;
pone = false fby one;
tel
assume (not pone or c)
enforce not (ca$_{1}$ or $\ldots$ or ca$_{n-1}$) & (c or not one)
with ($\ton{\mathtt{c}}{,}$)
let
a$_{1}$ = inlined delayable(r$_{1}$,c$_{1}$,e$_{1}$);
$\vdots$
a$_{n}$ = inlined delayable(r$_{n}$,c$_{n}$,e$_{n}$);
tel
\end{lstlisting}
\caption{Second contract refinement for the \texttt{ntasks} node}
\label{fig:n-del-tasks-3}
\end{figure}
We can then use this new \texttt{ntasks} version for the parallel composition,
by instantiating the \texttt{c} input by a controllable variable and its
negation. This composition can be found in Figure~\ref{fig:ntasks-compos}.
\begin{figure}[htb]
\centering
\begin{lstlisting}
node main($\ton[1][2n]{\mathtt{r}}{,}$,$\ton[1][2n]{\mathtt{e}}{,}$:bool) returns ($\ton[1][2n]{\mathtt{a}}{,}$:bool)
contract
let
ca$_{1}$ = a$_{1}$ & (a$_{2}$ or $\ldots$ or a$_{2n}$);
$\vdots$
ca$_{2n-1}$ = a$_{2n-1}$ & a$_{2n}$;
tel
enforce not (ca$_{1}$ or $\ldots$ or ca$_{2n-1}$)
with (c:bool)
let
($\ton{\mathtt{a}}{,}$) = ntasks(c,$\ton{\mathtt{r}}{,}$,$\ton{\mathtt{e}}{,}$);
($\ton[n+1][2n]{\mathtt{a}}{,}$) = ntasks(\Not c,$\ton[n+1][2n]{\mathtt{r}}{,}$,$\ton[n+1][2n]{\mathtt{e}}{,}$);
tel
\end{lstlisting}
\caption{Two \texttt{ntasks} parallel composition}
\label{fig:ntasks-compos}
\end{figure}
\appendix
\section{Generated code}
\label{sec:app-generated-code}
\subsection{C generated code}
\label{sec:c-generated-code}
C generated files from an Heptagon program \texttt{example.ept} are placed in a
directory named \texttt{example\_c}. This directory contains one file
\texttt{example.c}. For each node \texttt{f} of the source program, assuming
that \texttt{f} has inputs $(x_1:t_1,\ldots,x_n:t_n)$ and outputs
$(y_1:t'_1,\ldots,y_p:t'_p)$, $t_i$ and $t'_i$ being the data types of these
inputs and outputs, then the \texttt{example.c} file contains, for each node
\texttt{f}:
\begin{itemize}
\item A \texttt{Example\_\_f\_reset} function, with an argument \texttt{self} being a
memory structure instance:
\begin{lstlisting}[language=C]
void Example__f_reset(Example__f_mem* self);
\end{lstlisting}
\item A \texttt{Example\_\_f\_step} function, with as arguments the nodes inputs, a
structure \texttt{\_out} where the output will be put, and a memory structure
instance \texttt{self}:
\begin{lstlisting}[language=C]
void Example__f_step(t$_{1}$ x$_{1}$, ..., t$_{n}$ x$_{n}$,
Example__f_out* \_out,
Example__f_mem* self);
\end{lstlisting}
After the call of this function, the structure \texttt{\_out} contains the
outputs of the node:
\begin{lstlisting}[language=C]
typedef struct \{
t$'_1$ y$_{1}$;
...
t$'_p$ y$_{p}$;
\} Example__f_ans;
\end{lstlisting}
\end{itemize}
An example of main C code for the execution of this node would be then:
\begin{lstlisting}[language=C]
#include "example.h"
int main(int argc, char * argv[]) \{
Example__f_m mem;
t$_{1}$ x$_{1}$;
...
t$_{n}$ x$_{n}$;
Example__f_out ans;
/* initialize memory instance */
f_reset(&mem);
while(1) \{
/* read inputs */
scanf("...", &x$_{1}$, ..., &x$_{n}$);
/* perform step */
Example__f_step(x$_{1}$, ..., x$_{n}$, &ans, &mem);
/* write outputs */
printf("...", ans.y$_{1}$, ..., ans.y$_{p}$);
\}
\}
\end{lstlisting}
The above code is nearly what is produce for the simulator with the \texttt{-s}
option (see Section~\ref{sec:simulation}).
% \subsection{OCaml generated code}
% \label{sec:ocaml-generated-code}
% If the option \texttt{-target caml} is given, then the compiler generates OCaml
% code in a file named \texttt{example.ml}. Heptagon nodes are compiled into OCaml
% classes, where state variables are class properties, and the two functions
% ``reset'' and ``step'' are class methods. Thus, the class type of \texttt{f}
% would be:
% \begin{alltt}
% class f :
% object
% method reset : unit \(\rightarrow\) unit
% method step : t\ind{1} * ... * t\ind{n} \(\rightarrow\) (t\('\sb{1}\) * ... * t\('\sb{p}\))
% end
% \end{alltt}
\subsection{Java generated code}
\label{sec:java-generated-code}
Java generated files from an Heptagon program \texttt{example.ept} are placed in
a directory named \texttt{example\_java}. This directory contains one Java class
\texttt{f} (in the file \texttt{f.java}) for each node \texttt{f} of the source
program. Assuming that \texttt{f} has inputs $(x_1:t_1,\ldots,x_n:t_n)$ and
outputs $(y_1:t'_1,\ldots,y_p:t'_p)$, $t_i$ and $t'_i$ being the data types of
these inputs and outputs, then this \texttt{f} class implements the following
interface:
\begin{lstlisting}[language=Java]
public interface f {
public void reset();
public fAnswer step(t$_{1}$ x$_{1}$, ..., t$_{n}$ x$_{n}$);
}
\end{lstlisting}
The \texttt{fAnswer} class being a structure containing the outputs:
\begin{lstlisting}[language=Java]
public class fAnswer {
t$'\sb{1}$ y$_{1}$;
...
t$'\sb{p}$ y$_{p}$;
}
\end{lstlisting}
\end{document}

558
manual/macros.sty Normal file
View file

@ -0,0 +1,558 @@
\ProvidesPackage{macros}
\RequirePackage[T1]{fontenc}
\RequirePackage{xspace}
\RequirePackage{amsmath}
\RequirePackage{amssymb}
\RequirePackage{amsthm}
\RequirePackage{graphicx}
\RequirePackage{ifthen}
%% lambdas-trucs
\newcommand{\lambdavar}[1]{\expandafter\newcommand\csname #1\endcsname{\lambda #1}}
\lambdavar{p}
\lambdavar{x}
\lambdavar{y}
\lambdavar{z}
\let\corrital=\/
\renewcommand{\/}{\ifmmode\forall\else\corrital\fi}
\newcommand{\va}{\ensuremath{\alpha}\xspace}
\newcommand{\vb}{\ensuremath{\beta}\xspace}
\newcommand{\vc}{\ensuremath{\gamma}\xspace}
\newcommand{\vd}{\ensuremath{\delta}\xspace}
\newcommand{\vh}{\ensuremath{\eta}\xspace}
%% langages
\newcommand{\langage}[2]{\providecommand{#1}{}\renewcommand{#1}{\textsc{#2}\xspace}}
\langage{\ls}{Lucid Synchrone}
\langage{\lustre}{Lustre}
\langage{\signal}{Signal}
\langage{\esterel}{Esterel}
\langage{\maestro}{Maestro}
\langage{\ocaml}{OCaml}
\langage{\caml}{Caml}
\langage{\nemo}{Nemo}
\langage{\Acute}{Acute}
\langage{\Oz}{Oz}
\langage{\heptagon}{Heptagon}
\langage{\decade}{Decade}
\RequirePackage{listings}
% Definition langage decade
\lstdefinelanguage{Heptagon}
{%
keywords={node,returns,let,tel,var,pre,fby,when,whenot,merge,if,then,else,or,not},%
morekeywords=[2]{automaton,state,until,unless,end,present,switch,inlined},%
morekeywords=[2]{contract,assume,enforce,with},%
otherkeywords={->,&,=},%
comment=[n]{(*}{*)},%
}[keywords,comments]
% \lstdefinelanguage[dist]{Decade}
% {%
% morekeywords={link,to},%
% }[keywords,comments]
%% règles d'inférence
\RequirePackage{mathpartir}
\renewcommand{\TirName}[1]{\textsc{(#1)}}
\renewcommand{\RefTirName}[1]{\textsc{(#1)}}
\newcommand{\rulename}[1]{\ifthenelse{\equal{#1}{}}{}{\textsc{#1}}}
\newcommand{\sepname}{\:}
\newcommand{\sepprem}{\;\;\;}
\newcommand{\axiom}[2][]{\rulename{#1}\quad#2}
\newcommand{\infsimple}[3][]{\rulename{#1}\sepname\frac{#2}{#3}}
\newcommand{\infsimplespec}[3][]{
\begin{array}{c}
{#2}\\
\multicolumn{1}{l}{\rulename{#1}}\\\hline
{#3}
\end{array}
}
\newcommand{\infdouble}[4][]{\rulename{#1}\sepname\frac{#2\sepprem#3}{#4}}
\newcommand{\infdoublecol}[4][]{\rulename{#1}\sepname\frac{\array{c}#2\\#3\endarray}{#4}}
\newcommand{\inftriple}[5][]{\rulename{#1}\sepname\frac{#2\sepprem#3\sepprem#4}{#5}}
\newcommand{\inftriplecol}[5][]{\rulename{#1}\sepname\frac{\array{c}#2\\#3\\#4\endarray}{#5}}
\newcommand{\infquadruple}[6][]{\rulename{#1}\sepname\frac{#2\sepprem#3\sepprem#4\sepprem#5}{#6}}
%% Grammaires
\newcommand{\ou}{\;|\;}
\newcommand{\fun}{\rightarrow}
%\newcommand{\ovfun}[1]{\xrightarrow{#1}}
\newcommand{\ovfun}[1]{{\;-\mskip-1.5\thinmuskip\langle{#1}\rangle\!\!\!\rightarrow\;}}
%% Typage --- général
\DeclareMathOperator{\FV}{FV}
\DeclareMathOperator{\FTV}{FTV}
\DeclareMathOperator{\FSV}{FSV}
\DeclareMathOperator{\FLV}{FLV}
\DeclareMathOperator{\FCV}{FCV}
\DeclareMathOperator{\gen}{gen}
\DeclareMathOperator{\genall}{genall}
%\DeclareMathOperator{\Var}{Var}
\DeclareMathOperator{\merge}{merge}
\newcommand{\mergeenv}{\uplus}
%% Types de données
\newcommand{\type}[3]{\ensuremath{#1\vdash#2:#3}}
%% Horloges
\newcommand{\horloge}[3]{\ensuremath{#1\vdash#2:#3}}
%% Types spaciaux
\newcommand{\soussite}{\ensuremath{\prec_\cR}}
\newcommand{\connecte}{\ensuremath{\mapsto_\cC}}
\DeclareMathOperator{\site}{site}
\DeclareMathOperator{\sites}{sites}
\DeclareMathOperator{\locations}{locations}
\DeclareMathOperator{\loc}{loc}
\DeclareMathOperator{\names}{names}
\DeclareMathOperator{\out}{out}
\DeclareMathOperator{\com}{com}
\DeclareMathOperator{\channels}{channels}
\DeclareMathOperator{\constraints}{constr}
\DeclareMathOperator{\op}{op}
\DeclareMathOperator{\ifte}{ifte}
\DeclareMathOperator{\fby}{fby}
\newcommand{\fcom}[4]{\ensuremath{#1\xrightarrow{#2\vartriangleright#3}#4}}
\newcommand{\OutputType}[3]{\ensuremath{\uparrow_{#1,#2}(#3)}}
\newcommand{\pere}[2]{\ensuremath{\uparrow_#1(#2)}}
\newcommand{\set}[1]{\ensuremath{\{#1\}}}
\newcommand{\defprogram}[2]{\ensuremath{\vdash#1:#2}}
\newcommand{\defhierarchy}[3]{\ensuremath{#1\vdash#2:#3}}
\newcommand{\defarch}[3]{\ensuremath{#1\vdash#2:#3}}
\newcommand{\spacetype}[4]{\ensuremath{#1\vdash#3:#4/#2}}
\renewcommand{\spacetype}[5]{\ensuremath{#1|#2\vdash#4:#5/#3}}
\newcommand{\spacetypetrans}[4]{\ensuremath{#1|#2\vdash#4/#3}}
\newcommand{\spacetypeimpl}[5]{\ensuremath{#1|#2\vdash_i#4:#5/#3}}
\newcommand{\spacetypechan}[6]{\ensuremath{#1|#2\vdash#5:#6/#3/#4}}
\newcommand{\subtype}[3]{\ensuremath{#1\vdash#2\prec#3}}
\newcommand{\projsubtype}[4]{\ensuremath{#1\vdash#2:#3\prec#4}}
\newcommand{\emptydecl}{\ensuremath{\emptyset}}
\newcommand{\slicing}[3]{\ensuremath{#1\stackrel{#2}{\longrightarrow}#3}}
%\newcommand{\projection}[4]{\ensuremath{#1|#2\stackrel{#3}{\Longrightarrow}#4}}
\newcommand{\projection}[3]{\ensuremath{#1\stackrel{#2}{\Longrightarrow}#3}}
\newcommand{\projspacetype}[7]{\ensuremath{\projection{\spacetype{#1}{#2}{#3}{#4}{#5}}{#6}{#7}}}
\newcommand{\projtrans}[6]{\ensuremath{\projection{\spacetypetrans{#1}{#2}{#3}{#4}}{#5}{#6}}}
\newcommand{\projectioncol}[3]{\ensuremath{
\begin{array}{c}
#1\\
\stackrel{#2}{\Longrightarrow}#3
\end{array}}}
\newcommand{\projtype}[4]{\ensuremath{#1\vdash#2\stackrel{#3}{\Longrightarrow}#4}}
\newcommand{\canal}[3]{\ensuremath{#1\stackrel{#2}{\leftrightarrow}#3}}
\newcommand{\channel}[3]{\ensuremath{#1\stackrel{#2}{\mapsto} #3}}
\newcommand{\vs}{\ensuremath{\delta}\xspace}
\newcommand{\comm}{\triangleright}
\newcommand{\graph}[2]{\ensuremath{\langle#1,#2\rangle}}
\newcommand{\abs}{\ensuremath{\bot}}
\newcommand{\cabs}{\ensuremath{[]}}
\newcommand{\subck}{\ensuremath{<:}}
%% Sémantique synchrone
\newcommand{\clock}[1]{\ensuremath{\langle#1\rangle}}
\newcommand{\I}{\mathbb{I}}
%\newcommand{\N}{\mathbb{N}}
% dist. values and environments
\newcommand{\dv}{\hat v}
\newcommand{\lv}{vl}
\newcommand{\R}{\hat R}
\let\paragraphe=\S
\renewcommand{\S}{\hat S}
\newcommand{\G}{\hat G}
\newcommand{\C}{\hat C}
\newcommand{\A}{\hat A}
\newcommand{\semop}[3]{\ensuremath{#1\xrightarrow{#2}#3}}
\newcommand{\semdist}[5]{\ensuremath{#1\stackrel{#2}{\Vdash}#3\xrightarrow{#4}#5}}
\newcommand{\semproj}[4]{\ensuremath{#1\vdash#2\xrightarrow{#3}#4}}
\newcommand{\semcent}[4]{\ensuremath{#1\vdash#2\xrightarrow{#3}#4}}
\newcommand{\semcentshort}[4]{\ensuremath{#1\!\vdash\!#2\!\stackrel{#3}{\rightarrow}\!#4}}
\newcommand{\semprog}[3]{\ensuremath{#1\vdash#2:#3}}
\newcommand{\semdistprog}[3]{\ensuremath{#1\Vdash#2:#3}}
\newcommand{\compvt}[3]{#1\in I_{H}(#3)}
\newcommand{\relval}[4]{\ensuremath{#1\preccurlyeq^{#2}_{#3}#4}}
%\newcommand{\reaceq}[1]{\stackrel{#1}{\cong}}
%\newcommand{\reaceq}[1]{\stackrel{#1}{\preccurlyeq}}
\newcommand{\reaceq}[1]{\preccurlyeq_{#1}}
\def\leadstofill@{\arrowfill@\relbar\relbar\leadsto}
\newcommand{\xleadsto}[2][]{\ext@arrow 0359\leadstofill@{#1}{#2}}
\newcommand{\simu}[4]{#1\xleadsto[#3]{#2}#4}
%% lettres calligraphiques
\newcommand{\shortcal}[1]{\expandafter\newcommand\csname c#1\endcsname{\ensuremath{\mathcal{#1}}}}
\shortcal{A}
\shortcal{B}
\shortcal{C}
\shortcal{D}
\shortcal{E}
\shortcal{F}
\shortcal{G}
\shortcal{H}
\shortcal{I}
\shortcal{J}
\shortcal{K}
\shortcal{L}
\shortcal{M}
\shortcal{N}
\shortcal{O}
\shortcal{P}
\shortcal{Q}
\shortcal{R}
\shortcal{S}
\shortcal{T}
\shortcal{U}
\shortcal{V}
\shortcal{W}
\shortcal{X}
\shortcal{Y}
\shortcal{Z}
%% mots-clés
\newcommand{\m@thspace}{%
\ifmmode\ \fi%
}
\newcommand{\textname}[1]{\texttt{#1}}
\newcommand{\name}[2]{%
\providecommand{#1}{}%
\renewcommand{#1}{\textname{#2}\xspace}%
}
\newcommand{\textkw}[1]{\texttt{\textbf{#1}}}
\newcommand{\kw}[2]{%
\providecommand{#1}{}%
\renewcommand{#1}{\textkw{#2}\xspace}%
}
\newcommand{\akeyword}[1]{\expandafter\kw\csname #1\endcsname{#1}}
\newcommand{\midkw}[2]{%
\providecommand{#1}{}%
\renewcommand{#1}{\m@thspace\textkw{#2}\m@thspace\xspace}%
}
\newcommand{\midkeyword}[1]{\expandafter\midkw\csname #1\endcsname{#1}}
\newcommand{\begkw}[2]{%
\providecommand{#1}{}%
\renewcommand{#1}{\textkw{#2}\m@thspace\xspace}%
}
\newcommand{\begkeyword}[1]{\expandafter\begkw\csname #1\endcsname{#1}}
\newcommand{\closekw}[2]{%
\providecommand{#1}{}%
\renewcommand{#1}{\m@thspace\textkw{#2}\xspace}%
}
\newcommand{\closekeyword}[1]{\expandafter\closekw\csname #1\endcsname{#1}}
\newcommand{\typeconst}[2]{\kw{#1}{#2}}
\newcommand{\binop}[2]{\midkw{#1}{#2}}
\newcommand{\unop}[2]{\begkw{#1}{#2}}
\newcommand{\funct}[2]{\begkw{#1}{#2}}
%% Mots-clés Lucid Synchrone
\begkw{\Assume}{assume}
\begkw{\Automaton}{automaton}
\midkw{\And}{and}
\midkw{\Band}{\&}
\begkw{\Clock}{clock}
\begkw{\Contract}{contract}
\begkw{\Do}{do}
\closekw{\Done}{done}
\midkw{\Else}{else}
\begkw{\Emit}{emit}
\closekw{\End}{end}
\begkw{\Enforce}{enforce}
\midkw{\Every}{every}
\binop{\Fby}{fby}
\binop{\Fleche}{->}
\unop{\Fst}{fst}
\kw{\False}{false}
\begkw{\Guarantee}{guarantee}
\begkw{\If}{if}
\midkw{\In}{in}
\begkw{\Inlined}{inlined}
\begkw{\Last}{last}
\begkw{\Let}{let}
\begkw{\Letnode}{node}
\begkw{\Match}{match}
\funct{\Merge}{merge}
%\kw{\merge}{merge}
\begkw{\Node}{node}
\begkw{\Not}{not}
\midkw{\On}{on}
\midkw{\Or}{or}
\unop{\Pre}{pre}
\begkw{\Present}{present}
\kw{\Pv}{;}
\begkw{\Rec}{rec}
\begkw{\Reset}{reset}
\midkw{\Returns}{returns}
\begkw{\Run}{run}
\begkw{\Sig}{sig}
\unop{\Snd}{snd}
\begkw{\State}{state}
\closekw{\Tel}{tel}
\midkw{\Then}{then}
\kw{\True}{true}
\midkw{\Until}{until}
\midkw{\Unless}{unless}
\midkw{\Var}{var}
\midkw{\When}{when}
\midkw{\Whenot}{whenot}
\midkw{\Where}{where}
\midkw{\With}{with}
\kw{\Tick}{tick}
\typeconst{\Float}{float}
\typeconst{\Int}{int}
\typeconst{\Unit}{unit}
\typeconst{\Bool}{bool}
\newcommand{\Nil}{\ensuremath{\mathit{nil}}}
%% Mots-clés répartition
\midkw{\At}{at}
\begkw{\Site}{site}
\begkw{\Loc}{loc}
\begkw{\Subsite}{subsite}
\begkw{\Subloc}{subloc}
\begkw{\Link}{link}
\midkw{\To}{to}
\begkw{\Out}{out}
\midkw{\Of}{of}
\begkw{\Port}{port}
\newcommand{\TAt}{\m@thspace\texttt{at}\m@thspace\xspace}
\DeclareMathOperator{\typecl}{clock}
\funct{\Send}{send}
\funct{\Receive}{receive}
\newcommand{\match}[4][c]{
\begin{array}[#1]{l}
\Match #2\With\\
|\ \True \rightarrow #3\\
|\ \False \rightarrow #4\\
\end{array}
}
\newcommand{\linematch}[3]{
\Match #1\With
|\ \True \rightarrow #2
\ |\ \False \rightarrow #3
}
%% Théorèmes, définitions, remarques...
\RequirePackage{amsmath}
\newtheorem{definition}{D\'efinition}
\newtheorem{remarque}{Remarque}
\newtheorem{theoreme}{Th\'eor\`eme}
\newtheorem{lemme}{Lemme}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newcommand{\noeud}{n\oe ud\xspace}
\newcommand{\Noeud}{N\oe ud\xspace}
\newcommand{\noeuds}{n\oe uds\xspace}
\newcommand{\Noeuds}{N\oe uds\xspace}
%% Macros mathématiques
\providecommand{\tonfirst}{}
\newcommand{\ton}[1][1]{\renewcommand{\tonfirst}{#1}\tonbis}
\newcommand{\tonbis}[3][n]{\ensuremath{#2_{\tonfirst}#3\ldots#3#2_{#1}}}
\newcommand{\tonp}{\ton[1][p]}
\newcommand{\tonq}{\ton[1][q]}
\newcommand{\tontt}[1][1]{\renewcommand{\tonfirst}{#1}\tonttbis}
\newcommand{\tonttbis}[3][n]{\ensuremath{\mathtt{#2}_{\tonfirst}\mathtt{#3}\ldots\mathtt{#3}\mathtt{#2}_{#1}}}
\newcommand{\ind}[1]{\(\sb{#1}\)}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\codom}{cod}
%\DeclareMathOperator{\inst}{inst}
\DeclareMathOperator{\head}{hd}
\DeclareMathOperator{\tail}{tl}
\DeclareMathOperator{\DCS}{DCS}
\DeclareMathOperator{\Triang}{Triang}
\DeclareMathOperator{\Traces}{Traces}
\newcommand{\B}{\mathbb{B}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
%\newcommand{\R}{\mathbb{R}}
%\newcommand{\C}{\mathbb{C}}
\newcommand{\seq}[1]{\ensuremath{\overline{#1}}}
\newcommand{\cphant}{\hat{c}}
%% Flots de données
\newenvironment{streams}[1]{%
\setlength{\arraycolsep}{0.3cm}
\array{|c|*{#1}{c}|}
\hline
}{%
\hline
\endarray
}
%% Macros usuelles
%\RequirePackage[outerbars]{changebar}
%\newenvironment{change}[1][]{\cbstart}{\cbend}
\newenvironment{change}[1][]{}{}
\newenvironment{amodifier}%
{\textcolor{red}\bgroup%
\hrule
\begin{center}
\`A MODIFIER ?
\end{center}
\hrule
}%
{\hrule\egroup}
\renewenvironment{amodifier}{}{}
%% Boîte-noeud code
\RequirePackage{alltt}
\newenvironment{code}{%
\renewcommand{\textkw}[1]{\textbf{##1}}
\@beginparpenalty 10000 %
\quote%
\alltt}{\endalltt%
\endquote
\vspace{3mm}
}
\newenvironment{figcode}{%
\renewcommand{\textkw}[1]{\textbf{##1}}
\@beginparpenalty 10000 %
\alltt}{\endalltt%
\vspace{1mm}
}
\newcommand{\marc}[1]{}
\RequirePackage{varwidth}
\newenvironment{showproj}
{
\par\noindent\medskip
\renewenvironment{code}
{\varwidth{\linewidth}\vspace*{0.5em}\alltt}
{\endalltt\endvarwidth}
\tabular{>{\centering}p{0.45\linewidth}||>{\centering}p{0.45\linewidth}}
\multicolumn{1}{c}{\texttt{A}} & \multicolumn{1}{c}{\texttt{B}} \\\hline
}
{\vspace{-3cm}\endtabular\medskip}
\newcommand{\minildots}{\ensuremath{\!...}}
\newbox\subfigbox % Create a box to hold the subfigure.
\newenvironment{subfloat}% % Create the new environment.
{\def\caption##1{\gdef\subcapsave{\relax##1}}%
\let\subcapsave=\@empty % Save the subcaption text.
\let\sf@oldlabel=\label
\def\label##1{\xdef\sublabsave{\noexpand\label{##1}}}%
\let\sublabsave\relax % Save the label key.
\setbox\subfigbox\hbox
\bgroup}% % Open the box...
{\egroup % ... close the box and call \subfigure.
\let\label=\sf@oldlabel
\subfigure[\subcapsave]{\sublabsave\box\subfigbox}}%
\newenvironment{flushedproof}{%
\proof%
\flushleft%
}{%
\endflushleft%
\endproof%
}
%% MiniLustre & contrats
\newcommand{\semml}[5]{\ensuremath{#1,#2\vdash#3\xrightarrow{#4}#5}}

421
manual/mathpartir.sty Normal file
View file

@ -0,0 +1,421 @@
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
%
% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
%
% Author : Didier Remy
% Version : 1.2.0
% Bug Reports : to author
% Web Site : http://pauillac.inria.fr/~remy/latex/
%
% Mathpartir is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
%
% Mathpartir is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details
% (http://pauillac.inria.fr/~remy/license/GPL).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File mathpartir.sty (LaTeX macros)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
[2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
%%
%% Identification
%% Preliminary declarations
\RequirePackage {keyval}
%% Options
%% More declarations
%% PART I: Typesetting maths in paragraphe mode
\newdimen \mpr@tmpdim
% To ensure hevea \hva compatibility, \hva should expands to nothing
% in mathpar or in inferrule
\let \mpr@hva \empty
%% normal paragraph parametters, should rather be taken dynamically
\def \mpr@savepar {%
\edef \MathparNormalpar
{\noexpand \lineskiplimit \the\lineskiplimit
\noexpand \lineskip \the\lineskip}%
}
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
\let \MathparLineskip \mpr@lineskip
\def \mpr@paroptions {\MathparLineskip}
\let \mpr@prebindings \relax
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
\def \mpr@goodbreakand
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
\def \mpr@and {\hskip \mpr@andskip}
\def \mpr@andcr {\penalty 50\mpr@and}
\def \mpr@cr {\penalty -10000\mpr@and}
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
\def \mpr@bindings {%
\let \and \mpr@andcr
\let \par \mpr@andcr
\let \\\mpr@cr
\let \eqno \mpr@eqno
\let \hva \mpr@hva
}
\let \MathparBindings \mpr@bindings
% \@ifundefined {ignorespacesafterend}
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
\newenvironment{mathpar}[1][]
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
\noindent $\displaystyle\fi
\MathparBindings}
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
%%% HOV BOXES
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
\vbox \bgroup \tabskip 0em \let \\ \cr
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
\egroup}
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
\box0\else \mathvbox {#1}\fi}
%% Part II -- operations on lists
\newtoks \mpr@lista
\newtoks \mpr@listb
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
\mpr@flatten \mpr@all \mpr@to \mpr@one
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
\mpr@all \mpr@stripend
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
\ifx 1\mpr@isempty
\repeat
}
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
%% Part III -- Type inference rules
\newif \if@premisse
\newbox \mpr@hlist
\newbox \mpr@vlist
\newif \ifmpr@center \mpr@centertrue
\def \mpr@htovlist {%
\setbox \mpr@hlist
\hbox {\strut
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
\unhbox \mpr@hlist}%
\setbox \mpr@vlist
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
\else \unvbox \mpr@vlist \box \mpr@hlist
\fi}%
}
% OLD version
% \def \mpr@htovlist {%
% \setbox \mpr@hlist
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
% \setbox \mpr@vlist
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
% \else \unvbox \mpr@vlist \box \mpr@hlist
% \fi}%
% }
\def \mpr@item #1{$\displaystyle #1$}
\def \mpr@sep{2em}
\def \mpr@blank { }
\def \mpr@hovbox #1#2{\hbox
\bgroup
\ifx #1T\@premissetrue
\else \ifx #1B\@premissefalse
\else
\PackageError{mathpartir}
{Premisse orientation should either be T or B}
{Fatal error in Package}%
\fi \fi
\def \@test {#2}\ifx \@test \mpr@blank\else
\setbox \mpr@hlist \hbox {}%
\setbox \mpr@vlist \vbox {}%
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
\let \@hvlist \empty \let \@rev \empty
\mpr@tmpdim 0em
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
\def \\##1{%
\def \@test {##1}\ifx \@test \empty
\mpr@htovlist
\mpr@tmpdim 0em %%% last bug fix not extensively checked
\else
\setbox0 \hbox{\mpr@item {##1}}\relax
\advance \mpr@tmpdim by \wd0
%\mpr@tmpdim 1.02\mpr@tmpdim
\ifnum \mpr@tmpdim < \hsize
\ifnum \wd\mpr@hlist > 0
\if@premisse
\setbox \mpr@hlist
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
\else
\setbox \mpr@hlist
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
\fi
\else
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\else
\ifnum \wd \mpr@hlist > 0
\mpr@htovlist
\mpr@tmpdim \wd0
\fi
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\advance \mpr@tmpdim by \mpr@sep
\fi
}%
\@rev
\mpr@htovlist
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
\fi
\egroup
}
%%% INFERENCE RULES
\@ifundefined{@@over}{%
\let\@@over\over % fallback if amsmath is not loaded
\let\@@overwithdelims\overwithdelims
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
}{}
%% The default
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\mpr@over #2}$}}
\let \mpr@fraction \mpr@@fraction
%% A generic solution to arrow
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
\def \mpr@tail{#1}%
\def \mpr@body{#2}%
\def \mpr@head{#3}%
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
\setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
\setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
\dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
\dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
\setbox0=\hbox {$\box1 \@@atop \box2$}%
\dimen0=\wd0\box0
\box0 \hskip -\dimen0\relax
\hbox to \dimen0 {$%
\mathrel{\mpr@tail}\joinrel
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
$}}}
%% Old stuff should be removed in next version
\def \mpr@@reduce #1#2{\hbox
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
\def \mpr@@rewrite #1#2#3{\hbox
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
\def \mpr@empty {}
\def \mpr@inferrule
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\let \@rulename \mpr@empty
\let \@rule@options \mpr@empty
\let \mpr@over \@@over
\mpr@inferrule@}
\newcommand {\mpr@inferrule@}[3][]
{\everymath={\displaystyle}%
\def \@test {#2}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
\else
\def \@test {#3}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
\else
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
\fi \fi
\def \@test {#1}\ifx \@test\empty \box0
\else \vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{\hbox {\RefTirName {#1}}\box0}\fi
\egroup}
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
% They are two forms
% \inferrule [label]{[premisses}{conclusions}
% or
% \inferrule* [options]{[premisses}{conclusions}
%
% Premisses and conclusions are lists of elements separated by \\
% Each \\ produces a break, attempting horizontal breaks if possible,
% and vertical breaks if needed.
%
% An empty element obtained by \\\\ produces a vertical break in all cases.
%
% The former rule is aligned on the fraction bar.
% The optional label appears on top of the rule
% The second form to be used in a derivation tree is aligned on the last
% line of its conclusion
%
% The second form can be parameterized, using the key=val interface. The
% folloiwng keys are recognized:
%
% width set the width of the rule to val
% narrower set the width of the rule to val\hsize
% before execute val at the beginning/left
% lab put a label [Val] on top of the rule
% lskip add negative skip on the right
% left put a left label [Val]
% Left put a left label [Val], ignoring its width
% right put a right label [Val]
% Right put a right label [Val], ignoring its width
% leftskip skip negative space on the left-hand side
% rightskip skip negative space on the right-hand side
% vdots lift the rule by val and fill vertical space with dots
% after execute val at the end/right
%
% Note that most options must come in this order to avoid strange
% typesetting (in particular leftskip must preceed left and Left and
% rightskip must follow Right or right; vdots must come last
% or be only followed by rightskip.
%
%% Keys that make sence in all kinds of rules
\def \mprset #1{\setkeys{mprset}{#1}}
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
\define@key {mprset}{center}[]{\mpr@centertrue}
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\newbox \mpr@right
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
\define@key {mpr}{center}[]{\mpr@centertrue}
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{width}{\hsize #1}
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
\define@key {mpr}{before}{#1}
\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
\define@key {mpr}{narrower}{\hsize #1\hsize}
\define@key {mpr}{leftskip}{\hskip -#1}
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
\define@key {mpr}{rightskip}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
\define@key {mpr}{right}
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{RIGHT}
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{Right}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
\newdimen \rule@dimen
\newcommand \mpr@inferstar@ [3][]{\setbox0
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
\setbox \mpr@right \hbox{}%
$\setkeys{mpr}{#1}%
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
\box \mpr@right \mpr@vdots$}
\setbox1 \hbox {\strut}
\rule@dimen \dp0 \advance \rule@dimen by -\dp1
\raise \rule@dimen \box0}
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
\newcommand \mpr@err@skipargs[3][]{}
\def \mpr@inferstar*{\ifmmode
\let \@do \mpr@inferstar@
\else
\let \@do \mpr@err@skipargs
\PackageError {mathpartir}
{\string\inferrule* can only be used in math mode}{}%
\fi \@do}
%%% Exports
% Envirnonment mathpar
\let \inferrule \mpr@infer
% make a short name \infer is not already defined
\@ifundefined {infer}{\let \infer \mpr@infer}{}
\def \TirNameStyle #1{\small \textsc{#1}}
\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
\let \TirName \tir@name
\let \DefTirName \TirName
\let \RefTirName \TirName
%%% Other Exports
% \let \listcons \mpr@cons
% \let \listsnoc \mpr@snoc
% \let \listhead \mpr@head
% \let \listmake \mpr@makelist
\endinput

302
manual/varwidth.sty Normal file
View file

@ -0,0 +1,302 @@
% varwidth.sty v 0.9a Mar 2003 Donald Arseneau asnd@triumf.ca
%
% Copyright 2003 by Donald Arseneau (asnd@triumf.ca).
% This software is released under the terms of the LaTeX Project Public
% License (ftp://ctan.tug.org/tex-archive/macros/latex/base/lppl.txt).
% (Essentially: Free to use, copy, distribute (sell) and change, but, if
% changed, the name must be changed.)
%
% The varwidth environment is based on minipage, and takes the same
% parameters, but the specified width is just a maximum value -- the
% environment will be typeset with a narrower "natural" width if
% possible.
%
% In a varwidth environment, paragraph line-breaks are chosen
% according to the specified width, but each line is reset to
% match a narrower natural width, if there is one.
%
% The \narrowragged command works like \raggedright, but produces
% generally narrower lines in paragraphs, but more text in the last
% line (the lines have more-equal lengths).
%
% This version works fine, but there are still many questions about
% how it would work best. Should there be a version that avoids the
% usual minipage formatting style?
%
% Numbered equations are not handled well, especially with leqno.
% AMSmath environments have not been tried, and undoubtedly fail.
%
% To do: Extend v-list wrappers to handle all e-TeX primitives.
% (pdfTeX too?)
% Capture marks and floats, propagating them out of the box
% Support numbered equations, including ams math.
%
\ProvidesPackage{varwidth}[2003/03/10 ver 0.9a; \space
Variable-width minipages]
\newcommand\narrowragged{\rightskip \z@ plus .25\hsize
\@rightskip\rightskip \parfillskip\z@ plus .15\hsize
\sloppy }
\newbox\@vwid@box
% The varwidth environment is based on minipage, and takes the same
% parameters, but the specified width is only a limit -- a narrower
% natural width may be used. \varwidth uses \minipage.
\def\varwidth{\let\@minipagerestore\@vwid@setup \minipage}
% Many things may appear on vertical lists that can't be re-processed,
% so they have to be modified.
\def\@vwid@setup{%
% several things can't appear in vertical mode, so they may get
% a \vbox wrapped around them.
\let\@bsphack\@vwid@bsphack % \label and others
\let\mark\@gobble % Marks disappear in minipages anyway
\let\@special\@vwid@special % \color and others
\let\addtocontents\@vwid@addtocontents % \addcontentsline
% Shifted boxes (\parshape,\hangindent) will have their shifts
% indicated in a separate box.
\let\@hangfrom\@vwid@hangfrom % hanging indents
\let\list\@vwid@list
\let\endtrivlist\@vwid@endtrivlist
\postdisplaypenalty\@vwid@posteqp
\predisplaypenalty\@vwid@preeqp
\def\@eqnnum{\aftergroup\@vwid@afterva\@@vwid@eqnnum}%
\global\@vwid@roff\z@ \global\@vwid@loff\z@
% Begin an inner minipage-like vertical box (in \@tempboxa)
\let\@minipagerestore\@@vwid@minipagerestore \@minipagerestore
\setbox\@tempboxa\vbox\bgroup\begingroup
% Flag the top of the list
\penalty\@vwid@toppen
}
\let\@@vwid@minipagerestore\@minipagerestore
% At end of varwidth environment.
\def\endvarwidth{\par\@@par
% Handle minipage-style notes.
\ifvoid\@mpfootins\else
\vskip\skip\@mpfootins
\normalcolor
\@vwid@wrap\footnoterule
\unvbox\@mpfootins
\fi
\unskip
\endgroup\egroup % got my \@tempboxa
% {\showoutput\showbox\@tempboxa}%
% in a discarded box, sift through list measuring max width.
\begingroup\setbox\z@\vbox\bgroup
%\message{-------------------------------------------------------------}%
%\message{First pass; hsize=\the\hsize... }%{\tracingall\showlists}%%
\unvcopy\@tempboxa
\@tempdima-\maxdimen
\let\@vwid@resetb\@vwid@measure
\let\@vwid@append\relax
\sift@deathcycles\z@
\@vwid@sift
\xdef\@vwid@{\the\@tempdima}%
\egroup\endgroup
% Done measuring. Now empty \@tempboxa onto current vertical list
% which is the contents of a minipage environment
%\message{Got natural width \@vwid@. }%
\unvbox\@tempboxa
% If the natural width is narrower, then go back through the list
% reboxing and moving everything into \@vwid@box; then spill \@vwid@box
\ifdim\@vwid@<\hsize
\hsize\@vwid@
\setbox\@vwid@box\vbox{}%
\sift@deathcycles\z@
%\message{----------------------------------------------------------------}%
%\message{Second pass; hsize=\the\hsize... }%{\tracingall\showlists}%
\@vwid@sift
\unvbox\@vwid@box
\fi
% end the minipage environment
\endminipage}
%
% Here are definitions for sifting through the vertical list, either
% measuring things or reboxing them.
%
% Penalties used as signals to the vertical-list processor:
\mathchardef\@vwid@posteqp 17321 % Penalty below equations
\mathchardef\@vwid@preeqp 17322 % Penalty above equations
\mathchardef\@vwid@postnump 17323 % Penalty below numbered equations
\mathchardef\@vwid@toppen 17324 % Penalty marking top of vertical list
\mathchardef\@vwid@offsets 17325 % Penalty below special h-offsets box
\mathchardef\@vwid@postw 17326 % Penalty below a \vbox-wrapped object
\newcount\sift@deathcycles
\def\@vwid@sift{%
\skip@\lastskip\unskip
\dimen@\lastkern\unkern
\count@\lastpenalty\unpenalty
\setbox\z@\lastbox
%{\showoutput\showbox\z@}%
\ifvoid\z@ \advance\sift@deathcycles\@ne \else \sift@deathcycles\z@ \fi
\ifnum\sift@deathcycles>33
\let\@vwid@sift\relax
\PackageWarning{varwidth}{Failed to reprocess entire contents}%
\fi
%\message{\the\sift@deathcycles: skip \the\skip@; kern \the\dimen@; penalty \the\count@. }%
%\ifhbox\z@\setbox99\hbox to0pt{\unhcopy\z@}\fi % = message
\ifnum\count@=\@vwid@preeqp \@vwid@eqmodefalse\fi
%\ifnum\count@=\@vwid@preeqp \message{End equation mode. }\fi
\ifnum\count@=\@vwid@posteqp \@vwid@eqmodetrue\fi
%\ifnum\count@=\@vwid@posteqp\message{Begin equation mode. }\fi
%\if@vwid@eqmode {\showoutput\showbox\z@}\fi
\ifnum\count@=\@vwid@toppen % finished
\let\@vwid@sift\relax
\else\ifnum\count@=\@vwid@offsets
\@vwid@setoffsets
\else
\ifnum\count@=\@vwid@postw
\else
\@vwid@resetb % reset box \z@ or measure it
\fi
\@vwid@append
\fi\fi
\@vwid@sift}
\def\@vwid@setoffsets{%
\setbox\z@=\hbox{\unhbox\z@
\global\@vwid@roff\lastkern\unkern
\global\@vwid@loff\lastkern\unkern}%
%\message{Set offsets to \the\@vwid@loff, \the\@vwid@roff. }%
}
\def\@vwid@append{% Append contents of box \z@ and glue to \@vwid@box
\setbox\@vwid@box\vbox{%
\unvbox\z@
\ifdim\dimen@=\z@\else \kern\dimen@ \fi
\vskip\skip@
\unvbox\@vwid@box
}%{\tracingall\showbox\@vwid@box}%
}
% reset box \z@ to \hsize, applying shifts, and wrap in vbox
% Don't worry about numbered equations because we won't get
% here if there are any.
\def\@vwid@resetb{%
\setbox\z@\vbox\bgroup
\ifvoid\z@
\else
\ifvbox\z@
\box\z@
\else % \hbox
\@tempdima\hsize
\advance\@tempdima-\@vwid@roff
\advance\@tempdima-\@vwid@loff
\advance\@tempdima-\p@
\ifdim\wd\z@>\@tempdima % full-width line; rebox it
%\message{An ordinary line or alignment. }%
\hbox to\hsize
{\kern\@vwid@loff \unhbox\z@ \kern\@vwid@roff}%
\else % an equation or direct \hbox
\if@vwid@eqmode % re-center unnumbered equations
%\message{A centered equation hsize=\the\hsize. }%
\hbox to\hsize
{\hskip\@vwid@loff\@plus1fil
\unhbox\z@ \hskip\@vwid@roff\@plus1fil}%
\else % plain narrow \hbox; leave it as-is
\box\z@
\fi\fi\fi\fi
\egroup}
\def\@vwid@measure{%
\ifvoid\z@
\else
% numbered equations not part of alignments can't be reset,
% so force retention of full width.
\ifnum\count@=\@vwid@postnump \ifdim\wd\z@<\linewidth
\ifdim\@tempdima<\linewidth \@tempdima\linewidth \fi
\fi\fi
\ifhbox\z@
\setbox\z@=\hbox
{\kern\@vwid@loff \unhbox\z@ \kern\@vwid@roff}%
\fi
\ifdim\wd\z@>\@tempdima \@tempdima\wd\z@ \fi
\fi}
\newdimen\@vwid@loff
\newdimen\@vwid@roff
\let\@@bsphack\@bsphack
\let\@@esphack\@esphack
\let\@@esphack\@Esphack
\def\@vwid@bsphack{\@@bsphack
\ifx\@vwid@wrap\@firstofone
\bgroup
\else
\ifvmode
\setbox\@vwid@box \vbox\bgroup \vbox\bgroup
\let\@vwid@wrap\@firstofone
\def\@esphack{\@vwid@esphack\@@esphack}%
\def\@Esphack{\@vwid@esphack\@@Esphack}%
\fi
\fi}
\def\@vwid@esphack{\egroup
\ifx\@vwid@wrap\@firstofone\else
\egroup % end outer box
\unvbox\@vwid@box % put inner box on list without lineskip
\penalty\@vwid@postw
\fi}
% \vbox Wrapper for misc vlist items
\long\def\@vwid@wrap{\relax
\ifvmode\expandafter\@vwid@dowrap \else \expandafter\@firstofone \fi}
\long\def\@vwid@dowrap#1{%
\setbox\@vwid@box \vbox{\vbox{\let\@vwid@wrap\@firstofone
#1}\penalty\@vwid@postw
}\unvbox\@vwid@box }
\let\@@vwid@special\special
\let\@@vwid@addtocontents\addtocontents
\let\@@vwid@list\list
\let\@@vwid@endtrivlist\endtrivlist
\let\@@vwid@eqnnum\@eqnnum
\long\def\@vwid@special#1{\@vwid@wrap{\@@vwid@special{#1}}}
\long\def\@vwid@addtocontents#1#2{\@vwid@wrap{\@@vwid@addtocontents{#1}{#2}}}
\long\def\@vwid@hangfrom#1{\par
\setbox\@tempboxa\hbox{{#1}}%
\setbox\@vwid@box \vbox{\hbox{\kern\z@ \kern\z@
}\penalty\@vwid@offsets}\unvbox\@vwid@box
\def\par{\relax\ifhmode\unskip\fi
\vadjust{\hbox{\kern\hangindent\kern\z@}\penalty\@vwid@offsets}%
\@restorepar\par}%
\hangindent \wd\@tempboxa\noindent\box\@tempboxa}
\def\@vwid@list{\@vwid@setlist\@@vwid@list}
\def\@vwid@endtrivlist{\@vwid@setlist\@@vwid@endtrivlist}
\def\@vwid@setlist{\relax\ifhmode \unskip\expandafter\vadjust\fi
{\setbox\@vwid@box \vbox{\hbox{%
\advance\hsize-\linewidth \advance\hsize-\@totalleftmargin
\kern\@totalleftmargin \kern\hsize}%
\penalty\@vwid@offsets}%
\unvbox\@vwid@box}}
\newif\if@vwid@eqmode
\def\@vwid@afterva{\vadjust{\penalty\@vwid@postnump}}
% Should I do this? ...
\@ifundefined{newcolumntype}{}{%
\@ifundefined{NC@rewrite@V}{
\newcolumntype{V}[1]{%
>{\begin{varwidth}[t]{#1}\narrowragged\let\\\tabularnewline}%
l%
<{\@finalstrut\@arstrutbox\end{varwidth}}}
}{}
}