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.
1) Open the attached model
2) Enable OCRA constraint
Expected - contract should be successfully verified
Actual - It shows "ERROR" status