mbeddr/mbeddr.formal

Use NuSMV show_property and LTLSPEC names for unique mapping

mfgpcm opened this issue · 2 comments

mfgpcm commented

Currently, the .source file for nusmv is generated but not used. By adding show_property to the .source file, nusmv outputs a list of the LTLSPEC given in the .smv file including the name (if given, e.g. by LTLSPEC NAME x := true).
By adding unique names to LTLSPECs, running nusmv on the .source file and updating the class AGResultsLifter to support the additional output, the lifting of nusmv results could be improved. This is especially beneficial for vacuity checks of contracts that belong to the same component.

danielratiu commented

I have just added show_property. Will look into lifting the following days.

  • 👍1
danielratiu commented

I have fixed this - the results lifter now takes into consideration the info displayed by the show_properties (if available)