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