FV not working properly in case of nested structures
Tranformation to nusmv model is not working properly if we have actions in a state automaton using a port with nested structure.
Steps:
- Open the attached model
- Enable OCRA constraint
Expected - contract should be successfully verified
Actual - It shows “ERROR” status
(from redmine: issue id 3631, created on 2019-02-05, closed on 2019-03-01)
- Uploads: