Project

General

Profile

Bug #3631

FV not working properly in case of nested structures

Added by Anonymous over 1 year ago. Updated over 1 year ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
02/05/2019
Due date:
% Done:

0%

Estimated time:

Description

Tranformation to nusmv model is not working properly if we have actions in a state automaton using a port with nested structure.

Steps:
1) Open the attached model
2) Enable OCRA constraint

Expected - contract should be successfully verified
Actual - It shows "ERROR" status
AF3-Project_test1.af3_23 (57.6 KB) AF3-Project_test1.af3_23 Anonymous, 02/05/2019 05:50 PM

History

#1 Updated by Anonymous over 1 year ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous

#2 Updated by Anonymous over 1 year ago

Tested

#3 Updated by Anonymous over 1 year ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF