1 | % (c) 2016-2021 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 | :- module(ltsmin,[ltsmin_init/2,ltsmin_init/3,ltsmin_loop/1, | |
5 | ltsmin_teardown/2, start_ltsmin/4, | |
6 | ltsmin_generate_ltlfile/2, generate_bindings/3]). | |
7 | ||
8 | :- use_module(library(fastrw),[ fast_buf_read/2]). | |
9 | :- use_module(library(codesio), [write_to_codes/2]). | |
10 | :- use_module(library(lists)). | |
11 | ||
12 | :- use_module(extension('ltsmin/ltsmin_c_interface')). | |
13 | :- use_module(extension('ltsmin/msg_interop')). | |
14 | ||
15 | ||
16 | :- use_module('../../src/module_information.pl'). | |
17 | ||
18 | :- use_module(extension('plspec/plspec/plspec_core')). | |
19 | :- enable_spec_check(write_matrix/3). | |
20 | ||
21 | :- use_module(probsrc(specfile)). | |
22 | :- use_module(probsrc(bmachine)). | |
23 | :- use_module(probsrc(b_read_write_info), [tcltk_read_write_matrix/1]). | |
24 | :- use_module(probsrc(debug), [debug_println/2, debug_mode/1]). | |
25 | ||
26 | :- use_module(probsrc(typing_tools)). | |
27 | %:- enable_all_spec_checks. | |
28 | ||
29 | :- module_info(group,experimental). | |
30 | :- module_info(description,'This is the interface to C code for LTSmin integration.'). | |
31 | :- use_module(probsrc(b_state_model_check), [get_guard/2]). | |
32 | :- use_module(probsrc(bsyntaxtree), [conjunction_to_list/2, same_texpr/2, | |
33 | conjunct_predicates/2, is_truth/1, create_negation/2]). | |
34 | %:- use_module(probsrc(system_call), [system_call_keep_open/7]). | |
35 | :- use_module(library(process), [process_wait/2]). | |
36 | ||
37 | :- dynamic label_to_reads/2. | |
38 | ||
39 | :- spec_pre(msg_interop:write_matrix/3, [c_pointer, | |
40 | one_of([ltsmin_matrix(ltsmin_state_label, ltsmin_variable), % state label / guard / LTL matrices | |
41 | ltsmin_matrix(ltsmin_transition_group, ltsmin_variable), % read/write matrices | |
42 | ltsmin_matrix(ltsmin_state_label, ltsmin_transition_group), % NES / NDS | |
43 | ltsmin_matrix(ltsmin_transition_group, ltsmin_state_label), % guard info | |
44 | ltsmin_matrix(ltsmin_state_label, ltsmin_state_label), % may be co-enabled | |
45 | ltsmin_matrix(ltsmin_transition_group, ltsmin_transition_group)]), % DNA | |
46 | any]). | |
47 | ||
48 | :- defspec(ltsmin_flag, one_of([atom(por), | |
49 | atom(g), | |
50 | atom(nocache), | |
51 | compound(ltl_formula(any))])). | |
52 | :- defspec(ltsmin_backend, one_of([atom(sequential), atom(symbolic)])). | |
53 | :- defspec(atom_bool, one_of([atom(true), atom(false)])). | |
54 | :- defspec(c_pointer, int). | |
55 | :- defspec(ltsmin_matrix(X, Y), [tuple([X, list(Y)])]). | |
56 | :- defspec(b_pred_ish, compound(bpred(any))). | |
57 | ||
58 | ltsmin_variable(X) :- | |
59 | varname_list(Variables), member(X, Variables). | |
60 | :- defspec_pred(ltsmin_variable, ltsmin_variable). | |
61 | ||
62 | ltsmin_transition_group(X) :- | |
63 | get_transition_groups(TGs), member(X, TGs). | |
64 | :- defspec_pred(ltsmin_transition_group, ltsmin_transition_group). | |
65 | ||
66 | ltsmin_state_label(X) :- state_label(X, _, _). | |
67 | :- defspec_pred(ltsmin_state_label, ltsmin_state_label). | |
68 | ||
69 | :- spec_pre(ltsmin_loop/1, [c_pointer]). | |
70 | ltsmin_loop(Zocket) :- | |
71 | h_zocket2(Zocket, Ret), % this is a C function in ltsmin_c_interface, which does the call-backs to Prolog | |
72 | Ret == 0, !, | |
73 | ltsmin_loop(Zocket). | |
74 | ltsmin_loop(_). | |
75 | ||
76 | interpose([], _, []). | |
77 | interpose([X], _, [X]) :- !. | |
78 | interpose([H|T], I, [H,I|IT]) :- | |
79 | interpose(T, I, IT). | |
80 | ||
81 | atom_concat([X], X) :- !. | |
82 | atom_concat([H1, H2|T], R) :- | |
83 | atom_concat(H1, H2, H), | |
84 | atom_concat([H|T], R). | |
85 | ||
86 | :- spec_pre(get_ltsmin_invariant/2, [var, atom_bool]). | |
87 | :- spec_invariant(get_ltsmin_invariant/2, ['return value: an atom containing the flags for invariant checking for ltsmin':atom, | |
88 | 'input: true or false describing whether POR is disabled or enabled':atom_bool]). | |
89 | get_ltsmin_invariant(LTSminInv, Por) :- | |
90 | (Por == false -> Type = invariant ; Type = por_invariant), | |
91 | findall(InvLabel, state_label(InvLabel, Type, _AST), InvariantNames), | |
92 | (InvariantNames == [] -> Invariant = ['true']; interpose(InvariantNames, ' && ', Invariant)), | |
93 | atom_concat(Invariant, Invariant2), | |
94 | atom_concat(['--invariant=!is_init || (', Invariant2, ')'], LTSminInv). | |
95 | ||
96 | ||
97 | backend_specific_flags(symbolic, ['--lace-workers=1'], _). | |
98 | backend_specific_flags(sequential, FlagsSeq, MoreFlags) :- | |
99 | (member(nocache, MoreFlags) -> FlagsSeq = [] ; FlagsSeq = ['-c']). | |
100 | ||
101 | :- spec_pre(property_flags/4, [atom_bool, atom_bool, atom_bool, var]). | |
102 | :- spec_invariant(property_flags/4, ['no deadlock checking':atom_bool, | |
103 | 'no invariant checking':atom_bool, | |
104 | 'POR active':atom_bool, | |
105 | 'resulting flags':[atomic]]). | |
106 | property_flags(true, true, _, []). | |
107 | property_flags(false, true, _, ['-d']). | |
108 | property_flags(true, false, POR, [InvariantFlags]) :- | |
109 | get_ltsmin_invariant(InvariantFlags, POR). | |
110 | ||
111 | ||
112 | % TODO: maybe the path should be chosen in another way | |
113 | get_path_to_ltl_file('/tmp/prob-ltsmin-formula.ltl'). | |
114 | :- use_module(probsrc(system_call),[get_temporary_filename/2]). | |
115 | %get_path_to_trace_file('/tmp/prob-ltsmin-trace.gcf'). | |
116 | get_path_to_fresh_trace_file(File) :- get_temporary_filename('prob-ltsmin-trace.gcf',File). | |
117 | %get_path_to_csv_trace('/tmp/prob-ltsmin-trace.csv'). | |
118 | get_path_to_fresh_csv_trace_file(File) :- get_temporary_filename('prob-ltsmin-trace.csv',File). | |
119 | get_path_to_fresh_ltsmin_endpoint(File) :- get_temporary_filename('ltsmin.probz',File). | |
120 | ||
121 | :- spec_pre(ltsmin_flag/2, [ltsmin_flag, var]). | |
122 | :- spec_invariant(ltsmin_flag/2, [ltsmin_flag, atom]). | |
123 | ltsmin_flag(por, '--por'). | |
124 | ltsmin_flag(g, '-g'). | |
125 | ltsmin_flag(ltl_formula(_), Flag) :- | |
126 | get_path_to_ltl_file(Path), | |
127 | atom_concat('--ltl=', Path, Flag). | |
128 | ||
129 | ||
130 | % MoreFlags can contain: por, nocache, g (for guard splitting), ltl_formula(String) | |
131 | :- spec_pre(get_ltsmin_flags/6, [ltsmin_backend, atom_bool, atom_bool, [ltsmin_flag], atom, var]). | |
132 | :- spec_invariant(get_ltsmin_flags/6, ['symbolic_or_sequential':ltsmin_backend, | |
133 | % at least one of the checks has to be false | |
134 | 'no deadlock checking':atom_bool, | |
135 | 'no invariant checking':atom_bool, | |
136 | 'more flags that should be converted to LTSmin flags':[ltsmin_flag], | |
137 | 'trace_file':atom, | |
138 | 'resulting flags for LTSmin':[atom]]). | |
139 | get_ltsmin_flags(Backend, NoDead, NoInv, MoreFlags, TraceFile, ResFlags) :- | |
140 | backend_specific_flags(Backend, BackendFlags, MoreFlags), | |
141 | (member(por, MoreFlags) -> POR = true ; POR = false), | |
142 | property_flags(NoDead, NoInv, POR, PropertyFlags), | |
143 | convlist(ltsmin_flag, MoreFlags, EvenMoreFlags), | |
144 | TraceFlags = ['--trace', TraceFile], | |
145 | append([TraceFlags, BackendFlags, PropertyFlags, EvenMoreFlags], ResFlags). | |
146 | ||
147 | ||
148 | ||
149 | :- use_module(probsrc(tools_printing),[print_error/1]). | |
150 | :- use_module(probsrc(preferences), [get_preference/2]). | |
151 | :- use_module(probsrc(error_manager), [add_warning/3, add_internal_error/2]). | |
152 | :- use_module(probsrc(pathes),[runtime_application_path/1]). | |
153 | :- use_module(probsrc(pathes_lib), [lib_component_full_path/4]). | |
154 | ||
155 | :- use_module(library(file_systems),[file_exists/1,delete_file/1]). | |
156 | del_temp_file(F) :- (file_exists(F) -> delete_file(F) ; true). | |
157 | ||
158 | get_tool_name(symbolic, 'prob2lts-sym'). | |
159 | get_tool_name(sequential, 'prob2lts-seq'). | |
160 | get_tool_name(printtrace, 'ltsmin-printtrace'). | |
161 | ||
162 | :- spec_pre(start_ltsmin/4, [ltsmin_backend, tuple([atom_bool, atom_bool]), [ltsmin_flag],var]). | |
163 | :- spec_invariant(start_ltsmin/4, ['which backend should be used (symbolic or sequential)':ltsmin_backend, | |
164 | 'tuple of length 2: no deadlock checking, no invariant checking':tuple([atom_bool, atom_bool]), | |
165 | 'more ltsmin flags':[ltsmin_flag], | |
166 | 'resulting of LTSmin model-checking':any ]). | |
167 | start_ltsmin(Backend, [NoDead, NoInv], MoreFlags,Result) :- | |
168 | (NoDead = false, NoInv = false -> | |
169 | add_warning(start_ltsmin,'Turning off deadlock checking for LTSmin command: ',Backend), | |
170 | NoDead2 = true | |
171 | ; NoDead2 = NoDead), | |
172 | get_path_to_fresh_ltsmin_endpoint(Endpoint), | |
173 | ltsmin:ltsmin_init(Endpoint, Zocket), | |
174 | get_path_to_fresh_trace_file(TraceFile), | |
175 | get_ltsmin_flags(Backend, NoDead2, NoInv, MoreFlags, TraceFile, Flags), | |
176 | (member(ltl_formula(Formula), MoreFlags) | |
177 | -> get_path_to_ltl_file(LTLFile), | |
178 | ltsmin_generate_ltlfile(Formula, LTLFile) | |
179 | ; true), | |
180 | preferences:get_preference(path_to_ltsmin, Path), | |
181 | runtime_application_path(PROBPATH), | |
182 | get_tool_name(Backend, Tool), | |
183 | lib_component_full_path(executable, Tool, ltsmin_extension, LTSminCmd), | |
184 | catch( | |
185 | process:process_create(LTSminCmd, [Endpoint, '--stats', '--when'|Flags], [process(PID)]), | |
186 | % we could add stdout(pipe(STDOut)) option to process_create and try and parse output | |
187 | error(existence_error(_,_),E), | |
188 | (format(user_error,'process_create exception: ~w~n',[E]), | |
189 | format('LTSMIN preference is set to: "~w"~n',[Path]), | |
190 | format(' relative to ProB path: "~w"~n',[PROBPATH]), | |
191 | format(' using tool: "~w"~n',[Tool]), | |
192 | add_error_fail(ltsmin,'Path to LTSmin incorrect (LTSMIN preference) or LTSmin command not installed (copy prob2lts-sym, prob2lts-seq, ltsmin-printtrace from https://github.com/utwente-fmt/ltsmin/releases to ProB\'s lib folder), cannot execute: ',LTSminCmd))), | |
193 | ltsmin_loop(Zocket), | |
194 | process_wait(PID, ExitStatus), | |
195 | (ExitStatus == exit(0) | |
196 | -> Result = ltsmin_model_checking_ok | |
197 | ; ExitStatus = killed(_) | |
198 | -> Result = ltsmin_model_checking_aborted | |
199 | ; ExitStatus == exit(1) | |
200 | -> get_tool_name(printtrace, PrintTrace), | |
201 | lib_component_full_path(executable, PrintTrace, ltsmin_extension, PrintTraceCmd), | |
202 | get_path_to_fresh_csv_trace_file(CsvFile), | |
203 | format('writing trace to ~w~n', CsvFile), | |
204 | catch( | |
205 | process:process_create(PrintTraceCmd, [TraceFile, CsvFile, '-s,,'], [process(PID2)]), | |
206 | error(existence_error(_,_),E), | |
207 | (format(user_error,'process_create exception: ~w~n',[E]), | |
208 | add_error_fail(ltsmin,'Path to LTSmin incorrect or ltsmin-printtrace command not installed (copy command from https://github.com/utwente-fmt/ltsmin/releases to ProB\'s lib folder), cannot execute: ',PrintTraceCmd))), | |
209 | process_wait(PID2, _ExitStatus2), | |
210 | Result = ltsmin_counter_example_found(CsvFile) | |
211 | ; add_internal_error('Unexpected LTSmin exit status:',ExitStatus), | |
212 | Result = ltsmin_model_checking_aborted | |
213 | ), | |
214 | del_temp_file(TraceFile), | |
215 | del_temp_file(Endpoint), | |
216 | format('~w with ~w exited with status: ~w~n',[Tool, Flags, ExitStatus]), | |
217 | ltsmin:ltsmin_teardown(Zocket, Endpoint). | |
218 | ||
219 | ||
220 | :- use_module(probsrc(state_space),[get_operation_name_coverage_infos/4]). | |
221 | % can be called from ltsmin.c | |
222 | print_ltsmin_stats :- | |
223 | get_operation_name_coverage_infos(PossibleNr,_FeasibleNr,UncovNr,UncoveredList), | |
224 | Cov is PossibleNr - UncovNr, | |
225 | format('~w/~w operations covered, uncovered = ~w~n~n',[Cov,PossibleNr,UncoveredList]). | |
226 | ||
227 | :- dynamic varname_list/1. | |
228 | ||
229 | :- use_module(probltlsrc(ltl_tools), [temporal_parser/3]). | |
230 | ||
231 | :- dynamic(inv_state_label_matrix/1). | |
232 | :- dynamic(inv_state_label_matrix_for_por/1). | |
233 | ||
234 | write_to_ltl_file(Formula, Path) :- | |
235 | open(Path, write, Stream), | |
236 | tell(Stream), | |
237 | print(Formula), | |
238 | told. | |
239 | ||
240 | ltsmin_generate_ltlfile(Formula, OutputFile) :- | |
241 | %% firstly, wrap the Formula into X(Formula) | |
242 | %% this avoids that a property is already considered true | |
243 | %% because it is in the artificial initial state | |
244 | atom_concat('X(', Formula, XFormula), | |
245 | atom_concat(XFormula, ')', FinalFormula), | |
246 | format('parsing LTL formula ~a~N', [FinalFormula]), | |
247 | setup_ltl_formula(FinalFormula, ResAtom), | |
248 | format('done. writing to: ~a~N', [OutputFile]), | |
249 | write_to_ltl_file(ResAtom, OutputFile). | |
250 | ||
251 | ||
252 | setup_ltl_formula(Formula, ResAtom) :- | |
253 | temporal_parser(Formula, ltl, ParsedFormula), | |
254 | ltl_safety:pp_formula_to_ltl2ba_syntax(ParsedFormula, ResAtom). | |
255 | ||
256 | ||
257 | :- spec_pre(ltsmin_init/3, [atom, var, atom]). | |
258 | :- spec_pre(ltsmin_init/3, [atom, var, var]). | |
259 | :- spec_invariant(ltsmin_init/3, ['the path to the ZMQ endpoint':atom, | |
260 | 'return value: a C pointer to a ZMQ zocket':c_pointer, | |
261 | 'an LTL formula':atom]). | |
262 | ltsmin_init(Endpoint,Zocket, LtlFormula) :- | |
263 | (var(LtlFormula) -> true ; setup_ltl_formula(LtlFormula, _)), | |
264 | ltsmin_init(Endpoint, Zocket). | |
265 | ||
266 | :- spec_pre(ltsmin_init/2, [atom, var]). | |
267 | :- spec_pre(ltsmin_init/2, [atom, var]). | |
268 | :- spec_invariant(ltsmin_init/2, ['the path to the ZMQ endpoint':atom, | |
269 | 'return value: a C pointer to a ZMQ zocket':c_pointer]). | |
270 | ltsmin_init(Endpoint,Zocket) :- | |
271 | loadfr, | |
272 | reset_ltsmin_extension, | |
273 | split_invariant(ListOfInvariantConjuncts, InvNames, ListOfInvariantConjunctsForPOR, InvNamesForPOR), | |
274 | get_state_labels(ListOfInvariantConjuncts, InvNames, invariant, InvStateLabelMatrix), | |
275 | get_state_labels(ListOfInvariantConjunctsForPOR, InvNamesForPOR, por_invariant, InvStateLabelMatrixForPOR), | |
276 | assertz(inv_state_label_matrix(InvStateLabelMatrix)), | |
277 | assertz(inv_state_label_matrix_for_por(InvStateLabelMatrixForPOR)), | |
278 | ltsmin_initialize(Endpoint, Zocket). | |
279 | ||
280 | %assert_dir :- (user:library_directory('.') -> true ; | |
281 | %assertz(user:library_directory('.'))). | |
282 | ||
283 | ||
284 | :- use_module(probsrc(runtime_profiler),[profile_single_call/2]). | |
285 | :- use_module(probsrc(state_space),[mark_operation_as_covered/1]). | |
286 | :- public get_next_states/4. % not sure how this is called | |
287 | get_next_states(LongOrPattern, Msg, State,Op) :- % State is a list of bindings | |
288 | % TO DO: set_context_state(SomeID) and look if state_error(SomeID,Id,Error) were added | |
289 | profile_single_call(Op,ltsmin:compute_successors(Op, State, Succs)), | |
290 | length(Succs,NrStates), | |
291 | % format(" ~w successor states for ~w~n ~w~n",[NrStates,Op,Succs]),nl, | |
292 | (NrStates>0 -> mark_operation_as_covered(Op) ; true), % TO DO: we should probably use another Prolog fact for this; to avoid confusion which operations are covered in ProB's internal statespace | |
293 | put_number(Msg, NrStates), | |
294 | put_successors(LongOrPattern, Succs, Msg). | |
295 | ||
296 | ||
297 | read_state([],[]). | |
298 | read_state([Addr|T], [Arg|R]) :- read_state(T,R), fast_buf_read(Arg,Addr). | |
299 | ||
300 | :- meta_predicate mnf1(0). | |
301 | mnf1(Call) :- %format('Calling ~w~n',[Call]), flush_output, | |
302 | if( catch(Call, E, | |
303 | (add_internal_error('LTSMin Extension Exception: ',[E]),flush_output,fail) | |
304 | ), | |
305 | true, | |
306 | (add_internal_error('LTSMin Extension Call Failed: ',[Call]),flush_output,fail) | |
307 | ). | |
308 | ||
309 | :- use_module(probsrc(specfile),[csp_with_bz_mode/0]). | |
310 | % convert a list of values into a ProB environment [bind(x,Vx),...] | |
311 | generate_bound_long_state([CSP|BState],Res) :- csp_with_bz_mode,!, | |
312 | Res=csp_and_b(CSP,BoundState), | |
313 | varname_list(L), | |
314 | %print(gen_bind(BState,L)),nl, | |
315 | generate_bindings(BState, L, BoundState). | |
316 | /* this needs to be fixed for short states ; | |
317 | * it does not get the entire varname list */ | |
318 | generate_bound_long_state(BState,BoundState) :- | |
319 | varname_list(L), | |
320 | generate_bindings(BState, L, BoundState). | |
321 | ||
322 | generate_bound_state_short_label(BState,Label,BoundState) :- | |
323 | label_to_reads(Label, L), | |
324 | generate_bindings(BState, L, BoundState). | |
325 | ||
326 | :- spec_pre(generate_bindings/3, [list(any), list(atom), list(compound(bind(atom, any)))]). | |
327 | :- spec_pre(generate_bindings/3, [list(any), list(atom), var]). | |
328 | :- spec_pre(generate_bindings/3, [var, var, list(compound(bind(atom, any)))]). | |
329 | :- spec_invariant(generate_bindings/3, ['a list of values':list(any), | |
330 | 'a list of identifiers':list(atom), | |
331 | 'list of identifiers and values, wrapped in functor bind/2':list(compound(bind(atom, any)))]). | |
332 | ||
333 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
334 | :- if(environ(prob_safe_mode,true)). | |
335 | :- use_module(probsrc(bmachine),[b_is_variable/2]). | |
336 | :- use_module(probsrc(btypechecker), [unify_types_strict/2]). | |
337 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
338 | :- debug_println(19,'TYPE CHECKING LTSMIN BINDINGS:'). | |
339 | generate_bindings([], [], []) :- !. | |
340 | generate_bindings([H|T], [Name|TN], [bind(Name, H)|R]) :- | |
341 | (get_type(Name,Type) | |
342 | -> kernel_objects:infer_value_type(H,HType), | |
343 | (unify_types_strict(HType,Type) -> true | |
344 | ; add_internal_error('Unexpected type for:',id(Name,HType,Type,H)) | |
345 | ) | |
346 | ; add_internal_error('Unknown identifier:',Name) | |
347 | ), | |
348 | generate_bindings(T, TN, R). | |
349 | ||
350 | get_type(Name,Type) :- b_is_variable(Name,Type). | |
351 | get_type(Name,Type) :- b_get_machine_constants(Csts), | |
352 | member(b(identifier(Name),Type,_),Csts). | |
353 | :- else. | |
354 | generate_bindings([], [], []) :- !. | |
355 | generate_bindings([H|T], [Name|TN], [bind(Name, H)|R]) :- | |
356 | generate_bindings(T, TN, R). | |
357 | :- endif. | |
358 | ||
359 | :- public get_successors_short/3. % called from C code | |
360 | % implements R2W | |
361 | get_successors_short(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output, | |
362 | mnf1(get_successors_aux(short, Msg, OperationA, StateA)). | |
363 | ||
364 | :- public get_successors/3. % called from C code | |
365 | get_successors(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output, | |
366 | mnf1(get_successors_aux(long, Msg, OperationA, StateA)). | |
367 | ||
368 | get_successors_aux(Type, Msg, OperationA, StateA) :- | |
369 | read_state(StateA,State), | |
370 | fast_buf_read(Operation,OperationA), | |
371 | %print(operation(Operation)),nl, | |
372 | % print(successors(Operation, State)),nl, | |
373 | (Type == short -> black_magic_short_transformation(Operation, BoundState, State, LongPattern, ShortSucc, Defaults, _, _, _, _, _), ShortOrLong = LongPattern-ShortSucc-Defaults | |
374 | ; generate_bound_long_state(State, BoundState), ShortOrLong = long), | |
375 | %print(generate(BoundState)),nl, | |
376 | (debug:debug_mode(on) | |
377 | -> format('~n ** get_successors for ~w (~w)~n',[Operation,ShortOrLong]), | |
378 | translate:print_state(BoundState),nl | |
379 | ; true), | |
380 | get_next_states(ShortOrLong, Msg, BoundState,Operation). | |
381 | ||
382 | :- public get_state_label/3. % called by C | |
383 | get_state_label(Msg, LabelA, StateA) :- mnf1(get_state_label_aux(long, Msg, LabelA, StateA)). | |
384 | ||
385 | :- public get_state_label_short/3. % called by C | |
386 | get_state_label_short(Msg, LabelA, StateA) :- mnf1(get_state_label_aux(short, Msg, LabelA, StateA)). | |
387 | ||
388 | get_state_label_aux(Type, Msg, LabelA, StateA) :- | |
389 | read_state(StateA, State), | |
390 | fast_buf_read(Label,LabelA), %print(get_state_label(Label)),nl, | |
391 | (Type == long -> generate_bound_long_state(State,BoundState) | |
392 | ; generate_bound_state_short_label(State, Label, BoundState)), | |
393 | %print(get_state_label_state(Label, BoundState)),nl, | |
394 | eval_label(Msg, BoundState,Label). | |
395 | ||
396 | % NOTE: LTSMin assumes the first transition group is the initialisation action, it is called only once | |
397 | % all other events are not called in the initial state | |
398 | get_transition_groups(['$init_state'|L]) :- | |
399 | (specfile:b_or_z_mode | |
400 | -> findall(OperationName, bmachine:b_top_level_feasible_operation(OperationName), BL), | |
401 | (csp_with_bz_mode -> L = ['$CSP'|BL] ; L=BL) | |
402 | ; L=[]). % FIXME: provide list for CSP-M | |
403 | ||
404 | extract_name_and_type([],[], []). | |
405 | extract_name_and_type([b(identifier(HT),TypeTerm,_)|T], [HT|RT], [TypeTerm|RType]) :- | |
406 | extract_name_and_type(T,RT,RType). | |
407 | ||
408 | /* is that already defined somewhere? */ | |
409 | get_ltsmin_variable_names(Names, Types) :- | |
410 | bmachine:b_get_machine_variables(V), | |
411 | % bmachine:b_get_machine_all_constants(C), % this includes constants which have been moved to deferred sets; causes issue with hanoi model | |
412 | bmachine:b_get_machine_constants(C), % this does not include global set constants | |
413 | append(V,C,CV), % compatible with b_initialise_machine2 and expand_const_and_vars order | |
414 | extract_name_and_type(CV,Names,Types). | |
415 | % b_initialise_machine2 puts constants at end to make sharing of complete tail-list easier for successor states | |
416 | ||
417 | ||
418 | ||
419 | extract_tg_and_nth_entry([], _, R, R). | |
420 | extract_tg_and_nth_entry([list(H)|T], Arg, Acc, R) :- | |
421 | nth1(1, H, TransitionGroup), | |
422 | nth1(Arg, H, X), | |
423 | extract_tg_and_nth_entry(T, Arg, [[TransitionGroup, X]|Acc], R). | |
424 | ||
425 | % patch matrix for CSP||B | |
426 | put_patched_matrix(Msg, Type,M) :- | |
427 | patch_matrix(M,PM), | |
428 | (debug:debug_mode(on) -> print(put_matrix(Type,PM)),nl ; true), | |
429 | write_matrix(Msg, PM, Type). | |
430 | ||
431 | % add $CSP as read/write dependency to matrixes | |
432 | % [ [Odd,[]], [Even,[]], [Inc,[count]], [Reset,[count]]] | |
433 | patch_matrix(M,Res) :- csp_with_bz_mode, !, | |
434 | Res = [ ['$CSP',['$CSP_CHUNK']] | PM], % add virtual CSP transition for CSP only events; TO DO: also allow/treat other pure CSP events; the CSP transition can only modify the $CSP chunk | |
435 | maplist(patch_row,M,PM). | |
436 | patch_matrix(M,M). | |
437 | ||
438 | patch_row([Op,Vars], [Op,['$CSP_CHUNK'|Vars]]). | |
439 | ||
440 | ||
441 | build_initial_state(_, VType, VVal) :- | |
442 | any_value_for_type(VType, VVal). | |
443 | % do not use term undefined in order to avoid guard errors in the initial state | |
444 | %VVal = term(undefined). | |
445 | ||
446 | ||
447 | term_to_atom(T, A) :- | |
448 | write_to_codes(T, Codes), | |
449 | atom_codes(A, Codes). | |
450 | ||
451 | ||
452 | :- use_module(probsrc(b_operation_guards), [get_operation_propositional_guards/3]). | |
453 | ||
454 | ||
455 | guard_seen(G, [H|_]) :- | |
456 | same_texpr(G, H), !. | |
457 | guard_seen(G, [_|LofG]) :- | |
458 | guard_seen(G, LofG). | |
459 | ||
460 | ||
461 | setify_guards(L, R) :- | |
462 | setify_guards(L, [], R). | |
463 | setify_guards([], Seen, Seen). | |
464 | setify_guards([G|RGuards], Seen, Res) :- | |
465 | (guard_seen(G, Seen) | |
466 | -> setify_guards(RGuards, Seen, Res) | |
467 | ; setify_guards(RGuards, [G|Seen], Res)). | |
468 | ||
469 | ||
470 | guard_vector(ListOfListOfGuards, Res) :- | |
471 | append(ListOfListOfGuards, ListOfGuards), | |
472 | setify_guards(ListOfGuards, Res). | |
473 | ||
474 | ||
475 | get_name([H|_], [Name|_], G, Name) :- | |
476 | same_texpr(G, H), !. | |
477 | get_name([_|GV], [_|Names], G, R) :- | |
478 | get_name(GV, Names, G, R). | |
479 | ||
480 | ||
481 | guards_to_indices(GuardVector, Names, ListOfGuards, ListOfIndices) :- | |
482 | maplist(get_name(GuardVector, Names), ListOfGuards, ListOfIndices). | |
483 | ||
484 | split_guards(Por, ['$init_state'|TransitionGroups], GuardVector, Names, [[]|IndexVectors]) :- | |
485 | % if we use POR, the transition group has to be enabled iff all its guards are true; | |
486 | % thus, for POR we need to use get_guard that also provides | |
487 | % existential quantifications for parameters as additional guards | |
488 | (Por == false | |
489 | -> maplist(get_ltsmin_guards, TransitionGroups, RGuards, _Bodies) | |
490 | ; maplist(get_guard, TransitionGroups, Guards), | |
491 | maplist(conjunction_to_list, Guards, RGuards)), | |
492 | %% TODO: normalise guards | |
493 | guard_vector(RGuards, GuardVector), | |
494 | generate_names(GuardVector, 'guard_', Names), % get list [guardN, ..., guard1] | |
495 | maplist(guards_to_indices(GuardVector, Names), RGuards, IndexVectors). | |
496 | ||
497 | :- use_module(probsrc(bsyntaxtree),[always_well_defined/1]). | |
498 | get_ltsmin_guards(OpName,Guards,RestBody) :- | |
499 | get_preference(ltsmin_guard_splitting,true),!, | |
500 | get_operation_propositional_guards(OpName,Guards,RestBody). | |
501 | get_ltsmin_guards(OpName,ResGuards,RestBody) :- | |
502 | get_operation_propositional_guards(OpName,Guards,RestBody), | |
503 | conjunct_predicates(Guards,BigGuard), | |
504 | (always_well_defined(BigGuard) | |
505 | -> ResGuards = Guards | |
506 | ; ResGuards = [BigGuard] % avoid WD errors when splitting guard | |
507 | ). | |
508 | ||
509 | create_matrix([], [], Res, Res) :- !. | |
510 | create_matrix([H1|T1], [H2|T2], Acc, Res) :- | |
511 | create_matrix(T1, T2, [[H1,H2]|Acc], Res). | |
512 | create_matrix(Headings, Entries, Res) :- | |
513 | create_matrix(Headings, Entries, [], Res). | |
514 | ||
515 | ||
516 | generate_names(Terms, PrefixAtom, Names) :- | |
517 | atom_codes(PrefixAtom, PrefixChars), | |
518 | generate_names_aux(Terms, PrefixChars, 1, [], Names). | |
519 | generate_names_aux([], _, _, Acc, Acc) :- !. | |
520 | generate_names_aux([_|T], Prefix, N, Acc, Res) :- | |
521 | number_codes(N, NC), | |
522 | append(Prefix, NC, NamedC), | |
523 | atom_codes(Named, NamedC), | |
524 | N1 is N+1, | |
525 | generate_names_aux(T, Prefix, N1, [Named|Acc], Res). | |
526 | ||
527 | wrap_named_inv(Type, Name, Invariant, state_label(Name, Type, Invariant)). | |
528 | :- dynamic state_label/3. | |
529 | ||
530 | ||
531 | assert_all([]). | |
532 | assert_all([H|T]) :- | |
533 | assertz(H), assert_all(T). | |
534 | ||
535 | /* need to extract this from the atomic props of the formula, | |
536 | we can also use the prolog term of a formula as its state label */ | |
537 | get_state_labels(ListOfConjuncts, Names, Type, StateLabelMatrix) :- | |
538 | %% format of StateLabelMatrix is | |
539 | % [[label1, [id1, id2, ...]] | |
540 | % [label2, [id2, id4, ...]] | |
541 | % ...] | |
542 | maplist(wrap_named_inv(Type), Names, ListOfConjuncts, Facts), | |
543 | assert_all(Facts), | |
544 | maplist(bsyntaxtree:predicate_identifiers, ListOfConjuncts, SLSVars), | |
545 | create_matrix(Names, SLSVars, StateLabelMatrix). | |
546 | ||
547 | ||
548 | :- use_module(probsrc(bmachine),[get_unproven_invariants/1]). | |
549 | split_invariant(ListOfInvariantConjuncts, InvNames, ListOfInvariantConjunctsForPOR, InvNamesForPOR) :- | |
550 | get_unproven_invariants(ListOfInvariantConjuncts),!, % warning: does not check for INITIALISATION | |
551 | shorten_inv_list(ListOfInvariantConjuncts,ListOfInvariantConjunctsForPOR), | |
552 | generate_names(ListOfInvariantConjunctsForPOR, 'porinv', InvNamesForPOR), | |
553 | generate_names(ListOfInvariantConjuncts, 'inv', InvNames), | |
554 | (debug_mode(on) -> maplist(portray_invariant,InvNames,ListOfInvariantConjuncts) ; true). | |
555 | ||
556 | % shorten to maximal 8 invariants, as otherwise ltsmin segfaults | |
557 | shorten_inv_list([I1,I2,I3,I4,I5,I6,I7,I8|T],[I1,I2,I3,I4,I5,I6,I7,I8New]) :- T \= [], !, | |
558 | length([I8|T],Len), NrInvs is Len+7, | |
559 | format('Merging last ~w of ~w invariants (LTSMin POR supports max 8 invariants)~n',[Len,NrInvs]), | |
560 | conjunct_predicates([I8|T],I8New). | |
561 | shorten_inv_list([],R) :- !, format('No invariants to check~n',[]), R=[]. | |
562 | shorten_inv_list(I,I). | |
563 | ||
564 | :- use_module(probsrc(translate),[translate_bexpression_with_limit/3]). | |
565 | portray_invariant(Label,Inv) :- | |
566 | translate_bexpression_with_limit(Inv,100,IS), | |
567 | format(' ~w : ~w~n',[Label,IS]). | |
568 | ||
569 | ||
570 | :- use_module(probporsrc(static_analysis), [test_path/6, dependent_actions/5]). | |
571 | ||
572 | does_not_accord_with_aux([], _, []). | |
573 | does_not_accord_with_aux([H|T], TransitionGroup, [H|R]) :- | |
574 | debug_println(9,check_dependency(H,TransitionGroup)), | |
575 | get_preference(timeout_cbc_analysis,TO), | |
576 | dependent_actions(H, TransitionGroup, 0, TO, _), !, % TODO: handle interrupts? | |
577 | does_not_accord_with_aux(T, TransitionGroup, R). | |
578 | does_not_accord_with_aux([_|T], TransitionGroup, R) :- | |
579 | does_not_accord_with_aux(T, TransitionGroup, R). | |
580 | ||
581 | do_not_accord(['$init_state'|TransitionGroups], [[]|DoNotAccordMatrix]) :- | |
582 | maplist(does_not_accord_with_aux(TransitionGroups), TransitionGroups, DoNotAccordMatrix). | |
583 | ||
584 | can_enable(TransitionGroup, Guard, NGuard) :- | |
585 | ltsmin_test_path_possible(NGuard, [TransitionGroup], Guard). | |
586 | ||
587 | ltsmin_test_path_possible(Conjunction,Path,Guard) :- | |
588 | get_preference(use_cbc_analysis,true),!, | |
589 | get_preference(timeout_cbc_analysis,TO), | |
590 | temporary_set_preference(use_chr_solver,true,CHNG1), | |
591 | test_path(Conjunction, Path, Guard, 0, TO, Result), | |
592 | reset_temporary_preference(use_chr_solver,CHNG1), | |
593 | (Result = ok ; Result == timeout ; Result == unknown). | |
594 | ltsmin_test_path_possible(_,_,_). % assume possible | |
595 | ||
596 | ||
597 | calculate_enabling_set_aux([], _Guard, _NGuard, []) :- !. | |
598 | calculate_enabling_set_aux([Transition|Rest], Guard, NGuard, [Transition|ResList]) :- | |
599 | can_enable(Transition, Guard, NGuard), !, | |
600 | calculate_enabling_set_aux(Rest, Guard, NGuard, ResList). | |
601 | calculate_enabling_set_aux([_|Rest], Guard, NGuard, ResList) :- | |
602 | calculate_enabling_set_aux(Rest, Guard, NGuard, ResList). | |
603 | ||
604 | calculate_enabling_set(TransitionGroupList, Guard, Res) :- | |
605 | create_negation(Guard, NGuard), | |
606 | calculate_enabling_set_aux(TransitionGroupList, Guard, NGuard, Res). | |
607 | ||
608 | necessary_enabling_set(GuardVector, ['$init_state'|TransitionGroups], R) :- | |
609 | maplist(calculate_enabling_set(TransitionGroups), GuardVector, R). | |
610 | ||
611 | necessary_disabling_set(GuardVector, TransitionGroups, R) :- | |
612 | maplist(create_negation, GuardVector, NGuardVector), | |
613 | necessary_enabling_set(NGuardVector, TransitionGroups, R). | |
614 | ||
615 | ||
616 | may_be_coenabled_guards(G1, _G2Name, G2) :- | |
617 | conjunct_predicates([G1, G2], Conjunction), | |
618 | is_truth(Truth), | |
619 | ltsmin_test_path_possible(Conjunction, [], Truth). | |
620 | % fail on interrupt | |
621 | ||
622 | may_be_coenabled2([], [], []). | |
623 | may_be_coenabled2([_], [_], []). | |
624 | may_be_coenabled2([H|T], [Name|NameRest], [[Name,R]|RT]) :- | |
625 | include(may_be_coenabled_guards(H), NameRest, T, R), | |
626 | may_be_coenabled2(T, NameRest, RT). | |
627 | may_be_coenabled(GuardVector, Names, MayBeCoEnabledMatrix) :- | |
628 | % calculates an upper triangle matrix without the elements on the diagonal | |
629 | may_be_coenabled2(GuardVector, Names, MayBeCoEnabledMatrix). | |
630 | ||
631 | :- dynamic(guard_labels/1). | |
632 | ||
633 | get_label_group_guards(Msg, State) :- | |
634 | guard_labels(Labels), | |
635 | maplist(eval_label(Msg, State), Labels). | |
636 | ||
637 | :- public get_state_label_group/3. % this is called from ltmsin.c | |
638 | get_state_label_group(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output, | |
639 | mnf1(get_state_label_group_aux(Msg, OperationA, StateA)). | |
640 | get_state_label_group_aux(Msg, TypeA, StateA) :- | |
641 | read_state(StateA,State), | |
642 | %print(generate(State)),nl, | |
643 | generate_bound_long_state(State,BoundState), | |
644 | fast_buf_read(Type,TypeA), | |
645 | (debug:debug_mode(on) | |
646 | -> format('~n ** get_state_label_group for ~w~n',[Type]), | |
647 | translate:print_state(BoundState),nl | |
648 | ; true), | |
649 | (Type == '1' -> get_label_group_guards(Msg, BoundState) | |
650 | ; print(unhandled_group_type(Type)),nl,fail). | |
651 | ||
652 | get_ltl_labels(ASTs, Names) :- | |
653 | findall(ap_representation(Hash, AST), ltl_safety:ap_representation(Hash, AST), APReprs), | |
654 | maplist(arg(2), APReprs, ASTs), | |
655 | maplist(arg(1), APReprs, Names). | |
656 | ||
657 | ||
658 | :- use_module(probsrc(error_manager), [add_error_fail/3]). | |
659 | ||
660 | op_to_reads_guard(Op, ReadSet) :- | |
661 | get_opname(Op, OpName), | |
662 | op_guards(OpName, GuardList), | |
663 | maplist(guard_reads, GuardList, ReadSets), | |
664 | append(ReadSets, ReadSet). | |
665 | ||
666 | oplist_to_reads_guards(OpList, ReadSet) :- | |
667 | maplist(op_to_reads_guard, OpList, ReadSets), | |
668 | append(ReadSets, ReadSet). | |
669 | % identifiers might be contained multiple times due to append | |
670 | get_ltl_readsets(bpred(X), ReadSet) :- | |
671 | bsyntaxtree:predicate_identifiers(X, ReadSet). | |
672 | get_ltl_readsets(enabled(Op), ReadSet) :- | |
673 | op_to_reads_guard(Op, ReadSet). % get readset of guards of op | |
674 | get_ltl_readsets(det(OpList), ReadSet) :- | |
675 | oplist_to_reads_guards(OpList, ReadSet). | |
676 | get_ltl_readsets(dlk(OpList), ReadSet) :- | |
677 | oplist_to_reads_guards(OpList, ReadSet). | |
678 | get_ltl_readsets(ctrl(OpList), ReadSet) :- !, | |
679 | oplist_to_reads_guards(OpList, ReadSet). | |
680 | get_ltl_readsets(deadlock, ReadSet) :- | |
681 | get_transition_groups(OpList), | |
682 | oplist_to_reads_guards(OpList, ReadSet). | |
683 | get_ltl_readsets(AP,_) :- !, | |
684 | add_error_fail(ltsmin, 'operation is not supported for LTSmin', AP). | |
685 | ||
686 | :- dynamic(guard_reads/2). | |
687 | ||
688 | assert_guard_readsets([]). | |
689 | assert_guard_readsets([[GuardName, ReadSet]|R]) :- | |
690 | assertz(guard_reads(GuardName, ReadSet)), | |
691 | assert_guard_readsets(R). | |
692 | ||
693 | :- dynamic(op_guards/2). | |
694 | ||
695 | assert_op_guards([], []). | |
696 | assert_op_guards([Op|T], [GuardList|T2]) :- | |
697 | assertz(op_guards(Op, GuardList)), | |
698 | assert_op_guards(T, T2). | |
699 | ||
700 | :- spec_pre(ltl_to_state_label_matrix/3, [[b_pred_ish], [atom], var]). | |
701 | :- spec_invariant(ltl_to_state_label_matrix/3, [[b_pred_ish], [atom], ltsmin_matrix(ltsmin_state_label, ltsmin_variable)]). | |
702 | :- spec_post(ltl_to_state_label_matrix/3, [[b_pred_ish], [atom], var], [[b_pred_ish], [atom], ltsmin_matrix(ltsmin_state_label, ltsmin_variable)]). | |
703 | ltl_to_state_label_matrix(ListOfAPs, LtlApNames, LtlStateLabelMatrix) :- | |
704 | %% format of StateLabelMatrix is | |
705 | % [[label1, [id1, id2, ...]] | |
706 | % [label2, [id2, id4, ...]] | |
707 | % ...] | |
708 | maplist(wrap_named_inv(ltl_ap), LtlApNames, ListOfAPs, Facts), | |
709 | assert_all(Facts), | |
710 | maplist(get_ltl_readsets, ListOfAPs, SLSVars), | |
711 | create_matrix(LtlApNames, SLSVars, LtlStateLabelMatrix). | |
712 | ||
713 | ||
714 | calc_and_append_por_info(false, _Msg, _, _, _) :- !. | |
715 | calc_and_append_por_info(_Por, Msg, GuardVector, GuardNames, TransitionGroups) :- | |
716 | may_be_coenabled(GuardVector, GuardNames, MayBeCoEnabledMatrix), | |
717 | write_matrix(Msg, MayBeCoEnabledMatrix, may_be_coenabled_matrix), | |
718 | ||
719 | necessary_enabling_set(GuardVector, TransitionGroups, NES), | |
720 | create_matrix(GuardNames, NES, NesMatrix), | |
721 | write_matrix(Msg, NesMatrix, necessary_enabling_set), | |
722 | ||
723 | necessary_disabling_set(GuardVector, TransitionGroups, NDS), | |
724 | create_matrix(GuardNames, NDS, NdsMatrix), | |
725 | write_matrix(Msg, NdsMatrix, necessary_disabling_set), | |
726 | ||
727 | do_not_accord(TransitionGroups, DNA), | |
728 | create_matrix(TransitionGroups, DNA, DnaMatrix), | |
729 | write_matrix(Msg, DnaMatrix, do_not_accord_matrix). | |
730 | ||
731 | ||
732 | sort_by_and_distinct(SortByList, ToBeSortedMayContainDups, SortedUniqs) :- | |
733 | findall(X, (member(X, SortByList), member(X, ToBeSortedMayContainDups)), SortedWithDups), | |
734 | distinct(SortedWithDups, SortedUniqs). | |
735 | ||
736 | ||
737 | ||
738 | :- dynamic black_magic_short_transformation/11. | |
739 | % arg 1: Name of Operation | |
740 | % arg 2: a pattern in order to create a bound state | |
741 | % arg 3: a list of variables that unify the second argument to a bound state | |
742 | % arg 4: a long state pattern that can be unified in order to get a short state in arg 5 | |
743 | % arg 5: the corresponding short state | |
744 | % arg 6: default values in case variables are not written | |
745 | % arg 7-11: see arg 2-6, but for next_action | |
746 | ||
747 | ||
748 | % the last argument should be unified with the LTSmin short state values; | |
749 | % this way, we acquire a bound state in the second to last argument. | |
750 | prepare_binding([], [], [], []). | |
751 | prepare_binding([H|AccessedTail], [H|ReadTail], [bind(H, V)|BindingTail], [V|ValTail]) :- !, | |
752 | prepare_binding(AccessedTail, ReadTail, BindingTail, ValTail). | |
753 | prepare_binding([H|AccessedTail], Reads, [bind(H, term(undefined))|BindingTail], Vals) :- | |
754 | prepare_binding(AccessedTail, Reads, BindingTail, Vals). | |
755 | ||
756 | % TODO: maybe refactor this (pk, 07.03.2018) | |
757 | back_to_short([], [], [], [], [], _InitialState). | |
758 | back_to_short([bind(H, _)|T], [H|WriteTail], [bind(H, V)|LongStateTail], [bind(H, V)|ShortTail], [bind(H, Default)|DefaultBindingsTail], InitialState) :- !, | |
759 | % variable is written to | |
760 | memberchk(bind(H, Default), InitialState), | |
761 | back_to_short(T, WriteTail, LongStateTail, ShortTail, DefaultBindingsTail, InitialState). | |
762 | back_to_short([bind(H, _)|T], Writes, [bind(H, _)|LongStateTail], Short, DefaultBindings, InitialState) :- | |
763 | back_to_short(T, Writes, LongStateTail, Short, DefaultBindings, InitialState). | |
764 | ||
765 | assert_short_state_transformations([], InitialState) :- | |
766 | varname_list(L), | |
767 | prepare_binding(L, [], PreparedBinding, PreparedVarListForUnification), | |
768 | back_to_short(PreparedBinding, L, LongPattern, PreparedShort, InitialState, InitialState), | |
769 | assertz(black_magic_short_transformation('$init_state', PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, InitialState, | |
770 | PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, InitialState)). | |
771 | assert_short_state_transformations([list([Op, ReadsGuard, ReadsAction, MustWrite, MayWrite|_])|T], InitialState) :- | |
772 | varname_list(L), | |
773 | sort_by_and_distinct(L, ReadsAction, SortedReadsAction), | |
774 | append([ReadsGuard, ReadsAction, MustWrite, MayWrite], AllAccessedVarsWithDups), | |
775 | append([ReadsAction, MustWrite, MayWrite], AllAccessedVarsForActionWithDups), | |
776 | append([ReadsGuard, ReadsAction], AllReadsWithDups), | |
777 | append([MustWrite, MayWrite], AllWritesWithDups), | |
778 | sort_by_and_distinct(L, AllAccessedVarsWithDups, AllAccessedVars), | |
779 | sort_by_and_distinct(L, AllAccessedVarsForActionWithDups, AllAccessedVarsForAction), | |
780 | sort_by_and_distinct(L, AllReadsWithDups, AllReads), | |
781 | sort_by_and_distinct(L, AllWritesWithDups, AllWrites), | |
782 | prepare_binding(AllAccessedVars, AllReads, PreparedBinding, PreparedVarListForUnification), | |
783 | prepare_binding(AllAccessedVarsForAction, SortedReadsAction, PreparedBindingForNextAction, PreparedVarListForUnificationForNextActionFactoryProviderSingleton), | |
784 | back_to_short(PreparedBinding, AllWrites, LongPattern, PreparedShort, Defaults, InitialState), | |
785 | back_to_short(PreparedBindingForNextAction, AllWrites, LongPatternForAction, PreparedShortForNextAction, DefaultsForAction, InitialState), | |
786 | assertz(black_magic_short_transformation(Op, PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, Defaults, | |
787 | PreparedBindingForNextAction, PreparedVarListForUnificationForNextActionFactoryProviderSingleton, LongPatternForAction, PreparedShortForNextAction, DefaultsForAction)), | |
788 | assert_short_state_transformations(T, InitialState). | |
789 | ||
790 | ||
791 | assert_label_to_accessed_vars([]). | |
792 | assert_label_to_accessed_vars([[Label,ListOfVars]|T]) :- | |
793 | varname_list(L), | |
794 | findall(AccessedOrderedVars, (member(AccessedOrderedVars, L), | |
795 | member(AccessedOrderedVars, ListOfVars)), | |
796 | AccessedVarSet), % poor man's sort-by | |
797 | assertz(label_to_reads(Label, AccessedVarSet)), | |
798 | assert_label_to_accessed_vars(T). | |
799 | ||
800 | ||
801 | ||
802 | ||
803 | ||
804 | ||
805 | distinct(X, Y) :- | |
806 | distinct(X, [], Y). | |
807 | distinct([], _, []). | |
808 | distinct([H|T], Seen, Res) :- | |
809 | member(H, Seen), !, | |
810 | distinct(T, Seen, Res). | |
811 | distinct([H|T], Seen, [H|Res]) :- | |
812 | distinct(T, [H|Seen], Res). | |
813 | ||
814 | ||
815 | ||
816 | put_read_write_matrices(Msg, MR) :- | |
817 | %% read write matrices | |
818 | tcltk_read_write_matrix(M), | |
819 | (debug:debug_mode(on) -> print(M),nl,flush_output ; true), | |
820 | M = list([_Headings|MR]), | |
821 | (debug:debug_mode(on) -> print(MR),nl ; true), | |
822 | extract_tg_and_nth_entry(MR, 5, [], MayWriteMatrix), | |
823 | extract_tg_and_nth_entry(MR, 4, [], MustWriteMatrix), | |
824 | extract_tg_and_nth_entry(MR, 3, [], ReadsActionMatrix), | |
825 | extract_tg_and_nth_entry(MR, 2, [], ReadsGuardMatrix), | |
826 | put_may_write_matrix(Msg, MayWriteMatrix), | |
827 | put_patched_matrix(Msg, must_write_matrix,MustWriteMatrix), | |
828 | put_patched_matrix(Msg, reads_action_matrix,ReadsActionMatrix), | |
829 | put_patched_matrix(Msg, reads_guard_matrix,ReadsGuardMatrix). | |
830 | ||
831 | assert_short_state_info(MR, InitialState) :- | |
832 | varname_list(L), | |
833 | generate_bindings(InitialState, L, BoundInitialState), | |
834 | assert_short_state_transformations(MR, BoundInitialState). | |
835 | ||
836 | reset_ltsmin_extension :- | |
837 | reset_c_counters, | |
838 | retractall(black_magic_short_transformation(_,_,_,_,_,_,_,_,_,_,_)), | |
839 | retractall(label_to_reads(_,_)), | |
840 | retractall(inv_state_label_matrix(_)), | |
841 | retractall(inv_state_label_matrix_for_por(_)), | |
842 | retractall(varname_list(_)), | |
843 | retractall(op_guards(_, _)), | |
844 | retractall(state_label(_, _, _)), | |
845 | retractall(guard_labels(_)), | |
846 | retractall(guard_reads(_, _)). | |
847 | ||
848 | :- use_module(probsrc(debug),[formatsilent/2]). | |
849 | :- public get_init/2. | |
850 | get_init(Msg, PorInt) :- | |
851 | (PorInt == 0 -> Por = false ; Por = true), | |
852 | get_ltsmin_variable_names(VS, VTypes), | |
853 | assertz(varname_list(VS)), | |
854 | formatsilent('List of variables for LTSmin (por=~w): ~w~n',[Por,VS]), | |
855 | maplist(build_initial_state, VS, VTypes, BInitialState), | |
856 | %maplist(any_value_for_type,VTypes,InitialState), | |
857 | maplist(term_to_atom, VTypes, VTypeAtoms), | |
858 | get_transition_groups(TransitionGroups), | |
859 | (csp_with_bz_mode | |
860 | -> InitialState = [stop(no_loc_info_available) | BInitialState], % DUMMY Values | |
861 | Vars = ['$CSP_CHUNK'|VS], Types = ['csp_process'|VTypeAtoms] | |
862 | ; InitialState = BInitialState, | |
863 | Vars = VS, Types = VTypeAtoms | |
864 | ), | |
865 | debug_println(9,initial(InitialState)), | |
866 | write_chunklist(Msg, InitialState, initial_state), | |
867 | write_chunklist(Msg, TransitionGroups, transition_group_list), | |
868 | write_chunklist(Msg, Vars, variables_name_list), % we use $CSP_CHUNK as name for the CSP chunk | |
869 | write_chunklist(Msg, Types, variables_type_list), | |
870 | ||
871 | ||
872 | put_read_write_matrices(Msg, MR), | |
873 | assert_short_state_info(MR, InitialState), | |
874 | ||
875 | (Por == false -> inv_state_label_matrix(InvStateLabelMatrix) | |
876 | ; inv_state_label_matrix_for_por(InvStateLabelMatrix)), | |
877 | ||
878 | %print(slm(InvStateLabelMatrix)),nl, | |
879 | %% split guards to state labels | |
880 | split_guards(Por, TransitionGroups, GuardVector, GuardNames, IndexVectors), | |
881 | get_state_labels(GuardVector, GuardNames, guard, GuardStateLabelMatrix), | |
882 | ||
883 | % memoize mapping OpName -> GuardNames | |
884 | assert_op_guards(TransitionGroups, IndexVectors), | |
885 | % memoize mapping GuardName -> ReadSet(Guard) | |
886 | assert_guard_readsets(GuardStateLabelMatrix), | |
887 | ||
888 | reverse(GuardNames, GuardNamesInOrder), | |
889 | assertz(guard_labels(GuardNamesInOrder)), | |
890 | ||
891 | get_ltl_labels(ListOfLabelASTs, LtlApNames), | |
892 | ltl_to_state_label_matrix(ListOfLabelASTs, LtlApNames, LtlStateLabelMatrix), | |
893 | ||
894 | % accessed variable names in order (for short states) | |
895 | assert_label_to_accessed_vars(InvStateLabelMatrix), | |
896 | assert_label_to_accessed_vars(GuardStateLabelMatrix), | |
897 | assert_label_to_accessed_vars(LtlStateLabelMatrix), | |
898 | ||
899 | %% write all state labels (invariant conjuncts and guard conjuncts) | |
900 | write_matrix(Msg, InvStateLabelMatrix, state_label_matrix), | |
901 | write_matrix(Msg, GuardStateLabelMatrix, guard_label_matrix), | |
902 | write_matrix(Msg, LtlStateLabelMatrix, ltl_label_matrix), | |
903 | ||
904 | %% create guard info matrix, i.e. which transition depends on which guards | |
905 | create_matrix(TransitionGroups, IndexVectors, GuardInfoMatrix), | |
906 | write_matrix(Msg, GuardInfoMatrix, guard_info_matrix), | |
907 | calc_and_append_por_info(Por, Msg, GuardVector, GuardNames, TransitionGroups). | |
908 | ||
909 | ||
910 | ||
911 | compute_successors('$init_state',_,Result) :- !, | |
912 | findall(S,init_state(S),Result), | |
913 | debug:debug_println(9,res_init_state(Result)). | |
914 | compute_successors(OpName,L,Result) :- | |
915 | temporary_set_preference(try_operation_reuse,false,CHNG2), % operation reuse done by LTSmin; we would only get no_packed_state_info messages and no benefit | |
916 | (debug:debug_mode(on) -> nl,print(compute_successors(OpName)),nl,flush_output ; true), | |
917 | findall(S,specfile:specfile_trans(L,OpName,_,S,_,_),Result), | |
918 | reset_temporary_preference(try_operation_reuse,CHNG2). | |
919 | % this in turn will call b_execute_top_level_operation_update for normal operations | |
920 | ||
921 | :- public next_action/3. % called from C | |
922 | next_action(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output, | |
923 | mnf1(next_action_aux(long, Msg, OperationA, StateA)). | |
924 | next_action_short(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output, | |
925 | mnf1(next_action_aux(short, Msg, OperationA, StateA)). | |
926 | next_action_aux(Type, Msg, OperationA, StateA) :- | |
927 | read_state(StateA,State), | |
928 | fast_buf_read(Operation,OperationA), | |
929 | %print(generate(Type, State, Operation)),nl, | |
930 | (Type == short -> black_magic_short_transformation(Operation, _, _, _, _, _, BoundState, State, LongPattern, ShortSucc, Defaults), LongOrPattern = LongPattern-ShortSucc-Defaults | |
931 | ; generate_bound_long_state(State, BoundState), LongOrPattern = long), | |
932 | (debug:debug_mode(on) | |
933 | -> format('~n ** get_successors for ~w~n',[Operation]), | |
934 | translate:print_state(BoundState),nl | |
935 | ; true), | |
936 | get_next_action(LongOrPattern, Msg, BoundState,Operation). | |
937 | ||
938 | :- use_module(probsrc(preferences),[get_preference/2,temporary_set_preference/3,reset_temporary_preference/2]). | |
939 | get_next_action(Type, Msg, State,Op) :- % State is a list of bindings | |
940 | temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,true,CHNG), | |
941 | get_next_states(Type, Msg, State,Op), | |
942 | reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG). | |
943 | ||
944 | init_state(Res) :- specfile:specfile_trans(root,_,_,S,_,_), | |
945 | init_state2(S,Res). % , nl,print(init(Res)),nl. | |
946 | ||
947 | init_state2(csp_and_b_root,Res) :- !, | |
948 | specfile:specfile_trans(csp_and_b_root,_,_,S,_,_), | |
949 | init_state2(S,Res). | |
950 | init_state2(concrete_constants(L),FullRes) :- !, | |
951 | specfile:specfile_trans(concrete_constants(L),_,_,Res,_,_), | |
952 | expand_const_and_vars_to_full_store(Res,FullRes). | |
953 | init_state2(R,R). | |
954 | ||
955 | :- use_module(probsrc(b_interpreter),[b_test_boolean_expression_for_ground_state/5]). | |
956 | eval_label(Msg, State,invariant) :- | |
957 | bmachine:b_get_invariant_from_machine(Invariant),!, % Should we use: get_unproven_invariants | |
958 | (profile_single_call(check_invariant, | |
959 | b_interpreter:b_test_boolean_expression_for_ground_state(Invariant,[],State,'LTSMin invariant label',0)) -> | |
960 | put_number(Msg, 1); put_number(Msg, 0)). | |
961 | eval_label(Msg, State,Label) :- | |
962 | (debug:debug_mode(on) -> print(eval(Label)),nl,flush_output ; true), | |
963 | state_label(Label, Type, AST), | |
964 | profile_single_call(Label,ltsmin:eval_label2(Type, Msg, State, AST)). | |
965 | ||
966 | ||
967 | %:- use_module(probltlsrc(ltl_prepositions), [check_ap/2]). | |
968 | eval_label2(ltl_ap, Msg, State, AST) :- | |
969 | (check_ap_bound_state(AST,State) -> | |
970 | put_number(Msg, 1); put_number(Msg, 0)). | |
971 | eval_label2(_, Msg, State, AST) :- | |
972 | (b_test_boolean_expression_for_ground_state(AST,[],State,'LTSMin label',0) -> | |
973 | put_number(Msg, 1) ; put_number(Msg, 0)). | |
974 | % foreign predicate put_number(Msg, X) :: 0 = false, 1=true | |
975 | ||
976 | ||
977 | get_opname(bop(Name, _, _, _, _), Name). | |
978 | get_opname(btrans(event(Name)), Name). | |
979 | get_opname(btrans(event(Name, _, _)), Name). | |
980 | ||
981 | op_enabled(Op, State) :- | |
982 | get_opname(Op, OpName), | |
983 | get_guard(OpName, Guard), | |
984 | b_test_boolean_expression_for_ground_state(Guard, [], State,'LTSMin op_enabled',0). | |
985 | ||
986 | % check an atomic proposition in a given node (i.e. state) | |
987 | check_ap_bound_state(bpred(Property),Node) :- | |
988 | b_test_boolean_expression_for_ground_state(Property, [], Node,'LTSMin atomic proposition',0). | |
989 | check_ap_bound_state(enabled(Op),Node) :- !, | |
990 | op_enabled(Op, Node). | |
991 | check_ap_bound_state(det(OpList),Node) :- !, | |
992 | max_enabled(OpList, Node, 1, 0, R), | |
993 | R < 2. | |
994 | check_ap_bound_state(dlk(OpList),Node) :- !, | |
995 | max_enabled(OpList, Node, 0, 0, 0). | |
996 | check_ap_bound_state(ctrl(OpList),Node) :- !, | |
997 | max_enabled(OpList, Node, 1, 0, 1). | |
998 | check_ap_bound_state(deadlock,Node) :- !, | |
999 | get_transition_groups(OpList), | |
1000 | check_ap_bound_state(dlk(OpList), Node). | |
1001 | ||
1002 | %max_enabled(OpList, Max, EnabledSoFar, ResEnabled) | |
1003 | max_enabled([], _State, _Max, R, R). | |
1004 | max_enabled([Op|T], State, Max, EnabledSoFar, R) :- | |
1005 | (op_enabled(Op, State) | |
1006 | -> Enabled is EnabledSoFar + 1, | |
1007 | Max >= Enabled, | |
1008 | max_enabled(T, State, Max, Enabled, R) | |
1009 | ; max_enabled(T, State, Max, EnabledSoFar, R)). | |
1010 | ||
1011 |