Feature #9503
closed
when debug option is enabled, pass it to the model checker as well
Added by Sergey Smolov over 5 years ago.
Updated over 5 years ago.
Category:
Engine (Launcher)
Published in build:
1.1.1-beta-190722
Description
When the Retrascope is running at the debug mode ("--loglevel debug", AFAIR), the model checking tool (NuSMV) should also be launched with debug output enabled.
- Status changed from New to Resolved
- % Done changed from 0 to 100
Added the LOG_LEVEL parameter to the SmvModelCheckerLauncher class. Usage:
--smv-verbosity num
where
num is the desired level of the model checker's output verbosity (usually from 0 to 4).
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build set to 1.1.1-beta-190722
Also available in: Atom
PDF