1		% (c) 2016 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(state_space_explorer,[explore_state_space/5, compute_transitions_opt/3,
6		get_b_optimisation_options/2]).
7
8		/* ProB Libraries */
9		:- use_module(probsrc(error_manager)).
10		:- use_module(probsrc(tools),[print_message/1,print_mb/1]).
11		:- use_module(probsrc(state_space),[clear_context_state/0,visited_expression/2,state_error/3,set_context_state/1]).
12		:- use_module(probsrc(state_space_exploration_modes),[get_open_node_to_check/2,depth_breadth_first_mode/1]).
13		:- use_module(probsrc(specfile),[animation_mode/1]).
14		:- use_module(probsrc(preferences),[get_preference/2]).
15
16		%:- use_module(probporsrc(static_analysis),[compute_dependendency_relation_of_all_events_in_the_model/3]).
17		%:- use_module(probpgesrc(pge_algo), [compute_transitions_pge/2, compute_operation_relations_for_pge/1]).
18		%:- use_module(probporsrc(ample_sets),[check_cycle_proviso/0]).
19		:- use_module(probsrc(model_checker),[compute_transitions_opt/3, perform_static_analyses/3]).
20
21		:- use_module(probsrc(module_information),[module_info/2]).
22		:- module_info(group,ltl).
23		:- module_info(description,'This module provides predicates for state space exploration without performing any checks.').
24
25		explore_state_space(Nr,LimitNr,NodesAnalysed,LimitTime,Res) :-
26		animation_mode(MODE),
27		get_b_optimisation_options(MODE,Optimisations),
28		% 0 for not including the invariant into the respective analyses
29		perform_static_analyses(MODE,0,Optimisations),
30		depth_breadth_first_mode(DFMODE),
31		statistics(walltime,[ReferenceTime,_]),
32		model_checker: get_model_check_stats(States,_Transitions,_ProcessedTotal,Percentage),
33		RefStatus=refstatus(ReferenceTime,Percentage,States,ReferenceTime),
34		explore_one_state_stats(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res),
35		clear_context_state.
36
37		explore_one_state_stats(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res) :-
38		(Nr < LimitNr ; LimitNr=:= -1),!, % -1 for infinite
39		statistics(walltime,[NewTime,_]),
40		print_stats_and_update_refstatus(Nr,RefStatus,NewTime,RefStatus1),
41		((number(LimitTime), NewTime>LimitTime, Nr>0) ->
42		Res = [timeout,Nr],
43		NodesAnalysed=Nr
44		; otherwise ->
45		explore_one_state(Nr,LimitNr,RefStatus1,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res)
46		).
47		explore_one_state_stats(N,_LimitNr,_RefStatus,N,_,_,_,no).
48
49		explore_one_state(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res) :-
50		get_open_node_to_check(DFMODE,ID),!,
51		set_context_state(ID),
52		visited_expression(ID,CurState),!,
53		compute_transitions_opt(Optimisations,ID,CurState),
54		%user:do_one_gui_event,
55		(state_exploration_found_error(ID,Error)
56		-> model_checker: print_found_error(Error,ID),
57		clear_context_state,
58		NodesAnalysed=Nr
59		; N1 is Nr + 1,
60		explore_one_state_stats(N1,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res)
61		).
62		explore_one_state(N,_LimitNr,_RefStatus,N,_,_,_,all) :-
63		% in case get_open_node_to_check/2 at the previous clause fails we do not have any other states to explore
64		print_message('All open nodes visited').
65
66		:- use_module(probsrc(debug),[formatsilent/2]).
67		print_stats_and_update_refstatus(Nr,RefStatus,NewTime,RefStatus1) :-
68		( (Nr mod 1000 =:= 0, Nr\=0)
69		-> RefStatus = refstatus(RefTime,_RefPerc,PrevStates,StartTime),
70		Delta is NewTime-RefTime,
71		(Delta>20000 % more than 20 seconds since last message
72		-> model_checker: get_model_check_stats(States,Transitions,ProcessedTotal,Perc),
73		formatsilent('~n* ~w states explored (~1f% of total ~w), ~w transitions,',[ProcessedTotal,Perc,States,Transitions]),
74		statistics(memory_used,M),
75		print_mb(M),
76		DeltaStates is (States-PrevStates),
77		NodesPerSec is DeltaStates*1000 / (NewTime-RefTime),
78		formatsilent(', current ~2F states/sec~n',[NodesPerSec]),
79		RefStatus1 = refstatus(NewTime,Perc,States,StartTime)
80		; RefStatus1 = RefStatus)
81		; RefStatus1 = RefStatus).
82
83		state_exploration_found_error(ID,Error) :-
84		state_error(ID,_,Err),
85		Error = state_error(Err).
86		state_exploration_found_error(_ID,Error) :-
87		real_error_occurred,
88		Error = general_error_occurred.
89
90		get_b_optimisation_options(MODE,Optimisations) :-
91		(MODE == b),!,
92		Optimisations = opt(PORPrefs,PGEPref),
93		PORPrefs = por(POR,UseEnableGraph,Depth,PGEPref),
94		get_preference(por,POR),
95		get_preference(enable_graph,UseEnableGraph),
96		get_preference(enable_graph_depth,Depth),
97		get_preference(pge,PGEPref).
98		get_b_optimisation_options(_,Optimisations) :-
99		Optimisations = opt(off,off).