COMPX554 Coursework Two
Investigating Models
NOTE: your answers to this coursework are due in to the 554 Moodle site by 1000 on Monday 7th September 2020. The file you submit MUST be a PDF file produced using LATEX.
1. Get a copy of the Z birthday book model from the Moodle site for the course. Make sure that you can compile it (using LATEX) without any errors. The PDF of how it should look is also on the Moodle site, so you can check you are getting the right result.
2. Load your birthday book file into ProB. You will need to make sure that you select the “Other Formalisms” item in the “Open” menu in order to see the file.
Make sure you get no syntax or type errors (the file I’ve given doesn’t contain any!).
Gotothe“Preferences”menuinProBandmakesurethatthe“DEFAULT SETSIZE: Size of unspecified deferred sets in SETS section” preference has value 2, the “Max- Int, used for expressions such as xx::NAT (2147483647 for 4 byte ints)” has value 3 and the “MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte ints)” has value -1. (If you use larger numbers in these places then the models that are possible get so huge that checking takes a very long time.)
3. Play with the model, i.e. add both the possible names with some choice of the possible dates, reset, add names with different dates, keep playing until you are happy you understand what is happening. Make sure you understand what each operation you choose does, and why.
Note the information that ProB displays in the three panes at the bottom of its window. See how the current state information is shown in “State Properties”, how the operations that it is possible to perform (because their pre-conditions hold in the current state) show up in “Enabled operations“ and how “History” shows you what you have been doing. Also, use the arrows to go backwards and forwards through the evolution of the model.
Finally, explore the “Help” menu, particularly the parts which tell you about Z.
4. Change AddBirthday by commenting out (which you do by starting the line with %) the pre-condition (i.e. name? ∈/ known). Now see how the behaviour changes. What happens that’s different if you add NAME1 at DATE1? Why is this?
5. Now change the type of birthday to a relation rather than (as it is now) a partial function. See how the behaviour changes again. What happens now if you add NAME1 at DATE1? Why is this? Why is the type of birthday as a partial function so important?
1
6. Try uncommenting the pre-condition of AddBirthday. Run the experiments above again. What does this tell you about the relation between partial functions and relations and the pre-condition of AddBirthday?
7. Put back everything to how it was originally. Now add an operation RemoveBirthday which, given a name, removes it from the book. Do you need a pre-condition for this operation? If so, what is it, and why do you need it?
8. To see how model-checking works, add an invariant schema which checks that in every state the birthday book relates at most one date to any name. That is
∀b0,b1 : birthday • first b0 = first b1 ⇒ second b0 = second b1 What is the invariant schema?
9. Keeping the invariant schema, change the type of birthday to be a relation again, and comment-out the pre-condition of AddBirthday. Now, run the model checker again. You will get an error. Explain what the model-checker has found—use the History to guide your explanation.
10. Keeping the type of birthday as a relation (but making sure that AddBirthday has its pre-condition), add an operation UpdateName which allows the user to change the name of someone already in the book Model check to see if there are any problems. If there are, perhaps you need to add another pre-condition to UpdateName. Say what it is, and why it works.
11. Add to the state schema so that the book can now also record addresses from the set [ADDRESS]. Update the operations you have so far so that an address is also added when an entry for someone’s birthday is made and deleted, and when a name is updated too. Check the new system to see that no errors have been introduced. What are your new schemas for the state and the updated operations?
12. Add error reporting in order to define total operations that correspond the (in general) partial operations given so far.
Do this by adding a new type
Report ::= Ok | Error
and new schemas OK (which simply provides for an output of the value Ok from
the type Report) and schemas like
ErrorAdd name? : NAME ΞBirthdayBook report! : Report
name? ∈ known report! = Error
2
and
TotalAddBirthday = (AddBirthday ∧ OK ) ∨ ErrorAdd for each of the operations in questions 7 and 10.
13. Run all your checks to make sure that the total operations work as required.
14. Explain clearly how you can use ProB to explore, by animation, and see which operations might be total, and which non-total ones are not.
3