Skip to content
This repository has been archived by the owner on Apr 30, 2019. It is now read-only.

Commit

Permalink
added supported syntax description
Browse files Browse the repository at this point in the history
  • Loading branch information
@dohan
dohan committed May 23, 2012
1 parent 7591800 commit 4537913
Showing 1 changed file with 182 additions and 11 deletions.
193 changes: 182 additions & 11 deletions src/main/webapp/formalism/tla/syntax.html
View file
@@ -1,36 +1,207 @@
<div class="sixteen columns">
<h3>TLA<sup>+</sup> Syntax in a Nutshell</h3>
<h3>Supported TLA<sup>+</sup> Syntax</h3>
</div>

<div class="cheat-box-container eight columns">
<div class="cheat-box">
<h4>Foo</h4>
<h4>Logic</h4>
<table>
<tr class="row-one">
<td class="row-label">Boolean</td>
<td>TRUE, FALSE</td>
<td class="row-label">$P \wedge Q$</td>
<td>P /\ Q</td>
</tr>
<tr>
<td class="row-label">Integer</td>
<td>1,2,3, ...</td>
<td class="row-label">$P \vee Q$</td>
<td>P \/ Q</td>
</tr>
<tr class="row-one">
<td class="row-label">greatest implementable Integer</td>
<td>MAXINT</td>
<td class="row-label">$P \implies Q$</td>
<td>P => Q</td>
</tr>
<tr>
<td class="row-label">least implementable Integer</td>
<td>MININT</td>
<td class="row-label">$P \Leftrightarrow Q$</td>
<td>P <=> Q</td>
</tr>
<tr class="row-one">
<td class="row-label">$\neg P$</td>
<td>\neg P or ~P</td>
</tr>
<td class="row-label">boolean values </td>
<td>TRUE, FALSE</td>
</tr>
<tr class="row-one">
<td class="row-label">Strings</td>
<td class="row-label">$\neg P$</td>
<td>\neg P</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Quantifiers</h4>
<table>
<tr class="row-one">
<td class="row-label">$\exists x \in S \mid P$</td>
<td>\E x \in S : P</td>
</tr>
<tr>
<td class="row-label">$\forall x \in S \mid P$</td>
<td>\A x \in S : P</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Equality</h4>
<table>
<tr class="row-one">
<td class="row-label">$x = y$</td>
<td>x = y</td>
</tr>
<tr>
<td class="row-label">$x \not = y$</td>
<td>x /= y or x # y</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Set Construction</h4>
<table>
<tr class="row-one">
<td class="row-label">Set enumeration</td>
<td>{a,b,c}</td>
</tr>
<tr>
<td class="row-label">Set comprehension $ \{x \in S : P\} $</td>
<td>{x \in S : P}</td>
</tr>
<tr class="row-one">
<td class="row-label">Set comprehension2 $ \{e : x \in S \} $</td>
<td>{e : x \in S}</td>
</tr>
<tr>
<td class="row-label">$e \in S$</td>
<td>e \in S</td>
</tr>
<tr class="row-one">
<td class="row-label">$e \notin S$</td>
<td>e \notin S</td>
</tr>
<tr>
<td class="row-label">$ S \cup T$</td>
<td>S \cup T or S \union T</td>
</tr>
<tr class="row-one">
<td class="row-label">$S \cap T$</td>
<td>S \cap T or S \intersect T</td>
</tr>
<tr>
<td class="row-label">$S \subseteq T$</td>
<td>S \subseteq T</td>
</tr>
<tr class="row-one">
<td class="row-label">Set difference $S \backslash T$</td>
<td>S \ t</td>
</tr>
<tr>
<td class="row-label">Set of subsets</td>
<td>SUBSET S</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Functions</h4>
<table>
<tr class="row-one">
<td class="row-label">Function application</td>
<td>f[e]</td>
</tr>
<tr>
<td class="row-label">Domain</td>
<td>DOMAIN f</td>
</tr>
<tr class="row-one">
<td class="row-label">$[x \in S \mapsto e]$</td>
<td>[x \in S |-> e]</td>
</tr>
<tr>
<td class="row-label">$[ S \rightarrow T ]$</td>
<td>[S -> T]</td>
</tr>
<tr class="row-one">
<td class="row-label">$[ f$ EXCEPT $![h] = e]$</td>
<td>[f EXCEPT ![h] = e]</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Records</h4>
<table>
<tr class="row-one">
<td class="row-label">$r.id$</td>
<td>r.id</td>
</tr>
<tr>
<td class="row-label">$[h_1 \mapsto e_1, \ldots, h_n \mapsto e_n]$</td>
<td>[h_1|-> e_1, ..., h_n|-> e_n]</td>
</tr>
<tr class="row-one">
<td class="row-label">$[h_1 : S_1, \ldots, h_n : S_n] $</td>
<td>[h_1:S_1,...,h_n:S_n]</td>
</tr>
<tr>
<td class="row-label">$[r$ EXCEPT $!.h = e]$</td>
<td> [r EXCEPT !.h = e] </td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Strings and Numbers</h4>
<table>
<tr class="row-one">
<td class="row-label">String value</td>
<td>"..."</td>
</tr>
<tr>
<td class="row-label">Set of all strings</td>
<td>STRING</td>
</tr>
<tr class="row-one">
<td class="row-label">Integer value</td>
<td>1, 2, ...</td>
</tr>
</table>
</div>

<div class="cheat-box">
<h4>Miscellaneous constructs</h4>
<table>
<tr class="row-one">
<td class="row-label">if-then-else</td>
<td>IF p THEN e_1 ELSE e_2</td>
</tr>
<tr>
<td class="row-label">Case</td>
<td>CASE P_1 -> e_1 [] ... [] P_n ->e_n</td>
</tr>
<tr class="row-one">
<td class="row-label">let-in</td>
<td>LET d == e_1 IN e</td>
</tr>
</table>
</div>


</div>

<!-- /cheat-box-container -->




<div class="sixteen columns space">
<p>
some more stuff
Expand Down

0 comments on commit 4537913

Please sign in to comment.