Refactors introductionary material, adds exercises page

src/SUMMARY.md

@@ -4,6 +4,7 @@
     - [Contributing](./contributing.md)
 ----
 - [Learning TLA+](./learning/intro.md)
+    - [Exercises](./learning/exercises.md)
     - [Lamport's video tutorial]()
     - [Hyperbook]()
     - [Example repo]()

src/learning/exercises.md

@@ -0,0 +1,11 @@
+# Exercises
+This page provides some execises you can use when learning tla+ or to brush your memory on the language.
+
+
+### Table Of Contents:
+<!-- toc -->
+
+## Missionaries And Cannibals
+* Difficulty: Easy
+* Example solution: https://github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals
+In the missionaries and cannibals problem, three missionaries and three cannibals must cross a river using a boat which can carry at most two people, under the constraint that, for both banks, if there are missionaries present on the bank, they cannot be outnumbered by cannibals (if they were, the cannibals would eat the missionaries). The boat cannot cross the river by itself with no people on board. And, in some variations, one of the cannibals has only one arm and cannot row. From [Wikipedia](https://en.wikipedia.org/wiki/Missionaries_and_cannibals_problem).

src/learning/intro.md

@@ -5,11 +5,15 @@ First things first:
 1. Setup your IDE. Visual Studio code with [tlaplus plugin](../using/vscode.md) is recommended.
 2. If you have questions or if you feel stuck at any point, reach out to the [community](../community.md).
 
-If you want a good kickstart to TLA+, start with [Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1](https://www.youtube.com/watch?app=desktop&v=tw3gsBms-f8) and [Part 2](https://www.youtube.com/watch?v=8-Bc5Lqgx_c). It is a good introduction on TLA+ and uses Paxos and Consensus as an example. 
+Then as good kickstart to TLA+, start with [Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1](https://www.youtube.com/watch?app=desktop&v=tw3gsBms-f8) and [Part 2](https://www.youtube.com/watch?v=8-Bc5Lqgx_c). It is a good introduction on TLA+ and uses Paxos and Consensus as an example. 
 
-Another longer, popular and more complete option is Lamport's video course available on the [website](https://lamport.azurewebsites.net/video/videos.html).
+After that, you can start digging into Lamport's video course available on the [website](https://lamport.azurewebsites.net/video/videos.html). If you prefer a written medium, [Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools. It's well written and easy to follow.
 
-[Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools. It's well written and easy to follow.
+After learning some TLA+, it might be helpful to start learning some Pluscal. Checkout the [pluscal](./pluscal.md) page for more info and some resources. 
+
+Don't just learn the theory, start by solving some small exercises.
+
+----
 
 * [The Specification Language TLA+](https://members.loria.fr/SMerz/papers/tla+logic2008.pdf): Another good manuscript by Stephan Merz explaining TLA+ specification language:  Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. The fnal Sect. 7 contains some concluding remarks.