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