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