1		% (c) 2014-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(dot_graphs_static_analysis, [tcltk_create_dependence_graph/1, tcltk_create_enable_graph/1,tcltk_create_enable_graph_por/3,tcltk_create_disable_graph_por/2]).
6
7		/* Modules and Infos for the code coverage analysis */
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,model_checker).
10		:- module_info(description,'This module provides predicates for printing out graphs in dot-format calculated by computing some of the static analyses used for partial order reduction').
11
12		% Standard SICSTUS prolog libraries
13		:- use_module(library(lists)).
14
15		% Imports from the POR modules
16		:- use_module(probporsrc(static_analysis),[dependent_actions/5,enable_analysis/6,disable_analysis/5]).
17
18		% The dot-graph generator
19		:- use_module(probsrc(dot_graph_generator),[gen_dot_graph/6]).
20
21		% Preferences
22		:- use_module(probsrc(preferences), [get_preference/2]).
23
24		% TODO: move all enabling graph predicates in enabling_analysis.pl used for generating dot-graphs to a new module
25		:- use_module(probsrc(enabling_analysis), [translate_enable_res/6, eop_node_predicate/6, cbc_enable_analysis/4]).
26
27		% Predicates for creating an enable graphs
28		tcltk_create_enable_graph(File) :-
29		gen_dot_graph(File,dot_graphs_static_analysis,eop_node_predicate,cbc_enable_trans_predicate,none,none).
30
31		tcltk_create_enable_graph_por(File,Inv,UseEnableGraph) :-
32		EnablePred = cbc_enable_trans_predicate_por(Inv,UseEnableGraph),
33		gen_dot_graph(File,dot_graphs_static_analysis,enable_op_node_predicate,EnablePred,none,none).
34
35		tcltk_create_disable_graph_por(File,Inv) :-
36		DisablePred = cbc_disable_trans_por(Inv),
37		gen_dot_graph(File,dot_graphs_static_analysis,enable_op_node_predicate,DisablePred,none,none).
38
39		:- public enable_op_node_predicate/6.
40		enable_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :-
41		eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color),
42		NodeID \='INITIALISATION'.
43
44		:- public cbc_disable_trans_por/6.
45		cbc_disable_trans_por(Inv,NodeID,Label,SuccID,Color,Style) :-
46		get_preference(timeout_cbc_analysis,Timeout),
47		disable_analysis(NodeID,SuccID,Inv,Timeout,Res),
48		(Res=possible_disable; Res=timeout),
49		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
50
51		:- public cbc_enable_trans_predicate_por/7.
52		cbc_enable_trans_predicate_por(Inv,UseEnableGraph,NodeID,Label,SuccID,Color,Style) :-
53		get_preference(timeout_cbc_analysis,Timeout),
54		enable_analysis(NodeID,SuccID,Inv,UseEnableGraph,Timeout,Res),
55		(Res=possible_enable; Res=possible; Res=guaranteed; Res=timeout; Res=predicate(_Expr)),
56		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
57
58		:- public cbc_enable_trans_predicate/5.
59		cbc_enable_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
60		cbc_enable_analysis(NodeID,SuccID,Res,500),
61		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
62
63		% Predicates for creating a dependency graph
64		tcltk_create_dependence_graph(File) :-
65		gen_dot_graph(File,dot_graphs_static_analysis,enable_op_node_predicate,cbc_dependence_trans_predicate,none,none).
66
67		:- public cbc_dependence_trans_predicate/5.
68		cbc_dependence_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
69		Inv=0, % TODO: remove this later
70		get_preference(timeout_cbc_analysis,Timeout),
71		dependent_actions(NodeID,SuccID,Inv,Timeout,Res),
72		(Res=dependent; Res=race_dependent),
73		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).