” 辅导6CCS3VER程序、 写作Python，C++编程6CCS3VER 2020-21Project 30% of your markDeadline 18/12/2020 Please make sure you read the instructions fully before you start implementing theproject. The project is done on the Xchek tool, available as a part of the KCL VM installationor as a standalone software https://www.cs.toronto.edu/~arie/xchek/ , and it works onLinux and Mac machines. The final product of the project is the report accompanied by appropriate source codefiles for the models and the sets of properties. The source code files should be writtenin GCLang and compile in Xchek. Executing the properties should have the resultdescribed in your report. In the project, you will implement a system that simulates a counter (modulo 8 andthen modulo 16) interacting with the environment as a binary model for Xchek and aset of properties. The stages of the project are as follows:1. Build a model for the counter that counts the number of times a variablehas the value 1 modulo 8 with binary variables in GCLang. In other words,one of your variables should be a free variable, and the transitions of thecounter should depend on the value of this free variable. Keep in mind thatyou will have to extend your model to a counter modulo 16 with minimumchanges to the code.2. Write an initial set of CTL Properties to check correctness of your model.Argue that the set represents the intuitive specification of what we canexpect from the counter. For each property, indicate whether it is a safetyproperty or a liveness property and explain why.3. Show that one of your properties passes vacuously in the system; explainthe reason for the vacuous pass and fix the model or the property.Clarification: answer none of My properties pass vacuously will not beaccepted please have one of the properties passing vacuously.4. Introduce a bug in your model that is not caught by any of the properties.5. Explain why this happened and write an additional property that exposesthis bug. Demonstrate a counterexample.6. Does your initial model satisfy this additional property? If no, explain whynot and fix the model.7. Extend your model to a Counter modulo 16 (that counts the number oftimes the free variable has the value 1). Your initial design should havebeen general enough to allow this with a small number of changes. Explainthe changes.8. Out of the list of the properties you wrote, indicate which ones pass incounter modulo 16 and which fail. If none fail, introduce a new propertythat distinguishes between the counter modulo 8 and counter modulo 16(that is, passes in one of them and fails in the other). In your report, include figures of your models as Kripke structures. If the model istoo large, include a part of the figure and explain how the rest of the model lookslike. Models that do not Compile or do not run on Xchek will receive 0 for the relevantsubquestions (subquestions 1,3,4,5,6 for the model of counter modulo 8,subquestion 7 for the model of Counter modulo 16; for subquestion 8 both modelsshould compile and run). Properties that are grammatically incorrect and hencecannot be understood by Xchek will lead to reduction in the mark (depending onthe number of Grammatically incorrect properties). Reports without Kripkestructures will receive reduced marks for the matching subquestions 1. Marking scheme: 30% for the model (question 1), 10% for each of the questions如有需要，请加QQ：99515681 或邮箱：99515681@qq.com
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
