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