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). |