Bug #10104
open
Wiki documentation errata
Added by Nikita Chertok almost 5 years ago.
Updated over 4 years ago.
Description
Typos:
- Wiki/Command Line Options, Targets:
- "Every entity which representation is included into Retrascope is stronlge connected with the tool component called "engine"."
- Wiki/Command Line Options, SMT solver debug mode:
- Broken link to the Fortress
- Wiki/Overview:
- Fix line breaks for
"Models are based on the HDL code and can either be extracted ..."
"Engines are shown as black round nodes, models are shown as rectangles and artifacts are shown as elliptic nodes."
"Two components can be combined if one of them returns an entity of some type and the other takes this entity as input."
Suggestions:
- Wiki/Getting Started, Command Line Interface:
- Add a graphic legend to the dependency graph (as a complement to text)
Files
- Status changed from New to Open
- Status changed from Open to Resolved
- % Done changed from 0 to 100
- Subject changed from Documentation errata to Wiki documentation errata
- Status changed from Resolved to Open
Typos:
- Wiki/Installation Guide:
- Broken link to Python Interpreter
- Broken link to Command line options
Suggestions:
- Wiki/Installation Guide:
- If it is possible to use Retrascope with newer version of Z3 (newer than 4.3, current is 4.8.7), specify it.
- Add link to forge build page for downloading Retrascope.
- Add a one-line Command Line example, running which the user will make sure the installation is successful.
- Add "whats next" section with links like:
- "For quick overview of common use cases see Getting Started"
- "For detailed description of Retrascope see Command Line Options"
- Other useful links to documentation
Fixed. Thanks for the contribution!
Suggestions:
- Wiki/Getting started
- Reworked dependency graph image to make it more readable (files in attachment in png and xml for Draw.io)
- Assignee changed from Sergey Smolov to Mikhail Lebedev
- Detected in build changed from svn to master
Wiki/Command Line Options/Engine-specific options
- check-method option allows not only "bmc" and "bdd", but "psl-bmc" also. Please provide the full list of acceptable values for this option.
- formula-based option is not documented.
- spec-file option is not documented.
- smv-file option is not documented.
- collect-usedef option is not documented.
Model checking-based options fixed.
- Assignee changed from Mikhail Lebedev to Sergey Smolov
Wiki/Command Line Options
There are no "cgaa" and "clocked guarded atomic actions" in the project anymore. Engine names and descriptions need to be fixed.
Command Line Options
Mark obligatory options.
Also available in: Atom
PDF
