1 % (c) 2016-2025 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(msg_interop, [write_chunklist_to_lts_min/3, write_matrix_to_lts_min/3,
6 put_may_write_matrix/2, put_successors/3]).
7
8 :- use_module(library(fastrw),[ fast_buf_write/3 ]).
9 :- use_module(extension('ltsmin/ltsmin_c_interface')).
10 :- use_module(probsrc(debug),[debug_mode/1]).
11 :- use_module(probsrc(specfile),[csp_with_bz_mode/0]).
12 :- use_module(probsrc(error_manager),[add_internal_error/2]).
13 :- use_module(library(lists)).
14
15 write_and_put_chunk(Msg, C) :-
16 fast_buf_write(C,L,A),
17 put_chunk(Msg, A, L).
18
19 write_and_put_chunk_written(Msg, C) :-
20 fast_buf_write(C,L,A),
21 put_chunk_written(Msg, A, L).
22
23 put_termlist_elements([], _Msg).
24 put_termlist_elements([H|T], Msg) :-
25 write_and_put_chunk(Msg, H),
26 put_termlist_elements(T, Msg).
27
28 put_termlist(Msg, TermList) :-
29 length(TermList,ListSize),
30 put_number(Msg, ListSize),
31 put_termlist_elements(TermList, Msg).
32
33 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
34 get_state_chunks(csp_and_b(CSP,BState),[CSP|Vals]) :- !,
35 % TO DO: partition CSP into chunks
36 get_bind_value(BState, Vals).
37 :- if(environ(prob_safe_mode,true)).
38 get_state_chunks(BState,Vals) :-
39 check_bstate_order(BState),
40 get_bind_value(BState, Vals).
41 :- else.
42 get_state_chunks(BState,Vals) :- % extract values from environment of the form [bind(x,Vx),...]
43 get_bind_value(BState, Vals).
44 :- endif.
45
46 % this is more efficient than: maplist(arg(2),,)
47 get_bind_value([],[]).
48 get_bind_value([bind(_,Val)|T],[Val|VT]) :- get_bind_value(T,VT).
49
50 :- if(environ(prob_safe_mode,true)).
51 % check whether a state (list of bind/2 terms) is in the expected order
52 % TO DO: varname_list is no longer defined !!!
53 check_bstate_order(BindList) :- ltsmin:varname_list(VL), check_bstate_order(BindList,VL).
54 check_bstate_order(BindList,VL) :-
55 (maplist(check_varname,BindList,VL) -> true
56 ; add_internal_error('Unexpected variable order:',check_bstate_order(BindList,VL)),
57 format('Expected order: ~w~n',[VL]),
58 format('Provided order: ~w~n',[BindList])
59 ).
60 check_varname(bind(Name,_),Name).
61 :- endif.
62
63
64 put_long_successors([], _Msg).
65 put_long_successors([H|T], Msg) :-
66 get_state_chunks(H, Vals),
67 put_termlist(Msg, Vals),
68 put_long_successors(T, Msg).
69
70 put_successors(long, States, Msg) :-
71 (debug:debug_mode(on) -> print(put_long_successors(Msg)),nl, flush_output ; true),
72 put_long_successors(States, Msg).
73 put_successors(Pattern-ShortState-Defaults, States, Msg) :-
74 (debug:debug_mode(on) -> print(put_short_successors(Msg)),nl, flush_output ; true),
75 put_short_successors(States, Pattern, Defaults, ShortState, Msg).
76
77 % we need to pass info which maywrite variables were actually written to to LTSmin
78 %get_state_chunks_with_written_info([], [], []).
79 %get_state_chunks_with_written_info([bind(_, Val, WrittenOrDefault)|T], [Val|VT], [WrittenOrDefault|WODTail]) :-
80 % get_state_chunks_with_written_info(T, VT, WODTail).
81
82 put_termlist_elements_short([], [], _).
83 % TODO: CSP, CSP||B, ...
84 put_termlist_elements_short([bind(Varname, Val)|T], [bind(Varname, Default)|DefaultT], Msg) :-
85 (Val == term(undefined)
86 -> write_and_put_chunk(Msg, Default)
87 ; write_and_put_chunk_written(Msg, Val)),
88 put_termlist_elements_short(T, DefaultT, Msg).
89
90 put_termlist_short(TermList, Defaults, Msg) :-
91 length(TermList,ListSize),
92 put_number(Msg, ListSize),
93 put_termlist_elements_short(TermList, Defaults, Msg).
94
95 % this is gonna be a fail-loop
96 % side effect is putting the state into the C Msg
97 % this way, we do not have to copy the pattern
98 put_short_successors([], _Pattern, _Defaults, _ShortState, _Msg).
99 put_short_successors([LongState|_], LongState, Defaults, ShortState, Msg) :-
100 put_termlist_short(ShortState, Defaults, Msg), fail.
101 put_short_successors([_|MoreStates], Pattern, Defaults, ShortState, Msg) :-
102 put_short_successors(MoreStates, Pattern, Defaults, ShortState, Msg).
103
104
105
106
107 put_rows([], _Msg).
108 put_rows([[TransitionGroup, VarList]|R], Msg) :-
109 write_and_put_chunk(Msg, TransitionGroup),
110 put_termlist(Msg, VarList),
111 put_rows(R, Msg).
112
113
114 put_may_write_matrix(Msg, M) :- csp_with_bz_mode,!,
115 write_matrix_to_lts_min(Msg, [ ['$CSP',[]] | M], may_write_matrix).
116 put_may_write_matrix(Msg, M) :- write_matrix_to_lts_min(Msg, M, may_write_matrix).
117
118 put_matrix(Msg, M) :-
119 length(M, MLength),
120 put_number(Msg, MLength),
121 put_rows(M, Msg).
122
123
124
125
126
127 submsg_type_to_int(initial_state, 1).
128 submsg_type_to_int(transition_group_list, 2).
129 submsg_type_to_int(variables_name_list, 3).
130 submsg_type_to_int(variables_type_list, 4).
131 submsg_type_to_int(state_label_matrix, 5).
132 submsg_type_to_int(may_write_matrix, 6).
133 submsg_type_to_int(must_write_matrix, 7).
134 submsg_type_to_int(reads_action_matrix, 8).
135 submsg_type_to_int(reads_guard_matrix, 9).
136 submsg_type_to_int(guard_info_matrix, 10).
137 submsg_type_to_int(guard_label_matrix, 11). % split invariant and guard matrices
138 submsg_type_to_int(necessary_enabling_set, 12).
139 submsg_type_to_int(necessary_disabling_set, 13).
140 submsg_type_to_int(do_not_accord_matrix, 14).
141 submsg_type_to_int(may_be_coenabled_matrix, 15).
142 submsg_type_to_int(ltl_label_matrix, 16).
143
144
145 write_chunklist_to_lts_min(Msg, List, Type) :-
146 (debug:debug_mode(on) -> print(write_chunklist(Type,List)),nl, flush_output ; true),
147 create_message(FreshMsg),
148 submsg_type_to_int(Type, HeaderNum),
149 put_number(FreshMsg, HeaderNum),
150 put_termlist(FreshMsg, List),
151 append_message(Msg, FreshMsg).
152
153 write_matrix_to_lts_min(Msg, PM, Type) :-
154 (debug:debug_mode(on) -> print(write_matrix_to_lts_min(Type,PM)),nl, flush_output ; true),
155 write_matrix(Msg, PM, Type).
156
157 write_matrix(Msg, Matrix, Type) :-
158 create_message(FreshMsg),
159 submsg_type_to_int(Type, HeaderNum),
160 put_number(FreshMsg, HeaderNum),
161 put_matrix(FreshMsg, Matrix),
162 append_message(Msg, FreshMsg).