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 | format('Expected order: ~w~n',[VL]), | |
52 | format('Provided order: ~w~n',[BindList]) | |
53 | ). | |
54 | check_varname(bind(Name,_),Name). | |
55 | :- endif. | |
56 | ||
57 | ||
58 | put_long_successors([], _Msg). | |
59 | put_long_successors([H|T], Msg) :- | |
60 | get_state_chunks(H, Vals), | |
61 | put_termlist(Msg, Vals), | |
62 | put_long_successors(T, Msg). | |
63 | ||
64 | put_successors(long, States, Msg) :- | |
65 | put_long_successors(States, Msg). | |
66 | put_successors(Pattern-ShortState-Defaults, States, Msg) :- | |
67 | put_short_successors(States, Pattern, Defaults, ShortState, Msg). | |
68 | ||
69 | % we need to pass info which maywrite variables were actually written to to LTSmin | |
70 | %get_state_chunks_with_written_info([], [], []). | |
71 | %get_state_chunks_with_written_info([bind(_, Val, WrittenOrDefault)|T], [Val|VT], [WrittenOrDefault|WODTail]) :- | |
72 | % get_state_chunks_with_written_info(T, VT, WODTail). | |
73 | ||
74 | put_termlist_elements_short([], [], _). | |
75 | % TODO: CSP, CSP||B, ... | |
76 | put_termlist_elements_short([bind(Varname, Val)|T], [bind(Varname, Default)|DefaultT], Msg) :- | |
77 | (Val == term(undefined) | |
78 | -> write_and_put_chunk(Msg, Default) | |
79 | ; write_and_put_chunk_written(Msg, Val)), | |
80 | put_termlist_elements_short(T, DefaultT, Msg). | |
81 | ||
82 | put_termlist_short(TermList, Defaults, Msg) :- | |
83 | length(TermList,ListSize), | |
84 | put_number(Msg, ListSize), | |
85 | put_termlist_elements_short(TermList, Defaults, Msg). | |
86 | ||
87 | % this is gonna be a fail-loop | |
88 | % side effect is putting the state into the C Msg | |
89 | % this way, we do not have to copy the pattern | |
90 | put_short_successors([], _Pattern, _Defaults, _ShortState, _Msg). | |
91 | put_short_successors([LongState|_], LongState, Defaults, ShortState, Msg) :- | |
92 | put_termlist_short(ShortState, Defaults, Msg), fail. | |
93 | put_short_successors([_|MoreStates], Pattern, Defaults, ShortState, Msg) :- | |
94 | put_short_successors(MoreStates, Pattern, Defaults, ShortState, Msg). | |
95 | ||
96 | ||
97 | ||
98 | ||
99 | put_rows([], _Msg). | |
100 | put_rows([[TransitionGroup, VarList]|R], Msg) :- | |
101 | write_and_put_chunk(Msg, TransitionGroup), | |
102 | put_termlist(Msg, VarList), | |
103 | put_rows(R, Msg). | |
104 | ||
105 | ||
106 | put_may_write_matrix(Msg, M) :- csp_with_bz_mode,!, | |
107 | write_matrix(Msg, [ ['$CSP',[]] | M], may_write_matrix). | |
108 | put_may_write_matrix(Msg, M) :- write_matrix(Msg, M, may_write_matrix). | |
109 | ||
110 | put_matrix(Msg, M) :- | |
111 | length(M, MLength), | |
112 | put_number(Msg, MLength), | |
113 | put_rows(M, Msg). | |
114 | ||
115 | ||
116 | ||
117 | ||
118 | ||
119 | submsg_type_to_int(initial_state, 1). | |
120 | submsg_type_to_int(transition_group_list, 2). | |
121 | submsg_type_to_int(variables_name_list, 3). | |
122 | submsg_type_to_int(variables_type_list, 4). | |
123 | submsg_type_to_int(state_label_matrix, 5). | |
124 | submsg_type_to_int(may_write_matrix, 6). | |
125 | submsg_type_to_int(must_write_matrix, 7). | |
126 | submsg_type_to_int(reads_action_matrix, 8). | |
127 | submsg_type_to_int(reads_guard_matrix, 9). | |
128 | submsg_type_to_int(guard_info_matrix, 10). | |
129 | submsg_type_to_int(guard_label_matrix, 11). % split invariant and guard matrices | |
130 | submsg_type_to_int(necessary_enabling_set, 12). | |
131 | submsg_type_to_int(necessary_disabling_set, 13). | |
132 | submsg_type_to_int(do_not_accord_matrix, 14). | |
133 | submsg_type_to_int(may_be_coenabled_matrix, 15). | |
134 | submsg_type_to_int(ltl_label_matrix, 16). | |
135 | ||
136 | ||
137 | write_chunklist(Msg, List, Type) :- | |
138 | create_message(FreshMsg), | |
139 | submsg_type_to_int(Type, HeaderNum), | |
140 | put_number(FreshMsg, HeaderNum), | |
141 | put_termlist(FreshMsg, List), | |
142 | append_message(Msg, FreshMsg). | |
143 | ||
144 | write_matrix(Msg, Matrix, Type) :- | |
145 | create_message(FreshMsg), | |
146 | submsg_type_to_int(Type, HeaderNum), | |
147 | put_number(FreshMsg, HeaderNum), | |
148 | put_matrix(FreshMsg, Matrix), | |
149 | append_message(Msg, FreshMsg). |