Needing for more information about counter examples in approximate model checking

From: Jean-Luc Mercadier (jean-luc.mercadier@tni-valiosys.com)
Date: Tue May 28 2002 - 06:26:22 MDT

  • Next message: Hartmut Wittke: "[Fwd: "VIS Optimization Question"]"

    Hello,

    I would like to better understand why some of my CTL formulas fails on the design I'm checking.
    I 've got enough information when I use "- d 2" option with model-check command, but elapsed time for the verification is sometime too long.
    (I've got responses like "fails myVariable=1")

    It seems impossible to obtain such information with the command approximate_model_check. (I only got responses like "fails")

    Is it possible to obtain as information as mc -d2 does when using approximate_model_check ?
    If so, please, give me a tip.

    Thanks for your response

    Jean-Luc

    This archive was generated by hypermail 2b30 : Tue May 28 2002 - 05:46:56 MDT