update

diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex
index b676ffe..2c35ac5 100644 (file)
--- a/ar/assignments/a.tex
+++ b/ar/assignments/a.tex
@@ -1,6 +1,6 @@
 \section{Appendix}
 \newpage
-\lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/a1.smt}
+\lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/1.smt}
 
 \newpage
 \lstinputlisting[language=python,caption={a4.py},label={listing:4.py}]{src/4.py}

diff --git a/ar/assignments/ar.aux b/ar/assignments/ar.aux
new file mode 100644 (file)
index 0000000..f75a08e
--- /dev/null
+++ b/ar/assignments/ar.aux
@@ -0,0 +1,25 @@
+\relax 
+\@writefile{toc}{\contentsline {section}{\numberline {1}Problem 1}{1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Formal definition}{1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}SMT format solution}{2}}
+\newlabel{listing:1bash}{{1}{2}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Iteratively find the largest solution}{2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Solution}{2}}
+\@writefile{toc}{\contentsline {section}{\numberline {2}Problem 4}{3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Formal definition}{3}}
+\@writefile{toc}{\contentsline {paragraph}{Precondition}{3}}
+\newlabel{eq:4pre}{{1}{3}}
+\@writefile{toc}{\contentsline {paragraph}{Program}{3}}
+\newlabel{eq:4pro}{{2}{3}}
+\@writefile{toc}{\contentsline {paragraph}{Postcondition}{3}}
+\newlabel{eq:4pst}{{3}{3}}
+\@writefile{toc}{\contentsline {paragraph}{Total}{3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}SMT format solution}{3}}
+\newlabel{listing:4bash}{{2}{3}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}Iteratively find the shortest solution}{3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Solution}{4}}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Appendix}{4}}
+\newlabel{listing:a1.smt}{{3}{5}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}a1.smt}{5}}
+\newlabel{listing:4.py}{{4}{6}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}a4.py}{6}}

diff --git a/ar/assignments/ar.fmt b/ar/assignments/ar.fmt
new file mode 100644 (file)
index 0000000..ebcbaee
Binary files /dev/null and b/ar/assignments/ar.fmt differ

diff --git a/ar/assignments/ar.log b/ar/assignments/ar.log
new file mode 100644 (file)
index 0000000..89ca6cb
--- /dev/null
+++ b/ar/assignments/ar.log
@@ -0,0 +1,77 @@
+This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2015/dev/Debian) (preloaded format=ar 2015.10.19)  19 OCT 2015 20:25
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**ar
+(./ar.tex
+LaTeX2e <2014/05/01>
+Babel <3.9l> and hyphenation patterns for 79 languages loaded.
+(./ar.aux)
+\openout1 = `ar.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 2.
+LaTeX Font Info:    ... okay on input line 2.
+\c@lstlisting=\count107
+ (./1.tex
+Underfull \hbox (badness 10000) in paragraph at lines 3--6
+
+ []
+
+LaTeX Font Info:    Try loading font information for OMS+cmr on input line 7.
+(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd
+File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
+)
+LaTeX Font Info:    Font shape `OMS/cmr/m/it' in size <10> not available
+(Font)              Font shape `OMS/cmsy/m/n' tried instead on input line 7.
+ [1]
+(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty
+File: lstlang1.sty 2014/09/06 1.5e listings language file
+)
+(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty
+File: lstlang1.sty 2014/09/06 1.5e listings language file
+)
+LaTeX Font Info:    Try loading font information for OML+cmr on input line 72.
+
+(/usr/share/texlive/texmf-dist/tex/latex/base/omlcmr.fd
+File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
+)
+LaTeX Font Info:    Font shape `OML/cmr/m/n' in size <8> not available
+(Font)              Font shape `OML/cmm/m/it' tried instead on input line 72.
+LaTeX Font Info:    Font shape `OMS/cmr/m/n' in size <8> not available
+(Font)              Font shape `OMS/cmsy/m/n' tried instead on input line 72.
+) (./2.tex) (./3.tex)
+(./4.tex [2]
+Overfull \hbox (38.59985pt too wide) detected at line 46
+[] []
+ []
+
+[3]) (./a.tex [4]
+(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty
+File: lstlang1.sty 2014/09/06 1.5e listings language file
+)
+(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang2.sty
+File: lstlang2.sty 2014/09/06 1.5e listings language file
+) (./src/1.smt)
+[5] (/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty
+File: lstlang1.sty 2014/09/06 1.5e listings language file
+) (./src/4.py)) [6] (./ar.aux) ) 
+Here is how much of TeX's memory you used:
+ 807 strings out of 491017
+ 9506 string characters out of 6109189
+ 274834 words of memory out of 5000000
+ 6326 multiletter control sequences out of 15000+600000
+ 14800 words of font info for 52 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 35i,7n,51p,203b,1306s stack positions out of 5000i,500n,10000p,200000b,80000s
+
+Output written on ar.dvi (6 pages, 37960 bytes).

diff --git a/ar/assignments/ar.pdf b/ar/assignments/ar.pdf
new file mode 100644 (file)
index 0000000..8fa46dd
Binary files /dev/null and b/ar/assignments/ar.pdf differ

diff --git a/ar/assignments/src/1.model b/ar/assignments/src/1.model
new file mode 100644 (file)
index 0000000..cf9ab8f
--- /dev/null
+++ b/ar/assignments/src/1.model
@@ -0,0 +1,33 @@
+sat
+
+(= t5n 0)
+(= t1p 0)
+(= t1c 2)
+(= t3c 0)
+(= t2p 3)
+(= t1d 1)
+(= t4c 0)
+(= t4d 1)
+(= t5c 5)
+(= t3s 0)
+(= t3d 0)
+(= t5p 0)
+(= t2s 4)
+(= t5s 0)
+(= t6d 1)
+(= t1s 4)
+(= t6n 4)
+(= t2d 1)
+(= t3n 0)
+(= t4p 7)
+(= t6s 0)
+(= t4s 0)
+(= t4n 0)
+(= t1n 0)
+(= t6c 3)
+(= t5d 1)
+(= t2n 0)
+(= t2c 0)
+(= t6p 0)
+(= t3p 8)
+

diff --git a/ar/assignments/src/a1.smt b/ar/assignments/src/1.smt
similarity index 100%
rename from ar/assignments/src/a1.smt
rename to ar/assignments/src/1.smt

diff --git a/ar/assignments/src/marble.smv b/ar/assignments/src/marble.smv
deleted file mode 100644 (file)
index d9845a8..0000000
--- a/ar/assignments/src/marble.smv
+++ /dev/null
@@ -1,20 +0,0 @@
-MODULE main
-VAR
-a : 0..100;
-c : 0..20;
-INIT
-a = 1 & c = 0
-TRANS
-case 
-       c<20 : next(c) = c+1;
-       TRUE : next(c) = c;
-esac & (
-case 
-       a<100 : next(a) = a+1;
-       TRUE : next(a)=a;
-esac |
-case
-       a<=50 : next(a) = 2*a;
-       TRUE : next(a)=a;
-esac)
-LTLSPEC G !(a = 100 & c = 8)