The LABAS Justifier takes an extended logic program as input, either through uploading a .lp file
containing the logic program, or via the textbox.
Every clause in the logic program has to be of one of the two forms:
Note that, currently, the LABAS Justifier cannot handle variables, so all body literals have to be atoms (start with lower case letters). It also does not support integritiy constraints, aggregates, and other advanced constructs.
Inputting a logic program and uploading it, will take you to the main interface of the LABAS Justifier.
On the right, the logic program and its answer sets are displayed. On the left, you can choose which literal you want to justify and which type of justification should be computed.
By default, the LABAS Justifier will compute LABAS Justifications. If you want to compute Attack Trees instead, click the Attack Trees button on the left.
Choose with respect to which Answer Set you want to justify a literal, using the Select Answer Set dropdown menu (numbers are as shown in the "Answer Sets" box on the right). By default, the first Answer Set is selected.
By default, all justifications (LABAS or Attack Tree) are computed. You can choose a maximum number of justifications to be computed by selecting a different value (1, 5, 10, or 20) from the Generate all dropdown menu.
Consecutively computed justifications can be very similar. You can thus choose to only compute every second justification (with either even or odd index) using the Generate odd and even dropdown menu.
Choose which literal you want to justify using the CHOOSE LITERAL input box on the bottom left.
Finally, hit the Build button to compute the justifications with the chosen parameters.
After hitting the "Build" button, the first computed justification (either LABAS or Attack Tree) is displayed below the main interface.
The top part of the justification provides some basic information about the displayed LABAS Justification, in particular,
which literal is being justified with respect to which Answer Set, how many LABAS Justifications were computed, and
which LABAS Justicication is currently displayed (by default, the first justification is displayed).
The Select LABAS Justification to display dropdown menu is used to select which of the computed justifications should be displayed.
The nodes in a LABAS Justification can be dragged horizontally (except for the top node). In order to return to the initial layout of the justification, press the Reset Tree button.
As for LABAS Justifications, the top part of the Attack Tree view provides the respective basic information, and the Select Attack Tree to display dropdown menu is used to select which of the computed Attack Trees should be displayed.
In contrast to LABAS Justifications, the nodes in Attack Trees cannot be dragged. However, when clicking on a node in the Attack Tree, it collapses. A collapsed node can be expanded by clicking on it again. In order to return to the initial layout of the Attack Tree, press the Reset Tree button.