Self documenting parser

[bandali]

From literate-unitb created by aminb : unitb/literate-unitb#14

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

---

The file ./syntax.txt documents the top-most syntax of machines - not including expressions or proofs. Here are the first 7 lines:

#!text
\assumption{fresh-name}{expression}
\comment{text / comment}{text / comment}
\constant{text / comment}
\constraint{fresh-name}{expression}
\cschedule{concrete event-name}{fresh-name}{expression}
\dummy{text / comment}
\evassignment{concrete event-name}{fresh-name}{expression}

And the last two lines:

#!text

\begin{liveness}{proof-obligation-name} .. \end{liveness}
\begin{proof}{proof-obligation-name} .. \end{proof}

Note that they don't come with descriptive paragraphs and the inside of \begin / \end are not described.

Improvements:
o Include a paragraph for every command / environment
o Include a section for the syntax of expressions
o Include a section for predicate calculus proofs
o Include a section for liveness proofs

---

• Bitbucket: https://bitbucket.org/literateunitb/literate-unitb/issue/14