Test scenarios

[ivan-gavran]

Adding the list here in the form of PR.
The goal is that one the list is finalized, agreed upon, and implemented, we remove the .md document.
I chose the PR form because of its good infrastructure for discussing individual lines.

[hvanz]

Great list though I have the feeling that it describes many of all the possible scenarios in the model, and thus the model itself, which makes it a bit pointless as we want to let the model-checker explore all possible behaviours. If we write a TLA+ predicate for each test scenario in the list, there's not too much difference with writing them manually in Go.

Apart from that, I think we can try to cover different sets of behaviours by restricting the model. For example, we can cover all items in the Granting section by just disabling the Exec action, and explore the model until, let's say, depth 5. And for scenarios that are independent of the authorization logic, we can restrict the model to one authorization per time, and generate all the traces for each three kinds of authorizations.

[hvanz]

We have also to take into account the fact that executing a single trace takes time (at least ~10 seconds?) which is quite a lot if we want to cover hundreds of scenarios, including trivial ones.

[ivan-gavran]

As we agreed synchronously, I am merging this list into the repo.
The remarks on implementing it still hold:

• there are probably more elegant ways of implementing those checks, without enumerating them one by one. E.g., by manipulating the View predicate.
• when generating all possible cases for a particular invariant, we have to be careful because tests take time so there is no much space for having trivial tests