Project

General

Profile

Bug #2143

[Analyses] If a saved verification pattern is badly typed, NuSMV throws an error

Added by Anonymous about 6 years ago. Updated almost 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
10/24/2014
Due date:
% Done:

0%

Estimated time:

Description

To reproduce:
  1. open the attached model
  2. change the type of the port to int
  3. change the automaton accordingly: send an integer (any, does not matter) on the output instead of true
  4. open the "A/G, Contracts, Patterns"
  5. check the atom

Obtained behaviour: error "NuSMV terminated with ..."

Expected behaviour: AF3 error "this pattern is badly typed"

AF3-Project.af3_23 (8.16 KB) AF3-Project.af3_23 Anonymous, 10/24/2014 10:58 AM

History

#1 Updated by Anonymous almost 6 years ago

  • Assignee changed from Anonymous to Anonymous

#2 Updated by Anonymous almost 6 years ago

  • Status changed from New to In Progress

#3 Updated by Anonymous almost 6 years ago

  • Status changed from In Progress to Resolved
  • Assignee changed from Anonymous to Anonymous

#4 Updated by Anonymous almost 6 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF