blob: 05bf4167b541d0cd94cacd553525c467d6a70344 [file] [log] [blame]
<html>
<body>
<h1>Debug Tab : Part 1</h1>
<p>The first part of the tab is shown below :</p>
<img src="images/tab_debug_001.png" width=800, border="3">
<h2>Graph Files</h2>
<p>The Graph Files check boxes allows the production of diverse graphs (in .gv format (GraphViz)). Those graphs may describe the studied system and the symbolic execution that triggered their creation.</p>
<p>Three types of graph can be generated (we'll see details later). The files will be generated as follows :</p>
<img src="images/graph_files001.png" width=400, border="3">
<h3>Statemachine Graph</h3>
<p>This graph gives an overview of the system's components and of the possible state changes that can happen. However, it does not show communications between the components.</p>
<p>Example :</p>
<img src="images/systemgraph001.png" width=1100, border="3">
<h3>Execution Graph Phase 1</h3>
<p>This graph shows the succession of the evaluation contexts that were explored during the symbolic execution. It is displayed under the form of an oriented graph that can be interpreted as a tree. The graph normally covers all contexts reached therefore there may be several branches that stem from a single node (see <a href="../../5_symbexec/1_exploration.html">symbolic exploration</a>). This graph also displays additional data, among other things :</p>
<ul>
<li>the list of variable's new values when there are value changes when reaching a new state (displayed attached to a node)</li>
<li>the list of transitions that took place in an edge between two nodes</li>
<li>the list of input and output signals that were transmitted in an edge between two nodes</li>
<li>information about the nature of states (i.e. nodes of the graph) that may depend on the type of symbolic execution</li>
<li>...</li>
</ul>
<p>Here is a simple example :</p>
<img src="images/ex_graph_phase1_001.png" width=1100, border="3">
<h3>Execution Graph Phase 2</h3>
<p>This graph is a lightened version of the Execution Graph Phase 1. Some of the information is not displayed for better readability.</p>
<p>Here is a simple example (same system as previous) :</p>
<img src="images/ex_graph_phase2_001.png" width=500, border="3">
<h2>Console Trace</h2>
<p>The user can set the console trace level in order to filter the information that is displayed on the standard output of Eclipse's console during a symbolic execution.</p>
<p>The several levels are :</p>
<ul>
<li>SILENT</li>
<li>MINIMUM</li>
<li>MEDIUM</li>
<li>MAXIMUM</li>
</ul>
<p>For instance, a "SILENT" output on a simple model would be :</p>
<img src="images/console_trace_level_silent.png" width=500, border="3">
<p>Whereas a "MINIMUM" output on the same model would be :</p>
<img src="images/console_trace_level_mini.png" width=500, border="3">
<h2>Trace Files</h2>
<p>The user can optionally have the engine generate all sorts of trace files. This can be done by checking the "File Generation" check-box. When doing so the tab is extended as follows :</p>
<img src="images/tab_debug_trace_files.png" width=800, border="3">
<p>Two files will be generated as follows :</p>
<img src="images/trace_files001.png" width=400, border="3">
<p>For a simple system, the vanilla version (ZERO trace level and no trace options checked) of the "avm.trace" file would be :</p>
<img src="images/avm_trace_vanilla.png" width=800, border="3">
<p>And an excerpt of the "avm.log" file would be :</p>
<img src="images/avm_log_vanilla.png" width=800, border="3">
<h1>Debug Tab : Part 2</h1>
<p>The second part of the tab is shown below :</p>
<img src="images/tab_debug_002.png" width=800, border="3">
<h2>First Execution Page</h2>
<p>When checking "File Generation", after a symbolic execution, the following files appear :</p>
<img src="images/first_execution001.png" width=400, border="3">
<h3>The "phase1.fscn" file</h3>
<p>For the same simple system, the content of this file is the following :</p>
<img src="images/phase1_fscn001.png" width=800, border="3">
<p>Much like the "phase1_execution_graph.gv" graph, it describes the different evaluation contexts that have been reached. But id does so in text form and with additional displayed data.</p>
<h3>The ".fexe" files</h3>
<p>Those files contain the code describing the system and interpreted by the engine at different states of the compiling process. It is notably useful to debug issues concerning the "<a href="../../../3_xliaref/actprimdico/actprim_run/actprim_run0.html">@run{...}</a>", "<a href="../../../3_xliaref/actprimdico/actprim_schedule.html">@schedule{...}</a>" and/or "<a href="../../../3_xliaref/actprimdico/actprim_concurrency.html">@concurrency{...}</a>" primitives.</p>
<h2>Second Execution Page</h2>
<p>When checking "File Generation", after a symbolic execution, the following file appear :</p>
<img src="images/second_execution001.png" width=400, border="3">
<h3>The "phase2.fscn" file</h3>
<p>For the same simple system, the content of this file is the following :</p>
<img src="images/phase2_fscn001.png" width=800, border="3">
<p>For simple systems, it's content is exactly the same as the "phase1.fscn" file.</p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
<p></p>
</body>
</html>