1/* File: scasp_just_dot.pl 2 Author: Roy Ratcliffe 3 Created: Jun 8 2025 4 Purpose: Generate a DOT graph from a JSON source produced by s(CASP) 5 License: MIT License 6 Version: 1.0.0 7 Status: Stable 8 Updated: 2025-06-08 9 10Copyright (c) 2025, Roy Ratcliffe, Northumberland, United Kingdom 11 12Permission is hereby granted, free of charge, to any person obtaining a 13copy of this software and associated documentation files (the 14"Software"), to deal in the Software without restriction, including 15without limitation the rights to use, copy, modify, merge, publish, 16distribute, sub-license, and/or sell copies of the Software, and to 17permit persons to whom the Software is furnished to do so, subject to 18the following conditions: 19 20 The above copyright notice and this permission notice shall be 21 included in all copies or substantial portions of the Software. 22 23THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS 24OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 25MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. 26IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY 27CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, 28TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE 29SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 30 31*/ 32 33:- module(scasp_just_dot, 34 [ scasp_just_dot_print/3 % Stream, Src, Options 35 ]). 36:- autoload(library(http/json), [json_read_dict/2]). 37:- autoload(library(apply), [maplist/3]). 38:- autoload(library(option), [select_option/4, option/3]). 39:- autoload(library(dcg/high_order), [sequence//2]). 40:- use_module(library(settings), [setting/4, setting/2]). 41 42:- setting(tab, nonneg, 2, 'Tab size for indentation'). 43:- setting(rankdir, atom, 'LR', 'Direction of the graph layout'). 44:- setting(bgcolor, atom, transparent, 'Background colour of the graph'). 45:- setting(node, list(compound), [ style=filled, 46 fillcolor=lightyellow, 47 color=darkred, 48 fontname="Arial", 49 fontsize=10 50 ], 'Node attributes'). 51:- setting(edge, list(compound), [color=darkred], 'Edge default attributes'). 52:- setting(edge_true, list(compound), [color=darkgreen], 'Edge attributes for true'). 53:- setting(edge_false, list(compound), [color=darkred], 'Edge attributes for false'). 54:- setting(edge_likely, list(compound), [ color=darkgreen, 55 style=dashed 56 ], 'Edge attributes for likely'). 57:- setting(edge_unlikely, list(compound), [ color=darkred, 58 style=dashed 59 ], 'Edge attributes for unlikely').
s(CASP)
solver, and prints a DOT representation of the
justification graph to the specified Stream. The Options parameter
allows customisation of the output, such as indentation size, graph
direction, background colour, node attributes, edge attributes, and
nodes to elide.
The JSON source should contain a dictionary with the following structure, simplified for clarity:
{ "solver": {...}, "query": {...}, "answers": [ { "bindings": {...}, "model": [{"truth": ..., "value": {...}}], "tree": { "node": {"value": {...}}, "children": [ { "node": {"value": {...}}, "children": [...] }, ... ] } }, ... ] }
The answers
field is a list of answers, each containing bindings, a
model, and a tree structure. The tree
field represents the
justification tree, where each node has a value and may have children,
forming a hierarchical structure of implications.
The output is a DOT graph representation of the justification tree, where each node corresponds to a term in the justification, and edges represent implications between nodes. The graph is directed, with arrows indicating the direction of implications from one node to another.
The output is formatted as a DOT graph, which can be visualised using graph visualisation tools like Graphviz. The output can be customised using the Options parameter, which allows for setting various attributes of the graph, such as:
tab(Width)
: Specifies the indentation width for the output.rankdir(Direction)
: Sets the direction of the graph layout, e.g.
'LR' for left-to-right.bgcolor(Color)
: Sets the background colour of the graph.node(Attributes)
: Specifies attributes for the nodes in the graph.edge(Attributes)
: Specifies attributes for the edges in the graph.elides(Nodes)
: A list of nodes to elide in the graph, meaning they
will not be displayed.
This predicate is useful for visualising the justification structure of
s(CASP)
queries, making it easier to understand the relationships
between different terms and their implications in the context of logic
programming and answer set programming.
126scasp_just_dot_print(Stream, Src, Options) :- 127 read_json_dict(Src, Dict), 128 phrase(json_dot(Dict, Options), Lines), 129 print_message_lines(Stream, '', Lines). 130 131read_json_dict(Src, Dict) :- 132 setup_call_cleanup(open(Src, read, Stream), 133 json_read_dict(Stream, Dict), 134 close(Stream)). 135 136json_dot(Dict, Options) --> 137 tab_dot(Options), ['// solver ~s'-[Dict.solver], nl], 138 tab_dot(Options), ['// query '], value_w(Dict.query), [nl], 139 line_dot('digraph {', Options, Options_), 140 answers_dot(Dict.answers, Options_), 141 line_dot('}', Options). 142 143answers_dot(Answers, Options) --> 144 setting_dot(rankdir, Options), 145 setting_dot(bgcolor, Options), 146 setting_dot(node, Options), 147 setting_dot(edge, Options), 148 sequence(answer_dot(Options), Answers). 149 150answer_dot(Options, Answer) --> 151 dict_comment_dot(Answer, [excludes([ bindings, 152 model, 153 constraints, 154 tree, 155 time 156 ])|Options]), 157 { dict_pairs(Answer.bindings, _, Bindings) 158 }, 159 sequence(binding_comment_dot(Options), Bindings), 160 sequence(truth_comment_dot(Options), Answer.model), 161 answer_tree_dot(Answer.tree, Options). 162 163answer_tree_dot(_{node:Node, children:Children}, Options) --> 164 { value_term(Node.value, query) 165 }, 166 line_dot('subgraph {', Options, Options_), 167 sequence(answer_tree_query_dot([], Options_), Children), 168 line_dot('}', Options). 169 170answer_tree_query_dot(Implies, Options, Answer) --> 171 { Node = Answer.node, 172 value_term(Node.value, Value) 173 }, 174 line_dot('// ~w'-[Value], Options), 175 line_dot('subgraph {', Options, Options_), 176 sequence(implies_dot(Node, Options_), Implies), 177 sequence(answer_tree_query_dot([Node|Implies], Options_), Answer.children), 178 line_dot('}', Options).
If Node0 is not in the list of elided nodes, it generates a line indicating the implication from Node0 to Node. If Node0 is in the list of elided nodes, it generates a comment line indicating that the implication is elided.
The elision is controlled by the elides/1
option in Options,
which is a list of nodes that should not be displayed in the
graph.
The predicate constructs a DOT line in the format:
~s"~w" -> "~w";
where ~s
is replaced by the elided comment "// elided "
if
Node0 or Node is in the elides list, else ""
if neither Node0
nor Node is elided, and the ~w
format strings are replaced by
the string representations of Node0 and Node.
The predicate uses the line_dot//2 DCG rule to format the output line according to the DOT syntax, including the optional comment if the node is elided. The Elides variable is used to check if either Node0 or Node is in the list of elided nodes. If neither is elided, it generates a standard DOT line containing the implication. If either is elided, it generates a comment line indicating that the implication is elided.
208implies_dot(Node0, Options, Node) --> 209 { value_term(Node0.value, Value0), 210 value_term(Node.value, Value), 211 option(elides(Elides), Options, []), 212 ( \+ memberchk(Value0, Elides), 213 \+ memberchk(Value, Elides) 214 -> Elided = "" 215 ; Elided = "// elided " 216 ), 217 edge_attributes(Node0.truth, Attributes, Options) 218 }, 219 line_dot('~s"~w" -> "~w" ~w;'-[Elided, Value0, Value, Attributes], Options). 220 221edge_attributes(Truth, Attributes, Options) :- 222 atom_string(Truth_, Truth), 223 edge_attributes_(Truth_, Attributes, Options). 224 225edge_attributes_(Truth, Attributes, Options) :- 226 option(edge(Truth, Attributes), Options), 227 !. 228edge_attributes_(Truth, Attributes, _) :- 229 atomic_list_concat([edge, Truth], '_', Name), 230 setting(Name, Attributes), 231 !. 232edge_attributes_(_, [], _). 233 234binding_comment_dot(Options, Binding-Truth) --> 235 tab_dot(Options), ['// ~w: '-[Binding]], truth_w(Truth), [nl]. 236 237truth_comment_dot(Options, Truth) --> 238 tab_dot(Options), ['// '], truth_w(Truth), [nl]. 239 240dict_comment_dot(Dict, Options) --> 241 { dict_pairs(Dict, _, Pairs) 242 }, 243 sequence(pair_comment_dot(Options), Pairs). 244 245pair_comment_dot(Options, Key-Value) --> 246 { includes_or_not_excludes(Key, Options) 247 }, 248 !, 249 line_dot('// ~k ~k'-[Key, Value], Options). 250pair_comment_dot(_, _) --> [].
includes/1
is
present), not excluded (if excludes/1
is present), or always
succeeds if neither option is present.
If the includes/1
option is present, it checks if Key is a
member of the Includes list. If the excludes/1
option is
present, it checks that Key is not a member of the Excludes list.
263includes_or_not_excludes(Key, Options) :- 264 ( option(includes(Includes), Options) 265 -> memberchk(Key, Includes) 266 ; option(excludes(Excludes), Options) 267 -> \+ memberchk(Key, Excludes) 268 ; true % succeed if neither includes nor excludes (default behaviour) 269 ). 270 271setting_dot(Name, Options) --> 272 { setting(Name, Value) 273 }, 274 setting_dot(Name, Value, Options). 275 276setting_dot(Name, Value, Options) --> 277 { is_list(Value) 278 }, 279 !, 280 line_dot('~p ~p;'-[Name, Value], Options). 281setting_dot(Name, Value, Options) --> 282 line_dot('~w;'-[Name=Value], Options). 283 284tab_dot(Options0, Options) --> 285 { indent(Options0, Tab, Options) 286 }, 287 [Tab]. 288 289tab_dot(Options) --> tab_dot(Options, _). 290 291line_dot(Line, Options0, Options) --> tab_dot(Options0, Options), [Line, nl]. 292 293line_dot(Line, Options) --> line_dot(Line, Options, _). 294 295truth_w(_{truth:Truth, value:Value}) --> 296 { value_term(Value, Term) 297 }, 298 ['~w ~w'-[Truth, Term]]. 299 300value_w(Value) --> 301 { value_term(Value, Term) 302 }, 303 ['~w'-[Term]].
The predicate employs dictionary pattern matching (:<
) to safely extract
the relevant fields from the dictionary, and for clarity. It handles nested
compounds by recursively mapping the arguments to value terms. The predicate
is semi-deterministic, meaning it succeeds at most once; if the input
dictionary does not match any of the expected patterns, it fails silently.
This allows for safe handling of the JSON structure without raising
exceptions for unexpected formats.
The implementation assumes that the JSON structure follows a specific
format, where each term is represented as a dictionary with a type
field indicating whether it is a variable, atom, number, rational, or
compound. If the JSON structure changes or new term types are added,
the predicate will require updating.
The value_term/2 predicate is used to convert the JSON representation
of terms into Prolog terms, which can then be used in further processing
or output---particularly useful in the context of generating a DOT
graph from a JSON source produced by s(CASP)
, where terms represent nodes
in the justification tree. It is a crucial part of justification tree
processing, allowing the conversion of JSON representations of terms into
Prolog terms that can be used to construct the graph structure, and designed
to be used in conjunction with the dict_term/2 helper predicate, which
handles the conversion of a Prolog dictionary (parsed from JSON) into a
Prolog term. The dict_term/2 predicate is responsible for converting the
dictionary representation of terms into actual Prolog terms.
351value_term(Value, Term), is_dict(Value) => dict_term(Value, Term). 352value_term(Value, List), is_list(Value) => maplist(value_term, Value, List). 353 354dict_term(Value, Var), _{type:"var", 355 name:Var} :< Value => true. 356dict_term(Value, Atom), _{type:"atom", 357 value:String} :< Value => atom_string(Atom, String). 358dict_term(Value, Value), _{type:"number", 359 value:Value} :< Value => true. 360dict_term(Value, Rational), _{type:"rational", 361 numerator:Numerator, 362 denominator:Denominator} :< Value => 363 rational(Rational, Numerator, Denominator). 364dict_term(Value, Term), _{type:"compound", 365 functor:Functor, 366 args:Args} :< Value => 367 atom_string(Functor_, Functor), 368 maplist(value_term, Args, Args_), 369 Term =.. [Functor_|Args_].
indent/1
.'~t~*|'-[Indent0]
).indent/1
option.381indent(Options0, Width, '~t~*|'-[Indent0], [indent(Indent)|Options]) :- 382 select_option(indent(Indent0), Options0, Options, 0), 383 Indent is Indent0 + Width. 384 385indent(Options0, Tab, Options) :- 386 setting(tab, DefaultWidth), 387 option(tab(Width), Options0, DefaultWidth), 388 indent(Options0, Width, Tab, Options)