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