Bug #10104
Wiki documentation errata
Start date:
02/07/2020
Due date:
% Done:
100%
Estimated time:
Detected in build:
master
Platform:
Published in build:
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."
- Fix line breaks for
- Wiki/Getting Started, Command Line Interface:
- Add a graphic legend to the dependency graph (as a complement to text)
Files
History
Updated by Sergey Smolov 12 months ago
- % Done changed from 0 to 100
- Status changed from Open to Resolved
Updated by Sergey Smolov 12 months ago
- Subject changed from Documentation errata to Wiki documentation errata
Updated by Nikita Chertok 12 months ago
Typos:
- Wiki/Installation Guide:
- Broken link to Python Interpreter
- Broken link to Command line options
- 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
Updated by Nikita Chertok 12 months ago
- File Retrascope_graph.xml Retrascope_graph.xml added
- File Retrascope.png Retrascope.png added
Suggestions:
- Wiki/Getting started
- Reworked dependency graph image to make it more readable (files in attachment in png and xml for Draw.io)
Updated by Sergey Smolov 11 months ago
- Detected in build changed from svn to master
- Assignee changed from Sergey Smolov to Mikhail Lebedev
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.
Updated by Mikhail Lebedev 11 months ago
- 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.