Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo

Close

#646 Inconsistent generation of SIM POs

3.0
open
None
5
2013-01-23
2013-01-23
Laurent Voisin
No

As pointed out by Zheng Cheng on the User mailing list, the generation of SIM proof obligations is sometimes a bit erratic: some seemingly trivial proof obligations of the form "a = a" are generated, but not in a regular manner.

The example from Zheng is machine "mode_m4" from [http://deploy-eprints.ecs.soton.ac.uk/316/] where some SIM proof obligations are generated (e.g., INITIALISATION/act5/SIM).

Discussion

  • Laurent Voisin
    Laurent Voisin
    2013-01-23

    I have successfully reproduced this strange behavior on a smaller example (see attached archive): There is an abstract machine that initialises three boolean variables. I have then added three refinements, each one removing one variable.

    When the first or second variable is removed, a SIM proof obligation is generated for the initialisation of the variable following it. But there is never any SIM proof obligations for variables that have been retained in the same place.

    I think that the proof obligation generator only tests equality of actions that are at the exact same position in the event. Any shift in action positions produces a SIM proof obligation. The POG seems nevertheless to recover afterwards. In the case where the first variable is removed, we have a SIM proof obligation for the second variable, but not for the last one.

    If it is not too complicated, the POG should check for equality of actions whatever their respective positions in the event. Also, verify that the label of the action is ignored during this comparison, as it is not relevant.

     
    Attachments
  • Laurent Voisin
    Laurent Voisin
    2013-01-23

    Continuing on the same example, I have created other refinements of the original machine with the same variables and INITIALISATION, but with a different order of declaration. In all cases, no proof obligation is generated. So, the issue seems to be related to the fact that a variable has disappeared which triggers the strange behavior.