Added ch. 8 bubblesort exercise & ch. 9 exercises.

[dpdani]

No description provided.

[dpdani]

I've also added the exercises from chapter 9.

About these, I have some questions/notes:

• ferryman4.smv defeats the negation axiom. What went wrong? I have no clue.
• sudoku.smv is still running check_ltlspec after 30min, healp 🙏

[dpdani]

[dpdani]

24h in, nuXmv is still playing sudoku

[giuspek]

I finally found time to check them. Sorry for the delayed answer!

I'll split my answer into several comments, one for exercise. The bubblesort is perfect: I love the encoding, in particular how you decided to manage the array assignment after each update. For the sake of practice, you can also try to do that in constraint style, since the array assignments are usually easier to encode using TRANS conditions. This was a pleasant exception, and I prefer your option :)

[giuspek]

Nothing to add about hanoi5, it also work fine

[giuspek]

Regarding the ferryman exercise:

The ferryman can bring TWO passengers into the boat, meaning him + two of the creatures (it could be a bit misleading). If you only could take one single creature, then independently from the first move you would not be able to move correctly, since there would be at least one creature eating another one (e.g. if I move the caterpillar, then the fox can eat the chicken; the same if I move the cabbage). Using INVAR to encode them you create a system that can generate an initial state, but with no transitions. When this happens, verification of LTL properties could be messy: remember, the trace for LTLSPEC (and the same for CTLSPEC) is infinite, but if I have no transition, how can I generate it? Consequently, it returns TRUE since it cannot generate that infinite tracking contradicting it.

[giuspek]

Lastly, regarding sudoku, the encoding is a bit confusing. If you see it is running for long time, you can try to simulate it using bounded model checking and see how it behaves. In particular, I noticed that it stops at step 1 setting every variable to 1, definitely not the behavior we are expecting!
A clear mistake is in the definition of the constant variables: you initialize them to a value, but you should force them to assume the same value for every other iteration, which is missing. Moreover, the LTLSPEC should also include the condition to verify if all constraints are satisfied otherwise setting everything to random values works). For some reason, the modularity you encoded seemed nice theoretically, but the verifications do not hold, maybe you could try to encode it as a state variable so that you can use for sure the next values to create the verification variable.
Try to re-incode it, in particular solving the first issues I mentioned, then we will overcome somehow the last problem, I have to think a bit about it.