Repository: alecthomas/chroma
Pull request #906 (2024-01-02 04:01:38)

Add lexer for Promela
This pull request adds a lexer for Promela. (https://spinroot.com/spin/whatispin.html)

I have opened a similar pull request for Pygments: https://github.com/pygments/pygments/pull/2620
I generated the lexer using my branch of Pygments with Promela.

```bash
$ python3 -m venv pygments-promela
$ source pygments-promela/bin/activate
$ pip install pystache
$ pip install /path/to/pygments-promela 

$ python3 _tools/pygments2chroma_xml.py pygments.lexers.c_like.PromelaLexer > lexers/embedded/promela.xml
```

Verified expected formatting using `go run .` Playground.

alecthomas: Would you mind adding some test text please?

Patch:
diff --git a/README.md b/README.md
index c272c03..acf54bf 100644
--- a/README.md
+++ b/README.md
@@ -53,7 +53,7 @@ translators for Pygments lexers and styles.
 |   M    | Makefile, Mako, markdown, Mason, Materialize SQL dialect, Mathematica, Matlab, mcfunction, Meson, Metal, MiniZinc, MLIR, Modula-2, MonkeyC, MorrowindScript, Myghty, MySQL                                                                                    |
 |   N    | NASM, Natural, Newspeak, Nginx configuration file, Nim, Nix                                                                                                                                                                          |
 |   O    | Objective-C, OCaml, Octave, Odin, OnesEnterprise, OpenEdge ABL, OpenSCAD, Org Mode                                                                                                                                                   |
-|   P    | PacmanConf, Perl, PHP, PHTML, Pig, PkgConfig, PL/pgSQL, plaintext, Plutus Core, Pony, PostgreSQL SQL dialect, PostScript, POVRay, PowerQuery, PowerShell, Prolog, PromQL, properties, Protocol Buffer, PRQL, PSL, Puppet, Python, Python 2 |
+|   P    | PacmanConf, Perl, PHP, PHTML, Pig, PkgConfig, PL/pgSQL, plaintext, Plutus Core, Pony, PostgreSQL SQL dialect, PostScript, POVRay, PowerQuery, PowerShell, Prolog, PromQL, Promela, properties, Protocol Buffer, PRQL, PSL, Puppet, Python, Python 2 |
 |   Q    | QBasic, QML                                                                                                                                                                                                                          |
 |   R    | R, Racket, Ragel, Raku, react, ReasonML, reg, reStructuredText, Rexx, Ruby, Rust                                                                                                                                                     |
 |   S    | SAS, Sass, Scala, Scheme, Scilab, SCSS, Sed, Sieve, Smali, Smalltalk, Smarty, Snobol, Solidity, SourcePawn, SPARQL, SQL, SquidConf, Standard ML, stas, Stylus, Svelte, Swift, SYSTEMD, systemverilog                                 |
diff --git a/lexers/embedded/promela.xml b/lexers/embedded/promela.xml
new file mode 100644
index 0000000..6a47796
--- /dev/null
+++ b/lexers/embedded/promela.xml
@@ -0,0 +1,120 @@
+
+<lexer>
+  <config>
+    <name>Promela</name>
+    <alias>promela</alias>
+    <filename>*.pml</filename>
+    <filename>*.prom</filename>
+    <filename>*.prm</filename>
+    <filename>*.promela</filename>
+    <filename>*pr</filename>
+    <filename>*.pm</filename>
+    <mime_type>text/x-promela</mime_type>
+  </config>
+  <rules>
+    <state name="statements">
+      <rule pattern="(\[\]|&lt;&gt;|/\\|\\/)|(U|W|V)\b"><token type="Operator"/></rule>
+      <rule pattern="[@]"><token type="Punctuation"/></rule>
+      <rule pattern="(\.)([a-zA-Z_]\w*)"><bygroups><token type="Operator"/><token type="NameAttribute"/></bygroups></rule>
+      <rule><include state="keywords"/></rule>
+      <rule><include state="types"/></rule>
+      <rule pattern="([LuU]|u8)?(&quot;)"><bygroups><token type="LiteralStringAffix"/><token type="LiteralString"/></bygroups><push state="string"/></rule>
+      <rule pattern="([LuU]|u8)?(&#x27;)(\\.|\\[0-7]{1,3}|\\x[a-fA-F0-9]{1,2}|[^\\\&#x27;\n])(&#x27;)"><bygroups><token type="LiteralStringAffix"/><token type="LiteralStringChar"/><token type="LiteralStringChar"/><token type="LiteralStringChar"/></bygroups></rule>
+      <rule pattern="0[xX]([0-9a-fA-F](\&#x27;?[0-9a-fA-F])*\.[0-9a-fA-F](\&#x27;?[0-9a-fA-F])*|\.[0-9a-fA-F](\&#x27;?[0-9a-fA-F])*|[0-9a-fA-F](\&#x27;?[0-9a-fA-F])*)[pP][+-]?[0-9a-fA-F](\&#x27;?[0-9a-fA-F])*[lL]?"><token type="LiteralNumberFloat"/></rule>
+      <rule pattern="(-)?(\d(\&#x27;?\d)*\.\d(\&#x27;?\d)*|\.\d(\&#x27;?\d)*|\d(\&#x27;?\d)*)[eE][+-]?\d(\&#x27;?\d)*[fFlL]?"><token type="LiteralNumberFloat"/></rule>
+      <rule pattern="(-)?((\d(\&#x27;?\d)*\.(\d(\&#x27;?\d)*)?|\.\d(\&#x27;?\d)*)[fFlL]?)|(\d(\&#x27;?\d)*[fFlL])"><token type="LiteralNumberFloat"/></rule>
+      <rule pattern="(-)?0[xX][0-9a-fA-F](\&#x27;?[0-9a-fA-F])*(([uU][lL]{0,2})|[lL]{1,2}[uU]?)?"><token type="LiteralNumberHex"/></rule>
+      <rule pattern="(-)?0[bB][01](\&#x27;?[01])*(([uU][lL]{0,2})|[lL]{1,2}[uU]?)?"><token type="LiteralNumberBin"/></rule>
+      <rule pattern="(-)?0(\&#x27;?[0-7])+(([uU][lL]{0,2})|[lL]{1,2}[uU]?)?"><token type="LiteralNumberOct"/></rule>
+      <rule pattern="(-)?\d(\&#x27;?\d)*(([uU][lL]{0,2})|[lL]{1,2}[uU]?)?"><token type="LiteralNumberInteger"/></rule>
+      <rule pattern="[~!%^&amp;*+=|?:&lt;&gt;/-]"><token type="Operator"/></rule>
+      <rule pattern="[()\[\],.]"><token type="Punctuation"/></rule>
+      <rule pattern="(true|false|NULL)\b"><token type="NameBuiltin"/></rule>
+      <rule pattern="(?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8})+"><token type="Name"/></rule>
+    </state>
+    <state name="types">
+      <rule pattern="(bit|bool|byte|pid|short|int|unsigned)\b"><token type="KeywordType"/></rule>
+    </state>
+    <state name="keywords">
+      <rule pattern="(atomic|break|d_step|do|od|for|in|goto|if|fi|unless)\b"><token type="Keyword"/></rule>
+      <rule pattern="(assert|get_priority|printf|printm|set_priority)\b"><token type="NameFunction"/></rule>
+      <rule pattern="(c_code|c_decl|c_expr|c_state|c_track)\b"><token type="Keyword"/></rule>
+      <rule pattern="(_|_last|_nr_pr|_pid|_priority|else|np_|STDIN)\b"><token type="NameBuiltin"/></rule>
+      <rule pattern="(empty|enabled|eval|full|len|nempty|nfull|pc_value)\b"><token type="NameFunction"/></rule>
+      <rule pattern="(run)\b"><token type="OperatorWord"/></rule>
+      <rule pattern="(active|chan|D_proctype|hidden|init|local|mtype|never|notrace|proctype|show|trace|typedef|xr|xs)\b"><token type="KeywordDeclaration"/></rule>
+      <rule pattern="(priority|provided)\b"><token type="Keyword"/></rule>
+      <rule pattern="(inline|ltl|select)\b"><token type="KeywordDeclaration"/></rule>
+      <rule pattern="(skip)\b"><token type="Keyword"/></rule>
+    </state>
+    <state name="whitespace">
+      <rule pattern="^#if\s+0"><token type="CommentPreproc"/><push state="if0"/></rule>
+      <rule pattern="^#"><token type="CommentPreproc"/><push state="macro"/></rule>
+      <rule pattern="^(\s*(?:/[*].*?[*]/\s*)?)(#if\s+0)"><bygroups><usingself state="root"/><token type="CommentPreproc"/></bygroups><push state="if0"/></rule>
+      <rule pattern="^(\s*(?:/[*].*?[*]/\s*)?)(#)"><bygroups><usingself state="root"/><token type="CommentPreproc"/></bygroups><push state="macro"/></rule>
+      <rule pattern="(^[ \t]*)(?!(?:public|private|protected|default)\b)((?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8})+)(\s*)(:)(?!:)"><bygroups><token type="TextWhitespace"/><token type="NameLabel"/><token type="TextWhitespace"/><token type="Punctuation"/></bygroups></rule>
+      <rule pattern="\n"><token type="TextWhitespace"/></rule>
+      <rule pattern="[^\S\n]+"><token type="TextWhitespace"/></rule>
+      <rule pattern="\\\n"><token type="Text"/></rule>
+      <rule pattern="//(?:.|(?&lt;=\\)\n)*\n"><token type="CommentSingle"/></rule>
+      <rule pattern="/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/"><token type="CommentMultiline"/></rule>
+      <rule pattern="/(\\\n)?[*][\w\W]*"><token type="CommentMultiline"/></rule>
+    </state>
+    <state name="root">
+      <rule><include state="whitespace"/></rule>
+      <rule><include state="keywords"/></rule>
+      <rule pattern="((?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8}|::)+(?:[&amp;*\s])+)(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)((?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8}|::)+)(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)(\([^;&quot;\&#x27;)]*?\))(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)([^;{/&quot;\&#x27;]*)(\{)"><bygroups><usingself state="root"/><usingself state="whitespace"/><token type="NameFunction"/><usingself state="whitespace"/><usingself state="root"/><usingself state="whitespace"/><usingself state="root"/><token type="Punctuation"/></bygroups><push state="function"/></rule>
+      <rule pattern="((?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8}|::)+(?:[&amp;*\s])+)(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)((?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8}|::)+)(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)(\([^;&quot;\&#x27;)]*?\))(\s*(?:(?:(?://(?:.|(?&lt;=\\)\n)*\n)|(?:/(?:\\\n)?[*](?:[^*]|[*](?!(?:\\\n)?/))*[*](?:\\\n)?/))\s*)*)([^;/&quot;\&#x27;]*)(;)"><bygroups><usingself state="root"/><usingself state="whitespace"/><token type="NameFunction"/><usingself state="whitespace"/><usingself state="root"/><usingself state="whitespace"/><usingself state="root"/><token type="Punctuation"/></bygroups></rule>
+      <rule><include state="types"/></rule>
+      <rule><push state="statement"/></rule>
+    </state>
+    <state name="statement">
+      <rule><include state="whitespace"/></rule>
+      <rule><include state="statements"/></rule>
+      <rule pattern="\}"><token type="Punctuation"/></rule>
+      <rule pattern="[{;]"><token type="Punctuation"/><pop depth="1"/></rule>
+    </state>
+    <state name="function">
+      <rule><include state="whitespace"/></rule>
+      <rule><include state="statements"/></rule>
+      <rule pattern=";"><token type="Punctuation"/></rule>
+      <rule pattern="\{"><token type="Punctuation"/><push/></rule>
+      <rule pattern="\}"><token type="Punctuation"/><pop depth="1"/></rule>
+    </state>
+    <state name="string">
+      <rule pattern="&quot;"><token type="LiteralString"/><pop depth="1"/></rule>
+      <rule pattern="\\([\\abfnrtv&quot;\&#x27;]|x[a-fA-F0-9]{2,4}|u[a-fA-F0-9]{4}|U[a-fA-F0-9]{8}|[0-7]{1,3})"><token type="LiteralStringEscape"/></rule>
+      <rule pattern="[^\\&quot;\n]+"><token type="LiteralString"/></rule>
+      <rule pattern="\\\n"><token type="LiteralString"/></rule>
+      <rule pattern="\\"><token type="LiteralString"/></rule>
+    </state>
+    <state name="macro">
+      <rule pattern="(\s*(?:/[*].*?[*]/\s*)?)(include)(\s*(?:/[*].*?[*]/\s*)?)(&quot;[^&quot;]+&quot;)([^\n]*)"><bygroups><usingself state="root"/><token type="CommentPreproc"/><usingself state="root"/><token type="CommentPreprocFile"/><token type="CommentSingle"/></bygroups></rule>
+      <rule pattern="(\s*(?:/[*].*?[*]/\s*)?)(include)(\s*(?:/[*].*?[*]/\s*)?)(&lt;[^&gt;]+&gt;)([^\n]*)"><bygroups><usingself state="root"/><token type="CommentPreproc"/><usingself state="root"/><token type="CommentPreprocFile"/><token type="CommentSingle"/></bygroups></rule>
+      <rule pattern="[^/\n]+"><token type="CommentPreproc"/></rule>
+      <rule pattern="/[*](.|\n)*?[*]/"><token type="CommentMultiline"/></rule>
+      <rule pattern="//.*?\n"><token type="CommentSingle"/><pop depth="1"/></rule>
+      <rule pattern="/"><token type="CommentPreproc"/></rule>
+      <rule pattern="(?&lt;=\\)\n"><token type="CommentPreproc"/></rule>
+      <rule pattern="\n"><token type="CommentPreproc"/><pop depth="1"/></rule>
+    </state>
+    <state name="if0">
+      <rule pattern="^\s*#if.*?(?&lt;!\\)\n"><token type="CommentPreproc"/><push/></rule>
+      <rule pattern="^\s*#el(?:se|if).*\n"><token type="CommentPreproc"/><pop depth="1"/></rule>
+      <rule pattern="^\s*#endif.*?(?&lt;!\\)\n"><token type="CommentPreproc"/><pop depth="1"/></rule>
+      <rule pattern=".*?\n"><token type="Comment"/></rule>
+    </state>
+    <state name="classname">
+      <rule pattern="(?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8})+"><token type="NameClass"/><pop depth="1"/></rule>
+      <rule pattern="\s*(?=&gt;)"><token type="Text"/><pop depth="1"/></rule>
+      <rule><pop depth="1"/></rule>
+    </state>
+    <state name="case-value">
+      <rule pattern="(?&lt;!:)(:)(?!:)"><token type="Punctuation"/><pop depth="1"/></rule>
+      <rule pattern="(?!\d)(?:[\w$]|\\u[0-9a-fA-F]{4}|\\U[0-9a-fA-F]{8})+"><token type="NameConstant"/></rule>
+      <rule><include state="whitespace"/></rule>
+      <rule><include state="statements"/></rule>
+    </state>
+  </rules>
+</lexer>
+


Test patch:
diff --git a/lexers/testdata/promela/calc.actual b/lexers/testdata/promela/calc.actual
new file mode 100644
index 0000000..126685e
--- /dev/null
+++ b/lexers/testdata/promela/calc.actual
@@ -0,0 +1,20 @@
+// reverse polish
+
+mtype = { operator, value }
+
+chan f = [12] of { mtype, int }
+
+proctype calc(chan you)
+{	int s, lft, rgt
+	chan me = [0] of { int }
+
+	if
+	:: f?operator(s)
+		run calc(me); me?lft
+		run calc(me); me?rgt
+		if
+		:: s == '+' -> you!(lft+rgt)
+		fi
+	:: f?value(s) -> you!s
+	fi
+}
diff --git a/lexers/testdata/promela/calc.expected b/lexers/testdata/promela/calc.expected
new file mode 100644
index 0000000..0ca4425
--- /dev/null
+++ b/lexers/testdata/promela/calc.expected
@@ -0,0 +1,151 @@
+[
+  {"type":"CommentSingle","value":"// reverse polish\n"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"operator"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"value"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"KeywordDeclaration","value":"chan"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"f"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"["},
+  {"type":"LiteralNumberInteger","value":"12"},
+  {"type":"Punctuation","value":"]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"of"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordType","value":"int"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"KeywordDeclaration","value":"proctype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"calc"},
+  {"type":"Punctuation","value":"("},
+  {"type":"KeywordDeclaration","value":"chan"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"you"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"KeywordType","value":"int"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"s"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"lft"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"rgt"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"KeywordDeclaration","value":"chan"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"me"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"["},
+  {"type":"LiteralNumberInteger","value":"0"},
+  {"type":"Punctuation","value":"]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"of"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordType","value":"int"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"f"},
+  {"type":"Operator","value":"?"},
+  {"type":"Name","value":"operator"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"s"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"OperatorWord","value":"run"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"calc"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"me"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"me"},
+  {"type":"Operator","value":"?"},
+  {"type":"Name","value":"lft"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"OperatorWord","value":"run"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"calc"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"me"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"me"},
+  {"type":"Operator","value":"?"},
+  {"type":"Name","value":"rgt"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"s"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralStringChar","value":"'+'"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"you"},
+  {"type":"Operator","value":"!"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"lft"},
+  {"type":"Operator","value":"+"},
+  {"type":"Name","value":"rgt"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"f"},
+  {"type":"Operator","value":"?"},
+  {"type":"Name","value":"value"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"s"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"you"},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"s"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/do.actual b/lexers/testdata/promela/do.actual
new file mode 100644
index 0000000..b5df840
--- /dev/null
+++ b/lexers/testdata/promela/do.actual
@@ -0,0 +1,3 @@
+init {
+  a ? b -> a ! b;
+}
diff --git a/lexers/testdata/promela/do.expected b/lexers/testdata/promela/do.expected
new file mode 100644
index 0000000..f18f9d5
--- /dev/null
+++ b/lexers/testdata/promela/do.expected
@@ -0,0 +1,23 @@
+[
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n  "},
+  {"type":"Name","value":"a"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"?"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"b"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"a"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"b"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/dotted-assign.actual b/lexers/testdata/promela/dotted-assign.actual
new file mode 100644
index 0000000..9bc4988
--- /dev/null
+++ b/lexers/testdata/promela/dotted-assign.actual
@@ -0,0 +1,4 @@
+init {
+  intercepted.key = data.key
+  r.b[a] = a * 4 + 7;
+}
diff --git a/lexers/testdata/promela/dotted-assign.expected b/lexers/testdata/promela/dotted-assign.expected
new file mode 100644
index 0000000..a1cff0d
--- /dev/null
+++ b/lexers/testdata/promela/dotted-assign.expected
@@ -0,0 +1,38 @@
+[
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n  "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":"\n  "},
+  {"type":"Name","value":"r"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"b"},
+  {"type":"Punctuation","value":"["},
+  {"type":"Name","value":"a"},
+  {"type":"Punctuation","value":"]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"a"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"*"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"4"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"+"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"7"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/if.actual b/lexers/testdata/promela/if.actual
new file mode 100644
index 0000000..c773cfe
--- /dev/null
+++ b/lexers/testdata/promela/if.actual
@@ -0,0 +1,6 @@
+init {
+    if 
+    :: skip;
+    fi;
+    skip
+}
diff --git a/lexers/testdata/promela/if.expected b/lexers/testdata/promela/if.expected
new file mode 100644
index 0000000..e4c48c9
--- /dev/null
+++ b/lexers/testdata/promela/if.expected
@@ -0,0 +1,20 @@
+[
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n    "},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n    "},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Keyword","value":"skip"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n    "},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n    "},
+  {"type":"Keyword","value":"skip"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/intruder.actual b/lexers/testdata/promela/intruder.actual
new file mode 100644
index 0000000..16c045e
--- /dev/null
+++ b/lexers/testdata/promela/intruder.actual
@@ -0,0 +1,4 @@
+Crypt x;
+init {
+  Crypt x;
+}
diff --git a/lexers/testdata/promela/intruder.expected b/lexers/testdata/promela/intruder.expected
new file mode 100644
index 0000000..dfaf812
--- /dev/null
+++ b/lexers/testdata/promela/intruder.expected
@@ -0,0 +1,18 @@
+[
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"x"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n  "},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"x"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/ltl.actual b/lexers/testdata/promela/ltl.actual
new file mode 100644
index 0000000..4d3f9f7
--- /dev/null
+++ b/lexers/testdata/promela/ltl.actual
@@ -0,0 +1,1 @@
+ltl alwayserr { [] ((statusa == err) || (statusb == err)) }
diff --git a/lexers/testdata/promela/ltl.expected b/lexers/testdata/promela/ltl.expected
new file mode 100644
index 0000000..9771bd9
--- /dev/null
+++ b/lexers/testdata/promela/ltl.expected
@@ -0,0 +1,30 @@
+[
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"alwayserr"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"[]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"(("},
+  {"type":"Name","value":"statusa"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"||"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusb"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":"))"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/msg.actual b/lexers/testdata/promela/msg.actual
new file mode 100644
index 0000000..35eb5cd
--- /dev/null
+++ b/lexers/testdata/promela/msg.actual
@@ -0,0 +1,4 @@
+
+init {
+  1 == 1 -> 3
+}
diff --git a/lexers/testdata/promela/msg.expected b/lexers/testdata/promela/msg.expected
new file mode 100644
index 0000000..c03df99
--- /dev/null
+++ b/lexers/testdata/promela/msg.expected
@@ -0,0 +1,19 @@
+[
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n  "},
+  {"type":"LiteralNumberInteger","value":"1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"3"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/sample.actual b/lexers/testdata/promela/sample.actual
new file mode 100644
index 0000000..7610f40
--- /dev/null
+++ b/lexers/testdata/promela/sample.actual
@@ -0,0 +1,275 @@
+/**
+	Needham-Schroeder message passing protocol (patched). 
+	|	msg1:	agentA -> agentB	(keyB, agentA, nonceA, 0)
+	|	msg2:	agentB -> agentA	(keyA, agentB, nonceA, nonceB)
+	|	msg3:	agentA -> agentB	(keyB, nonceB, 0, 0)
+
+	Note that sending (keyB, agentA, nonceA) from agentA to agentB 
+	over the network (chan)nel models agentA encrypting the message 
+	"[agentA, nonceB]" with agentB's public key.
+*/
+
+mtype = {
+	/* Status Codes */
+	ok, 
+	err, 
+
+	/* Message Codes */
+	msg1, 
+	msg2, 
+	msg3, 
+
+	/*	Agent (A)lice */
+	keyA,
+	agentA, 
+	nonceA,
+
+	/*	Agent (B)ob */
+	keyB, 
+	agentB,
+	nonceB,
+
+	/*	Agent (I)ntruder */
+	keyI, 
+	agentI, 
+	nonceI 
+};
+
+
+/**
+	Declare a structured data type to model our encrypted messages.
+	Messages will contain either 2 or 3 content fields.
+*/
+typedef Crypt { 
+	mtype key, 
+	content1, 
+	content2,
+	content3 
+};
+
+
+/**
+	Model network between agents via a rendezvous channel. 
+	Send and recieve operations are performed synchronously. 
+*/
+chan network = [0] of {mtype, mtype, Crypt};
+
+
+/* global variables for verification*/
+mtype partnerA; 
+mtype partnerB;
+mtype statusA = err;
+mtype statusB = err;
+bool knows_nonceA; 
+bool knows_nonceB;
+
+/* Agent (A)lice */
+active proctype Alice() {
+
+	/* local variables */
+	mtype pkey;			/* reciever's public key */
+	mtype pnonce;		/* reciever's nonce	 */
+	Crypt messageAB;	/* sent messages			 */
+	Crypt data;			/* recieved messages	 */
+
+	/* 
+		Initialization: In this example we non-deterministically choose between 
+		agents (B)ob and (I)ntruder
+	*/
+	if 
+	:: partnerA = agentB; pkey = keyB;
+	:: partnerA = agentI; pkey = keyI;
+	fi;
+
+	/* prepare (msg1) */
+	messageAB.key = pkey;
+	messageAB.content1 = agentA;
+	messageAB.content2 = nonceA;
+	messageAB.content3 = 0;
+
+	/* send (msg1) */
+	network ! msg1 (partnerA, messageAB);
+
+	/* recv (msg2) : blocking */
+	network ? (msg2, agentA, data);
+
+	/* verify (msg2) : blocking	*/
+	(data.key == keyA) && (data.content1 == partnerA) && (data.content2 == nonceA);
+
+	/* obtain (msg2) sender's nonce */
+	pnonce = data.content3;
+
+	/* prepare (msg3) */
+	messageAB.key = pkey;
+	messageAB.content1 = pnonce;
+	messageAB.content2 = 0;
+	messageAB.content3 = 0;
+
+	/* send (msg3) */
+	network ! msg3 (partnerA, messageAB);
+
+	/* update status */
+	statusA = ok;
+}
+
+/* Agent (B)ob */
+active proctype Bob() {
+		
+	/* local variables */
+	mtype pkey;			/* reciever's public key */
+	mtype pnonce;		/* reciever's nonce	 */
+	Crypt messageBA;	/* sent messages			 */
+	Crypt data;			/* recieved messages	 */
+
+	/* Initialization	*/
+	partnerB = agentA;
+	pkey	 = keyA;
+
+	/* recv (msg1) : blocking */
+	network ? (msg1, agentB, data)
+
+	/* verify (msg1) : blocking */
+	(data.key == keyB) && (data.content1 == agentA);
+
+	/* obtain (msg1) sender's nonce */
+	pnonce = data.content2;	
+
+	/* prepare (msg2) */
+	messageBA.key = pkey;
+	messageBA.content1 = agentB;
+	messageBA.content2 = pnonce;
+	messageBA.content3 = nonceB;
+
+	/* send (msg2) */
+	network ! msg2 (partnerB, messageBA);
+
+	/* recv (msg3) : blocking */
+	network ? (msg3, agentB, data);
+
+	/* verify (msg3) : blocking */
+	(data.key == keyB) && (data.content1 == nonceB);
+
+	statusB = ok;
+}
+
+/* Agent (I)ntruder */
+active proctype Intruder() {
+
+	mtype msg, recpt;
+	Crypt data, intercepted;
+
+	/* Initialize knows_nonce variables to false */
+	knows_nonceA = false;
+	knows_nonceB = false;
+
+	do
+	:: network ? (msg, _, data) -> 
+	if /* perhaps store the message */
+			
+		::	intercepted.key		 = data.key;
+			intercepted.content1 = data.content1;
+			intercepted.content2 = data.content2;
+			
+			/*	
+				Message contains (I)ntruder's (public) key, the intruder can 
+				decrypt the message. Note that we can learn nonce values from 
+				either content1 or content2
+				|	msg1:	(keyB, agentA, nonceA, 0)
+				|	msg2:	(keyA, agentB, nonceA, nonceB)
+				|	msg3: 	(keyB, nonceB, 0, 0)
+			*/
+			if 
+			::  (intercepted.key == keyI) -> if 
+				:: intercepted.content1 == nonceA -> knows_nonceA = true; 
+				:: intercepted.content1 == nonceB -> knows_nonceB = true; 
+				:: intercepted.content2 == nonceA -> knows_nonceA = true; 
+				:: intercepted.content2 == nonceB -> knows_nonceB = true; 
+				:: intercepted.content3 == nonceA -> knows_nonceA = true; 
+				:: intercepted.content3 == nonceB -> knows_nonceB = true;
+				fi 
+
+			:: skip;
+			fi 
+
+		:: skip;
+	fi;
+
+	:: /* Replay or send a message */
+	if /* choose message type */
+		:: msg = msg1;
+		:: msg = msg2;
+		:: msg = msg3;
+	fi;
+		
+	if /* choose a recepient */
+		:: recpt = agentA;
+		:: recpt = agentB;
+	fi;
+			 
+	if /* replay intercepted message or assemble it */
+		::	data.key		= intercepted.key;
+			data.content1	= intercepted.content1;
+			data.content2	= intercepted.content2;
+			data.content3	= intercepted.content3;
+		
+		:: 
+		if /* assemble content1 */
+			:: data.content1 = agentA;
+			:: data.content1 = agentB;
+			:: data.content1 = agentI;
+			:: (knows_nonceA) -> data.content1 = nonceA
+			:: (knows_nonceB) -> data.content1 = nonceB
+			:: (!knows_nonceA && !knows_nonceB) -> data.content1 = nonceI;
+		fi;
+		
+		if /* assemble key */
+			:: data.key = keyA;
+			:: data.key = keyB;
+			:: data.key = keyI;
+		fi;
+		
+		if 
+		:: (knows_nonceA) -> data.content2 = nonceA
+		:: (knows_nonceB) -> data.content2 = nonceB
+		:: (!knows_nonceA && !knows_nonceB) -> data.content2 = nonceI;
+		fi 
+
+		if 
+		:: (knows_nonceA) -> data.content3 = nonceA
+		:: (knows_nonceB) -> data.content3 = nonceB
+		:: (!knows_nonceA && !knows_nonceB) -> data.content3 = nonceI;
+		fi 
+		
+	fi;
+
+	network ! msg (recpt, data);
+	od
+}
+
+/**
+	Always, one process will terminate in error
+*/
+ltl alwaysErr { [] ( (statusA == err) || (statusB == err) ) }
+
+/**
+	Eventually the protocol will complete without error
+*/
+ltl eventuallyOk { <> ( (statusA == ok) && (statusB == ok) ) }
+
+/*
+	propAB: If both Alice and Bob reach the end of their runs (i.e. both statusA and statusB are ok) 
+	then Alice's communication partner is Bob, and Bob's communication partner is Alice.
+*/
+ltl propAB { [] ( ( (statusA == ok) && (statusB == ok) ) -> ( (partnerB == agentA) && (partnerA == agentB) ) ) }
+
+/*
+	propA: If agent A reaches the end of its run (statusA is ok) and A believes it is talking to B 
+	(partnerA is agentB) then the intruder does not know A's nonce (!knows_nonceA).
+*/
+ltl propA { [] ( ( (statusA == ok)  && (partnerA == agentB) ) ->  ( knows_nonceA == false ) ) }
+
+/*
+	propB: If agent B reaches the end of its run (statusB is ok) and it believes it is talking to A 
+	(partnerB is agentA) then the intruder does not know B's nonce (!knows_nonceB)
+*/
+ltl propB { [] ( ( (statusB == ok)  && (partnerB == agentA) ) ->  ( knows_nonceB == false ) ) }
diff --git a/lexers/testdata/promela/sample.expected b/lexers/testdata/promela/sample.expected
new file mode 100644
index 0000000..7d32b94
--- /dev/null
+++ b/lexers/testdata/promela/sample.expected
@@ -0,0 +1,1491 @@
+[
+  {"type":"CommentMultiline","value":"/**\n\tNeedham-Schroeder message passing protocol (patched). \n\t|\tmsg1:\tagentA -\u003e agentB\t(keyB, agentA, nonceA, 0)\n\t|\tmsg2:\tagentB -\u003e agentA\t(keyA, agentB, nonceA, nonceB)\n\t|\tmsg3:\tagentA -\u003e agentB\t(keyB, nonceB, 0, 0)\n\n\tNote that sending (keyB, agentA, nonceA) from agentA to agentB \n\tover the network (chan)nel models agentA encrypting the message \n\t\"[agentA, nonceB]\" with agentB's public key.\n*/"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"CommentMultiline","value":"/* Status Codes */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\n\t"},
+  {"type":"CommentMultiline","value":"/* Message Codes */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"msg1"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"msg2"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"msg3"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\n\t"},
+  {"type":"CommentMultiline","value":"/*\tAgent (A)lice */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"keyA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"nonceA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/*\tAgent (B)ob */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"keyB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"nonceB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/*\tAgent (I)ntruder */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"keyI"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"agentI"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"nonceI"},
+  {"type":"TextWhitespace","value":" \n"},
+  {"type":"Punctuation","value":"};"},
+  {"type":"TextWhitespace","value":"\n\n\n"},
+  {"type":"CommentMultiline","value":"/**\n\tDeclare a structured data type to model our encrypted messages.\n\tMessages will contain either 2 or 3 content fields.\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"typedef"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"key"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"content1"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Name","value":"content2"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"content3"},
+  {"type":"TextWhitespace","value":" \n"},
+  {"type":"Punctuation","value":"};"},
+  {"type":"TextWhitespace","value":"\n\n\n"},
+  {"type":"CommentMultiline","value":"/**\n\tModel network between agents via a rendezvous channel. \n\tSend and recieve operations are performed synchronously. \n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"chan"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"["},
+  {"type":"LiteralNumberInteger","value":"0"},
+  {"type":"Punctuation","value":"]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"of"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"Crypt"},
+  {"type":"Punctuation","value":"};"},
+  {"type":"TextWhitespace","value":"\n\n\n"},
+  {"type":"CommentMultiline","value":"/* global variables for verification*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"partnerA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"partnerB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordType","value":"bool"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n"},
+  {"type":"KeywordType","value":"bool"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/* Agent (A)lice */"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"active"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"proctype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"Alice"},
+  {"type":"Punctuation","value":"()"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* local variables */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t\t"},
+  {"type":"CommentMultiline","value":"/* reciever's public key */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pnonce"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t"},
+  {"type":"CommentMultiline","value":"/* reciever's nonce\t */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"CommentMultiline","value":"/* sent messages\t\t\t */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t\t"},
+  {"type":"CommentMultiline","value":"/* recieved messages\t */"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* \n\t\tInitialization: In this example we non-deterministically choose between \n\t\tagents (B)ob and (I)ntruder\n\t*/"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"partnerA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"partnerA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* prepare (msg1) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"0"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* send (msg1) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* recv (msg2) : blocking */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"?"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"msg2"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* verify (msg2) : blocking\t*/"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"partnerA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* obtain (msg2) sender's nonce */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"pnonce"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* prepare (msg3) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pnonce"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"0"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"LiteralNumberInteger","value":"0"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* send (msg3) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerA"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"messageAB"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* update status */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/* Agent (B)ob */"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"active"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"proctype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"Bob"},
+  {"type":"Punctuation","value":"()"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n\t\t\n\t"},
+  {"type":"CommentMultiline","value":"/* local variables */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t\t"},
+  {"type":"CommentMultiline","value":"/* reciever's public key */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pnonce"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t"},
+  {"type":"CommentMultiline","value":"/* reciever's nonce\t */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"CommentMultiline","value":"/* sent messages\t\t\t */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\t\t"},
+  {"type":"CommentMultiline","value":"/* recieved messages\t */"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* Initialization\t*/"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"partnerB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"pkey"},
+  {"type":"TextWhitespace","value":"\t "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* recv (msg1) : blocking */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"?"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"msg1"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* verify (msg1) : blocking */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* obtain (msg1) sender's nonce */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"pnonce"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\t\n\n\t"},
+  {"type":"CommentMultiline","value":"/* prepare (msg2) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pkey"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"pnonce"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* send (msg2) */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"messageBA"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* recv (msg3) : blocking */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"?"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"msg3"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* verify (msg3) : blocking */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/* Agent (I)ntruder */"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"active"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"proctype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"Intruder"},
+  {"type":"Punctuation","value":"()"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"KeywordDeclaration","value":"mtype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"recpt"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"Crypt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"CommentMultiline","value":"/* Initialize knows_nonce variables to false */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"false"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"false"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"Keyword","value":"do"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"?"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"msg"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"_"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" \n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* perhaps store the message */"},
+  {"type":"TextWhitespace","value":"\n\t\t\t\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":"\t\t "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t\n\t\t\t"},
+  {"type":"CommentMultiline","value":"/*\t\n\t\t\t\tMessage contains (I)ntruder's (public) key, the intruder can \n\t\t\t\tdecrypt the message. Note that we can learn nonce values from \n\t\t\t\teither content1 or content2\n\t\t\t\t|\tmsg1:\t(keyB, agentA, nonceA, 0)\n\t\t\t\t|\tmsg2:\t(keyA, agentB, nonceA, nonceB)\n\t\t\t\t|\tmsg3: \t(keyB, nonceB, 0, 0)\n\t\t\t*/"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":"  "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyI"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":" \n\t\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"true"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":" \n\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Keyword","value":"skip"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":" \n\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Keyword","value":"skip"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* Replay or send a message */"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* choose message type */"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg1"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg2"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg3"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* choose a recepient */"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"recpt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"recpt"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t \n\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* replay intercepted message or assemble it */"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":"\t\t"},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":"\t"},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"intercepted"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" \n\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* assemble content1 */"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content1"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"CommentMultiline","value":"/* assemble key */"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyA"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyB"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"key"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"keyI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t\n\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content2"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":" \n\n\t\t"},
+  {"type":"Keyword","value":"if"},
+  {"type":"TextWhitespace","value":" \n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceA"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceB"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Operator","value":"::"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Operator","value":"."},
+  {"type":"NameAttribute","value":"content3"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"nonceI"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\t\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"TextWhitespace","value":" \n\t\t\n\t"},
+  {"type":"Keyword","value":"fi"},
+  {"type":"Punctuation","value":";"},
+  {"type":"TextWhitespace","value":"\n\n\t"},
+  {"type":"Name","value":"network"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"!"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"msg"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"recpt"},
+  {"type":"Punctuation","value":","},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"data"},
+  {"type":"Punctuation","value":");"},
+  {"type":"TextWhitespace","value":"\n\t"},
+  {"type":"Keyword","value":"od"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/**\n\tAlways, one process will terminate in error\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"alwaysErr"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"[]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"||"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"err"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/**\n\tEventually the protocol will complete without error\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"eventuallyOk"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u003c\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/*\n\tpropAB: If both Alice and Bob reach the end of their runs (i.e. both statusA and statusB are ok) \n\tthen Alice's communication partner is Bob, and Bob's communication partner is Alice.\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"propAB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"[]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/*\n\tpropA: If agent A reaches the end of its run (statusA is ok) and A believes it is talking to B \n\t(partnerA is agentB) then the intruder does not know A's nonce (!knows_nonceA).\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"propA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"[]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"  "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentB"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":"  "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceA"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"false"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n\n"},
+  {"type":"CommentMultiline","value":"/*\n\tpropB: If agent B reaches the end of its run (statusB is ok) and it believes it is talking to A \n\t(partnerB is agentA) then the intruder does not know B's nonce (!knows_nonceB)\n*/"},
+  {"type":"TextWhitespace","value":"\n"},
+  {"type":"KeywordDeclaration","value":"ltl"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"propB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"[]"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"statusB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"ok"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":"  "},
+  {"type":"Operator","value":"\u0026\u0026"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"("},
+  {"type":"Name","value":"partnerB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"agentA"},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"-\u003e"},
+  {"type":"TextWhitespace","value":"  "},
+  {"type":"Punctuation","value":"("},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"knows_nonceB"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Operator","value":"=="},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"NameBuiltin","value":"false"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":")"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/skip.actual b/lexers/testdata/promela/skip.actual
new file mode 100644
index 0000000..b085ad2
--- /dev/null
+++ b/lexers/testdata/promela/skip.actual
@@ -0,0 +1,1 @@
+init { skip }
diff --git a/lexers/testdata/promela/skip.expected b/lexers/testdata/promela/skip.expected
new file mode 100644
index 0000000..ba146bd
--- /dev/null
+++ b/lexers/testdata/promela/skip.expected
@@ -0,0 +1,10 @@
+[
+  {"type":"KeywordDeclaration","value":"init"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Keyword","value":"skip"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"}"},
+  {"type":"TextWhitespace","value":"\n"}
+]
diff --git a/lexers/testdata/promela/welfare.actual b/lexers/testdata/promela/welfare.actual
new file mode 100644
index 0000000..a67dff7
--- /dev/null
+++ b/lexers/testdata/promela/welfare.actual
@@ -0,0 +1,1 @@
+active proctype cr() {}
diff --git a/lexers/testdata/promela/welfare.expected b/lexers/testdata/promela/welfare.expected
new file mode 100644
index 0000000..6004342
--- /dev/null
+++ b/lexers/testdata/promela/welfare.expected
@@ -0,0 +1,11 @@
+[
+  {"type":"KeywordDeclaration","value":"active"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"KeywordDeclaration","value":"proctype"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Name","value":"cr"},
+  {"type":"Punctuation","value":"()"},
+  {"type":"TextWhitespace","value":" "},
+  {"type":"Punctuation","value":"{}"},
+  {"type":"TextWhitespace","value":"\n"}
+]