You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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. byLTLSPEC 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.The text was updated successfully, but these errors were encountered: