1		% (c) 2014-2022 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(dotsrc(dot_graph_generator), [gen_dot_graph/3]).
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(cbcsrc(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,eop_node_predicate,cbc_enable_trans_predicate).
30
31		tcltk_create_enable_graph_por(File,Inv,UseEnableGraph) :-
32		gen_dot_graph(File,enable_op_node_predicate,cbc_enable_trans_predicate_por(Inv,UseEnableGraph)).
33
34		tcltk_create_disable_graph_por(File,Inv) :-
35		gen_dot_graph(File,enable_op_node_predicate,cbc_disable_trans_por(Inv)).
36
37		enable_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :-
38		eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color),
39		NodeID \='INITIALISATION'.
40
41		cbc_disable_trans_por(Inv,NodeID,Label,SuccID,Color,Style) :-
42		get_preference(timeout_cbc_analysis,Timeout),
43		disable_analysis(NodeID,SuccID,Inv,Timeout,Res),
44		(Res=possible_disable; Res=timeout),
45		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
46
47		cbc_enable_trans_predicate_por(Inv,UseEnableGraph,NodeID,Label,SuccID,Color,Style) :-
48		get_preference(timeout_cbc_analysis,Timeout),
49		enable_analysis(NodeID,SuccID,Inv,UseEnableGraph,Timeout,Res),
50		(Res=possible_enable; Res=possible; Res=guaranteed; Res=timeout; Res=predicate(_Expr)),
51		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
52
53		cbc_enable_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
54		get_preference(timeout_cbc_analysis,Timeout),
55		cbc_enable_analysis(NodeID,SuccID,Res,Timeout), % was 500
56		translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).
57
58		% Predicates for creating a dependency graph
59		tcltk_create_dependence_graph(File) :-
60		gen_dot_graph(File,enable_op_node_predicate,cbc_dependence_trans_predicate).
61
62		cbc_dependence_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
63		Inv=0, % TODO: remove this later
64		get_preference(timeout_cbc_analysis,Timeout),
65		dependent_actions(NodeID,SuccID,Inv,Timeout,Res),
66		% Res can be action, general, race
67		translate_por_res(Res,EnableRes),
68		translate_enable_res(EnableRes,NodeID,SuccID,Label,Color,Style).
69
70		translate_por_res(action,action_dependent).
71		translate_por_res(guard,guard_dependent).
72		translate_por_res(predicate(_),guard_dependent).
73		translate_por_res(race,race_dependent).
74		% general: self_dependent, =