1		% (c) 2016-2022 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
5		:- module(trace_generator,[generate_all_traces_until/4, generate_traces/0]).
6
7		:- use_module(probsrc(error_manager)).
8		:- use_module(probsrc(state_space),[visited_expression/2,
9		try_set_trace_by_transition_ids/1, transition/4]).
10
11		:- use_module(probltlsrc(ltl_propositions),[check_atomic_property_formula/2]).
12		:- use_module(probsrc(tcltk_interface),[compute_all_transitions_if_necessary/2]).
13		:- use_module(probsrc(b_trace_checking),[tcltk_save_history_as_trace_file/3]).
14		:- use_module(probsrc(tools_strings),[ajoin/2]).
15		:- use_module(probsrc(specfile),[b_or_z_mode/0,currently_opened_file/1]).
16
17		:- use_module(ltl_tools,[temporal_parser/3]).
18		:- use_module(probsrc(preferences), [get_preference/2]).
19		:- use_module(probsrc(tools_meta),[safe_time_out/3]).
20		:- use_module(visbsrc(visb_visualiser),[load_default_visb_file_if_necessary/0, get_default_visb_file/2,
21		generate_visb_html_for_history_with_vars/1]).
22
23		:- use_module(probsrc(module_information),[module_info/2]).
24		:- module_info(group,ltl).
25		:- module_info(description,'This module generates all traces under a certain condition.').
26
27		generate_all_traces_until(LTL_Stop_AsAtom,FilePrefix,Result,NrTracesGenerated) :-
28		( temporal_parser(LTL_Stop_AsAtom,ltl,LtlStopFormula) ->
29		FromID=root,
30		generate_traces(FromID,LtlStopFormula,FilePrefix,Result),
31		bb_get(traces_generated,NrTracesGenerated)
32		;
33		add_error(ltl,'LTL Parser failed: ',LTL_Stop_AsAtom),
34		Result = ltl_parse_error, NrTracesGenerated=0
35		).
36
37		% generate a single trace until either stop condition or deadlock reached
38		generate_trace(StateId,AtomicLTL_StopCond,[],stop_condition) :-
39		compute_all_transitions_if_necessary(StateId,false), % could be made optional
40		check_atomic_property_formula(AtomicLTL_StopCond,StateId),!,
41		print(trace_stop_condition_found_in_state(StateId)),nl.
42		generate_trace(StateId,_,[],deadlock) :-
43		\+ transition(StateId,_,_,_),
44		print(deadlock_in_state(StateId)),nl.
45		generate_trace(StateId,AtomicLTL_StopCond,[TransID|T],EndResult) :-
46		transition(StateId,_TransitionTerm,TransID,ToID),
47		generate_trace(ToID,AtomicLTL_StopCond,T,EndResult).
48
49		generate_traces :- generate_traces(root).
50		generate_traces(FromID) :- generate_traces(FromID,false,'Trace_',_). % only generate deadlocking traces
51
52		generate_traces(FromID,AtomicLTL_StopCond,FilePrefix,Res) :-
53		load_default_visb_file_if_necessary,
54		get_preference(trace_generation_time_out,TO),
55		safe_time_out(generate_traces2(FromID,AtomicLTL_StopCond,FilePrefix,Res),
56		TO, TORes),
57		(TORes = time_out
58		-> add_message(trace_generator,'Time-out, increase TRACES_TIME_OUT preference: ',TO),
59		Res=time_out
60		; true).
61
62		generate_traces2(FromID,AtomicLTL_StopCond,FilePrefix,Res) :-
63		get_preference(trace_generation_limit,Limit),
64		bb_put(traces_generated,0),
65		generate_trace(FromID,AtomicLTL_StopCond,TraceIDs,EndResult),
66		bb_inc(Nr),
67		save_trace(FilePrefix,json,Nr,EndResult,TraceIDs),
68		(Nr >= Limit -> !,add_message(trace_generator,'Limit of number of traces reached, increase MAX_TRACES preference: ',Nr), Res=limit_reached
69		; fail).
70		generate_traces2(_,_,_,all_traces_generated). % we could check max_reached, ...
71
72		bb_inc(Nr) :- bb_get(traces_generated,Old),
73		New is Old+1, bb_put(traces_generated,New), Nr=New.
74
75		save_trace(FilePrefix,Format,Nr,EndResult,TraceIDs) :-
76		try_set_trace_by_transition_ids(TraceIDs),
77		%loaded_main_file(_,MainFile),
78		% currently_opened_file(File),
79		% (b_or_z_mode -> b_machine_name(Model) ; get_modulename_filename(File,Model)),
80		(EndResult = deadlock
81		-> DLK = '_DLK' % we could make adding this to the name optional
82		; DLK=''
83		),
84		ajoin([FilePrefix,Nr,DLK,'.prob2trace'],HistFile), % If FilePrefix ends in a / we could add Trace?
85		format('% Saving history to JSON ProB2-UI trace file: ~w~n',[HistFile]),
86		ajoin(['Trace ',Nr,' generated ending in ',EndResult],Desc),
87		tcltk_save_history_as_trace_file(Format,[description/Desc],HistFile),
88		ajoin([FilePrefix,Nr,DLK,'.html'],VisBHTMLFile),
89		save_visb_html_his(VisBHTMLFile).
90
91		save_visb_html_his(File) :-
92		get_default_visb_file(_,_),!,
93		format('% Saving history to VisB HTML file: ~w~n',[File]),
94		generate_visb_html_for_history_with_vars(File).
95		save_visb_html_his(_). % No file provided; do not generate: we could foresee another option for this
96
97
98		% :- use_module(probltlsrc(trace_generator)), generate_traces.