diff --git a/tutorial/tutorial.pdf b/tutorial/tutorial.pdf
new file mode 100644
index 000000000..0da23652f
Binary files /dev/null and b/tutorial/tutorial.pdf differ
diff --git a/tutorial/tutorial.toc b/tutorial/tutorial.toc
index b06e150d1..8fe247058 100644
--- a/tutorial/tutorial.toc
+++ b/tutorial/tutorial.toc
@@ -1,43 +1,47 @@
 \contentsline {chapter}{\numberline {1}Introduction}{5}{chapter.1}
-\contentsline {section}{\numberline {1.1}Getting Started: A Simple \textsc {Uclid5}{} Model}{5}{section.1.1}
+\contentsline {section}{\numberline {1.1}Getting Started: A Simple {\textsc {Uclid5}}\xspace {} Model}{5}{section.1.1}
 \contentsline {subsubsection}{\nonumberline The System Model}{6}{section*.3}
 \contentsline {subsubsection}{\nonumberline The System Specification}{6}{section*.4}
-\contentsline {subsubsection}{\nonumberline The Proof Script}{6}{section*.5}
-\contentsline {section}{\numberline {1.2}Installing \textsc {Uclid5}{}}{7}{section.1.2}
+\contentsline {subsubsection}{\nonumberline The Proof Script}{7}{section*.5}
+\contentsline {section}{\numberline {1.2}Installing {\textsc {Uclid5}}\xspace {}}{7}{section.1.2}
 \contentsline {subsection}{\numberline {1.2.1}Prerequisites}{7}{subsection.1.2.1}
 \contentsline {subsection}{\numberline {1.2.2}Detailed Installation Instructions}{7}{subsection.1.2.2}
