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