” COMPX554编程 辅导、 写作Python编程设计编程Coursework TwoInvestigating ModelsNOTE: your answers to this coursework are due in to the 554 Moodle site by 1000 onMonday 7th September 2020. The file you submit MUST be a PDF file produced usingLATEX.1. Get a copy of the Z birthday book model from the Moodle site for the course. Makesure that you can compile it (using LATEX) without any errors. The PDF of how itshould look is also on the Moodle site, so you can check you are getting the rightresult.2. Load your birthday book file into ProB. You will need to make sure that you selectthe Other Formalisms item in the Open Menu in order to see the file.Make sure you get no syntax or type errors (the file Ive given doesnt 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 value3 and the MinInt, used for expressions such as xx::INT (-2147483648 for 4 byteints) has value -1. (If you use larger numbers in these places then the models thatare 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 thepossible dates, reset, add names with different dates, keep playing until you arehappy you understand what is happening. Make sure you understand what eachoperation you choose does, and why.Note the information that ProB displays in the three panes at the bottom of itswindow. See how the current state information is shown in State Properties, howthe operations that it is possible to perform (because their pre-conditions hold inthe current state) show up in Enabled operations and how History shows youwhat you have been doing. Also, use the arrows to go backwards and forwardsthrough 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 thats 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 partialfunction. See how the behaviour changes again. What happens now if you addNAME1 at DATE1? Why is this? Why is the type of birthday as a partial functionso important?COMPX554作业 辅导、 写作Python编程设6. Try uncommenting the pre-condition of AddBirthday. Run the experiments aboveagain. What does this tell you about the relation between partial functions andrelations and the Pre-condition of AddBirthday?7. Put back everything to how it was originally. Now add an operation RemoveBirthdaywhich, given a name, removes it from the book. Do you need a pre-condition forthis 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 inevery state the birthday book relates at most one date to any name. That is b0, b1 : birthday first b0 = first b1 second b0 = second b1What 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 checkeragain. You will get an error. Explain what the model-checker has founduse theHistory to guide your explanation.10. Keeping the type of birthday as a relation (but making sure that AddBirthday has itspre-condition), add an operation UpdateName which allows the user to change thename 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. Saywhat it is, and why it works.11. Add to the state schema so that the book can now also record addresses from theset [ADDRESS]. Update the operations you Have so far so that an address is alsoadded when an entry for someones birthday is made and deleted, and when a nameis 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 (ingeneral) partial operations given so far.Do this by adding a new typeReport ::= Ok | Errorand new schemas OK (which simply provides for an output of the value Ok fromthe type Report) and schemas likeErrorAddname? : NAMEBirthdayBookreport! : Reportname? knownreport! = Error2andTotalAddBirthday = ( b AddBirthday OK) ErrorAddfor 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 whichoperations might be total, and which non-total ones are not.3如有需要，请加QQ：99515681 或邮箱：99515681@qq.com
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
