First draft of the spec

[Kukovec]

closes #8

Introduces a basic specification, with the following components:

• the state, as the view of a single node
• the method get_slashabe_nodes, and all necessary sub-methods in its call tree
• an alternate implementation of the above, which directly follows translation rules without human judgement, to use as a case study
• rudimentary Init and Next

[Kukovec]

@thpani

[Kukovec]

I was just about to write: we have to roll-back the lambdas. While apalache does support lambdas in place of operators (e.g. for HL operator args, or in fold), you can't use them in a filter expression, since you don't pass a raw operator there. The reason I pulled out the operators with LET-IN was for readability, since you can separate the definition from where it is used inside the set.