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