-\contentsline {subsection}{\numberline {1.2.3}Running \textsc {Uclid5}{}}{8}{subsection.1.2.3}
-\contentsline {section}{\numberline {1.3}Looking Forward}{8}{section.1.3}
-\contentsline {chapter}{\numberline {2}Basics: Types and Statements}{9}{chapter.2}
-\contentsline {section}{\numberline {2.1}Types in \textsc {Uclid5}{}}{9}{section.2.1}
-\contentsline {section}{\numberline {2.2}Statements in \textsc {Uclid5}{}}{9}{section.2.2}
-\contentsline {subsection}{\numberline {2.2.1}For Loops}{11}{subsection.2.2.1}
-\contentsline {subsection}{\numberline {2.2.2}If and Case Statements}{11}{subsection.2.2.2}
-\contentsline {subsection}{\numberline {2.2.3}Expressions}{11}{subsection.2.2.3}
-\contentsline {section}{\numberline {2.3}Computation/Verification Model}{11}{section.2.3}
-\contentsline {subsection}{\numberline {2.3.1}Initialization}{11}{subsection.2.3.1}
-\contentsline {subsection}{\numberline {2.3.2}Next State Computation}{11}{subsection.2.3.2}
-\contentsline {subsection}{\numberline {2.3.3}Verification}{12}{subsection.2.3.3}
-\contentsline {subsection}{\numberline {2.3.4}Running \textsc {Uclid5}{}}{12}{subsection.2.3.4}
-\contentsline {chapter}{\numberline {3}Verification Techniques}{13}{chapter.3}
-\contentsline {section}{\numberline {3.1}Inductive Proofs}{13}{section.3.1}
-\contentsline {subsection}{\numberline {3.1.1}Debugging Counterexamples}{13}{subsection.3.1.1}
-\contentsline {subsection}{\numberline {3.1.2}Inductive Proof for the Fibonacci Model}{15}{subsection.3.1.2}
-\contentsline {chapter}{\numberline {4}Compositional Reasoning with Modules}{17}{chapter.4}
-\contentsline {section}{\numberline {4.1}Common Type Definitions Across Modules}{17}{section.4.1}
-\contentsline {section}{\numberline {4.2}Uninterpreted Functions and Types}{17}{section.4.2}
-\contentsline {subsection}{\numberline {4.2.1}Uninterpreted Types}{17}{subsection.4.2.1}
-\contentsline {subsection}{\numberline {4.2.2}Uninterpreted Functions}{19}{subsection.4.2.2}
-\contentsline {section}{\numberline {4.3}Procedure Definition}{19}{section.4.3}
-\contentsline {subsection}{\numberline {4.3.1}Procedure Invocation}{19}{subsection.4.3.1}
-\contentsline {section}{\numberline {4.4}Module Instantiation and Scheduling}{21}{section.4.4}
-\contentsline {subsection}{\numberline {4.4.1}Accessing Instance Variables}{21}{subsection.4.4.1}
-\contentsline {section}{\numberline {4.5}Running \textsc {Uclid5}{} On The CPU Model}{21}{section.4.5}
-\contentsline {subsection}{\numberline {4.5.1}Exercise: Inductive Proof of CPU model}{21}{subsection.4.5.1}
-\contentsline {chapter}{\numberline {A}Appendix: \textsc {Uclid5}{} Grammar}{22}{appendix.A}
-\contentsline {section}{\numberline {A.1}Grammar of Modules and Declarations}{22}{section.A.1}
-\contentsline {section}{\numberline {A.2}Statement Grammar}{24}{section.A.2}
-\contentsline {section}{\numberline {A.3}Expression Grammar}{25}{section.A.3}
-\contentsline {section}{\numberline {A.4}Types}{26}{section.A.4}
-\contentsline {section}{\numberline {A.5}Control Block}{27}{section.A.5}
-\contentsline {section}{\numberline {A.6}Miscellaneous Nonterminals}{27}{section.A.6}
+\contentsline {subsection}{\numberline {1.2.3}Running {\textsc {Uclid5}}\xspace {}}{8}{subsection.1.2.3}
+\contentsline {section}{\numberline {1.3}Looking Forward}{9}{section.1.3}
+\contentsline {chapter}{\numberline {2}Basics: Types and Statements}{10}{chapter.2}
+\contentsline {section}{\numberline {2.1}Types in {\textsc {Uclid5}}\xspace {}}{10}{section.2.1}
+\contentsline {section}{\numberline {2.2}Statements in {\textsc {Uclid5}}\xspace {}}{10}{section.2.2}
+\contentsline {subsection}{\numberline {2.2.1}For Loops}{12}{subsection.2.2.1}
+\contentsline {subsection}{\numberline {2.2.2}If and Case Statements}{12}{subsection.2.2.2}
+\contentsline {subsection}{\numberline {2.2.3}Expressions}{12}{subsection.2.2.3}
+\contentsline {section}{\numberline {2.3}Computation/Verification Model}{12}{section.2.3}
+\contentsline {subsection}{\numberline {2.3.1}Initialization}{12}{subsection.2.3.1}
+\contentsline {subsection}{\numberline {2.3.2}Next State Computation}{12}{subsection.2.3.2}
+\contentsline {subsection}{\numberline {2.3.3}Verification}{13}{subsection.2.3.3}
+\contentsline {subsection}{\numberline {2.3.4}Running {\textsc {Uclid5}}\xspace {}}{13}{subsection.2.3.4}
+\contentsline {chapter}{\numberline {3}Verification Techniques}{14}{chapter.3}
+\contentsline {section}{\numberline {3.1}Inductive Proofs}{14}{section.3.1}
+\contentsline {subsection}{\numberline {3.1.1}Debugging Counterexamples}{14}{subsection.3.1.1}
+\contentsline {subsection}{\numberline {3.1.2}Inductive Proof for the Fibonacci Model}{16}{subsection.3.1.2}
+\contentsline {section}{\numberline {3.2}Bounded Model Checking}{17}{section.3.2}
+\contentsline {subsection}{\numberline {3.2.1}Embedded assume and assert statements}{17}{subsection.3.2.1}
+\contentsline {subsection}{\numberline {3.2.2}Running {\textsc {Uclid5}}\xspace {}}{18}{subsection.3.2.2}
+\contentsline {section}{\numberline {3.3}Future Directions}{19}{section.3.3}
+\contentsline {chapter}{\numberline {4}Compositional Modeling and Abstraction}{20}{chapter.4}
+\contentsline {section}{\numberline {4.1}Common Type Definitions Across Modules}{20}{section.4.1}
+\contentsline {section}{\numberline {4.2}Uninterpreted Functions and Types}{20}{section.4.2}
+\contentsline {subsection}{\numberline {4.2.1}Uninterpreted Types}{22}{subsection.4.2.1}
+\contentsline {subsection}{\numberline {4.2.2}Uninterpreted Functions}{22}{subsection.4.2.2}
+\contentsline {section}{\numberline {4.3}Procedure Definition}{22}{section.4.3}
+\contentsline {subsection}{\numberline {4.3.1}Procedure Invocation}{24}{subsection.4.3.1}
+\contentsline {section}{\numberline {4.4}Module Instantiation and Scheduling}{24}{section.4.4}
+\contentsline {subsection}{\numberline {4.4.1}Accessing Instance Variables}{24}{subsection.4.4.1}
+\contentsline {section}{\numberline {4.5}Running {\textsc {Uclid5}}\xspace {}}{24}{section.4.5}
+\contentsline {subsection}{\numberline {4.5.1}Exercise: Inductive Proof of CPU model}{24}{subsection.4.5.1}
+\contentsline {chapter}{\numberline {A}Appendix: {\textsc {Uclid5}}\xspace {} Grammar}{26}{appendix.A}
+\contentsline {section}{\numberline {A.1}Grammar of Modules and Declarations}{26}{section.A.1}
+\contentsline {section}{\numberline {A.2}Statement Grammar}{28}{section.A.2}
+\contentsline {section}{\numberline {A.3}Expression Grammar}{29}{section.A.3}
+\contentsline {section}{\numberline {A.4}Types}{30}{section.A.4}
+\contentsline {section}{\numberline {A.5}Control Block}{31}{section.A.5}
+\contentsline {section}{\numberline {A.6}Miscellaneous Nonterminals}{31}{section.A.6}