Second Project
Deadline
The Alloy Model to the second project is due on the 7th of December, 2017, 21:59:59. The final report, is due on the 8th of December, 2017, 21:59:59. The delivery protocol, as well as the documentation to be delivered,FAQ
[ALLOY] I was checking an assertion that was showing a counterexample. I fixed it by adding a fact that forbids this counterexample. Did I do it right?
NO. This is not the way one should fix the counterexamples.
Whenever one writes an assertion, we want the stated property to be
true. However, it should be true because our system is well-developed
and not because it is imposed by royal decree. For instance, in Theatre we want that registered and banned clients do not intersect. We
should thus make sure that whenever we add a client,
that he is not banned, and that whenever a client is banned, that he is also unregistered.
Solving it by adding a fact would be equivalent to solving the problem by royal decree. It means that the validity of the property would not be a consequence of our model, but rather would be true because we do not even allow any model that falsifies it.
Now, obviously sometimes we might need to
add facts otherwise the properties would not follow. This should
however be done very conservatively, and to the least extent necessary.
[GENERAL] What is the difference between facts and assertions?
Facts are those conditions that we are sure to be true by hypothesis. Assertions, are those properties that we wish to be true in our model. Two examples:
- The API of Theatre only has the operations defined in Section 2.6. So, we know as a fact that state transitions can only be done using those operations and no other. FACT! Similarly, we know for sure that the initial state has some properties. FACT!
- In Theatre, for each performance, the total number of seat reservations must not exceed the capacity of the theatre. Do we know this for sure? Or do we want to have a model that enforces this? This is true only if we do the things in the right way. Thus, this is clearly something that we want to verify that is true in our model. ASSERTION!
[ALLOY] When a registered performances is cancelled, should the reservations to the performance be be removed?
Yes.
First Project
Deadline
The first project is due on the 10th of November, 2015, 21:59:59. The delivery protocol, can be found in the document below.Information
If event banClient is correctly specified, the invariant preservation PO corresponding the restriction 26 (banClient/inv26/INV) might be hard to prove. There is no need to prove this PO.
FAQ
[RODIN] I have an Invariant that cannot be proved for a given action in Rodin. Is this action incorrect and should I change it?
It might be correct or not. Just because Rodin cannot prove it, it does not mean that it is incorrect. It can be the case that it is indeed wrong, but it can also be the case that Rodin's proof tactics are not "smart-enough" to complete this proof. The solution is to either use the Interactive Prover to try to prove the action, or take the "simpler approach" of looking at the Invariant/action and try to do the proof by hand.
[RODIN] I have an Invariant that cannot be proved for a given action in Rodin. But I am sure that the action is correct and that I have added all the necessary guards for the proof to be completed. What should I do?
Same as above. Rodin is not able to do all the proofs automatically even if the actions are correct. You need to use the Interactive Prover to help Rodin doing the proof.
[RODIN-PLUGINS] It may be of help to install the Atelier-B Provers and the ProB plugins. You cannot prove much without the former, while the later performs some animation that allows one to detect simple bugs.You may also want to install Event B to LaTeX in order to generate "good-looking" tex files of your machines.
Instructions can be found at http://handbook.event-b.org/current/html/tut_install_plugins.html
[REFINEMENTS] Do all the new events introduced by Refinements need to be convergent and provide a variant for them?
Not all new events need to be convergent. Convergent events are those that we want to be sure that will not "take-over" the system and interact forever (see the traffic-light example). For those yes, we need to provide a variant and guarantee that they do not run forever (although I suspect that this is not the case in the project....).
[REFINEMENTS] In a refinement, do we have to implement the events that did not change from the abstract model?
No. If the events do not change just say that they refine and extend the old event.
[REFINEMENTS] When I refine a model, do I have to write all the events all over again even those that are not changed?
No. If you right-click over a machine, there is an option Refine that generates a new machine with all the existing events extended.
[GENERAL] Many of the requisites of the project can be
ensured by guards of the events. Do I also need to state the requisites as invariants?
Desired properties that should always hold, should be stated as invariants.
GENERAL] How can we use relational over-riding to update a function when there are many changes?
You can use a lambda abstraction. See slides T8-ES-Event-B-loose-ends-EN.pdf.
GENERAL] How can we extract an element from a singleton set of natural numbers?
You can use the axiomatization of SUM in the slides T8-ES-Event-B-loose-ends-EN.pdf.