Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
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!).
Go to the “Preferences” menu in ProB and make sure that the “DEFAULT SETSIZE:
Size of unspecified deferred sets in SETS section” preference has value 2, the “MaxInt,
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?