Feature #24

Optimize result verification

Added by Grégoire Sutre over 6 years ago. Updated over 4 years ago.

Status:Closed Start date:
Priority:Low Due date:
Assignee:Grégoire Sutre % Done:

0%

Category:-
Target version:1.3 Estimated time:2.00 hours

Description

The verification performed by the Verifier module takes a long time in some cases:

./bin/mcscm.native -statistics examples/scm/sliding.scm
CEGAR: 1577 loops, 1801 nodes, 15544 edges
Execution times:      28.69 s   (total)
                      19.31 s   (model-checking)
                       9.34 s   (verification)
./bin/mcscm.native -statistics examples/scm/ring.scm
CEGAR: 1728 loops, 2352 nodes, 19661 edges
Execution times:      95.15 s   (total)
                      32.74 s   (model-checking)
                      62.27 s   (verification)

In the above ring.scm example, the verification of the forward invariant is immediate, the problem comes from the verification of the backward invariant.

Even though this verification is only useful for development (and may be disabled by default in the future), some optimization would help.

Suggestions:
  • apply minimization before checking the invariant.

History

Updated by Grégoire Sutre almost 6 years ago

  • Start date deleted (07/22/2010)

Updated by Grégoire Sutre over 4 years ago

  • Status changed from New to Resolved
  • Assignee set to Grégoire Sutre
  • Target version set to 1.3
  • Estimated time set to 2.00

Fixed in trunk (revision 1552).

Updated by Grégoire Sutre over 4 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF