Project

General

Profile

Bug #1599

CProver analyses permits idle action even if transition(s) could be performed.

Added by Andreas Bayha about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
08/08/2013
Due date:
% Done:

0%

Estimated time:

Description

Due to injecting nodeterministic choice behavior for which traversable transition to perform, CBMC might find traces which perform a states idle action instead of possible outgoing transitions.

History

#1 Updated by Andreas Bayha about 7 years ago

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

#2 Updated by Anonymous about 7 years ago

  • Status changed from Resolved to Closed
  • Assignee deleted (Anonymous)

Also available in: Atom PDF